Compositional Controller Synthesis for Stochastic Games

Abstract

Design of autonomous systems is facilitated by automatic synthesis of correct-by-construction controllers from formal models and speci cations. 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 veri cation 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 eciency at a cost of restricting the class of controllers.