Oink: An implementation and evaluation of modern parity game solvers

Tom van Dijk*

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

35 Citations (Scopus)
12 Downloads (Pure)

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, 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.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsDirk Beyer, Marieke Huisman
PublisherSpringer
Pages291-308
Number of pages18
ISBN (Print)9783319899596
DOIs
Publication statusPublished - 2018
Externally publishedYes
Event24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 - Makedonia Palace, Thessaloniki, Greece
Duration: 14 Apr 201820 Apr 2018
Conference number: 24
https://etaps.org/2018/tacas

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10805 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018
Abbreviated titleTACAS 2018
Country/TerritoryGreece
CityThessaloniki
Period14/04/1820/04/18
Internet address

Fingerprint

Dive into the research topics of 'Oink: An implementation and evaluation of modern parity game solvers'. Together they form a unique fingerprint.

Cite this