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 deeply this
model and get acquainted with the different mathematical techniques
used in its analysis.
The course is mainly aimed at Ph.D and Master level students,
interested in Automata theory and Formal Verification.
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 (which are being
studied as part of respective Ph.Ds!).
A detailed description of the topics covered
during the course is given in the "Lecture plan" below.
This is a non-credit course and would consist in 10 lectures,
spanning 1 hour each. The lectures would carry a theoretical flavour and
would involve a good bit of problem solving during the lecture
itself.
As it is a non-credit course, it goes without saying that there
would be no homeworks or exams! One could consider this course as a
series of 10 self-contained (entertaining) talks. Optional practice
exercises would be provided from time to time, which could help
enhance the understanding.
The lectures would be given in English.
Lecture 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
|
Lecture 2: Determinization
-
The role of non-determinism 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
|
Lecture 3: Language inclusion is undecidable
-
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
|
Lecture 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
|
Lecture 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
|
Lecture 6: Emptiness problem - introduction to zones and
abstractions
-
Zones - potentially infinite zone graph
-
Abstractions - coarse abstractions - abstractions from
simulations - maximal bounds
-
Order of exploration affecting the search
|
Lecture 7: More on abstractions
-
Optimality of the region-closure abstraction, given only
maximal bounds
-
Lower-upper bound abstractions
-
To get coarser, get better parameters for abstraction - static
analysis - an insight into constant propagation during search
|
Lecture 8: Infinite runs and non-Zenoness
-
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!
|
Lecture 9: Time bounded verification
-
What happens when we say that time is bounded by N?
-
Decidability of emptiness for alternating timed automata
|
Lecture 10:Diagonal constraints
-
Diagonal constraints do not add expressive power
-
Timed automata with diagonal constraints are exponentially
more concise than diagonal free timed automata
|
