Timed Automata

August - November 2020

Course description

Timed automata are an interesting model of automata, offering challenging language theoretic as well as verification questions. A number of mathematical 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.

Lecture hours

Tue, Thu: 21:00 - 22:15

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

Prerequisites

Theory of Computation

Schedule

Lecture 1 18.08.2020 (Tue) Timed languages and timed automata Slides Video
Lecture 2 20.08.2020 (Thu) Timed regular languages, Closure properties, Epsilon transitions Slides Video Problem sheet 1
Lecture 3 25.08.2020 (Tue) Untiming construction - Part I Slides Video Problem sheet 2
Lecture 4 27.08.2020 (Thu) Untiming construction - Part II Slides Video Notes
Lecture 5 01.09.2020 (Tue) Undecidability of language inclusion Slides Video
Lecture 6 03.09.2020 (Thu) Undecidability of language inclusion - details Slides Video Problem sheet 3
Lecture 7 09.09.2020 (Tue) Deterministic timed automata Slides Video
Lecture 8 11.09.2020 (Thu) Event-clock automata Slides Video Sections 1, 2 and 3 of [4]
Lecture 9 15.09.2020 (Tue) Comparison of expressive power: ECA and TA Slides Video Section 5 of [4]
Lecture 10 22.09.2020 (Tue) Emptiness problem: introduction to zone based algorithm Slides Video
Lecture 11 22.09.2020 (Thu) Adding simulations to the zone based forward analysis Slides Video
Lecture 12 29.09.2020 (Tue) Problem solving session Problem sheet 4     Some solutions Video
Lecture 13 01.10.2020 (Thu) Universality is decidable for one-clock timed automata - I Slides Video [6]
Lecture 14 06.10.2020 (Tue) Universality is decidable for one-clock timed automata - II Slides Video [6]
Lecture 15 08.10.2020 (Thu) Timed automata with diagonal constraints Slides Video Notes
Lecture 16 13.10.2020 (Tue) Problem solving session Problem sheet 5     Some solutions Video
Lecture 17 15.10.2020 (Thu) When are timed automata determinizable? Slides Video
Lecture 18 20.10.2020 (Tue) Alternating Timed Automata - Part 1 Slides Video
Lecture 19 22.10.2020 (Thu) Alternating Timed Automata - Part 2 Slides Video
Lecture 20 27.10.2020 (Tue) Alternating Timed Automata - Part 3 Slides Video
29.10.2020 (Thu) Student project presentations - Stage 1
Lecture 21 04.11.2020 (Tue) Updatable Timed Automata - Part 1 Slides Video
Lecture 22 05.11.2020 (Thu) Updatable Timed Automata - Part 2 Slides Video
12.11.2020 (Thu) Student Project presentations - Stage 2
Lecture 23 19.11.2020 (Tue) Updatable Timed Automata - Part 3 Slides Video
Lecture 24 21.11.2020 (Thu) Problem solving session Problem sheet 6     Some solutions

Topics

The course would focus on four fundamental problems of timed automata: determinization, language inclusion, emptiness and Zenoness.

A tentative list of topics follows.

Topic 1: Timed languages and timed automata

  • Introduction to timed languages and timed automata - examples of timed languages - notion of timed languages as "properties" over time

  • What languages (properties) can one express using timed automata? - Timed regular languages

  • Closure properties of timed regular languages - non-closure under complementation

  • Adding silent transitions to timed automata

Topic 2: Determinization

  • The role of non-determism on time - a timed automaton that cannot be determinized

  • Closure properties of deterministic timed regular languages

  • What power of the timed automaton can one remove to get determinizable subclasses? - Event recording automata - Integer reset automata

Topic 3: Undecidability of the inclusion problem

  • Given timed automata A and B, the question L(B) ⊆ L(A)? is undecidable

  • A careful working out of the proof of undecidability to understand what is the cause

Topic 4: A decidable case of the inclusion problem

  • Inclusion L(B) ⊆ L(A)? becomes decidable when A has at most one clock

  • Proof of this decidability

Topic 5: Alternating timed automata

  • Adding universal transitions to timed automata - notion of alternation

  • A class of languages closed under boolean operations

  • Decidable emptiness when restricted to one clock - non-primitive recursive complexity

Topic 6: Reachability problem - introduction to zones

  • Zones - potentially infinite zone graph

  • Simulations

Topic 7: Infinite runs of timed automata and the strongly non-Zeno construction

  • Zeno runs - the question of existence of a non-Zeno run

  • Adding an auxiliary clock to take care of non-Zenoness

  • This extra clock can give rise to exponential blowup!

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] G. Behrmann, P. Bouyer, K.G. Larsen, R. Pelánek. Lower and upper bounds in zone based abstractions of timed automata. STTT 8(3): 204-215, 2006.

[12] F. Herbreteau, D. Kini, B. Srivathsan and I. Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. Proceedings of FSTTCS, 2011.

[13] S. Tripakis, S. Yovine, A. Bouajjani. Checking timed Büchi automata emptiness efficiently. FMSD 26(3): 267-292, 2005.

[14] F. Herbreteau, B. Srivathsan and I. Walukiewicz. Efficient emptiness check for timed Büchi automata. FMSD 40(2): 122-146, 2012.

[15] F. Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect. Proceedings of CONCUR, 2011.

[16] B. Srivathsan. Abstractions for timed automata. Ph.D Thesis, Université of Bordeaux, 2012.