Permissive Controller Synthesis for Probabilistic Systems
Permissive Controller Synthesis for Probabilistic Systems
复制标题
DOI：
10.2168/lmcs-11(2:16)2015
复制
发表时间：
2014-04
期刊：
影响因子：
--
通讯作者：
Klaus Dräger;Vojtěch Forejt;M. Kwiatkowska;D. Parker;Mateusz Ujma
中科院分区：
文献类型：
--
作者：
Klaus Dräger;Vojtěch Forejt;M. Kwiatkowska;D. Parker;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 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.