Timed Automata

August - November 2024

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:   2023   2022  2021  2020   2019

Lecture hours

Wed, Fri: 09:10 - 10:30

Lecture Hall 801

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 07.08.2024 (Wed) Timed languages, timed automata, role of clocks and the maximum constant Slides: Motivation for languages

Slides: Lecture 1
Lecture 2 09.08.2024 (Fri) Closure properties Slides: Lecture 2
Lecture 3 12.08.2024 (Mon) Untime of a timed regular language is regular: Region automaton construction Notes Problem sheet 1
Lecture 4 16.08.2024 (Fri) Undecidability of language inclusion Slides Problem sheet 2
Lecture 5 28.08.2024 (Wed) Deterministic Timed Automata; Introduction to event-clock automata Slides

Slides
Lecture 6 30.08.2024 (Fri) Event-clock automata - II Slides
Lecture 7 04.09.2024 (Wed) Event-clock automata - no finite region equivalence Sections 2 and 3 of this paper
Lecture 8 06.09.2024 (Fri) Discussion of Problem Sheet 1
Lecture 9 11.09.2024 (Wed) Discussion of Problem Sheet 2
13.09.2024 (Fri) Quiz 1
Module 2: Verification
Lecture 10 18.09.2024 (Wed) Networks of automata; introduction to zone graphs Slides
Lecture 11 20.09.2024 (Fri) Zone graph examples; truncating the zone graph using simulations Slides

Slides 		Notes

Survey paper

Another survey paper
Lecture 12 25.09.2024 (Wed) Operations on zones using distance graph representation
Module 3: Advanced topics
Lecture 13-14 Universality for one-clock timed automata Slides Video 1     Video 2
Lecture 15 18.10.2024 (Fri) Timed Automata with Diagonal Constraints Notes
Lectures 16-17 Problem Sheet 3

Problem Sheet 4 		Solutions

Solutions 		Video

Video

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