Timed Automata Reading Group

If you like to participate, please drop me a mail.

• Martin Stigge
• Nan Guan
• Pontus Ekberg
• Xiaoyue Pan
• Jonatan Lindén
• Jari Stenman
• Zhang Yi
• Mingsong Lv
• Jonas Flodin
• Philipp Rümmer
• Kai Lampka
• Wang Yi

1. Timed Automata Basics (definition, reachability, region equivalence)
   • Sections 1, 3, 4 of "A Theory of Timed Automata", R. Alur and D. L. Dill , 1994
2. Efficient reachability analysis using DBMs
   • Sections 1-4 of "Timed Automata: Semantics, Algorithms and Tools", J. Bengtsson and W. Yi, 2004
3. Properties supported by UPPAAL
   • "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications", E. M. Clarke, E. A. Emerson and A. P. Sistla, 1986
4. Hybrid Automata, Stopwatch Automata
   • Sections 1, 2 and 4 up to 4.1 of "What's Decidable about Hybrid Automata?", T. Henzinger, P. Kopke, A. Puri and P. Varaiya, 1995
   • Sections 7 and 8 of "Foundations Of Timed And Hybrid Automata: A Survey", V. Suman and P. Pandya, 2006
5. Task Automata
   • "Task Automata: Schedulability, Decidability and Undecidability", E. Fersman, P. Krcal, P. Pettersson and W. Yi, 2007
6. Event-recording Automata
   • "Event-Clock Automata: A Determinizable Class of Timed Automata", R. Alur, L. Fix and T. Henzinger, 1999
7. Timed Games
   • "Efficient On-the-fly Algorithms for the Analysis of Timed Games.", F. Cassez, A. David, E. Fleury, K. Larsen and D. Lime, 2005
8. Priced Timed Automata
   • "As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata", K. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson and J. Romijn, 2001
9. Partial Order Reduction
   • "On Interleaving in Timed Automata", R. B. Salah, M. Bozga, O. Maler, 2006
   • Chapter 3 of "On Timing Analysis of Large Systems", Ph.D. Thesis of Ramzi Ben Salah
10. Timed Pushdown Automata
    • "Dense-Timed Pushdown Automata", P. Abdulla, M. F. Atig and J. Stenman, 2012
    • Long version with proof appendix
11. Stochastic Timed Automata
    • ?

Additional Reading

• "Decision problems for timed automata: A Survey", R. Alur and P. Madhusudan, 2004
• "Symbolic Model Checking for Real-Time Systems", T. Henzinger, X. Nicollin, J. Sifakis and S. Yovine, 1992
• "Defining Liveness", B. Alpern and F. B. Schneider, 1985
• "Partial Order Reductions for Timed Systems", J. Bengtsson, B. Jonsson, J. Lilius and W. Yi, 1998
• "Adding Symmetry Reduction to UPPAAL", M. Hendriks, G. Behrmann, K. Larsen, P. Niebert and F. Vaandrager, 2004