Abstractions for Symbolic Controller Synthesis are Composable

TL;DR

This paper introduces a compositional approach to generate abstractions for symbolic controller synthesis, significantly reducing computational costs for high-dimensional systems by modularly combining smaller abstract modules.

Contribution

It presents a novel composition operation for abstract modules, enabling scalable and modular abstraction construction for complex control systems.

Findings

Composition of abstract modules preserves abstraction properties.

Modular approach reduces runtime and memory for high-dimensional systems.

Enables scalable controller synthesis through compositional abstractions.

Abstract

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.