Klaus Drager ; Vojtech Forejt ; Marta Kwiatkowska ; David Parker ; Mateusz Ujma - Permissive Controller Synthesis for Probabilistic Systems

lmcs:1576 - Logical Methods in Computer Science, June 30, 2015, Volume 11, Issue 2 - https://doi.org/10.2168/LMCS-11(2:16)2015
Permissive Controller Synthesis for Probabilistic Systems

Authors: Klaus Drager ; Vojtech Forejt ; Marta Kwiatkowska ; David Parker ORCID-iD; Mateusz Ujma

    We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. 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 permissivity using penalties, which are incurred each time a possible control action is disallowed 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 establish 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.


    Volume: Volume 11, Issue 2
    Published on: June 30, 2015
    Submitted on: November 8, 2014
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Systems and Control,Mathematics - Optimization and Control
    Fundings :
      Source : OpenAIRE Research Graph
    • From Software Verification to Everyware Verification; Funder: European Commission; Code: 246967
    • LSCITS-RPv2: Large-Scale Complex IT Systems Initiative - Research Programme v2; Funder: UK Research and Innovation; Code: EP/F001096/1
    • Towards comprehensive verification of stochastic systems; Funder: UK Research and Innovation; Code: EP/M023656/1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-319-91908-9_21
    • 10.1007/978-3-319-91908-9_21
    • 10.1007/978-3-319-91908-9_21
    • 10.1007/978-3-319-91908-9_21
    The 10,000 Facets of MDP Model Checking
    Baier, Christel ; Hermanns, Holger ; Katoen, Joost-Pieter ; Steffen, Bernhard ; Woeginger, Gerhard ;

    6 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 489 times.
    This article's PDF has been downloaded 331 times.