Timed Automata

March - April 2019

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 this model and get acquainted with the different techniques used in its analysis.

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.

Lecture hours

Tue, Wed, Thu: 9:10 - 10:25 AM

Prerequisites

Introductory course on automata theory

Schedule

Lecture 1 05.03.2019 (Tue) Introduction to timed languages; timed automata Slides (1 - 20)
Lecture 2 07.03.2019 (Thu) Closure properties; Untiming construction Slides (21 - 32)

Notes
Lecture 3 12.03.2019 (Tue) Universality is undecidable for two-clock timed automata Slides

Homework 1 (due March 19)
Lecture 4 14.03.2019 (Thu) Problem solving session
19.03.2019 (Tue) Quiz 1
Lecture 5 21.03.2019 (Thu) Deterministic timed automata, closure properties, introduction to event-clock automata Slides (1 - 16)
Lecture 6 26.03.2019 (Tue) Formal syntax and semantics, determinization, expressive power Paper [4]

Homework 2 (due April 2)
Lecture 7 28.03.2019 (Thu) Universality for one-clock timed automata is decidable Slides
02.04.2019 (Tue) Quiz 2
Lecture 8 03.04.2019 (Wed) Universality for one-clock timed automata is decidable (contd.) Slides
Lecture 9 05.04.2019 (Thu) Universality for one-clock timed automata is decidable (contd.) [6]

Topics

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

A tentative list of topics follows.

Topic 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

Topic 2: Determinization

  • The role of non-determism 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

Topic 3: Undecidability of the inclusion problem

  • 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

Topic 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

Topic 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

Topic 6: Reachability problem - introduction to zones

  • Zones - potentially infinite zone graph

  • Simulations

Topic 7: Infinite runs of timed automata and the strongly non-Zeno construction

  • 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!

References

[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] 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.

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

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

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

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

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

[11] 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.

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

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

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

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

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