21st International Conference on Application and Theory of Petri Nets
Aarhus, Denmark, June 26-30, 2000

 Advanced Tutorial on Timed and
Hybrid  Automata

Kim G. Larsen, Mogens Nielsen, P.S. Thiagarajan
Tuesday, June 27, 2000


 


Aims

In 1989, Rajeev Alur and David Dill introduced the notion of timed automata together with some basic decidability (and undecidability) results. Since then, this formalism and its hybrid extensions have proved extremely useful in modeling real-time and hybrid behaviour, while allowing for efficient  automatic analysis of real-time temporal properties.  In this tutorial we aim at familiarizing the audience with  the basic ideas of these models, the associated real-time logics, and the fundamental techniques underlying a number of associated decidability results. We will also address the relationship to timed extensions of Petri Nets.   The first theoretical decidability results was based on the so-called region technique.  Since then a number of tools for automatic verification of real-time and hybrid systems has emerged (e.g.UPPAAL and HyTech). These  tools have been successfully applied in a number of industrial case studies, and their implementations are based  on variety of newly developed, efficient data structures and algorithms for symbolic representation and manipulation of the state-space of real-time and hybrid systems.  In the tutorial, we will offer a detailed explanation to the most promising of these techniques.
 

Schedule of the tutorial
 
 9.00-9:45 Basic Models for Timed Systems
by Mogens Nielsen and P.S. Thiagarajan
 10.00-10.45 The Region Technique
by Mogens Nielsen and P.S. Thiagarajan
10.45-11.15 Coffee Break
11.15-12.00 Efficient Symbolic Verification of Timed Systems
by Kim G. Larsen
12.00-14.00 Lunch
14.00-14.45 Tools and Case Studies
by Kim G. Larsen
15.00-15.45 Logics and Preorders for Timed Systems
by Kim G. Larsen
15.45-16.15 Coffee Break
16.15-17.00 Hybrid Automata
by Mogens Nielsen and P.S. Thiagarajan

 

Suggested Material

Basic Reading Material

Joost-Pieter Katoen:
    Concepts, Algorithms, and Tools for Model Checking. (Lecture Notes from Erlangen),
    chapter 4.

Kim G. Larsen, Paul Pettersson and Wang Yi: UPPAAL in a Nutshell. In Springer International
     Journal of Software Tools for Technology Transfer 1(1+2), 1997.

Larsen, Steffen, Weise: Continuous Modelling of Real Time and Hybrid Systems, in Journal for Software Tools
     for Technology Transfer, vol 1, 1997.
 
 

Relevant Research papers:

R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science 126:183-235, 1994 (preliminary
     versions appeared in Proc. 17th ICALP, LNCS 443, 1990, and Real Time: Theory in Practice, LNCS 600, 1991).

R. Alur, C. Courcoubetis, D.L. Dill. Model-checking in dense real-time. Information and Computation 104(1):2-34,
     1993 (preliminary version appeared in Proc. 5th LICS, 1990).

Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic model checking for real-time
     systems. Information and Computation 111:193-244, 1994. A preliminary version appeared in the Proceedings of     the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992), pp. 394-406.

 Kim G. Larsen, Paul Pettersson and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time
     Systems. In Proceedings of the 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 5-7 December, 1995.

Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: a determinizable class of timed
     automata. Proceedings of the Sixth International Conference on Computer-aided Verification (CAV 1994), Lecture
     Notes in Computer Science 818, Springer-Verlag, 1994, pp. 1-13.

Johan Bengtsson, Bengt Jonsson, Johan Lilius and Wang Yi. Partial Order Reductions for Timed Systems. In
     proceedings of the 9th International Conference on Concurrency Theory. Nice, France, September 1998.

Gerd Behrmann, Kim G.Larsen, Justin Pearson, Carsten Weise, and Wang Yi.: Efficient Timed Reachability Analysis Using Clock Difference Diagrams.   Computer Aided Verification 1999.

Kim G. Larsen, Carsten Weise, Wang Yi and Justin Pearson. Clock Difference Diagrams. DoCS Technical
     Report Nr 98/99, Uppsala University, ISSN 0283-0574, August 1998. To appear in special NWPT issue of Nordic Journal of Computing.

M. Minea : Partial Order Reductions for Model Checking of Timed Automata.
           Proceedings of CONCUR'99, LNCS 1633
 
 

Most of the material can be obtained from the homepages of