Memoryless concretization relation
Julien Calbert, Sébastien Mattenet, Antoine Girard, Raphaël M. Jungers · 2024
We introduce the concept of memoryless concretization relation ( Math 1 ) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation ( Math 2 ), where it is possible to simplify the controller architecture. In the case of Math 3 , the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for Math 4 , the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between Math 5 and Math 6 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 Math 7 at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the Math 8 and the feedback refinement relation ( Math 9 ), 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.