Solving Emerson-Lei Games via Zielonka Trees

We show how Emerson-Lei games can be solved symbolically by providing a fixpoint-based characterization of the winning region, which results from analysis of the Zielonka tree of the winning condition. The proposed algorithm generalizes the solutions of known winning conditions such as parity, Streett, Rabin, and GR[1] objectives, and in the case of these conditions reproduces previously known algorithms and complexity results; the algorithm solves unrestricted Emerson-Lei games with n nodes, m edges and d colors in time O((n^(d/2)) d! m). Contributed talk given by Daniel Hausmann

Authors

• Daniel Hausmann

Keywords

No keywords are indexed for this paper.