Abstractions for Symbolic Controller Synthesis are Composable
For researchers in formal methods and control theory, this work provides a modular abstraction construction pipeline that mitigates the scalability bottleneck of symbolic controller synthesis for high-dimensional systems.
The paper addresses the high computational cost of constructing symbolic abstractions for high-dimensional continuous control systems by introducing a compositional approach where smaller abstract modules are connected in series and parallel, yielding a valid abstraction that satisfies a feedback refinement relation. This reduces runtime and memory requirements.
Translating continuous control system models into finite automata allows us to use powerful discrete tools to synthesize controllers for complex specifications. The abstraction construction step is unfortunately hamstrung by high runtime and memory requirements for high dimensional systems. This paper describes how the transition relation encoding the abstract system dynamics can be generated by connecting smaller abstract modules in series and parallel. We provide a composition operation and show that composing a collection of abstract modules yields another abstraction satisfying a feedback refinement relation. Through compositionality we circumvent the acute computational cost of directly abstracting a high dimensional system and also modularize the abstraction construction pipeline.