Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives

  • Nicolas Basset
  • Marta Kwiatkowska
  • Ufuk Topcu
  • Clemens Wiltsche
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9035)


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 ε-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.


Markov Decision Process Stochastic Game Reward Structure Strategy Synthesis Strategy Construction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Baier, C., Dubslaff, C., Klüppelholz, S., Leuschner, L.: Energy-utility analysis for resilient systems using probabilistic model checking. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 20–39. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  2. 2.
    Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. Technical Report RR-14-10, University of Oxford (2014)Google Scholar
  3. 3.
    Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional controller synthesis for stochastic games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 173–187. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  4. 4.
    Brázdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. LMCS 10(1) (2014)Google Scholar
  5. 5.
    Chatterjee, K., Randour, M., Raskin, J.F.: Strategy synthesis for multi-dimensional quantitative objectives. Acta Inf. 51(3-4), 129–163 (2014)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266–277. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  7. 7.
    Chen, T., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: Synthesis for multi-objective stochastic games: An application to autonomous urban driving. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 322–337. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  8. 8.
    Automation Direct. Part number AD-SSR610-AC-280A, Relays and Timers, Book 2 (14.1), eRL-45 (2014)Google Scholar
  9. 9.
    Gimbert, H., Horn, F.: Solving simple stochastic tail games. In: SODA, pp. 847–862. SIAM (2010)Google Scholar
  10. 10.
    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. I&C, 232:38–65 (2013)Google Scholar
  11. 11.
    Michalko, R.G.: Electrical starting, generation, conversion and distribution system architecture for a more electric vehicle, US Patent 7,439,634 (2008)Google Scholar
  12. 12.
    Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)Google Scholar
  13. 13.
    Shapley, L.S.: Stochastic games. Proc. Natl. Acad. Sci. USA 39(10), 1095 (1953)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Sinnett, M.: 787 no-bleed systems: saving fuel and enhancing operational efficiencies. Aero Quarterly, 6–11 (2007)Google Scholar
  15. 15.
    von Essen, C.: Quantitative Verification and Synthesis. PhD thesis, VERIMAG (2014)Google Scholar
  16. 16.
    Xu, H., Topcu, U., Murray, R.M.: Reactive protocols for aircraft electric power distribution. In: CDC. IEEE (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Nicolas Basset
    • 1
  • Marta Kwiatkowska
    • 1
  • Ufuk Topcu
    • 2
  • Clemens Wiltsche
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK
  2. 2.Department of Electrical and Systems EngineeringUniversity of PennsylvaniaPhiladelphiaUSA

Personalised recommendations