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  nonclosure
under complementation

Adding silent transitions to timed automata

Lecture 2: Determinization

The role of nondeterminism 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 
nonprimitive 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 regionclosure abstraction, given only
maximal bounds

Lowerupper bound abstractions

To get coarser, get better parameters for abstraction  static
analysis  an insight into constant propagation during search

Lecture 8: Infinite runs and nonZenoness

Zeno runs  the question of existence of a nonZeno run

Adding an auxiliary clock to take care of nonZenoness

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
