# zbMATH — the first resource for mathematics

Quasipolynomial set-based symbolic algorithms for parity games. (English) Zbl 1415.68142
Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 233-253 (2018).
Summary: Solving parity games, which are equivalent to modal $$\mu$$-calculus model checking, is a central algorithmic problem in formal methods, with applications in reactive synthesis, program repair, verification of branching-time properties, etc. 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) the basic 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. In this work, 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 immediately 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(d\cdot \log n)$$ symbolic space. Moreover, for the important special case of $$d\le \log n$$, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.
For the entire collection see [Zbl 1407.68021].
##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.) 68W30 Symbolic computation and algebraic computation
Full Text: