# 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 existence
of a timed transition system (*S, s _{0},* →) 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
*s _{0}*→

*s*→…→

_{1}*s*, where

_{n}*s*is the initial state and

_{0}*s*satisfies

_{n}*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
*s _{0}*→

*s*→…→

_{1}*s*→… for which

_{i}*p*holds in all states

*s*and which either:

_{i}- is infinite, or
- ends in a state (
*L*) such that either_{n}, v_{n}- for all
*d*: (*L*) satisfies_{n}, v_{n}+d*p*and*Inv*(*L*), or_{n} - there is no outgoing transition from (
*L*)_{n}, v_{n}

- 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.ℓ`, 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*).

## Statistical Properties

UPPAAL can estimate the probability of expression values statistically. There are four types of statistical properties: quantitative, qualitative, comparison and probable value estimation.

### Probability Estimation (Quantitative Model Checking)

`'Pr[' ( Clock | '#' ) '<=' CONST '](' ('<>' | '[]') Expression ')'`

Quantitative query estimates the probability of a path expression being true given that the predicate in probability brackets is true. Intuitively the model exploration is bounded by an expression in the brackets: it can be limited by setting the bound on a clock value, model time or the number of steps (discrete transitions).

The result is an estimated probability (with ε confidence interval specified in statistical parameters) and a number of histograms over the values of the variable specified in the probability brackets. Note that histograms omit runs that do not satisfy the property.

### Hypothesis Testing (Qualitative Model Checking)

`'Pr[' ( Clock | '#' ) '<=' CONST '](' ('<>' | '[]') Expression ')'`

**('<='|'>=') PROB**Hypothesis testing checks whether the probability of a property is less or greater than specified bound. The query is more efficient than probability estimation as it is one sided and requires fewer simulations to attain the same level of significance.

### Probability Comparison

`'Pr[' ( Variable | '#' ) '<=' CONST '](' ('<>' | '[]') Expression ')'`

**('<='|'>=')**'Pr[' ( Variable | '#' ) '<=' CONST '](' ('<>' | '[]') Expression ')'Compares two probabilities indirectly without estimating them.

### Value Estimation

`'E[' ( Clock | '#' ) '<=' CONST ';' CONST ']' '(' ('min:'|'max:' Expression ')'`

Estimates the value of an expression by running a given number of simulations.

### Examples

`Pr[<=100] (<> Train.Cross)`- estimates the probability of the process
`Train`reaching the location`Cross`within 100 model time units. The tool will produce a number of histograms over model time, like probability density distribution of`Train.Cross`becoming true over model time, thus allowing to inspect what the most likely moment in time is when the train arrives at crossing. `Pr[cost<=1000] (<> Plane.Landing)`- estimates the probability of the process
`Plane`reaching the location`Landing`within 1000 cost units where clock variable`cost`has various rates in different locations. The tool will produce a number of histograms over the`cost`values, like a probability density distribution of`Plane.Landing`becoming true over cost, thus allowing to inspect what the most likely cost is when the plane lands.

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