License: 
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2008.1756
URN: urn:nbn:de:0030-drops-17565
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1756/
Horn, Florian
Explicit Muller Games are PTIME
Abstract
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 \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.
BibTeX - Entry
@InProceedings{horn:LIPIcs:2008:1756,
author = {Florian Horn},
title = {{Explicit Muller Games are PTIME}},
booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
pages = {235--243},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-08-8},
ISSN = {1868-8969},
year = {2008},
volume = {2},
editor = {Ramesh Hariharan and Madhavan Mukund and V Vinay},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2008/1756},
URN = {urn:nbn:de:0030-drops-17565},
doi = {10.4230/LIPIcs.FSTTCS.2008.1756},
annote = {Keywords: Games, authomata, model checking}
}
|
Keywords: |
|
Games, authomata, model checking |
|
Collection: |
|
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science |
|
Issue Date: |
|
2008 |
|
Date of publication: |
|
05.12.2008 |
