Semantics of the Symbolic Queries

In the following we give a pseudo-formal semantics for the requirement specification language of UPPAAL. We assume the existence of a timed transition system (S, s₀, →) as defined in the semantics of UPPAAL timed automata. In the following, p and q are state properties for which we define the following temporal properties:

Possibly

The property E<> p evaluates to true for a timed transition system if and only if there is a sequence of delay and action transitions s₀ → s₁ → … → s_n, where s₀ is the initial state and s_n satisfies p.

Invariantly

The property A[] p evaluates to true if (and only if) every reachable state satisfy p.

An invariantly property A[] p can be expressed as the possibly property not E<> not p.

Potentially always

The property E[] p evaluates to true for a timed transition system if and only if there is a sequence of delay and action transitions s₀ → s₁ → … → s_i → … for which p holds in all states s_i and which either:

• is infinite, or
• ends in a state (L_n, v_n) such that either
  • for all d: (L_n, v_n+d) satisfies p and Inv(L_n), or
  • there is no outgoing transition from (L_n, v_n)

Eventually

The property A<> p evaluates to true if (and only if) all possible transition sequences eventually reaches a state satisfying p.

An eventually property A<> p can be expressed as the potentially property not E[] not p.

Leads To

The syntax p --> q denotes a leads to property meaning that whenever p holds eventually q will hold as well. Since UPPAAL uses timed automata as the input model, this has to be interpreted not only over action transitions but also over delay transitions.

A leads to property p --> q can be expressed as the property A[] (p imply A<> q).

State Properties

Any side-effect free expression is a valid state property. In addition it is possible to test whether a process is in a particular location and whether a state is a deadlock. State proprerties are evaluated for the initial state and after each transition. This means for example that a property A[] i != 1 might be satisfied even if the value of i becomes 1 momentarily during the evaluation of initializers or update-expressions on edges.

Locations

Expressions on the form P.ℓ, where P is a process and ℓ is a location, evaluate to true in a state (L, v) if and only if P.ℓ is in L.

Deadlocks

The state property deadlock evaluates to true for a state (L, v) if and only if for all d ≥ 0 there is no action successor of (L, v + d).

Property Equivalences

The UPPAAL requirement specification language supports five types of properties, which can be reduced to two types as illustrated by the following table.