A theory of robust omega-regular software synthesis
A theory of robust omega-regular software synthesis
复制标题
稳健的 omega-regular 软件综合理论
DOI：
10.1145/2539036.2539044
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
P. Tabuada
中科院分区：
文献类型：
--
作者：
R. Majumdar;Elaine Render;P. Tabuada
对于在其操作环境中受到不确定性影响的系统，一个关键特性是鲁棒性：确保未建模但有界的干扰对系统的行为只有比例有界的影响。受鲁棒控制和耗散系统理论的启发，给出了鲁棒性的形式化定义，并给出了离散过渡系统的最优鲁棒控制器设计的算法工具。形式上，我们定义了度量自动机，自动机配备了一个度量的状态和策略的度量自动机，保证ω-正则性能的鲁棒性。我们提出了不动点算法，在多项式时间内构造最优鲁棒策略。与经典图论方法计算的策略相比，我们的算法计算的策略确保了受控系统的行为在干扰的作用下优雅地退化;退化的程度由干扰的大小参数化。我们展示了我们的理论的控制器的设计，容忍无限多的瞬态错误，只要他们很少发生足够的应用。
A key property for systems subject to uncertainty in their operating environment is robustness: ensuring that unmodeled but bounded disturbances have only a proportionally bounded effect upon the behaviors of the system. Inspired by ideas from robust control and dissipative systems theory, we present a formal definition of robustness as well as algorithmic tools for the design of optimally robust controllers for ω-regular properties on discrete transition systems. Formally, we define metric automata—automata equipped with a metric on states—and strategies on metric automata which guarantee robustness for ω-regular properties. We present fixed-point algorithms to construct optimally robust strategies in polynomial time. In contrast to strategies computed by classical graph theoretic approaches, the strategies computed by our algorithm ensure that the behaviors of the controlled system gracefully degrade under the action of disturbances; the degree of degradation is parameterized by the magnitude of the disturbance. We show an application of our theory to the design of controllers that tolerate infinitely many transient errors provided they occur infrequently enough.