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.
More information on this clip and others video formats
Send this URL to a friend
