The correctness of control software in safety-critical applications like autonomous vehicles is crucial. One approach to achieve this goal is through “symbolic control”, where physical systems are approximated by finite-state abstractions. Then, using those abstractions, provably-correct digital controllers are algorithmically-synthesized for concrete systems, satisfying some complex high-level requirements. Unfortunately, the complexity of constructing such abstractions and synthesizing their controllers grows exponentially in the number of state variables in the system which limits its applicability to simple systems.

This poster clarifies more visually what we presented in the accepted paper as a unified approach that utilizes the sparsity of the interconnection structure in dynamical systems for both construction of finite abstractions and synthesis of symbolic controllers. We also present visually the parallel algorithms we proposed to target HPC platforms. We show the effectiveness of the results on a 7-dimensional model of a BMW 320i car by designing a controller to keep the car in the travel lane unless it is blocked.