Permissive Controller Synthesis for Probabilistic Systems.

D 2014

Permissive Controller Synthesis for Probabilistic Systems.

DRAEGER, Klaus; Vojtěch FOREJT; Marta KWIATKOWSKA; David PARKER; Mateusz UJMA et. al.

Základní údaje

Originální název

Permissive Controller Synthesis for Probabilistic Systems.

Autoři

DRAEGER, Klaus; Vojtěch FOREJT; Marta KWIATKOWSKA; David PARKER a Mateusz UJMA

Vydání

Berlin, Tools and Algorithms for the Construction and Analysis of Systems, od s. 531-546, 16 s. 2014

Nakladatel

Springer Berlin Heidelberg

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/14:00080050

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-54861-1

ISSN

DOI

https://doi.org/10.1007/978-3-642-54862-8_44

EID Scopus

2-s2.0-84900537126

Klíčová slova anglicky

controller synthesis; stochastic games; optimisation

Štítky

core_A, firank_A

Změněno: 27. 4. 2015 05:04, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

MUNI/33/IP1/2014, interní kód MU

Název: Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky (Akronym: PVT-VVPZ)

Investor: Masarykova univerzita, Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky

Citovat

DRAEGER, Klaus; Vojtěch FOREJT; Marta KWIATKOWSKA; David PARKER a Mateusz UJMA. Permissive Controller Synthesis for Probabilistic Systems. In Erika Ábrahám, Klaus Havelund. Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer Berlin Heidelberg, 2014, s. 531-546. ISBN 978-3-642-54861-1. Dostupné z: https://doi.org/10.1007/978-3-642-54862-8_44.

@inproceedings{1297489,
   author = {Draeger, Klaus and Forejt, Vojtěch and Kwiatkowska, Marta and Parker, David and Ujma, Mateusz},
   address = {Berlin},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
   doi = {https://doi.org/10.1007/978-3-642-54862-8_44},
   editor = {Erika Ábrahám, Klaus Havelund},
   keywords = {controller synthesis; stochastic games; optimisation},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin},
   isbn = {978-3-642-54861-1},
   pages = {531-546},
   publisher = {Springer Berlin Heidelberg},
   title = {Permissive Controller Synthesis for Probabilistic Systems.},
   year = {2014}
}

TY  - CONF
ID  - 1297489
AU  - Draeger, Klaus - Forejt, Vojtěch - Kwiatkowska, Marta - Parker, David - Ujma, Mateusz
PY  - 2014
TI  - Permissive Controller Synthesis for Probabilistic Systems.
PB  - Springer Berlin Heidelberg
CY  - Berlin
SN  - 9783642548611
KW  - controller synthesis
KW  - stochastic games
KW  - optimisation
N2  - 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.
ER  -

DRAEGER, Klaus; Vojtěch FOREJT; Marta KWIATKOWSKA; David PARKER a Mateusz UJMA. Permissive Controller Synthesis for Probabilistic Systems. In Erika Ábrahám, Klaus Havelund. \textit{Tools and Algorithms for the Construction and Analysis of Systems}. Berlin: Springer Berlin Heidelberg, 2014, s.~531-546. ISBN~978-3-642-54861-1. Dostupné z: https://doi.org/10.1007/978-3-642-54862-8\_{}44.

Přehled o publikaci