Mathematical Structures in Formal Methods (AY 2018)

General

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)

Overview

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.

Objectives

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

Course structure

(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

References

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.

Prerequisites

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

Schedule

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

Ichiro Hasuo