Title
Timed Automata
Type
Weekly Seminar in Theoretical CS (at Aachen)
News
27. Jan. 2009 | Die Ergebnisse der Evaluierung sind verfügbar. |
21. Juli 2008 | Mit einem Wochenende Verspätung, aber immerhin: die Zuteilung der Themen findet sich unten. In Kürze werden auch die relevanten Literaturreferenzen online gestellt.
Update: auch die Literatur sowie die den Themen zugeordneten Betreuer sind unten angegeben. |
17. Juli 2008 |
Contents
Reactive systems such as device drivers, coffee machines, communication
protocols, and automatic teller machines, to mention a few, must react
in time: They are time-critical. The behavior of time-critical systems
is typically subject to rather stringent timing constraints. For a
train crossing it is essential that on detecting the approach of a
train, the gate is closed within a certain time bound in order to halt
car and pedestrian traffic before the train reaches the crossing. For a
radiation machine the time period during which a cancer patient is
subjected to a high dose of radiation is extremely important; a small
extension of this period is dangerous and can cause the patient's death.
To put it in a nutshell:
protocols, and automatic teller machines, to mention a few, must react
in time: They are time-critical. The behavior of time-critical systems
is typically subject to rather stringent timing constraints. For a
train crossing it is essential that on detecting the approach of a
train, the gate is closed within a certain time bound in order to halt
car and pedestrian traffic before the train reaches the crossing. For a
radiation machine the time period during which a cancer patient is
subjected to a high dose of radiation is extremely important; a small
extension of this period is dangerous and can cause the patient's death.
To put it in a nutshell:
Correctness in time-critical systems not only depends on the logical
result of the computation but also on the time at which the results
are produced.
As timeliness is of vital importance to reactive systems, it is
essential that the timing constraints of the system are guaranteed to be
met. Checking timing constraints is the subject of this seminar. The
central theme of this seminar is timed automata, basically an extension
of classical finite-state automata with clock variables. All papers in
this seminar are based on timed automata. Topics include:
essential that the timing constraints of the system are guaranteed to be
met. Checking timing constraints is the subject of this seminar. The
central theme of this seminar is timed automata, basically an extension
of classical finite-state automata with clock variables. All papers in
this seminar are based on timed automata. Topics include:
- How can we model-check real-time constraints?
- Which decision problems on timed automata are decidable?
- Is there a relation between timed automata and timed regular expressions?
- How to solve scheduling problems using timed automata?
- Extensions of timed automata with energy consumption and continuously
changing variables, such as temperature: What remains decidable and
what does not? - What happens if clocks are subject to perturbations?
Topics
In the following table you shall find the list of topics. A short introduction to each topic will be given on Thursday, 17. July, 14:00, Room 4201b.
Talks are scheduled as "double features" from 15:45 to 17:15 on Tuesday. The calendar dates are shown below.
Nr | Date | Topic | Student | Supervisor |
|---|---|---|---|---|
1 | 28.10. | History Lesson: David Dills first approach towards timed automata | ||
2 | 28.10. | Timed automata: the classical Alur/Dill paper. | ||
3 | 04.11. | Decision problems with timed automata | ||
4 | 04.11. | Timed CTL | (entfällt) | |
5 | 11.11. | Time-abstracting bisimulations for discrete abstraction | ||
6 | 11.11. | Complexity of model checking timed automata | (entfällt) | |
7 | 18.11. | Parametric model checking | ||
8 | 18.11. | Timed regular expressions. | ||
9 | 25.11. | Efficient zone automaton computation | (entfällt) | |
10 | 25.11. | Hybrid automata | (entfällt) | |
11 | 02.12. | Timed testing using timed automata | ||
12 | 09.12. | Modest: A compositional modeling formalism for real-time and stochastic systems | ||
13 | 09.12. | Using timed automata to solve scheduling problems | ||
14 | 16.12. | More on scheduling | ||
15 | 16.12. | How much does it cost? Priced timed automata | ||
16 | 13.01. | More about priced timed automata | ||
17 | 13.01. | Adding probability: probabilistic timed automata | ||
18 | 20.01. | Robustness of timed automata | (entfällt) | |
19 | 20.01. | A tool for hybrid automata verification: PHAVER | Koch | |
20 | 20.01. | Implementation Aspects: Clock Difference Diagrams |
Literature
Topic | Literature |
|---|---|
1 | David L. Dill: Timing Assumptions and Verification of Finite-State Concurrent Systems. Automatic Verification Methods for Finite State Systems 1989: 197-212 |
2 | Rajeev Alur, David L. Dill: A Theory of Timed Automata. Theor. Comput. Sci. 126(2): 183-235 (1994) |
3 | Rajeev Alur, P. Madhusudan: Decision Problems for Timed Automata: A Survey. SFM 2004: 1-24 |
4 | Rajeev Alur, Costas Courcoubetis, David L. Dill: Model-Checking in Dense Real-time Inf. Comput. 104(1): 2-34 (1993) |
5 | Stavros Tripakis, Sergio Yovine: Analysis of Timed Systems Using Time-Abstracting Bisimulations. Formal Methods in System Design 18(1): 25-68 (2001) |
6 | François Laroussinie, Nicolas Markey, Ph. Schnoebelen: Model Checking Timed Automata with One or Two Clocks. CONCUR 2004: 387-401. LNCS, Springer Verlag. |
7 | Véronique Bruèyre, Emmanuel Dall'Olio, Jean-François Raskin: Durations and parametric model-checking in timed automata. ACM Trans. Comput. Log. 9(2), 2008. |
8 | Eugene Asarin, Paul Caspi, Oded Maler: Timed regular expressions. J. ACM 49(2): 172-206 (2002) |
9 | Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek: Lower and upper bounds in zone-based abstractions of timed automata. STTT 8(3): 204-215 (2006) |
10 | Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, Sergio Yovine: The Algorithmic Analysis of Hybrid Systems. Theor. Comput. Sci. (TCS) 138(1):3-34 (1995) |
11 | Anders Hessel, Kim Guldstrand Larsen, Marius Mikucionis, Brian Nielsen, Paul Pettersson, Arne Skou: Testing Real-Time Systems Using UPPAAL. Formal Methods and Testing 2008: 77-117 |
12 | Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, and Joost-Pieter Katoen. MoDeST: A compositional modeling formalism for real-time and stochastic systems. IEEE Transactions on Software Engineering, 32(10):812–830, 2006. |
13 | Elena Fersman, Pavel Krcal, Paul Pettersson, Wang Yi: Task automata: Schedulability, decidability and undecidability. Inf. Comput. 205(8): 1149-1172 (2007) |
14 | Yasmina Abdeddaïm, Eugene Asarin, Oded Maler: Scheduling with timed automata. Theor. Comput. Sci. 354(2): 272-300 (2006) |
15 | Patricia Bouyer, Ed Brinksma, Kim Guldstrand Larsen: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design 32(1): 3-23 (2008) |
16 | Goran Frehse: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3): 263-279 (2008) |
17 | Patricia Bouyer, Thomas Brihaye, Véronique Bruèyre, Jean-François Raskin: On the optimal reachability problem of weighted timed automata. Formal Methods in System Design 31(2): 135-175 (2007) |
18 | Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282(1): 101-150 (2002) |
19 | Anuj Puri: Dynamical Properties of Timed Automata. FTRTFT 1998: 210-227. |
21 | Gerd Behrmann, Kim Guldstrand Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient Timed Reachability Analysis using Clock Difference Diagrams. CAV '99. Lecture Notes In Computer Science; Vol. 1633, pages 341 - 353. Springer-Verlag, 1999. |
Requirements
- Vordiplom Informatik or Bachelor in Computer Science (in particular:
basic knowledge in Automata Theory and Formal Languages) - The written exposition and the presentation can be done in either
German or English. - Basic knowledge in Model-Checking techniques is not mandatory
but helpful.
Contact person
Thomas Noll (noll at cs.rwth-aachen.de)
