An Improved Algorithm for Three-Color Parity Games

EPFL IC Tresor talks

by Marco Faella Abstract: Three-color parity games capture the disjunction of a Buchi and a co-Buchi condition. The most efficient known algorithm for these games is the progress measure algorithm by Jurdzinski. In this talk we present an acceleration technique that, while leaving the worst-case complexity unchanged, often leads to considerable speed-ups in games arising in practice. As an application, we consider games played in discrete real time, where players should be prevented from stopping time by always choosing moves with delay zero. The time progress condition can be encoded as a three-color parity game and checked using a symbolic implementation of the above-mentioned algorithm.