Recursive algorithm for parity games requires exponential time
Institut für Informatik, LMU München 80538 Munich, Germany
Received: 23 January 2011
Accepted: 22 September 2011
This paper presents a new lower bound for the recursive algorithm for solving parity games which is induced by the constructive proof of memoryless determinacy by Zielonka. We outline a family of games of linear size on which the algorithm requires exponential time.
Mathematics Subject Classification: 05C57
Key words: Parity games / recursive algorithm / lower bound / μcalculus / model checking
© EDP Sciences 2011