Course name:

Games, Logic and Automata

Course Syllabus

Lecturer:  Alex  Rabinovich

Credit:  3pt

Prerequisites: Logic for  CS, Computational Models.

Course Objectives:

In this course  we will study topics related to games, logic and automata and a rich interplay between them. These provide  the  mathematical foundations to  formal verification.

Automata on infinite words and trees serve as a computational model for reactive systems; Logics are  the basis of  specification formalisms and

games are a conceptual framework for understanding the interaction between

a system and its environment.

Course Syllabus:

Infinite  behavior of finite automata: closure properties, succinctness,

deteminization  algorithms.

Specification formalisms and their expressive power and succinctness properties: : Monadic second order logic, temporal  logics, algebraic formalisms.  

Decidability of monadic second-order logics over the naturals and over  the full binary tree. Reduction to finite automata, EF games, Shelah's compositional method.

Church Synthesis problem:   Infinite two-persons perfect information games.  Determinacy, computational and descriptive complexity of winning strategies.

Model Checking  Problem.  Algorithms for model-checking and their complexity.

Recommended reading:

D. Perrin and J. E. Pin. Infinite Words Automata, Semigroups, Logic and

Games. Pure and Applied Mathematics Vol 141 Elsevier, 2004.

W. Thomas Automata and Reactive systems. (draft of a book).

Grade:  80% home exam + 20% HW