Sparsity-Sensitive Finite Abstraction
For formal controller synthesis, this work addresses the scalability bottleneck of finite abstraction by leveraging sparsity, enabling application to higher-dimensional systems.
The paper presents a modification to the finite abstraction algorithm for continuous-space models that exploits sparsity in the interconnection structure, reducing exponential runtime. It achieves speed-ups on existing benchmarks and enables abstraction of a 51-dimensional vehicular traffic network.
Abstraction of a continuous-space model into a finite state and input dynamical model is a key step in formal controller synthesis tools. To date, these software tools have been limited to systems of modest size (typically $\leq$ 6 dimensions) because the abstraction procedure suffers from an exponential runtime with respect to the sum of state and input dimensions. We present a simple modification to the abstraction algorithm that dramatically reduces the computation time for systems exhibiting a sparse interconnection structure. This modified procedure recovers the same abstraction as the one computed by a brute force algorithm that disregards the sparsity. Examples highlight speed-ups from existing benchmarks in the literature, synthesis of a safety supervisory controller for a 12-dimensional and abstraction of a 51-dimensional vehicular traffic network.