Parisian Master of Research in Computer Science

Master Parisien de Recherche en Informatique (MPRI)

Foundations of quantitative and real-time verification (48h, 6 ECTS)

Fondements pour la vérification quantitative et temps-réel

Year 2010-2011: Lecturers

Schedule:

To be announced.

Language:

Students will be allowed to take the exam in French and in English.

Prerequisites and related courses:

Related courses include course 2.09 "Verification of dynamic and parameterized systems", and 2.20.1 "Game-theoretic techniques in computer science" and 2.20.2 "Mathematical foundations of automata theory".

Motivations and objectives of this course

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.

Outline of the course

1. Timed and hybrid automata [24h] (Nicolas Markey)
2. Weighted automata [12h] (Marc Zeitoun)
3. Modeling and verification of real-time distributed systems [12h] (Benedikt Bollig)

Detailled descrition

Part I: Timed and hybrid automata

Lecturer: Nicolas Markey.

This first part will span the first half of the course (8 lectures). The schedule below is tentative:

• Lecture 1: reminders on untimed verification, "weakly-timed" automata.
• Lecture 2: timed automata: definitions, examples, basic properties.
• Lecture 3: timed automata: reachability, region equivalence.
• Lecture 4: timed temporal logics.
• Lecture 5: hybrid automata: definitions, undecidability.
• Lecture 6: hybrid automata: what's decidable?
• Lecture 7: priced timed automata.
• Lecture 8: robustness issues in timed automata.

Sessions 9 and 10 will be revision courses for preparing the mid-term exam.

I will try to post lecture notes here after each course.

Part II: Weighted automata

Lecturer: Marc Zeitoun.

Tentative topics:

• Models for quantitative analysis: weighted automata.
• Decidable and undecidable problems for weighted automata.
• Probabilistic automata and stochastic languages.
• Logics for weighted and probabilistic automata.

References for Part II:

• M. Droste and P. Gastin, Chapter 5 "Weighted Automata and Weighted Logics" of Handbook of weighted automata, Springer, 2009.
• Ch. Baier and J-P. Katoen, Principles of model-checking, MIT Press, 2007. Chapter 10, Probabilistic systems.

Part III: Modeling and verification of real-time distributed systems

Lecturer: Benedikt Bollig.

Tentative topics:

• Models for real-time distributed systems: time Petri-nets, networks of timed automata (with independently evolving clocks), message-passing automata
• Verification: reachability, safety, liveness, state-explosion problem
• Specification languages: message sequence charts

References for Part III:

• S. Akshay, B. Bollig, P. Gastin, M. Mukund and K. Narayan Kumar: Distributed Timed Automata with Independently Evolving Clocks. In CONCUR'08, LNCS 5201, pages 82-97. Springer, 2008.
• D. Lugiez, P. Niebert, S. Zennou: A partial order semantics approach to the clock explosion problem of timed automata. Theoretical Computer Science 345(1), 27–59 (2005).
• S. Akshay: Spécification et vérification pour des systèmes distribués et temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification, ENS Cachan, France, 2010.

References

• Principles of Model Checking. C. Baier, J.P. Katoen. MIT Press, 2008.
• Reactive Systems: Modelling, Specification and Verification. L. Aceto, A. Ingólfsdóttir, K.G. Larsen, J. Srba. Cambridge Univ. Press, 2007.
• Model Checking. E.M. Clarke, O. Grumberg, D.A. Peled. MIT Press, 1999.
• Systems and Software Verification. Model-Checking Techniques and Tools. B. Bérard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit, L. Petrucci, and Ph. Schnoebelen. Springer, 2001.
• The Temporal Logic of Reactive and Concurrent Systems: Specification. Z. Manna and A. Pnueli. Springer, 1991.
• Temporal Verification of Reactive Systems: Safety. Z. Manna and A. Pnueli. Springer, 1995.
• Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems by David Parker, J.J.M.M. Rutten, Marta Kwiatkowska, Gethin Norman, Volume 23 of CRM Monograph Series. American Mathematical Society. P. Panangaden and F. van Breugel (eds.). March 2004.

Previous courses

• Year 2009-2010
• Year 2008-2009
• Year 2007-2008
• Year 2006-2007

Staff