Quasipolynomial set-based symbolic algorithms for parity games

DOI10.29007/5Z5KzbMATH Open1415.68142arXiv1909.04983OpenAlexW3105831223MaRDI QIDQ5222958FDOQ5222958

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)

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.

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

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

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)

Cited In (8)

• Title not available (Why is that?)
• The Theory of Universal Graphs for Infinite Duration Games
• Fine-grained complexity lower bounds for problems in computer aided verification
• Improved set-based symbolic algorithms for parity games
• Solving parity games: explicit vs symbolic
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
• Quasipolynomial computation of nested fixpoints
• Universal algorithms for parity games and nested fixpoints

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)