Feedback Refinement Relations for the Synthesis of Symbolic Controllers
Feedback Refinement Relations for the Synthesis of Symbolic Controllers
复制标题
DOI：
10.1109/tac.2016.2593947
复制
发表时间：
2017-04-01
影响因子：
6.8
通讯作者：
Rungger, Matthias
中科院分区：
文献类型：
--
作者：
Reissig, Gunther;Weber, Alexander;Rungger, Matthias
我们为自动化控制器合成以执行一般预定义的规格提供了一种抽象和完善方法。设计的控制器仅需要量化（或符号）状态信息，并且可以通过静态量化器与系统连接。对于设计控制器的任何实际实施，这两个功能尤其重要，正如我们所证明的，其特征是植物与抽象之间存在反馈改进关系。反馈改进关系是本文介绍的一个新颖概念。我们的工作建立在系统的一般概念的基础上，具有设定值的动力学和可能的非确定性量化器，以允许在存在各种不确定性和干扰的情况下稳健地且可证明其稳健地执行规范的控制器。我们在明确的意义上确定了一类规范的抽象，并提供了一种有效计算规范抽象的方法。我们在两个例子上证明了我们方法的实用性。
We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.