PIGGY · Reasoning using tangles on parity games

Reasoning using tangles on parity games

The main problem addressed by the project is that of solving parity games in polynomial time. Parity games are one of the conceptually simplest problems that are expected to have a polynomial-time algorithm, but for which no such algorithm has been found. Primary objective of the project was to use tangle attractors, that is, attractor-based reasoning extended by knowledge of tangles, that is, regions of a parity game that are known to be won by one of the two players, as the basic building block of a polynomial-time parity game algorithm. The conclusion is that no such algorithm has been found. Different approaches have been tried resulting in several counterexamples (of games that require more than polynomial time) which are insightful. These counterexamples may be used to find a general framework for classes of algorithms that cannot be solved in polynomial time. Several modifications to tangle learning algorithms remain open at this time. Another objective was towards symbolic representation of tangles. I have made significant progress here using a different approach than originally envisioned in the project, and have a semisymbolic approach that translates a symbolic parity game to an explicit parity game. While efficient symbolic representation of a set of tangles remains an open problem and likely requires as many symbolic representations as there are tangles, I have found that the expected improvement from using symbolic algorithms can already be reached by using the semisymbolic approach. Three other objectives were to use tangles to improve solving large games, using tangles in neighboring graph problems, and to develop tangles into a format suitable for the general public, such as board games that rely on tangle-similar concepts. These objectives have not been reached for various reasons, including limitations due to COVID19. The project is important for society in two broader contexts. First, understanding theoretical limits of computing is fundamental in computer science. The most famous problem is the P vs NP problem. If parity games are proven to be unsolvable in polynomial time, then this solves the P vs NP problem. If parity games can be shown to be solvable in polynomial time, then this solves one of the pieces of the puzzle, namely both the parity game problem and the related model checking problem of the mu calculus, which have been open for 40 years. Secondly, parity games play a central role for verification and synthesis problems of reactive controllers. Thus, improved algorithms for parity games and a better understanding of the complexity of synthesis problems and structures helps towards more practical application of controller synthesis in the future, that is, reliable controllers that are correct by construction.

Data: CORDIS, © European Union