Automata, Games, and Verification Bernd Finkbeiner, Hadar Frenkel


Currently, no news are available

Automata, Games, and Verification


The theory of automata over infinite objects provides a succinct, expressive, and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

The course is addressed to students interested in the theoretical concepts to analyze reactive systems using automata over infinite words, automata over infinite trees, and two-player games. The course continues on the topics of the core lecture “Verification”, the Verification lecture is not, however, a prerequisite for the AG&V course.


  • Automata over infinite words and trees (omega-automata)
  • Infinite two-player games
  • Logical systems for the specification of nonterminating behavior
  • Transformation of automata according to logical operations

Privacy Policy | Legal Notice
If you encounter technical problems, please contact the administrators