Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach
The correctness of control software in many safety-critical applications such as autonomous vehicles is very crucial. One approach to achieve this goal is through “symbolic control”, where complex 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. This limits its applicability to simple physical systems. One approach to mitigate the computational complexity in the construction of finite abstractions is to utilize inherent sparsity of the interconnection structure of dynamical systems. While it helps reducing the complexity of constructing finite abstractions, symbolic controllers are still computed monolithically, where controllers are synthesized from the overall state sets without taking into account the sparsity of the interconnection structure. Another approach to reduce computational complexity of symbolic controllers is to use parallelized algorithms and data structures and targeting modern high-performance computing (HPC) platforms, including CPUs, GPUs, HW accelerators, and Cloud computing, all with large numbers of processing elements (PEs). Although it scales well with respect to the number of PEs, it still takes a monolithic view of the entire system without considering its sparsity structure. This paper presents a unified approach that utilizes sparsity of the interconnection structure in dynamical systems for both construction of finite abstractions and synthesis of symbolic controllers. In addition, parallel algorithms are proposed to target HPC platforms and results show remarkable reductions in computation times. In particular, 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.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | |||
10:30 30mTalk | Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach TACAS Link to publication | ||
11:00 30mTalk | StocHy: automated verification and synthesis of stochastic processes TACAS Link to publication | ||
11:30 30mTalk | Minimal-Time Synthesis for Parametric Timed Automata TACAS Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Vincent Bloemen University of Twente, Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University Link to publication | ||
12:00 30mTalk | Environmentally-friendly GR(1) Synthesis TACAS Link to publication |