Improved set-based symbolic algorithms for parity games

DOI10.4230/LIPICS.CSL.2017.18MaRDI QIDQ5111185zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Wolfgang Dvořák, Veronika Loitzenbauer, Monika R. Henzinger

Publication date 26 May 2020

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

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) Games involving graphs (91A43)

Abstract: Graph games with {omega}-regular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify {omega}-regular winning conditions. Graph games with parity conditions are equivalent to {mu}-calculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finite-state systems, as well as algorithms for the analysis of infinite-state systems with finite quotient. A set-based symbolic algorithm uses the basic set operations and the one-step predecessor operators. We consider graph games with $n$ vertices and parity conditions with $c$ priorities. While many explicit algorithms exist for graph games with parity conditions, for set-based symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires $O(n^c)$ symbolic operations and linear space; and (b) an improved algorithm that requires $O(n^{c/2+1})$ symbolic operations but also $O(n^{c/2+1})$ space (i.e., exponential space). In this work we present two set-based symbolic algorithms for parity games: (a) our first algorithm requires $O(n^{c/2+1})$ symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires $O(n^{c/3+1})$ symbolic operations and only linear space. We also present the first linear space set-based symbolic algorithm for parity games that requires at most a sub-exponential number of symbolic operations.

Recommendations

• Quasipolynomial set-based symbolic algorithms for parity games
• Solving parity games: explicit vs symbolic
• Solving μ-Calculus Parity Games by Symbolic Planning
• Faster algorithms for mean-payoff parity games
• Solving parity games via priority promotion

Cited in

(11)

• The Symbolic Approach to Repeated Games (Abstract)
• scientific article; zbMATH DE number 7455738 (Why is no real title available?)
• Fine-grained complexity lower bounds for problems in computer aided verification
• Solving parity games: explicit vs symbolic
• Quasipolynomial set-based symbolic algorithms for parity games
• Faster algorithms for mean-payoff parity games
• scientific article; zbMATH DE number 7447737 (Why is no real title available?)
• scientific article; zbMATH DE number 1863183 (Why is no real title available?)
• Symbolic algorithms for graphs and Markov decision processes with fairness objectives
• Improved algorithms for parity and Streett objectives
• Symbolic computational techniques for solving games

This page was built for publication: Improved 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 Q5111185)