We introduce the concept of memoryless concretization relation (MCR) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation (ASR), where it is possible to simplify the controller architecture. In the case of ASR, the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for MCR, the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between ASR and MCR becomes significant only when a non-deterministic quantizer is involved, such as in cases where the state space discretization consists of overlapping cells. We also show that any abstraction of a system that alternatingly simulates a system can be completed to satisfy MCR at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the MCR and the feedback refinement relation (FRR), showing in particular that the former allows for non-constant controllers within cells. This provides greater flexibility in constructing a practical abstraction, for instance, by reducing non-determinism in the abstraction. Finally, we prove that this relation is not only sufficient, but also necessary, for ensuring the above properties.
翻译:我们引入无记忆具体化关系(MCR)的概念,以描述控制器综合背景下的抽象行为。该关系是交替仿真关系(ASR)的一个具体实例,能够简化控制器架构。在ASR情况下,具体化控制器需要同时模拟原始系统与抽象系统的并发演化过程;而针对MCR,设计的控制器仅需感知当前具体状态。我们证明:仅当涉及非确定性量化器时(例如状态空间离散化由重叠单元构成),ASR与MCR之间的差异才具有显著意义。同时表明,任何对系统进行交替仿真的抽象系统均可通过增加抽象中的非确定性程度,补全为满足MCR的系统。我们阐明MCR与反馈细化关系(FRR)之间的区别,特别指出前者允许单元内采用非恒定控制器。这为构建实用抽象系统提供了更大灵活性,例如通过减少抽象中的非确定性。最后,我们证明该关系不仅是保证上述性质的充分条件,更是必要条件。