Sciweavers

Share
CAV
2007
Springer

An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games

8 years 9 months ago
An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games
Three-color parity games capture the disjunction of a B¨uchi and a co-B¨uchi condition. The most efficient known algorithm for these games is the progress measures algorithm by Jurdzi´nski. 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. Using the tool TICC as a platform, we compare the performance of a BDD-based symbolic implementation of the progress measure algorithm with acceleration, and of the symbolic implementation of the classical µ-calculus algorithm of Emerson and Jutla.
Luca de Alfaro, Marco Faella
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CAV
Authors Luca de Alfaro, Marco Faella
Comments (0)
books