Mathematical Structures in Formal Methods (AY 2020)

General

Thursday 10.45 - 12.15
Remote lectures, live. Connection information has been sent by email.
Lectures are in English
Evaluation: Term-end report 80%, other reports 20%

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

Up-to-date schedule, handouts, and other information are available at the Attendant Portal Page (URL is shared with the registered attendants).

2020.4.16 (Thu) No lecture (Start of course delayed due to COVID-19)
2020.4.23 (Thu) No lecture (Start of course delayed due to COVID-19)
2020.4.30 (Thu)
2020.5.7 (Thu)
2020.5.14 (Thu)
2020.5.21 (Thu)
2020.5.28 (Thu)
2020.6.4 (Thu)
2020.6.11 (Thu)
2020.6.18 (Thu)
2020.6.25 (Thu)
2020.7.2 (Thu)
2020.7.9 (Thu)
2020.7.16 (Thu)
2020.7.30 (Thu)

Ichiro Hasuo