Random games

Games are a classical tool for the synthesis of controllers in reactive systems. In this setting, a game is defined by: an arena, which is a graph modelling the system and its evolution; and a winning condition, which models the specification that the controller must ensure. In each state, the outgoing transition is chosen either by the controller (Eve), an hostile environment (Adam), or a stochastic law (Random). This process is repeated for an infinite number of times, generating an infinite play whose winner depends on the winning condition. Our first object of study is the fundamental case of reachability games. We present a new effective approach to the computation of the values, based on permutations of random states. In terms of complexity, the resulting "permutation algorithm" is orthogonal to the classical, strategy-based algorithms: it is exponential in the number of random states, but not in the number of controlled states. We also present an improvement heuristic for this algorithm, inspired by the "strategy improvement" algorithm. We turn next to the very general class of prefix-independent games. We prove the existence of optimal strategies in these games. We also show that our permutation algorithm can be extended into a "meta-algorithm", turning any qualitative algorithm into a quantitative algorithm. We study then the complexity of optimal strategies for Muller games, focusing on the amount of memory that can be saved through the use of randomised strategies. Using the Zielonka tree, we show tight bounds on the necessary and sufficient memory needed to define randomised optimal strategies for any given Muller condition. We also propose a polynomial algorithm for the winner problem in explicit Muller games. The results of the former chapter yield immediately NP and co-NP algorithms for the values problem. Lastly, we consider the finitary versions of parity and Streett games, where the regular conditions are supplemented by universal bounds on delays. We propose a polynomial algorithm for the winner problem on finitary parity games. For finitary Streett games, a reduction to Request-Response games provides an EXPTIME algorithm for qualitative problems, and we show that the problem is PSPACE-hard.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2008

Author dc:creator

• Horn, Florian

Contributors dc:contributor

• Thomas, Wolfgang

• info:eu-repo/classification/ddc/004
• Verifikation
• Logiksynthese
• Kombinatorisches Spiel
• Stochastisches Spiel
• Randomisierung
• Informatik
• verification
• controller synthesis
• graph games
• stochastic games
• randomised control

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-113742%22

OAI record oai:identifier

https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A51451