City Research Online

Improving parity games in practice

Di Stasio, A. ORCID: 0000-0001-5475-2978, Murano, A., Prignano, V. & Sorrentino, L. (2021). Improving parity games in practice. Annals of Mathematics and Artificial Intelligence, 89(5-6), pp. 551-574. doi: 10.1007/s10472-020-09721-3

Abstract

Parity gamesare infinite-round two-player games played on directed graphs whose nodes are labeled with priorities. The winner of a play is determined by the smallest priority (even or odd) that is encountered infinitely often along the play. In the last two decades, several algorithms for solving parity games have been proposed and implemented in , a platform written in OCaml. includes theZielonka’s recursive algorithm(, for short) which is known to be the best performing one over random games. Notably, several attempts have been carried out with the aim of improving the performance of in , but with small advances in practice. In this work, we deeply revisit the implementation of by dealing with the use of specific data structures and programming languages such asScala,Java,C++, andGo. Our empirical evaluation shows that these choices are successful, gaining up to three orders of magnitude in running time over the classic version of the algorithm implemented in PGSolver.

Publication Type: Article
Additional Information: This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
Publisher Keywords: Formal verification, Zielonka Recursive algorithm, PGSolver
Subjects: Q Science > QA Mathematics
Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Departments: School of Science & Technology
School of Science & Technology > Computer Science
SWORD Depositor:
[thumbnail of s10472-020-09721-3.pdf]
Preview
PDF - Published Version
Download (1MB) | Preview

Export

Add to AnyAdd to TwitterAdd to FacebookAdd to LinkedinAdd to PinterestAdd to Email

Downloads

Downloads per month over past year

View more statistics

Actions (login required)

Admin Login Admin Login