Oxford logo
[BKTW15] N. Basset, M. Kwiatkowska, U. Topcu, and C. Wiltsche. Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives. In C. Baier, and C. Tinelli (editors), Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 9035 of LNCS, pages 256-271, Springer. 2015. [pdf] [bib]
Downloads:  pdf pdf (449 KB)  bib bib
Notes: An extended version of this paper, including proofs, can be found at http://www.cs.ox.ac.uk/files/7080/CS-RR-14-10.pdf. The original publication is available at link.springer.com.
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.