Oxford logo
[BKW14] N. Basset, M. Kwiatkowska and C. Wiltsche. Compositional Controller Synthesis for Stochastic Games. In P. Baldan and D. Gorla (editors), Proc. 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704 of LNCS, pages 173-187, Springer. 2014. [pdf] [bib]
Downloads:  pdf pdf (259 KB)  bib bib
Notes: An extended version of this paper, including proofs, can be found at http://www.cs.ox.ac.uk/files/6600/CS-RR-14-05.pdf. The original publication is available at link.springer.com.
Abstract. 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.