Lecture 1
|
06.03.2017 (Mon)
|
Introduction to omega-languages; Büchi automata;
deterministic vs non-deterministic Büchi automata
|
Slides
|
Sections 1.1, 1.2 (except complementation) of [2]
|
Lecture 2
|
10.03.2017 (Fri)
|
More on Büchi automata, omega-regular expressions, exercises
|
|
Section 1.3 of [2]
|
Lecture 3
|
17.03.2017 (Fri)
|
Linear Temporal Logic; syntax, semantics and examples
|
|
Section 2.1, 2.2, 2.3 of [2]
|
Lecture 4
|
20.03.2017 (Mon)
|
LTL to Büchi automata
|
|
Section 2.4 of [2], [3]
|
Lecture 5
|
24.03.2017 (Fri)
|
Kripke structures, LTL model checking, reducing 3CNF SAT to
LTL model checking
|
|
Section 2.5 of [2] (except Theorem 2.2)
|
Lecture 6
|
27.03.2017 (Mon)
|
Computation Tree Logics CTL, CTL*; comparison with LTL
|
Slides
|
Lemma 6.19 of [1]
|
Lecture 7
|
31.03.2017 (Fri)
|
CTL model checking algorithm
|
Slides
|
|
Lecture 8
|
03.04.2017 (Mon)
|
Timed languages and timed automata
|
Slides
|
|
Lecture 9
|
07.04.2017 (Fri)
|
Closure properties of timed languages
|
Slides
|
|
Lecture 10
|
10.04.2017 (Mon)
|
Untiming construction
|
Notes
|
|
Lecture 11
|
12.04.2017 (Wed)
|
Undecidability of language inclusion for timed automata
|
Slides
|
|
Lecture 12
|
14.04.2017 (Fri)
|
Determinizing timed automata; Determinizable subclasses - ERA,
IRTA, SNZ (only ERA needed for exam)
|
Slides
|
|