Memoryless concretization relation

We introduce the concept of memoryless concretization relation (<Formula format="inline"><TexMath><?TeX MCR?></TexMath><AltText>Math 1</AltText><File name="hscc24-15-inline1" type="svg"/></Formula>) to describe abstraction within the context of controller synthesis. This relation is a specific instance of alternating simulation relation (<Formula format="inline"><TexMath><?TeX ASR?></TexMath><AltText>Math 2</AltText><File name="hscc24-15-inline2" type="svg"/></Formula>), where it is possible to simplify the controller architecture. In the case of <Formula format="inline"><TexMath><?TeX ASR?></TexMath><AltText>Math 3</AltText><File name="hscc24-15-inline3" type="svg"/></Formula>, the concretized controller needs to simulate the concurrent evolution of two systems, the original and abstract systems, while for <Formula format="inline"><TexMath><?TeX MCR?></TexMath><AltText>Math 4</AltText><File name="hscc24-15-inline4" type="svg"/></Formula>, the designed controllers only need knowledge of the current concrete state. We demonstrate that the distinction between <Formula format="inline"><TexMath><?TeX ASR?></TexMath><AltText>Math 5</AltText><File name="hscc24-15-inline5" type="svg"/></Formula> and <Formula format="inline"><TexMath><?TeX MCR?></TexMath><AltText>Math 6</AltText><File name="hscc24-15-inline6" type="svg"/></Formula> 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 <Formula format="inline"><TexMath><?TeX MCR?></TexMath><AltText>Math 7</AltText><File name="hscc24-15-inline7" type="svg"/></Formula> at the expense of increasing the non-determinism in the abstraction. We clarify the difference between the <Formula format="inline"><TexMath><?TeX MCR?></TexMath><AltText>Math 8</AltText><File name="hscc24-15-inline8" type="svg"/></Formula> and the feedback refinement relation (<Formula format="inline"><TexMath><?TeX FRR?></TexMath><AltText>Math 9</AltText><File name="hscc24-15-inline9" type="svg"/></Formula>), 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.