Timed Automata

September - December 2021

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.