Explicit Muller Games are PTIME

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 NP and co-NP. 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.

• Type: Conference
• Year: 2008
• Where: FSTTCS
• Authors: Florian Horn
• Keywords: Coloured Condition, Explicit Muller Games, FSTTCS 2008, Software Engineering, Winner Problem