Skip to content
master
Switch branches/tags
Code

Latest commit

 

Git stats

Files

Permalink
Failed to load latest commit information.
Type
Name
Latest commit message
Commit time
src
 
 
 
 
 
 
 
 
 
 
 
 

Oink

Oink is an 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:

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)

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:

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:

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

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:

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.

See also:

Algorithm Description
PSI (parallel) 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:

Algorithm Description
TSPM Traditional small progress measures (standard variant without cycle acceleration)
SPM Accelerated version of small progress measures (cycle acceleration variant by TvD)
MSPM Maciej Gazda's modified small progress measures
SSPM Quasi-polynomial time succinct progress measures
BSSPM Quasi-polynomial time succinct progress measures (bounding variant by TvD and MJ, often faster)
QPT Quasi-polynomial time ordered progress measures
BQPT Quasi-polynomial time ordered progress measures (bounding variant by TvD and MJ, often faster)

Preprocessing

Oink can also apply the following preprocessors before solving the game:

  • Removing all self-loops (recommended)
  • Removing winner-controlled winning cycles (recommended)
  • Inflating or compressing the priorities before solving the parity game.
    Compression is useful for several solvers. By default, priorities are simply renumbered (to remove gaps). Several algorithms actually perform on-the-fly compression and are not affected by renumbering or compression.
  • SCC decomposition to solve the parity game one SCC at a time.
    May either improve or deteriorate performance.

Tools

Oink comes with several simple tools that are built around the library liboink.

Main tools

Tool Description
oink The main tool for solving parity games
verify Small tool that just verifies a solution (can be done by Oink too)
nudge Swiss army knife for transforming parity games
dotty Small tool that just generates a .dot graph of a parity game
test_solvers Main testing tool for parity game solvers and benchmarking

Game generators

Tool Description
rngame Faster version of the random game generator of PGSolver
stgame Faster version of the steady game generator of PGSolver
counter_rr Counterexample to the RR solver
counter_dp Counterexample to the DP solver
counter_m Counterexample of Maciej Gazda, PhD Thesis, Sec. 3.5
counter_qpt Counterexample of Fearnley et al, An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In: SPIN 2017.
counter_core Counterexample of Benerecetti, Dell'Erba, Mogavero, Robust Exponential Worst Cases for Divide-et-Impera Algorithms for Parity Games. In: GandALF 2017.
counter_rob SCC version of counter_core.
counter_dtl Counterexample to the DTL solver
counter_ortl Counterexample to the ORTL solver
tc Two binary counters generator (game family that is an exponential lower bound for many algorithms). See also Tom van Dijk (2019) A Parity Game Tale of Two Counters. In: GandALF 2019.
tc+ TC modified to defeat the RTL solver

Two binary counters

The two binary counters game family is an exponential lower bound for many algorithms:

  • The tangle learning algorithm TL
  • All fixpoint algorithms FPI, FPJ, FPJG
  • All priority promotion algorithms NPP, PP, PPP, DP, RRDP
  • All normal Zielonka algorithms ZLK, UZLK, ZLKPP-STD
  • The progress measures algorithms TSPM, SPM, MSPM

The two binary counters game family appears to be a quasi-polynomial lower bound for the QP algorithms:

  • The Zielonka variations ZLKQ, ZLKPP-WAW, ZLKPP-LIV
  • The progress measures variations SSPM, QPT

Some algorithms can solve the two binary counters games in polynomial time:

  • The tangle learning algorithms RTL, ORTL, PTL, SPPTL, DTL, IDTL
  • The strategy improvement algorithm PSI
  • Unsure: the BSSPM and BQPT algorithms

Usage

Oink is compiled using CMake. Optionally, use ccmake to set options. By default, Oink does not compile the extra tools, only the library liboink and the main tools oink and test_solvers. Oink requires several Boost libraries.

mkdir build && cd build
cmake .. && make
ctest

Oink provides usage instructions via oink --help. Typically, Oink is provided a parity game either via stdin (default) or from a file. The file may be zipped using the gzip or bzip2 format, which is detected if the filename ends with .gz or .bz2.

What you want? But how then?
To quickly solve a gzipped parity game: oink -v game.pg.gz game.sol
To verify some solution: oink -v game.pg.gz --sol game.sol

A typical call to Oink is: oink [options] [solver] <filename> [solutionfile]. This reads a parity game from filename, solves it with the chosen solver (default: --tl), then writes the solution to <solutionfile> (default: don't write). Typical options are:

  • -v verifies the solution after solving the game.
  • -w <workers> sets the number of worker threads for parallel solvers. By default, these solvers run their sequential version. Use -w 0 to automatically determine the maximum number of worker threads.
  • --inflate and --compress inflate/compress the game before solving it.
  • --scc repeatedly solves a bottom SCC of the parity game.
  • --no-wcwc, --no-loops and --no-single disable preprocessors that eliminate winner-controlled winning cycles, self-loops and single-parity games. Use --no to disable all preprocessors.
  • -z <seconds> kills the solver after the given time.
  • --sol <filename> loads a partial or full solution.
  • --dot <dotfile> writes a .dot file of the game as loaded.
  • -p writes the vertices won by even/odd to stdout.
  • -t (once or multiple times) increases verbosity level.

About

Oink, an implementation of modern parity game solvers

Resources

License

Releases

No releases published

Packages

No packages published