Parity games : descriptive complexity and algorithms for new solvers
Author(s)
Kuo, Huan-Pu
Type
Thesis
Abstract
Parity games are 2-person, 0-sum, graph-based, and determined games
that form an important foundational concept in formal methods (see e.g.,
[Zie98]), and their exact computational complexity has been an open problem
for over twenty years now.
In this thesis, we study algorithms that solve parity games in that they
determine which nodes are won by which player, and where such decisions
are supported with winning strategies. We modify and so improve a known
algorithm but also propose new algorithmic approaches to solving parity
games and to understanding their descriptive complexity.
For all of our contributions, we write our own custom frameworks, in the
Scala programming language, to perform tailored experiments and empirical
studies to demonstrate and support our theoretical findings.
First, we improve on one of the solver algorithms, based on small progress
measures [Jur00], by use of concurrency. We show that, for many parity
games, it is possible to deliver extra performance using this technique in a
multi-core environment.
Second, we design algorithms to reduce the computational complexity
of parity games, and create implementations to observe and evaluate the
behaviours of these reductions in our experimental settings. The measure
Rabin index, arising from the design of the said algorithm, is shown to be a
new descriptive complexity for parity games.
Finally, we define a new family of attractors and derive new parity game solvers from them. Although these new solvers are “partial”, in that they
do not solve all parity games completely, our experiments show that they do
solve a set of benchmark games (i.e., games with known structures) designed
to stress test solvers from PGSolver toolkit [FL10] completely, and some of
these partial solvers deliver favourable performance against a known high
performance solver in many circumstances.
that form an important foundational concept in formal methods (see e.g.,
[Zie98]), and their exact computational complexity has been an open problem
for over twenty years now.
In this thesis, we study algorithms that solve parity games in that they
determine which nodes are won by which player, and where such decisions
are supported with winning strategies. We modify and so improve a known
algorithm but also propose new algorithmic approaches to solving parity
games and to understanding their descriptive complexity.
For all of our contributions, we write our own custom frameworks, in the
Scala programming language, to perform tailored experiments and empirical
studies to demonstrate and support our theoretical findings.
First, we improve on one of the solver algorithms, based on small progress
measures [Jur00], by use of concurrency. We show that, for many parity
games, it is possible to deliver extra performance using this technique in a
multi-core environment.
Second, we design algorithms to reduce the computational complexity
of parity games, and create implementations to observe and evaluate the
behaviours of these reductions in our experimental settings. The measure
Rabin index, arising from the design of the said algorithm, is shown to be a
new descriptive complexity for parity games.
Finally, we define a new family of attractors and derive new parity game solvers from them. Although these new solvers are “partial”, in that they
do not solve all parity games completely, our experiments show that they do
solve a set of benchmark games (i.e., games with known structures) designed
to stress test solvers from PGSolver toolkit [FL10] completely, and some of
these partial solvers deliver favourable performance against a known high
performance solver in many circumstances.
Date Issued
2013
Date Awarded
2013-07
Copyright Statement
Attribution NoDerivatives 4.0 International Licence (CC BY-ND)
Advisor
Huth, Michael
Piterman, Nir
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)