Topics in Timed Automata

Instructor :   B Srivathsan        Email :

Course description

Timed automata are an interesting model of automata, offering challenging language theoretic as well as verification questions. A number of mathematical techniques have been employed in the study of this model. The goal of this course is to understand deeply this model and get acquainted with the different mathematical techniques used in its analysis.

The course is mainly aimed at Ph.D and Master level students, interested in Automata theory and Formal Verification. The skills developed during the course are fairly general and the hope is that they could be used in the analysis of various other models (which are being studied as part of respective Ph.Ds!).

A detailed description of the topics covered during the course is given in the "Lecture plan" below.


This is a non-credit course and would consist in 10 lectures, spanning 1 hour each. The lectures would carry a theoretical flavour and would involve a good bit of problem solving during the lecture itself.

As it is a non-credit course, it goes without saying that there would be no homeworks or exams! One could consider this course as a series of 10 self-contained (entertaining) talks. Optional practice exercises would be provided from time to time, which could help enhance the understanding.

The lectures would be given in English.


Introductory course on automata theory, Turing machines and complexity classes


6 consecutive Wednesdays starting from 31.10.2012 and

4 consecutive Fridays starting from 16.11.2012

Lecture 1 31.10.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides
Lecture 2 07.11.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides
Lecture 3 14.11.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides
Lecture 4 16.11.2012 (Fri) 9:30 - 10:30 Room 5055 Slides
Lecture 5 21.11.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides
Lecture 6 23.11.2012 (Fri) 9:30 - 10:30 Room 5055 Slides
Lecture 7 28.11.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides
Lecture 8 30.11.2012 (Fri) 9:30 - 10:30 Room 5055 Slides
Lecture 9 05.12.2012 (Wed) 15:30 - 16:30 i1 Seminar Room Slides     Slides of Ouaknine on this subject
Lecture 10 07.12.2012 (Fri) 9:30 - 10:00 Room 5055 Board presentation

Lecture plan

The course would focus on four fundamental problems of timed automata: determinization, language inclusion, emptiness and Zenoness.

A tentative division into lectures follows.

Lecture 1: Timed languages and timed automata

  • Introduction to timed languages and timed automata - examples of timed languages - notion of timed languages as "properties" over time

  • What languages (properties) can one express using timed automata? - Timed regular languages

  • Closure properties of timed regular languages - non-closure under complementation

  • Adding silent transitions to timed automata

Lecture 2: Determinization

  • The role of non-determinism on time - a timed automaton that cannot be determinized

  • Closure properties of deterministic timed regular languages

  • What power of the timed automaton can one remove to get determinizable subclasses? - Event recording automata - Integer reset automata

Lecture 3: Language inclusion is undecidable

  • Given timed automata A and B, the question L(B) ⊆ L(A)? is undecidable

  • A careful working out of the proof of undecidability to understand what is the cause

Lecture 4: A decidable case of the inclusion problem

  • Inclusion L(B) ⊆ L(A)? becomes decidable when A has at most one clock

  • Proof of this decidability

Lecture 5: Alternating timed automata

  • Adding universal transitions to timed automata - notion of alternation

  • A class of languages closed under boolean operations

  • Decidable emptiness when restricted to one clock - non-primitive recursive complexity

Lecture 6: Emptiness problem - introduction to zones and abstractions

  • Zones - potentially infinite zone graph

  • Abstractions - coarse abstractions - abstractions from simulations - maximal bounds

  • Order of exploration affecting the search

Lecture 7: More on abstractions

  • Optimality of the region-closure abstraction, given only maximal bounds

  • Lower-upper bound abstractions

  • To get coarser, get better parameters for abstraction - static analysis - an insight into constant propagation during search

Lecture 8: Infinite runs and non-Zenoness

  • Zeno runs - the question of existence of a non-Zeno run

  • Adding an auxiliary clock to take care of non-Zenoness

  • This extra clock can give rise to exponential blowup!

Lecture 9: Time bounded verification

  • What happens when we say that time is bounded by N?

  • Decidability of emptiness for alternating timed automata

Lecture 10:Diagonal constraints

  • Diagonal constraints do not add expressive power

  • Timed automata with diagonal constraints are exponentially more concise than diagonal free timed automata


[1] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183-225, 1994.

[2] R. Alur and P. Madhusudhan. Decision problems for timed automata: A survey. Proceedings of SFM, 2004.

[3] B. Bérard, A. Petit, V. Diekert, P. Gastin. Characterization of the expressive power of silent transitions in timed automata. Fundam. Infor. 36(2-3): 145-182, 1998

[4] R. Alur, L. Fix and T. A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theor. Comp. Sci., 211(1-2): 253-273, 1999.

[5] C. Baier, N. Bertrand, P. Bouyer, T. Brihaye. When are timed automata determinizable? Proceedings of ICALP, 2009.

[6] P. V. Suman, P.K. Pandya, S.N. Krishna, and L. Manasa. Timed automata with integer resets: Language inclusion and expressiveness. Proceedings of FORMATS, 2008.

[7] J. Ouaknine and J. Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. Proceedings of LICS, 2005.

[8] S. Lasota and I. Walukiewicz. Alternating timed automata. ACM Trans. Comput. Log., 9(2), 2008.

[9] C. Daws and S. Tripakis. Model-checking of real-time reachability properties using abstractions. Proceedings of TACAS, 1998

[10] P. Bouyer. Forward analysis of updateable timed automata. FMSD 24(3): 281-320, 2004.

[11] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Better abstractions for timed automata. Proceedings of LICS, 2012.

[12] G. Behrmann, P. Bouyer, K.G. Larsen, R. Pelánek. Lower and upper bounds in zone based abstractions of timed automata. STTT 8(3): 204-215, 2006.

[13] F. Herbreteau, D. Kini, B. Srivathsan and I. Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. Proceedings of FSTTCS, 2011.

[14] S. Tripakis, S. Yovine, A. Bouajjani. Checking timed Büchi automata emptiness efficiently. FMSD 26(3): 267-292, 2005.

[15] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient emptiness check for timed Büchi automata. FMSD 40(2): 122-146, 2012.

[16] F. Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect. Proceedings of CONCUR, 2011.

[17] B. Srivathsan. Abstractions for timed automata. Ph.D Thesis, Université of Bordeaux, 2012.

[18] P. Bouyer, F. Chevalier. On conciseness of extensions of timed automata. Journal of Automata, Languages and Combinatorics 10(4), pages 393-405, 2005.