[an error occurred while processing this directive]
An error occured whilst processing this directive
Stochastic Games for Verification
CWI, Amsterdam
3pm Friday 6th of February, 2009
Room G07a, Informatics Forum
Abstract
Graph 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.
An error occured whilst processing this directive