### Authors:

- Tom van Dijk

Published in: CAV (2) pp 198–215

DOI: `10.1007/978-3-319-96142-2\_14`

### Abstract:

Parity games have important practical applications in formal verification and synthesis, especially to solve the model-checking problem of the modal mu-calculus. They are also interesting from the theory perspective, because they are widely believed to admit a polynomial solution, but so far no such algorithm is known.

We propose a new algorithm to solve parity games based on learning tangles, which are strongly connected subgraphs for which one player has a strategy to win all cycles in the subgraph. We argue that tangles play a fundamental role in the prominent parity game solving algorithms. We show that tangle learning is competitive in practice and the fastest solver for large random games.

### BibTeX entry:

```
@inproceedings{Dijk18b,
author = {Tom van Dijk},
booktitle = {CAV (2)},
doi = {10.1007/978-3-319-96142-2\_14},
pages = {198--215},
publisher = {Springer},
series = {LNCS},
talk = {2018tangles_talk.pdf},
title = {Attracting Tangles to Solve Parity Games},
volume = {10982},
year = {2018}
}
```