Permissive Controller Synthesis for Probabilistic Systems

Klaus Dräger, Vojtěch Forejt, Marta Kwiatkowska, David Parker, Mateusz Ujma

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution

16 Citations (Scopus)

Abstract

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 permissiveness using penalties, which are incurred each time a possible control 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 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.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings
EditorsErika Abraham, Klaus Havelund
PublisherSpringer
Pages531-546
Number of pages16
Volume8413
ISBN (Electronic)978-3-642-54862-8
ISBN (Print)978-3-642-54861-1
DOIs
Publication statusPublished - 2014
Event20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - v, France
Duration: 5 Apr 201413 Apr 2014

Publication series

NameLecture Notes in Computer Science
Volume8413
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Country/TerritoryFrance
Cityv
Period5/04/1413/04/14

Fingerprint

Dive into the research topics of 'Permissive Controller Synthesis for Probabilistic Systems'. Together they form a unique fingerprint.

Cite this