Parity games are 2-person, 0-sum, graph-based, and determined gamesudthat form an important foundational concept in formal methods (see e.g.,ud[Zie98]), and their exact computational complexity has been an open problemudfor over twenty years now.udIn this thesis, we study algorithms that solve parity games in that theyuddetermine which nodes are won by which player, and where such decisionsudare supported with winning strategies. We modify and so improve a knownudalgorithm but also propose new algorithmic approaches to solving parityudgames and to understanding their descriptive complexity.udFor all of our contributions, we write our own custom frameworks, in theudScala programming language, to perform tailored experiments and empiricaludstudies to demonstrate and support our theoretical findings.udFirst, we improve on one of the solver algorithms, based on small progressudmeasures [Jur00], by use of concurrency. We show that, for many parityudgames, it is possible to deliver extra performance using this technique in audmulti-core environment.udSecond, we design algorithms to reduce the computational complexityudof parity games, and create implementations to observe and evaluate theudbehaviours of these reductions in our experimental settings. The measureudRabin index, arising from the design of the said algorithm, is shown to be audnew descriptive complexity for parity games.udFinally, we define a new family of attractors and derive new parity game solvers from them. Although these new solvers are “partial”, in that theyuddo not solve all parity games completely, our experiments show that they doudsolve a set of benchmark games (i.e., games with known structures) designedudto stress test solvers from PGSolver toolkit [FL10] completely, and some ofudthese partial solvers deliver favourable performance against a known highudperformance solver in many circumstances.
展开▼
