Oink

Oink is a modern implementation of parity game solvers written in C++. Oink aims to provide high-performance implementations of state-of-the-art algorithms representing different approaches to solving parity games.

Oink is licensed with the Apache 2.0 license and is aimed at both researchers and practitioners. For convenience, Oink compiles into a library that can be used by other projects.

Oink was initially developed (© 2017-2021) by Tom van Dijk and the Formal Models and Verification group at the Johannes Kepler University Linz as part of the RiSE project, and now in the Formal Methods and Tools group at the University of Twente.

The main author of Oink is Tom van Dijk who can be reached via tom@tvandijk.nl. Please let us know if you use Oink in your projects. If you are a researcher, please cite the following publication.

Tom van Dijk (2018) Oink: An Implementation and Evaluation of Modern Parity Game Solvers. In: TACAS 2018.

The main repository of Oink is https://github.com/trolando/oink.

Implemented algorithms

Oink implements various modern algorithms. Several of the algorithms can be run with multiple threads. These parallel algorithms use the work-stealing framework Lace.

Tangle learning family

The tangle learning algorithms are a focus of research for finding a polynomial-time algorithm to solve parity games.

See also:

• Tom van Dijk (2018) Attracting Tangles to Solve Parity Games. In: CAV 2018.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- TL | Tangle learning (standard variant) RTL | Recursive Tangle Learning (research variant) ORTL | One-sided Recursive Tangle Learning (research variant) PTL | Progressive Tangle Learning (research variant) SPPTL | Single-player Progressive Tangle Learning (research variant) DTL | Distance Tangle Learning (research variant based on 'good path length') IDTL | Interleaved Distance Tangle Learning (interleaved variant of DTL) TLQ | Tangle Learning applied to the quasi-polynomial time recursive algorithm

Fixpoint algorithms

The fixpoint algorithms are based on a translation of parity games to a formula of the modal mu-calculus, which can be solved using a naive fixpoint algorithm. Despite its atrocious behavior on constructed hard games, for practical parity games they are among the fastest algorithms. The FPI algorithm has a scalable parallel implementation.

See also:

• Tom van Dijk and Bob Rubbens (2019) Simple Fixpoint Iteration To Solve Parity Games. In: GandALF 2019.
• Ruben Lapauw, Maurice Bruynooghe, Marc Denecker (2020) Improving Parity Game Solvers with Justifications. In: VMCAI 2020.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- FPI | (parallel) Distraction Fixpoint Iteration (similar to APT algorithm and to Bruse/Falk/Lange) FPJ | Fixpoint Iteration using Justifications FPJG | Fixpoint Iteration using Justifications (greedy variant by TvD)

Priority promotion family

The priority promotion algorithms are efficient algorithms described in several papers by Benerecetti, Dell'Erba and Mogavero. The implementations PP, PPP, RR, DP and RRDP are by TvD; the authors provided their own implementation NPP.

See also:

• Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero (2016) Solving Parity Games via Priority Promotion. In: CAV 2016.
• Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero (2016) A Delayed Promotion Policy for Parity Games. In: GandALF 2016.
• Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero (2016) Improving Priority Promotion for Parity Games. In: HVC 2016.
• Massimo Benerecetti, Daniele Dell'Erba, Fabio Mogavero, Sven Schewe, Dominik Wojtczak Priority Promotion with Parysian Flair. In: arXiv.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- NPP | Priority promotion (implementation by authors BDM) PP | Priority promotion (basic algorithm) PPP | Priority promotion PP+ (better reset heuristic) RR | Priority promotion RR (even better reset heuristic) DP | Priority promotion PP+ with the delayed promotion strategy RRDP | Priority promotion RR with the delayed promotion strategy PPQ | Pawel Parys's QP recursive algorithm augmented with priority promotion

Zielonka's recursive algorithm

One of the oldest algorithms for solving parity games is the recursive algorithm due to Zielonka, based on work by McNaughton. The standard implementation ZLK is described in the TACAS 2018 paper about Oink. It is an optimized version based on earlier optimizations by various authors. The UZLK variant removes some of the optimizations for research purposes.

The ZLKQ algorithm is an implementation by TvD based on work by Parys and by Lehtinen et al., with additional optimizations, including a shortcut in the tree to the next priority in the subgame and skipping recursions if the remaining game is smaller than the precision parameter.

The ZLKPP algorithms are the implementations by Pawel Parys accompanying the paper with Lehtinen et al.

See also:

• Pawel Parys (2019) Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time. In: MFCS 2019.
• Karoliina Lehtinen, Pawel Parys, Sven Schewe, Dominik Wojtczak (2021) A Recursive Approach to Solving Parity Games in Quasipolynomial Time.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- ZLK | (parallel) Zielonka's recursive algorithm UZLK | an unoptimized version of Zielonka for research purposes ZLKQ | Quasi-polynomial time recursive algorithm (optimized implementation by TvD) ZLKPP-STD | Zielonka's recursive algorithm (standard version, by Pawel Parys) ZLKPP-WAW | Quasi-polynomial time recursive algorithm (Warsaw version, by Pawel Parys) ZLKPP-LIV | Quasi-polynomial time recursive algorithm (Liverpool version, by Pawel Parys)

Strategy improvement

The strategy improvement algorithm is one of the older algorithms, receiving a lot of attention from the academic community in the past. The parallel strategy improvement implementation is inspired by the work of Fearnley in CAV 2017 but uses a different approach with work-stealing. This is described in the TACAS 2018 paper about Oink. The symmetric strategy improvement algorithm is my own take on the 2015 ICALP paper by Schewe et al. It applies the principle of only updating strategies that are also the best response to the SI variation of PSI, that is, considering only finite paths simplifying the valuation.

See also:

• John Fearnley (2017) Efficient Parallel Strategy Improvement for Parity Games. In: CAV 2017.
• Sven Schewe, Ashutosh Trivedi, Thomas Varghese (2015) Symmetric Strategy Improvement. In: ICALP 2015.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- PSI | (parallel) strategy improvement SSI | symmetric strategy improvement

Progress measures

Progress measures algorithms are based on a monotonically increasing value attached to every vertex of the parity game. Several of the quasi-polynomial solutions to parity games are modifications of the small progress measures algorithm.

The original algorithm by Jurdzinski in 2000 is implemented as the TSPM algorithm. The accelerated SPM approach is a novel approach developed by TvD. The idea is to let progress measures increase until a bound, then analyse the halted result. The measures are then immediately increased to a higher value, skipping many small increases.

The QPT ordered progress measures algorithm was published by Fearnley et al in SPIN 2016. The QPT succinct progress measures algorithm was published by Jurdzinski et al in LICS 2017.

The bounded variants BSSPM and BQPT are an idea by Tom van Dijk and Marcin Jurdzinski.

See also:

• Marcin Jurdzinski (2000) Small Progress Measures for Solving Parity Games. In: STACS 2000.
• Maciej Gazda, Tim Willemse (2015) Improvement in Small Progress Measures. In: GandALF 2015.
• John Fearnley, Sanjay Jain, Sven Schewe, Frank Stephan, Dominik Wojtczak (2017) An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: SPIN 2017.
• Marcin Jurdzinski, Ranko Lazic (2017) Succinct progress measures for solving parity games. In: LICS 2017.

Algorithm | Description :-------------- | :------------------------------------------------------------------------------------------------- TSP