Automata, Logic and Games:  2024-2025

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
• Connections between logical reasoning over arbitrary structrures and automata over trees

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 between property-checking games and modal mu-calculus model checking.

Prerequisites

Knowledge of first-order 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 mu-calculus: Fundamental Theorem, decidability and finite model property. Parity Games and the Model-Checking Problem: memoryless determinacy, algorithmic issues.
• Monadic Second-order Logic and its relationship with the modal mu-calculus.
• Using automata to reason about arbitrary structures

Reading list

Selected parts from:

• J. Bradfield and C. P. Stirling. Modal logics and mu-calculi. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 293{332. Elsevier, North-Holland, 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. Springer-Verlag, 2001.
• W. Thomas. Languages, Automata and Logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, volume 3. Springer-Verlag, 1997.
• M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, ed. F. Moller and G. Birtwistle, LNCS vol. 1043, pp. 238-266, Springer-Verlag, 1996.
• M. Benedikt, Decidable Logics via Automata https://www.cs.ox.ac.uk/michael.benedikt/readingcourse/coursenotes.pdf

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.