Projects per year
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 language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems |
Subtitle of host publication | 20th 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 |
Editors | Erika Abraham, Klaus Havelund |
Publisher | Springer |
Pages | 531-546 |
Number of pages | 16 |
Volume | 8413 |
ISBN (Electronic) | 978-3-642-54862-8 |
ISBN (Print) | 978-3-642-54861-1 |
DOIs | |
Publication status | Published - 2014 |
Event | 20th 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 2014 → 13 Apr 2014 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Volume | 8413 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 20th 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/Territory | France |
City | v |
Period | 5/04/14 → 13/04/14 |
Fingerprint
Dive into the research topics of 'Permissive Controller Synthesis for Probabilistic Systems'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Automated Game-Theoretic Verification of Security Systems
Parker, D. (Principal Investigator)
Engineering & Physical Science Research Council
4/11/13 → 31/10/14
Project: Research Councils