Explicit Muller Games are PTIME
Florian Horn · Data Archiving and Networked Services (DANS) · 2008
Regular games provide a very useful model for the synthesis of controllers in reactive systems. The complexity of these games depends on the representation of the winning condition: if it is represented through a win-set, a coloured condition, a Zielonka-DAG or Emerson-Lei formulae, the winner problem is \pspace-complete; if the winning condition is represented as a Zielonka tree, the winner problem belongs to p and \conp. In this paper, we show that explicit Muller games can be solved in polynomial time, and provide an effective algorithm to compute the winning regions.