Automata and games
Automata and games provide the mathematical foundations for reasoning about complex computational systems. Automata serve as formal acceptors of specification languages such as Linear Temporal Logic (LTL), (omega-)regular languages, and formal specifications of systems used in verification and synthesis. Games offer a natural framework for modelling interactions, choices, and uncertainty.
At Liverpool, we study both qualitative and quantitative aspects of these foundational models. This includes:
- Model checking and verification: using automata-theoretic methods to automatically verify system properties. Decision questions such as acceptance and emptiness: developing efficient algorithms for automata analysis.
- Efficient Representations: developing new efficient methods to represent and translate formal languages and system specifications.
- Synthesis games: constructing correct-by-design systems by solving games between a system and its environment.
- Connections with logic: exploring the interplay between formal logics, automata, and infinite games.
- Infinite-state systems: We study rich models that go beyond finite state systems, including Vector Addition Systems (VAS) / Petri Nets, Timed Automata, and Pushdown Systems, which capture concurrency, real-time behaviour, and recursion.
- Quantitative and Probabilistic automata: We extend classical models to incorporate probability, cost, and resources, using Weighted Automata for costs and rewards, and Markov Chains, Markov Decision Processes (MDPs), and Probabilistic Automata for stochastic and probabilistic behaviour.
Our researchers make significant contributions to the fundamental theory of automata and games, including questions of complexity, decidability, and expressive power. These theoretical insights form the basis for practical advances in areas such as software model checking and system verification. Liverpool is internationally recognised as a leading centre in automata theory, infinite games, and their role in verification and synthesis.
Why It Matters
The study of automata and games underpins many areas of computer science and informatics.
- In software and hardware verification, automata-based techniques are central to ensuring safety and reliability.
- In autonomous systems, synthesis games enable the design of controllers that can adapt to unpredictable environments.
- In cybersecurity, game-theoretic models support the analysis of adversarial behaviour.
- In formal methods for AI, automata and games provide rigorous guarantees for learning and decision-making under uncertainty.
Our team
- Daniel Hausmann
Infinite-duration games, temporal model checking - David Purser
Weighted automata, infinite state systems, vector addition systems - Sven Schewe
Games, temporal model checking, infinite automata, MDPs - Qiyi Tang
Markov chains, MDPs, quantitative systems, games - Patrick Totzke
Infinite state systems, timed automata - Shufang Zhu
Temporal model checking, games for synthesis
Opportunities
We welcome opportunities to engage with students, researchers, and industry partner:
- PhD opportunities: Please contact us if you are interested in pursuing a PhD in automata and/or games.
- Postdoctoral and visiting researchers: We encourage applications from researchers interested in short- or long-term visits. We also welcome applications interested in pursuing a fellowship hosted at Liverpool.
- Consultancy and research collaborations: We are open to partnerships with academia, industry, and government.
- Workshops and networks: We regularly organise seminars, reading groups, and international workshops to advance knowledge exchange.
Contact Us
If you are interested in learning more or collaborating with us, please contact the relevant academic staff working in automata and games.