Quasipolynomial set-based symbolic algorithms for parity games

DOI10.29007/5Z5KMaRDI QIDQ5222958zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Wolfgang Dvořák, Alexander Svozil, Monika R. Henzinger

Publication date 4 July 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1909.04983

zbMATH Keywords

model checkingsymbolic computationparity gamesgraph gamesprogress measure

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Solving parity games, which are equivalent to modal $mu$-calculus model checking, is a central algorithmic problem in formal methods. Besides the standard computation model with the explicit representation of games, another important theoretical model of computation is that of set-based symbolic algorithms. Set-based symbolic algorithms use basic set operations and one-step predecessor operations on the implicit description of games, rather than the explicit representation. The significance of symbolic algorithms is that they provide scalable algorithms for large finite-state systems, as well as for infinite-state systems with finite quotient. Consider parity games on graphs with $n$ vertices and parity conditions with $d$ priorities. While there is a rich literature of explicit algorithms for parity games, the main results for set-based symbolic algorithms are as follows: (a) an algorithm that requires $O(n^d)$ symbolic operations and $O(d)$ symbolic space; and (b) an improved algorithm that requires $O(n^{d/3+1})$ symbolic operations and $O(n)$ symbolic space. Our contributions are as follows: (1) We present a black-box set-based symbolic algorithm based on the explicit progress measure algorithm. Two important consequences of our algorithm are as follows: (a) a set-based symbolic algorithm for parity games that requires quasi-polynomially many symbolic operations and $O(n)$ symbolic space; and (b) any future improvement in progress measure based explicit algorithms imply an efficiency improvement in our set-based symbolic algorithm for parity games. (2) We present a set-based symbolic algorithm that requires quasi-polynomially many symbolic operations and $O(dcdotlogn)$ symbolic space. Moreover, for the important special case of $dleqlogn$, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.

Recommendations

• Improved set-based symbolic algorithms for parity games
• Solving parity games: explicit vs symbolic
• scientific article; zbMATH DE number 1500523
• A modal \(\mu\) perspective on solving parity games in quasi-polynomial time
• Succinct progress measures for solving parity games

Cited in

(8)

• Solving parity games: explicit vs symbolic
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
• Quasipolynomial computation of nested fixpoints
• Fine-grained complexity lower bounds for problems in computer aided verification
• Universal algorithms for parity games and nested fixpoints
• scientific article; zbMATH DE number 7455738 (Why is no real title available?)
• The Theory of Universal Graphs for Infinite Duration Games
• Improved set-based symbolic algorithms for parity games

This page was built for publication: Quasipolynomial set-based symbolic algorithms for parity games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5222958)