Timed Automata

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

Lecture hours

Mon, Wed: 09:10 - 10:25

Lectures will be delivered via Zoom. Please join Moodle course page for the link.

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

Quizzes + Homeworks: 50%

Project: 50%

Schedule

 Module 1: Basics Lecture 1 20.09.2021 (Mon) Timed languages, timed automata, closure properties Slides Video Problem Sheet 1 Lecture 2 22.09.2021 (Wed) Untiming construction: why a naïve construction is wrong, adding clock information to states, a neighbourhood equivalence Slides Video Problem Sheet 2 Lecture 3 27.09.2021 (Mon) Untiming construction: discussion of Problem Sheet 2, properties of the neighbourhood equivalence, neighbourhood automaton Slides Video Lecture 4 29.09.2021 (Wed) Untiming construction: the region equivalence and region automaton Slides    Notes Video Problem Sheet 3 Lecture 5 04.10.2021 (Mon) Discussion of Problem Sheets 1 and 3, some new problems Slides Video Lecture 6 11.10.2021 (Mon) Universality is undecidable Slides Video Problem Sheet 4 Lecture 7 13.10.2021 (Wed) Deterministic Timed Automata Slides Video Lecture 8 18.10.2021 (Mon) Event-Recording Automata Slides Video Paper Lecture 9 20.10.2021 (Wed) Event-Predicting Automata, Event-Clock Automata Slides Video  Part 1   Part 2 Lecture 10 25.10.2021 (Mon) ECA to NTA, Expressiveness of ERA, EPA, ECA with DTA and NTA Slides Video Problem Sheet 5 Module 2: Verification Lecture 11 27.10.2021 (Wed) Networks of timed automata, Introduction to zone based algorithm Slides Video Lecture 12 01.11.2021 (Mon) Zone graphs: examples, formal definition, some properties Slides Video Lecture 13 03.11.2021 (Wed) Getting finite truncations of zone graphs Slides Notes Video Problem Sheet 6 Lecture 14 10.11.2021 (Wed) Discussion of Problem Sheets 4, 5 and 6 Slides Video Module 3: Advanced topics Lecture 15 15.11.2021 (Mon) Universality is decidable for one-clock timed automata - Part I Slides Video Lecture 16 17.11.2021 (Wed) Universality is decidable for one-clock timed automata - Part II Slides Video Lecture 17 22.11.2021 (Mon) Universality is decidable for one-clock timed automata - Part III Slides Video Lecture 18 24.11.2021 (Wed) Timed Automata with diagonal constraints - Part I Slides Notes Video Lecture 19 29.11.2021 (Mon) Timed Automata with diagonal constraints - Part II Slides Notes Video Lecture 20 1.12.2021 (Wed) Alternating Timed Automata: model, example, acceptance game Slides Video Lecture 21 06.12.2021 (Mon) Alternating Timed Automata: closure properties, emptiness and one-clock restriction, expressive power of 1-ATAs Slides Video Lecture 22 08.12.2021 (Wed) Alternating Timed Automata: 1-ATA incomparable with 2-NTA Slides Video Lecture 23 13.12.2021 (Mon) Alternating Timed Automata: Emptiness for 1-ATA is non-primitive recursive Slides Video Lecture 24 15.12.2021 (Wed) Updatable Timed Automata: syntax, examples Slides Video Lecture 25 20.12.2021 (Mon) Updatable Timed Automata: emptiness problem Slides Video Lecture 26 22.12.2021 (Wed) Updatable Timed Automata: expressiveness Slides 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.