Compositional Controller Synthesis for Stochastic Games

  • Nicolas Basset
  • Marta Kwiatkowska
  • Clemens Wiltsche
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and specifications. We focus on stochastic games, which can model the interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. We leverage rules for compositional assume-guarantee verification of probabilistic automata to synthesise controllers for games with multi-objective quantitative winning conditions. By composing winning strategies synthesised for the individual components, we can thus obtain a winning strategy for the composed game, achieving better scalability and efficiency at a cost of restricting the class of controllers.


Normal Form Stochastic Game Winning Strategy Conjunctive Query Normal Form Game 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baier, C., Groesser, M., Ciesinski, F.: Quantitative analysis under fairness constraints. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 135–150. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  2. 2.
    Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional controller synthesis for stochastic games. University of Oxford, Technical Report CS-RR-14-05 (2014)Google Scholar
  3. 3.
    Campbell, M., Egerstedt, M., How, J.P., Murray, R.M.: Autonomous driving in urban environments: approaches, lessons and challenges. Phil. Trans. R. Soc. A 368, 4649–4672 (1928)CrossRefGoogle Scholar
  4. 4.
    Chatterjee, K., Jurdziński, M., Henzinger, T.A.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 100–113. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: PRISM-games: A model checker for stochastic multi-player games. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 185–191. Springer, Heidelberg (2013)Google 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.
    Cheung, L., Lynch, N., Segala, R., Vaandrager, F.: Switched PIOA: Parallel composition via distributed scheduling. TCS 365(1-2), 83–108 (2006)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26(5), 109–120 (2001)CrossRefGoogle Scholar
  10. 10.
    Filar, J., Vrieze, K.: Competitive Markov decision processes. Springer (1996)Google Scholar
  11. 11.
    Gelderie, M.: Strategy composition in compositional games. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 263–274. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  12. 12.
    Ghosh, S., Ramanujam, R., Simon, S.: Playing extensive form games in parallel. In: Dix, J., Leite, J., Governatori, G., Jamroga, W. (eds.) CLIMA XI. LNCS, vol. 6245, pp. 153–170. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  13. 13.
    Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Information and Computation 232, 38–65 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  14. 14.
    Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  15. 15.
    Ozay, N., Topcu, U., Murray, R.M., Wongpiromsarn, T.: Distributed synthesis of control protocols for smart camera networks. In: ICCPS 2011, pp. 45–54. IEEE (2011)Google Scholar
  16. 16.
    Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE (1977)Google Scholar
  17. 17.
    Segala, R.: Modelling and Verification of Randomized Distributed Real Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)Google Scholar
  18. 18.
    Shapley, L.S.: Stochastic games. Proc. Natl. Acad. Sci. USA 39(10), 1095 (1953)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Sokolova, A., de Vink, E.P.: Probabilistic automata: system types, parallel composition and comparison. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 1–43. Springer, Heidelberg (2004)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Nicolas Basset
    • 1
  • Marta Kwiatkowska
    • 1
  • Clemens Wiltsche
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordUnited Kingdom

Personalised recommendations