## Lecture 12: A Taste of Behavioural Relations and Logics for Timed
Automata

Over the last two lectures, we have introduced timed automata, and
networks of those, as a suitable model for real time
systems. Analyzing models of real time systems, you have also
formulated, and verified, correctness criteria for such systems in
terms of the specification language supported by UPPAAL.

In this lecture, we shall introduce suitable timed versions of the
behavioural equivalences and logics that we had previously studied
over labelled transition systems. In particular, we shall look at
*timed bisimulation* and the logic *L*_{nu} (a timed version of Hennessy-Milner logic
with recursion). We shall see that the logic *L*_{nu} captures timed bisimilarity in much the
same way as Hennessy-Milner logic characterizes standard
bisimilarity.

### Reading Material

### Exercises

You can use the exercise session to finish your work on the mini
project. If you are done with it, or you prefer to have a different
challenge, you can try to solve the following exercises.
#### Exercise 1

Model and analyze the following gossiping girls problem in
UPPAAL. A number of girls initially know one distinct secret
each. Each girl has access to a phone which can be used to call
another girl to share their secrets. Each time two girls talk to each
other they always exchange all secrets with each other (thus after the
phone call they both know all secrets they knew together before the
phone call). Only binary communication (between two girls during each
phone call) is possible.

Task 1: Use UPPAAL to find the minimum number of phone calls needed
for five girls to know all secrets.

Task 2: Try to find an (inductive) argument for how many phone
calls are needed to solve the gossiping girls problem for *n*
girls.

Task 3: Refine your model so that each phone call requires start
time units to connect, and in addition transfer time units to exchange
each secret. Find the minimum time needed to solve the gossiping girls
problem for four girls if start is 30 and transfer is 60.

#### Exercise 2

Consider the two timed automata P1 and P2 above (x is a local clock in
each of the automata). The automata are interacting over an urgent
channel a. Use the test automata for
analyzing bounded liveness properties of the form:

o whenever P1.S1 then P2.S0 within
t time units,

o whenever P1.S0 then P2.S4 within
t time units,

o whenever P1.S0 then P2.S0 will
not occur before t time units.

You can find a downloadable version of the system here (right click and select *Save
target as...*).

Last modified: .