Memoryless concretization relation

TL;DR

This paper introduces the memoryless concretization relation (MCR), a new abstraction concept for controller synthesis that simplifies controller design by requiring only current state knowledge, especially useful with non-deterministic quantizers.

Contribution

The paper defines MCR as a novel abstraction relation, distinguishes it from existing relations, and proves its necessity and sufficiency for controller synthesis with non-deterministic discretizations.

Findings

MCR simplifies controller architecture by using current state only.

MCR allows for non-constant controllers within cells.

MCR is both necessary and sufficient for certain abstraction properties.

Abstract

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.