---
res:
bibo_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
(equivalently, a mu-calculus formula with c alternations of least and greatest
fixed points). 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. @eng'
bibo_authorlist:
- foaf_Person:
foaf_givenName: Krishnendu
foaf_name: Chatterjee, Krishnendu
foaf_surname: Chatterjee
foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0002-4561-241X
- foaf_Person:
foaf_givenName: Wolfgang
foaf_name: Dvorák, Wolfgang
foaf_surname: Dvorák
- foaf_Person:
foaf_givenName: Monika
foaf_name: Henzinger, Monika
foaf_surname: Henzinger
- foaf_Person:
foaf_givenName: Veronika
foaf_name: Loitzenbauer, Veronika
foaf_surname: Loitzenbauer
bibo_doi: 10.4230/LIPICS.CSL.2017.18
bibo_volume: 82
dct_date: 2017^xs_gYear
dct_language: eng
dct_publisher: Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik@
dct_title: Improved set-based symbolic algorithms for parity games@
...