Automata, Logics and Games

Prerequisites

Familiarity with the basics of finite automata theory and computability, for example, as covered by the first-year CS course, Models of Computation. Basic familiarity with logic: propositional and predicate calculus. Some familiarity with complexity theory would be helpful, but not essential.

Overview

To introduce the mathematical theory underpinning the Computer-Aided Verification of computing systems. The main ingredients are:

• Automata (on infnite words and trees) as a computational model of state-based systems.
• Logical systems (such as temporal and modal logics) for specifying operational behaviour.
• Two-person games as a conceptual basis for understanding interactions between a system and its environment.

Learning Outcomes

At the end of the course students will be able to:

• Describe in detail what is meant by a Buchi automaton, and the languages recognised by simple examples of Buchi automata.
• Use linear-time temporal logic to describe behaviourial properties such as recurrence and periodicity, and translate LTL formulas to Buchi automata.
• Use S1S to define omega-regular languages, and give an account of the equivalence between S1S definability and Buchi recognisability.
• Explain the intuitive meaning of simple modal mu-calculus formulas, and describe the correspondence bewteen property-checking games and modal mu-calculus model checking.