Timed Automata

August - November 2023

Course description

Timed automata are an extension of finite automata to deal with timing constraints between actions. They offer challenging language theoretic as well as verification questions. A number of formal 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.

Previous versions of this course can be found here:   2022 2021  2020   2019

Lecture hours

Tue, Thu: 10:30 - 11:45

Lecture Hall 802

Prerequisites

Theory of Computation

Course content

Basics: Timed regular languages, Decidability of language emptiness, Determinization, Event-clock automata, Undecidability of language inclusion

Verification: Zone based algorithms, Introduction to timed automata tools

Advanced topics: Decidability of language inclusion for one-clock timed automata, Alternating timed automata, Various timed automata extensions

Evaluation

2 Quizzes : 30%

Mid-semester exam: 30%

Project: 40%

Schedule

Module 1: Basics
Lecture 1 08.08.2023 (Tue) Timed languages, timed automata, role of clocks and the maximum constant Slides: Motivation for languages

Slides: Lecture 1
Lecture 2 17.08.2023 (Thu) Closure properties Slides
Lecture 3 31.08.2023 (Thu) Untime of a timed regular language is regular: Region automaton construction Notes Problem Sheet 1

Homework 1
Lecture 4 05.09.2023 (Tue) Undecidability of universality Slides
Lecture 5 07.09.2023 (Thu) Deterministic TA; introduction to event-recording clocks Slides

Slides
Lecture 6 12.09.2023 (Tue) Properties of ERA; Event-predicting automata and event-clock automata Slides Problem Sheet 2
Module 2: Verification
Lecture 7 11.10.2023 (Tue) Networks of timed automata; reachability problem; introduction to zone graphs Slides
Lecture 8 13.10.2023 (Thu) Zone graph examples; truncating the zone graph using simulations Slides

Slides 		Notes

Survey paper

Another survey paper
Lecture 9 17.10.2023 (Tue) Operations on zones using distance graphs
Module 3: Advanced topics
Lecture 10 18.10.2023 (Wed) Universality is decidable for 1-clock timed automata Slides Paper
Lecture 11 19.10.2023 (Thu) Universality for 1-clock timed automata is non-primitive recursive Slides Section 4 of paper
Lecture 12 24.10.2023 (Tue) Timed automata with diagonal constraints Notes
Lecture 13 25.10.2023 (Wed) Updatable timed automata: examples, reachability is undecidable Slides
Lecture 14 26.10.2023 (Thu) Updatable timed automata: expressiveness
Lecture 15 31.10.2023 (Tue) Alternating timed automata
Lecture 16 1.11.2023 (Wed) Alternating timed automata: expressiveness of 1-clock ATA Slides
Lecture 17 2.11.2023 (Thu) Complexity of reachability in timed automata with 2 clocks Slides

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] B. Srivathsan. Reachability in timed automata ACM SIGLOG News, Volume. 9, No. 3, 2022