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 _{0},* →) as defined in the semantics of UPPAAL timed automata. In the following,

The property `E<> p` evaluates to true for a timed transition system if and only if there is a sequence of alternating delay transitions and action transitions *s*_{0} → *s*_{1} → … → *s*_{n}, where *s*_{0} is the initial state and *s*_{n} satisfies *p*.

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`.

The property `E[] p` evaluates to true for a timed transition system if and only if there is a sequence of alternating delay or action transitions *s*_{0} → *s*_{1} → … → *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}_)

- for all

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`.

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)`.

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.

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*.

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*).

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

Name | Property | Equivalent to |
---|---|---|

Posibly | E<> p | |

Invariantly | A[] p | not E<> not p |

Potentially always | E[] p | |

Eventually | A<> p | not E[] not p |

Leads to | p –> q | A[] (p imply A<> q) |