Reading course (seminar): Quantitative Verification and Timed Automata

Dates and rooms

The reading course will be held in one block towards the end of the term. In a first meeting we will discuss possible topics and participants can then choose from the papers listed below.

The date of the initial meeting is Wednesday, 26th October 2011, Room FR 6079.

Contents

Model-checking has become a widely used and successful method for verifying reactive systems - such as hardware systems, controllers or communication protocols - and is increasingly used in the verification of software systems as well. Many current model-checkers focus on deciding whether a process meets a certain requirement such as responsiveness, fairness and similar properties which can either be true or false.

However, for many applications it is not only enough to verify that certain error states cannot be reached, but timing constraints become equally important. A typical example is the verification of electronic brake systems: it is not enough to certify that every time the driver uses the break pedal of his car, the car will eventually engage the breaks. Instead we usually want to verify that the break is engaged within a certain time span after the pedal has been pressed.

In this reading course we will study the fundamental methods developed for such verification tasks. More specifically, we will study automata models incorporating time constraints and associated timed logics. We will study the various models of time that can be used and the effects this has on complexity and applicability of quantitative model-checking.

Possible topics

  1. "A Theory of Timed Automata" by Alur and Dill
  2. "On the language inclusion problem for timed automata: Closing a decidability gap" by Ouaknine and Worrell
  3. Alur, Feder, Henzinger: The Benefits of Relaxing Punctuality. PODC 1991: 139-152
  4. Henzinger, Manna, Pnueli: What Good Are Digital Clocks? ICALP 1992: 545-558
  5. Alur, Courcoubetis, Dill: Model-Checking in Dense Real-time Inf. Comput. 104(1): 2-34 (1993)
  6. "Minimum-Cost Reachability for Priced Timed Automata" by Behrmann et al.
  7. Hirshfeld, Rabinovich: Timer formulas and decidable metric temporal logic. Inf. Comput. 198(2): 148-178 (2005)
  8. Hirshfeld, Rabinovich: Decidable metric logics. Inf. Comput. 206(12): 1425-1442 (2008)
  9. Ouaknine, Worrell: On Metric Temporal Logic and Faulty Turing Machines. FoSSaCS 2006: 217-230
  10. Ouaknine, Worrell: On the Decidability of Metric Temporal Logic. LICS 2005: 188-197
  11. Alur, P. Madhusudan: Decision Problems for Timed Automata: A Survey. SFM 2004: 1-24
  12. Henzinger, Kopke, Puri, Varaiya: What's decidable about hybrid automata? STOC 1995: 373-382
  13. Puri: Dynamical Properties of Timed Automata. FTRTFT 1998: 210-227
  14. Bouyer, Brinksma, Larsen: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1): 3-23 (2008)
  15. Bouyer, Chevalier and Markey. On the Expressiveness of TPTL and MTL. In FSTTCS'05, LNCS 3821, pages 432-443. Springer, 2005.
  16. Bouyer. Forward Analysis of Updatable Timed Automata. Formal Methods in System Design 24(3), pages 281-320, 2004
  17. Ouaknine, Rabinovich, and Worrell. Time-bounded verification. Proceedings of CONCUR 09, LNCS 5710, 2009.