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,

`p`

and `q`

are state properties for which we define the following temporal properties: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*_{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 delay and 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)` |