[Back to Teaching]

Mathematical Structures in Formal Methods (AY 2018)

General

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

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

Prerequisites

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

Schedule