Lecture 1

06.03.2017 (Mon)

Introduction to omegalanguages; Büchi automata;
deterministic vs nondeterministic Büchi automata

Slides

Sections 1.1, 1.2 (except complementation) of [2]

Lecture 2

10.03.2017 (Fri)

More on Büchi automata, omegaregular 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

