Permissive Controller Synthesis for Probabilistic Systems

Abstract. We propose novel controller synthesis techniques for proba-bilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probabil-ity is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust con-trollers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be im-posed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permis-siveness using penalties, which are incurred each time a possible con-trol action is blocked by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We estab-lish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.