# Contents

# Semantics

In the following we give a pseudo-formal semantics for UPPAAL. The
semantics defines a timed transition system (*S, s0,* ->)
describing the behaviour of a network of extended timed automata. The
set of states *S* is defined as {(*L, v*) | *v
satisfies Inv*(*L*)}, where *L* is a location
vector, *v* is a function (called a *valuation*) mapping
integer variables and clocks to their values, and *Inv* is a
function mapping locations and location vectors to invariants. The
initial state *s0* is the state where all processes are in the
initial location, all variables have their initial value, and all
clocks are zero. The transition relation, ->, contains two kinds of
transitions: delay transitions and action transitions. We will
describe each type below.

Given a valuation *v* and an expression *e*, we say
that *v* satifies *e* if *e* evaluates to non-zero
for the given valuation *v*.

## Invalid Evaluations

If during a successor computation any expression evaluation is invalid (consult the section on expressions for further details about invalid evaluations), the verification is aborted.

## Delay Transitions

Delay transitions model the passing of time without changing the
current location. We have a delay transition (*L, v*) --(d)-->
(*L, v'*), where *d* is a non-negative real, if and only
if:

*v' = v + d*, where*v+d*is obtained by incrementing all clocks with*d*.- for all
*0 <= d' <= d: v + d' satisfies Inv*(*L*) *L*contains neither committed nor urgent locations- for all locations
*l*in*L*and for all locations*l'*(not necessarily in*L*), if there is an edge from*l*to*l'*then either:- this edge does not synchronise over an urgent channel, or
- this edge does synchronise over an urgent channel, but for all
*0 <= d' <= d*we have that*v + d'*does not satisfy the guard of the edge.

## Action Transitions

For action transtions, the synchronisation label of edges is important. Since UPPAAL supports arrays of channels, we have that the label contains an expression evaluating to a channel. The concrete channel depends on the current valuation. To avoid cluttering the semantics we make the simplifying assumption that each synchronisation label refers to a channel directly.

Priorities increase the determinism of a system by letting a high priority action transition block a lower priority action transition. Note that delay transitions can never be blocked, and no action transition can be blocked by a delay transition.

For action transitions, there are three cases: Internal transitions, binary synchronisations and broadcast synchronisations. Each will be described in the following.

### Internal Transitions

We have a transition (*L, v*) --*--> (*L', v'*) if
there is an edge *e=*(*l,l'*) such that:

- there is no synchronisation label on
*e* *v*satisfies the guard of*e**L' = L*[*l'/l*]*v'*is obtained from*v*by executing the update label given on*e**v'*satisfies*Inv*(*L'*)- Either
*l*is committed or no other location in*L*is committed. - There is no action transition from (
*L, v*) with a strictly higher priority.

### Binary Synchronisations

We have a transition (*L, v*) --*--> (*L', v'*) if
there are two edges *e1=*(*l1,l1'*) and
*e2=*(*l2,l2'*) in two different processes such that:

*e1*has a synchronisation label*c!*and*e2*has a synchronisation label*c?*, where*c*is a binary channel.*v*satisfies the guards of*e1*and*e2*.*L' = L*[*l1'/l1, l2'/l2*]*v'*is obtained from*v*by first executing the update label given on*e1*and then the update label given on*e2*.*v'*satisfies*Inv*(*L'*)- Either
*l1*or*l2*or both locations are committed, or- no other location in
*L*is committed.

- There is no action transition from (
*L, v*) with a strictly higher priority.

### Broadcast Synchronisations

Assume an order *p1, p2, ... pn* of processes given by the
order of the processes in the system declaration statement. We have a
transition (*L, v*) --*--> (*L', v'*) if there is an
edge *e=*(*l,l'*) and *m* edges
*ei=*(*li,li'*) for *1<=i<=m* such that:

- Edges
*e, e1, e2, ..., em*are in different processes. *e1, e2, .... em*are ordered according to the process ordering*p1, p2,... pn*.*e*has a synchronisation label*c!*and*e1, e2, ... em*have synchronisation labels*c?*, where*c*is a broadcast channel.*v*satisfies the guards of*e, e1, e2, ... em*.- For all locations
*l*in*L*not a source of one of the edges*e, e1, e2, ... em*, all edges from*l*either do not have a synchronisation label*c?*or*v*does not satisfy the guard on the edge. *L' = L*[*l'/l, l1'/l1, l2'/l2, ... lm'/lm*]*v'*is obtained from*v*by first executing the update label given on*e*and then the update labels given on*ei*for increasing order of*i*.*v'*satisfies*Inv*(*L'*)- Either
- one or more of the locations
*l, l1, l2, ... lm*are committed, or - no other location in
*L*is committed.

- one or more of the locations
- There is no action transition from (
*L, v*) with a strictly higher priority.