Zielonka's recursive algorithm : dull, weak and solitaire games and tighter bounds

M.W. Gazda, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

Dull, weak and nested solitaire games are important classes of parity games, capturing, among others, alternation-free mu-calculus and ECTL* model checking problems. These classes can be solved in polynomial time using dedicated algorithms. We investigate the complexity of Zielonka's Recursive algorithm for solving these special games, showing that the algorithm runs in O(d (n + m)) on weak games, and, somewhat surprisingly, that it requires exponential time to solve dull games and (nested) solitaire games. For the latter classes, we provide a family of games G, allowing us to establish a lower bound of 2^(n/3). We show that an optimisation of Zielonka's algorithm permits solving games from all three classes in polynomial time. Moreover, we show that there is a family of (non-special) games M that permits us to establish a lower bound of 2^(n/3), improving on the previous lower bound for the algorithm.
Original languageEnglish
Title of host publicationFourth International Symposium on Games, Automata, Logics and Formal Verification (Borca di Cadore, Dolomites, Italy, August 29-31, 2013)
EditorsG. Puppis, T. Villa
PublisherEPTCS
Pages7-20
DOIs
Publication statusPublished - 2013

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume119
ISSN (Print)2075-2180

Fingerprint

Dive into the research topics of 'Zielonka's recursive algorithm : dull, weak and solitaire games and tighter bounds'. Together they form a unique fingerprint.

Cite this