EPSRC Reference: 
EP/P020909/1 
Title: 
Solving Parity Games in Theory and Practice 
Principal Investigator: 
Schewe, Dr S 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Liverpool 
Scheme: 
Standard Research 
Starts: 
01 May 2017 
Ends: 
30 April 2020 
Value (£): 
409,109

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
12 Jan 2017

EPSRC ICT Prioritisation Panel Jan 2017

Announced


Summary on Grant Application Form 
Parity games are an intriguing problem class, because they are simple to state and have proven to be resistant to countless attempts to classify their complexity. At the same time, algorithms for solving parity games play a paramount role in model checking, satisfiability checking, and synthesis.
In this project, we will approach the objectives stated above as follows.
1. Determine or narrow down the complexity of solving parity and payoff games.
The fundamental open question is the membership of parity games in P. We will research in both directions, trying to improve the known upper and lower bounds and studying the relation between different types of parity and payoff games.
1a. Upper bounds
Assuming that solving parity games is tractable, the goldbrim solution would be to find a polynomial time algorithm for solving parity games. A second best upper bound would be to establish an FPTAS algorithm, where the number of priorities is the parameter. Further interesting questions are improving the dependency on the number of priorities, which have previously improved from n^p through n^(p/2) to n^(p/3) for parity games with n states and p priorities, and to improve the known subexponential bounds, which are currently n^\sqrt(n).
Another branch of research under this item is to estimate the complexity of known algorithms with unknown complexity.
1b. Lower bounds
Assuming that parity games are not tractable, finding a superpolynomial lower bound would be the goldbrim solution. However, there are no nontrivial polynomial bounds available, and proofs of lower bounds based, e.g. on the strong exponential time hypothesis, could provide a starting point for an intractability proof.
1c. Connecting 2 player parity with mean, discounted, and simple stochastic games.
There is a simple polynomial time reduction from parity through mean payoff and discounted payoff to simple stochastic games. The latter are polynomial time equivalent to the 2.5 player (2 antagonistic players and a random player) version of all of these games. We will research reductions in the other directions.
2. To describe classes of parity and payoff games that can be solved efficiently.
Many different cases where parity games can be solved in polynomial time are known. This prominently includes games with a bounded number of priorities, but also games with a bounded number of nodes of either player (especially one player games) and games with arenas that have a simple structure, such as bounded treewidth, DAG width, clique width, Kelly width, or entanglement.
We will further the research on restricted classes of graphs with weaker restrictions, such as local bounded treewidth, excluded minors, and nowhere dense graphs, and extend this analysis to payoff games. We will also further current research on the combination of partial solvers based on using polynomial algorithms that only solve subclasses of parity games with the aim of defining increasingly larger classes of games that can be solved in polynomial time.
3. To develop algorithms for solving parity and payoff games with good performance.
To approach this goal, we use the insights from the first two workpackages to develop further algorithms with good performance, especially strategy improvement algorithms. An additional aspect we will focus on is to study distributed algorithms for solving parity games, harnessing the power of GPUs for solving parity and payoff games.
4. To develop fast algorithms for solving parity and payoff games.
Finally, we will implement the most promising algorithms in model checking and synthesis tools.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.liv.ac.uk 