# Contents

# Semantics of the Requirement Specification Language

In the following we give a pseudo-formal semantics for the
requirement specification language of UPPAAL. We assume the existens
of a timed transition system (*S, s0,* ->) as defined in the
semantics of UPPAAL.
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 alternating
delay transitions and action transitions
*s0*-->*s1*-->...-->*sn*, where *s0* is
the initial state and *sn* 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 alternating
delay or action transitions
*s0*-->*s1*-->...-->*si*-->... for which
*p* holds in all states *si* and which either:

- is infinite, or
- ends in a state (
*Ln, vn*) such that either- for all
*d*: (*Ln, vn + d*) satisfies*p*and*Inv*(*Ln*), or - there is no outgoing transition from (
*Ln, vn*)

- for all

### 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.l`, where `P` is a process
and `l` is a location, evaluate to true in a state (*L,
v*) if and only if *P.l* 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.

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

Possibly | 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) |