Lecture 10

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

François Laroussinie, Kim G. Larsen and Carsten Weise. From Timed Automata to Logic - and Back. BRICS report RS-95-2, January 1995. Read at least Sections 1-3 of that paper.
Slides of lecture.
[JPK] Sections 4.3-4.5 of Chapter 4

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: .