Solving Parity Games in Theory and Practice

点击翻译按钮获取中文摘要

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 boundsAssuming that solving parity games is tractable, the gold-brim 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 sub-exponential 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 boundsAssuming that parity games are not tractable, finding a super-polynomial lower bound would be the gold-brim solution. However, there are no non-trivial 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 sub-classes 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.