[Back to Teaching]

- Thursday 10.45 - 12.15
- Room: (not yet decided)
- Lectures are in English
- Evaluation: Term-end report 80%, other reports 20%
- Course video available here (username and password distributed at the lectures)

Formal methods refer to a body of mathematical techniques used for guaranteeing correctness of computer systems. This course introduces the mathematical foundation of formal methods. Our technical focus will be on automata theory, especially on automata that classify infinite words.

- In-depth understanding of basic automata theory
- Understanding of use of automata theory for formal methods purposes like verification and synthesis
- Hands-on knowledge on implementation of automata-based algorithms

(1-3) Automata on finite words, from an algorithmic point of view

(4-6) Automata on infinite words

(7) Linear temporal logic (LTL) as a specification language

(8) LTL model checking via translation to automata

(9-10) Parity games and their decision procedure

(11-12) Model checking and synthesis by parity games

(13-15) Probabilistic systems and probabilistic LTL model checking

- Moshe Y. Vardi: An Automata-Theoretic Approach to Linear Temporal Logic. Banff Higher Order Workshop 1995: 238-266
- S. Demri and P. Gastin. Specification and Verification using Temporal Logics. In Modern applications of automata theory, IISc Research Monographs 2, chapter 15, pages 457-494. World Scientific, 2012.
- Jurdzinski M. (2000) Small Progress Measures for Solving Parity Games. In: Reichel H., Tison S. (eds) STACS 2000. STACS 2000. Lecture Notes in Computer Science, vol 1770. Springer, Berlin, Heidelberg
- Wilke, Thomas. Alternating tree automata, parity games, and modal {$\mu$}-calculus. Bull. Belg. Math. Soc. Simon Stevin 8 (2001), no. 2, 359--391.
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.

Familiarity with the following topics is desirable (but not mandatory): propositional logic, computational complexity, formal language theory

**2018.4.19 (Thu)**No lecture (due to the lecturer's absence)**2018.4.26 (Thu)**handout Review of basic automata theory (for finite words): Pumping Lemma, the powerset construction. Next: regular expressions, the Kleene theorem, the Myhill-Nerode theorem, minimization.**2018.5.10 (Thu)**Reviewed the Kleene theorem (including the RE -> DFA and NFA -> RE translations). Started discussion of the Myhill-Nerode theorem and minimization. Next: intuition behind the Myhill-Nerode theorem. handout**2018.5.17 (Thu)**Reviewed the Myhill-Nerode theorem. Algorithms for automata for finite words. Definition of Buechi automata and their algorithms. Next: closure properties of Buechi automata. handout**2018.5.24 (Thu)**Boolean closure of omega-regularity. Impossibility of determinization. Rabin automata. Emptiness check of Buechi automata, characterization by lasso. Next: an emptiness check algorithm. handout**2018.5.31 (Thu)**Theory of Buechi automata. LTL syntax and semantics. Next: fixed points and LTL. handout**2018.6.7 (Thu)**Basic lattice theory, and the Knaster-Tarski theorem. Next: Cousot-Cousot construction, alternating automata.**Report assignments have been canceled.**handout**2018.6.14 (Thu)**The Cousot-Cousot sequence. Next: invariants for safety, ranking functions for liveness, and how they can be derived from the KT and CC theorems. Alternating automata. handout**2018.6.21 (Thu)**Proof methods for fixed points (invariants and ranking functions). Definitions of games, and simple games for propositional truth. Next: alternating automata. handout**2018.6.28 (Thu)**Alternating automata, translation of LTL formulas to ABA. Next: examples. handout**2018.7.5 (Thu): No Lecture****2018.7.12 (Thu): No Lecture****2018.7.19 (Thu)**Translation of LTL formulas to ABA via parse trees. Its use in satisfiability and model checking. Introduction to reactive synthesis. Next: parity games and progress measures, using my POPL'16 slides and Jurdzinski's STACS'00 paper. handout**2018.7.26 (Thu)**Introduction to parity games, using my POPL'16 slides. Jurdzinski's STACS'00 paper, up to Section 2.

**NB: the report assignments have been updated**. handout**2018.8.2 (Thu)**handout