Memoization of Parity Games: a practical proposal

Memoization of Parity Games: a practical proposal
Speaker:  Giorgio Audrito - Università di Torino
  Wednesday, April 19, 2017 at 2:30 PM Rinfresco 14.15, inizio seminario 14.30.
Parity games have gathered an increasing amount of attention during the last few decades, for two main reasons. Firstly, an algorithm for solving them provides a backend to many problems in automated verification and controller synthesis: for instance, the model checking problem for modal mu-calculus (and CTL, CTL*, LTL) is reducible to it. Secondly, this problem features a peculiar complexity-theoretic status: parity games solving is known to be both in NP and in co-NP, while still not known to be in P.

Several radically different approaches have been used to tackle this problem: recursion, strategy improvement, genetic algorithms and iterative lifting of progress measures; with the best algorithms achieving quasi-polynomial worst time. However, "worse" algorithms are often preferable for practical inputs, even though having an exponential worst case time; such as the recursive algorithm. After a brief survey of the state of the art, we present a joint ongoing work with Romeo Rizzi about a new recursive algorithm with memoization. This algorithm is always faster than naive recursion, while achieving linear execution time on the infinite classes of graphs which are known to have exponential solving time for the recursive algorithm. Even though our current asymptotic bound for this algorithm is super-polynomial, it is still open whether there exists an infinite class of graphs witnessing super-polynomial time for it.

Ca' Vignal 3 - Piramide, Floor 0, Hall Verde

Contact person
Romeo Rizzi

Publication date
March 24, 2017