ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Thu 11 Apr 2019 10:30 - 11:00 at SUN I - Synthesis Chair(s): Roland Meyer

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 Apr

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - Synthesis at SUN I
Chair(s): Roland MeyerTechnical University of Braunschweig
tacas-2019-papers10:30 - 11:00
Talk
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Nathalie CauchiUniversity of Oxford, Alessandro AbateUniversity of Oxford
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Link to publication