• The lecturers for 2013-2014 are Eugene Asarin, François Laroussinie, and Benedikt Bollig.
• This course is 48h and corresponds to 6 ECTS.
• Lectures will take place on Tuesday, 16:15-19:15, in Bat. Sophie Germain, Room 1008.
• The first lecture takes place on September 17.
• The exam is expected to take place on March 11, 16:15-19:15, in Bat. Sophie Germain, Room 1008.
• The first two parts of the course are given by default in French, but it can be decided that they will be in English. The last part is given in English. Exams can be taken in French or English.
• The prerequisites are basic knowledge in automata theory, logics and complexity theory. It is advised to take or have taken course 1.22 “Introduction to verification”. Related courses include course 2.9.1 “Mathematical foundations of the theory of infinite transition systems” and 2.9.2 “Algorithmic verification of programs”, and 2.20.1 “Game-theoretic techniques in computer science” and 2.20.2 “Mathematical foundations of automata theory”.

Embedded systems are more and more widespread (in various applications including telecommunications, transportation, etc.), more and more complex, and often play a critical role. Verifying that they have the expected behaviour is often crucial, and formal verification of embedded systems (in particular model-checking) has been a very active field of research in the last 30 years.

This course focuses on quantitative aspects of model-checking, especially in the model of timed automata and several extensions.

1. Timed and hybrid automata [24h] (Eugene Asarin)
2. Temporal logic for the specification of real-time systems [12h] (François Laroussinie)
3. Modeling and verification of real-time distributed systems [12h] (Benedikt Bollig)

]

Hybrid automata (HA), combining a discrete and a continuous behavior are a natural mathematical model of cyberphysical systems, explored since early 90s. They allow precise modeling of various phenomena. Unfortunately, most of exact verification problems are undecidable even for simple classes of HA. For this reason, two lines of research are extremely important: identification of decidable subclasses of HA and development of methods and tools for approximate verification. The most important subclass of HA with decidable verification problems is the class of timed automata TA. This class is capable to represent and analyze discrete behaviors in continuous time, which is well-adapted to modeling real-time systems, communication protocols, scheduling problems. Verification algorithms, based on results of Alur and Dill, are implemented in several software tools, and used in practice. On the other hand, TA are a popular object of theoretical studies.

We will address most of the following topics:

• Definition of HA
• Modeling by HA (examples from Control, biology, scheduling etc)
• Important subclasses of hybrid automata
• Verification and reachability problems
• Undecidability results
• How to verify HA: theory and practice
• Definition of TA and modeling by TA
• Region graph and decision procedure for TA
• Verification techniques and tools for TA
• Back to HA: some decidable subclasses

—Some references:

1. E. Asarin “Hybrid and Timed Systems: modeling, theory, verification”, 2010, slides
2. P. Koiran, M. Cosnard, and M. Garzon. Computability with low-dimensional dynamical systems. Theoretical Computer Science, 132:113-128, 1994.
3. T. Henzinger, P. Kopke, A. Puri, and P. Varaiya, What's Decidable about Hybrid Automata? Journal of Computer and System Sciences 57:94–124, 1998.
4. E. Asarin, O. Maler, A. Pnueli, Reachability analysis of dynamical systems having piecewise-constant derivatives, Theoretical Computer Science 138, 35-65, 1995
5. R. Alur. Timed Automata (Survey of theory of timed automata for the School on Formal Methods, real-Time, Bertinoro, 2004) slides PPT
6. R. Alur. Timed Automata. in 11th International Conference on Computer-Aided Verification, LNCS 1633, pp. 8-22, Springer-Verlag, 1999
7. E. Asarin, P. Caspi, O. Maler, Timed Regular Expressions, Journal of the ACM 49, No.2, 2002, 172-206

—Lecture notes:

• Cours 1 et 2 : automates hybrides,semi-decidability,undecidability
• TD1 : TD modeling
• TD2 : TD undecidability
• TD3 : TD timed
• TD4 : TD decidability

More details to come.

Lecture Notes:

• Version as of 18/02/2014: Slides; Handout

Tentative Dates:

• 04/02/2014
• 11/02/2014
• 18/02/2014
• 25/02/2014

Topics:

• Networks of Timed Automata
• Message Sequence Charts
• Time(d) Petri Nets

Some References:

• S. Akshay, B. Bollig, P. Gastin, M. Mukund, and K. Narayan Kumar. Distributed Timed Automata with Independently Evolving Clocks. Fundamenta Informaticae, 2013. To appear.
• R. Alur, G.J. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70-77, 1996.
• P. Gastin, M. Mukund, and K. Narayan Kumar. Reachability and boundedness in time-constrained MSC graphs. In Perspectives in Concurrency Theory, IARCS-Universities, pages 157-183. Universities Press, 2009.
• P. Bouyer, S. Haddad, and P.-A. Reynier. Timed Petri Nets and Timed Automata: On the Discriminating Power of Zeno Sequences. Information and Computation 206(1), pages 73-107, 2008.