Oink: An implementation and evaluation of modern parity game solvers

Tom van Dijk

doi:10.1007/978-3-319-89960-2_16

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 proceeding › Conference contribution › Academic › peer-review

48 Citations (Scopus)

66 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 language	English
Title of host publication	Tools 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
Editors	Dirk Beyer, Marieke Huisman
Publisher	Springer
Pages	291-308
Number of pages	18
ISBN (Print)	9783319899596
DOIs	https://doi.org/10.1007/978-3-319-89960-2_16
Publication status	Published - 2018
Externally published	Yes
Event	24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 - Makedonia Palace, Thessaloniki, Greece Duration: 14 Apr 2018 → 20 Apr 2018 Conference number: 24 https://etaps.org/2018/tacas

Publication series

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

Conference

Conference	24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018
Abbreviated title	TACAS 2018
Country/Territory	Greece
City	Thessaloniki
Period	14/04/18 → 20/04/18
Internet address	https://etaps.org/2018/tacas

Access to Document

10.1007/978-3-319-89960-2_16Licence: CC BY

978-3-319-89960-2_16Final published version, 473 KBLicence: CC BY

Cite this

van Dijk, T. (2018). Oink: An implementation and evaluation of modern parity game solvers. In D. Beyer, & M. Huisman (Eds.), Tools 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 (pp. 291-308). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10805 LNCS). Springer. https://doi.org/10.1007/978-3-319-89960-2_16

van Dijk, Tom. / Oink : An implementation and evaluation of modern parity game solvers. Tools 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. editor / Dirk Beyer ; Marieke Huisman. Springer, 2018. pp. 291-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{02395c14463443f4b535055fda9051e3,

title = "Oink: An implementation and evaluation of modern parity game solvers",

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

author = "\{van Dijk\}, Tom",

note = "Funding Information: Supported by FWF, NFN Grant S11408-N23 (RiSE). We thank Tim Willemse and John Fearnley for their helpful comments and Jaco van de Pol for the use of their computer cluster. We thank Tim Willemse and John Fearnley for their helpful comments and Jaco van de Pol for the use of their computer cluster. Publisher Copyright: {\textcopyright} The Author(s) 2018.; 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, TACAS 2018 ; Conference date: 14-04-2018 Through 20-04-2018",

year = "2018",

doi = "10.1007/978-3-319-89960-2\_16",

language = "English",

isbn = "9783319899596",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "291--308",

editor = "Dirk Beyer and Marieke Huisman",

booktitle = "Tools 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",

address = "Germany",

url = "https://etaps.org/2018/tacas",

}

van Dijk, T 2018, Oink: An implementation and evaluation of modern parity game solvers. in D Beyer & M Huisman (eds), Tools 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10805 LNCS, Springer, pp. 291-308, 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, Thessaloniki, Greece, 14/04/18. https://doi.org/10.1007/978-3-319-89960-2_16

Oink: An implementation and evaluation of modern parity game solvers. / van Dijk, Tom.
Tools 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. ed. / Dirk Beyer; Marieke Huisman. Springer, 2018. p. 291-308 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10805 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Oink

T2 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018

AU - van Dijk, Tom

N1 - Conference code: 24

PY - 2018

Y1 - 2018

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

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

UR - https://www.scopus.com/pages/publications/85045850148

U2 - 10.1007/978-3-319-89960-2_16

DO - 10.1007/978-3-319-89960-2_16

M3 - Conference contribution

AN - SCOPUS:85045850148

SN - 9783319899596

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 291

EP - 308

BT - Tools 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

A2 - Beyer, Dirk

A2 - Huisman, Marieke

PB - Springer

Y2 - 14 April 2018 through 20 April 2018

ER -

van Dijk T. Oink: An implementation and evaluation of modern parity game solvers. In Beyer D, Huisman M, editors, Tools 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. Springer. 2018. p. 291-308. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-89960-2_16

Oink: An implementation and evaluation of modern parity game solvers

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this