{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T21:33:27Z","timestamp":1725744807100},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Solving parity games, which are equivalent to modal \u03bc-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 compu- tation 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(nd) symbolic operations and O(d) symbolic space; and (b) an improved algorithm that requires O(nd\/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 \u00b7 log n) symbolic space. Moreover, for the important special case of d \u2264 log n, our algorithm requires only polynomially many symbolic operations and poly-logarithmic symbolic space.<\/jats:p>","DOI":"10.29007\/5z5k","type":"proceedings-article","created":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T16:06:42Z","timestamp":1540310802000},"page":"233-211","source":"Crossref","is-referenced-by-count":4,"title":["Quasipolynomial Set-Based Symbolic Algorithms for Parity Games"],"prefix":"10.29007","volume":"57","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Wolfgang","family":"Dvo\u0159\u00e1k","sequence":"additional","affiliation":[]},{"given":"Monika","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Svozil","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,10,23]],"date-time":"2018-10-23T16:06:59Z","timestamp":1540310819000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/L8b1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/5z5k","relation":{},"ISSN":["2398-7340"],"issn-type":[{"type":"print","value":"2398-7340"}],"subject":[]}}