Automata, Logic and Games: 20172018
Lecturer 

Degrees 
Schedule C1 (CS&P) — Computer Science and Philosophy Schedule C1 — Computer Science Schedule C1 — Mathematics and Computer Science 
Term 
Michaelmas Term 2017 (24 lectures) 
Overview
To introduce the mathematical theory underpinning the ComputerAided Verification of computing systems. The main ingredients are:
 Automata (on infnite words and trees) as a computational model of statebased systems
 Logical systems (such as temporal and modal logics) for specifying operational behaviour
 Twoperson 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 lineartime temporal logic to describe behaviourial properties such as recurrence and periodicity, and translate LTL formulas to Buchi automata.
 Use S1S to define omegaregular languages, and give an account of the equivalence between S1S definability and Buchi recognisability.
 Explain the intuitive meaning of simple modal mucalculus formulas, and describe the correspondence bewteen propertychecking games and modal mucalculus model checking.
Prerequisites
Knowledge of firstorder predicate calculus will be assumed. Familiarity with the basics of Finite Automata Theory and Computability (for example, as covered by the course, Models of Computation) and Complexity Theory would be very helpful. Candidates who do not have the required background are expected to have taken the course, Introduction to the Foundations of Computer Science.
Synopsis
 Automata on infinite words. Buchi automata: Closure properties. Determinization and Rabin automata.
 Nonemptiness and Nonuniversality problems for Buchi automata.
 Linear temporal logic and alternating Buchi automata.
 Modal mucalculus: Fundamental Theorem, decidability and finite model property. Parity Games and the ModelChecking Problem: memoryless determinacy, algorithmic issues.
 Monadic Secondorder Logic and its relationship with the modal mucalculus.
Reading list
Selected parts from:
 J. Bradfield and C. P. Stirling. Modal logics and mucalculi. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 293{332. Elsevier, NorthHolland, 2001.
 B. Khoussainov and A. Nerode. Automata Theory and its Applications. Progress in Computer Science and Applied Logic, Volume 21. Birkhauser, 2001.
 C. P. Stirling. Modal and Temporal Properties of Processes. Texts in Computer Science. SpringerVerlag, 2001.
 W. Thomas. Languages, Automata and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3. SpringerVerlag, 1997.
 M. Y. Vardi. An automatatheoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, ed. F. Moller and G. Birtwistle, LNCS vol. 1043, pp. 238266, SpringerVerlag, 1996.