# Oink: an Implementation and Evaluation of Modern Parity Game Solvers

arXiv: https://arxiv.org/abs/1801.03859 · HTML: https://mlsanity.com/paper/1801.03859/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jan 2018.

## Built on by (most cited first, 4 of 4)

- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces](https://mlsanity.com/paper/2411.09366/) (2024)
- [On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing](https://mlsanity.com/paper/2312.12403/) (2023)
- [Predicting Winning Regions in Parity Games via Graph Neural Networks (Extended Abstract)](https://mlsanity.com/paper/2210.09924/) (2022)

## Abstract (arXiv)

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, as they are widely believed to admit a polynomial solution, but so far no such algorithm is known. In recent years, a number of new algorithms and improvements to existing algorithms have been proposed. We implement a new and easy to extend tool Oink, which is a high-performance implementation of modern parity game algorithms. We further present a comprehensive empirical evaluation of modern parity game algorithms and solvers, both on real world benchmarks and randomly generated games. Our experiments show that our new tool Oink outperforms the current state-of-the-art.