Title: Improved Set-based Symbolic Algorithms for Parity Games,
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.