www.prismmodelchecker.org
[BKW17] Nicolas Basset, Marta Kwiatkowska and Clemens Wiltsche. Compositional Strategy Synthesis for Stochastic Games with Multiple Objectives. Information and Computation, 261(3), pages 536-587. 2017. [pdf] [bib] [Proposes multi-objective strategy synthesis techniques for stochastic games, along with a compositional assume-guarantee strategy synthesis framework.]
Downloads:  pdf pdf (1.72 MB)  bib bib
Links: [Google] [Google Scholar]
Abstract. Design of autonomous systems is facilitated by automatic synthesis of controllers from formal models and specifi cations. We focus on stochastic games, which can model interaction with an adverse environment, as well as probabilistic behaviour arising from uncertainties. Our contribution is twofold. First, we study long-run specifi cations expressed as quantitative multi-dimensional mean-payoff and ratio objectives. We then develop an algorithm to synthesise ε-optimal strategies for conjunctions of almost sure satisfaction for mean payoffs and ratio rewards (in general games) and Boolean combinations of expected mean-payoffs (in controllable multi-chain games). Second, we propose a compositional framework, together with assume-guarantee rules, which enables winning strategies synthesised for individual components to be composed to a winning strategy for the composed game. The framework applies to a broad class of properties, which also include expected total rewards, and has been implemented in the software tool PRISM-games.

Publications