Timed Automata

August - November 2022

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

Lecture hours

Mon, Wed, Fri: 09:10 - 10:25

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, Complexity of reachability in timed automata with two clocks, Timed logics

Evaluation

2 Quizzes : 30%

Mid-semester exam: 30%

Project: 40%

Schedule

Module 1: Basics
Lecture 1 01.08.2022 (Mon) Timed languages, timed automata, role of clocks and the maximum constant, epsilon transitions Slides: Motivation for languages

Slides: Lecture 1
Lecture 2 03.08.2022 (Wed) Closure under union, intersection; non-closure under complement Slides Tutorial 1
Lecture 3 05.08.2022 (Fri) Untiming construction: region equivalence and region automaton Notes Tutorial 2
Lecture 4 08.08.2022 (Mon) Deterministic Timed Automata Slides
Lecture 5 10.08.2022 (Wed) Event-recording automata Slides
Lecture 6 12.08.2022 (Fri) Event-Predicting Automata, Event-Clock Automata Slides Tutorial 3
Lecture 7 17.08.2022 (Wed) Converting ECA to NTA Slides
Lecture 8 22.08.2022 (Mon) Language inclusion is undecidable Slides
Module 2: Verification
Lecture 9 24.08.2022 (Wed) Reachability algorithm using zones Notes
Lecture 10 26.08.2022 (Fri) Zone graph; zone graph with simulations Notes
Lecture 11 29.08.2022 (Mon) Distance graphs for representing zones; algorithms for the successor computation
Lecture 12 02.09.2022 (Fri) Algorithm for checking region-closure-inclusion between zones
Long break
Lecture 13 05.10.2022 (Wed) Illustrating the region-closure-inclusion test on examples Notes
Lecture 14 07.10.2022 (Fri) Two variable lemma: region does not intersect a zone iff there is a small negative cycle Notes
Lecture 15 12.10.2022 (Wed) Proof of final test: one direction
Lecture 16 14.10.2022 (Fri) Proof of final test: the other direction Notes

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