Scalable Controller Synthesis with Formal Guarantees

点击翻译按钮获取中文摘要

Cyber-physical systems are complex systems that combine physical capabilities with computational capabilities. These include medical devices and systems, process controls, autonomous vehicles, avionic systems, energy systems, robots, manufacturing systems, and smart structures. The increasingly complex requirements of cyber-physical systems makes it very difficult to control them or even prove that their specification is met. For this reason, automatic controller synthesis with formal guarantees is an active area of research. However, there exist no scalable and formally correct synthesis methods for arbitrary nonlinear systems whose algorithmic parameters are automatically tuned. To address this problem, we propose a synthesis approach that does not rely on any discretization and instead uses optimization techniques in combination with reachability analysis. We plan to translate temporal logic specifications into hybrid automata and compute the product automaton with the system to be controlled. This way, each synthesis problem can be reformulated as solving reach-avoid problems for constrained and disturbed hybrid systems. Through optimization, we will obtain an optimal nominal solution and ensure that all other solutions originating from uncertain initial states, disturbances, and sensor noise also meet all constraints. We obtain the set of all solutions for each optimization iteration using reachability analysis. A final analysis is performed in an over-approximative way to ensure formal guarantees. The combination of optimization techniques and reachability analysis has the critical advantage that only solutions around an optimal reference solution have to be explored, ensuring scalable solutions. To fully automate this process, we will automatically tune the algorithm parameters of our approach. Among other use cases, we will evaluate our approach on our autonomous vehicle EDGAR. The vehicle is shared with the other professorships at TUM and was funded as part of a DFG Major Research Instrumentation grant. All developed algorithms will be available through our software tools CORA (cora.in.tum.de) for reachability analysis and AROC (aroc.cps.in.tum.de) for formal controller synthesis.