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 PSPACS-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.
|graph games, verification|
|2-person games (msc 91A05)|
|Logistics (theme 3)|
|Schloss Dagstuhl - Leibniz Center of Informatics|
|R. Hariharan , M. Mukund , V. Vinay|
|Leibniz International Proceedings in Informatics|
|IARCS Annual Conference on the Foundations of Software Technology and Theoretical Computer Science|
|Organisation||Networks and Optimization|
Horn, F. (2008). Explicit Muller Games are PTIME. In R Hariharan, M Mukund, & V Vinay (Eds.), Proceedings of the 28th IARCS Annual Conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS\'08) (pp. 235–243). Schloss Dagstuhl - Leibniz Center of Informatics.