[BKTW15]
Nicolas Basset, Marta Kwiatkowska, Ufuk Topcu and Clemens Wiltsche.
Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives.
In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), volume 9035 of LNCS, pages 256-271, Springer.
April 2015.
[pdf]
[bib]
[Proposes strategy synthesis for stochastic games with multiple long-run objectives, implemented in an extension of PRISM.]
|
Notes:
The original publication is available at link.springer.com.
|
Links:
[Google]
[Google Scholar]
|
Abstract.
We consider turn-based stochastic games whose winning conditions are conjunctions of satisfaction objectives for long-run average rewards, and address the problem of finding a strategy that almost surely maintains the averages above a given multi-dimensional threshold vector. We show that strategies constructed from Pareto set approximations of expected energy objectives are epsilon-optimal for the corresponding average rewards. We further apply our methods to compositional strategy synthesis for multi-component stochastic games that leverages composition rules for probabilistic automata, which we extend for long-run ratio rewards with fairness. We implement the techniques and illustrate our methods on a case study of automated compositional synthesis of controllers for aircraft primary electric power distribution networks that ensure a given level of reliability.
|