Solving parity games with tangles

ABSTRACT. Parity games are well known for their applications in formal verification and synthesis, especially to solve both the model-checking and synthesis problems of the modal mu-calculus and related logics like LTL. We have published two novel contributions to this field in the past year and are working on a third. This presentation is based on publications at TACAS'2018 and CAV'2018 containing the following contributions. Oink is a new implementation of parity game solvers much like the well known PGSolver, but it has a much improved practical performance and we use Oink to perform a new modern comparison of parity game solvers. The tool is designed for easy integration with other toolchains and for easy replication of research results. We propose a new algorithm to solve parity games called tangle learning. The idea is that all algorithms for parity games explore so-called "tangles" in the parity game and they often repeat exploring the same tangle again and again, which can lead to exponential runtimes. The insight ("highlight") of the tangle learning algorithm is that these tangles can be combined with the attractor computation and then we can use this with a memoization strategy ("learning") to never explore the same tangle twice. The tangles are very much related to another concept called "distractions" that we're currently developing further, and we can show that the interaction of tangles and distractions drives parity game difficulty.

Authors

• Tom van Dijk University of Twente

Keywords

No keywords are indexed for this paper.