Scalable Controller Synthesis with Formal Guarantees

网络物理系统是将物理能力和计算能力结合在一起的复杂系统。这些领域包括医疗设备和系统、过程控制、自动驾驶车辆、航空电子系统、能源系统、机器人、制造系统和智能结构。网络物理系统日益复杂的需求使得控制它们变得非常困难，甚至很难证明它们的规范得到了满足。因此，具有形式保证的自动控制器综合是一个活跃的研究领域。然而，对于算法参数可自动调整的任意非线性系统，目前还没有可扩展且形式正确的综合方法。为了解决这一问题，我们提出了一种综合方法，该方法不依赖于任何离散化，而是结合可达性分析使用优化技术。我们计划将时序逻辑规格说明转化为混合自动机，并计算出带有被控系统的乘积自动机。这样，每个综合问题都可以转化为求解约束和扰动混合系统的到达-回避问题。通过优化，我们将得到一个最优标称解，并确保源于不确定初始状态、干扰和传感器噪声的所有其他解也满足所有约束。通过可达性分析，我们得到了每次优化迭代的所有解的集合。最后的分析是以一种过度近似的方式进行的，以确保正式的保证。优化技术和可达性分析的组合具有关键优势，即只需探索最佳参考解决方案周围的解决方案，从而确保可扩展的解决方案。为了使这个过程完全自动化，我们将自动调整我们方法的算法参数。在其他用例中，我们将评估我们在自动驾驶汽车Edga上的方法。这辆车是与TUM的其他教授共享的，并作为DFG重大研究仪器拨款的一部分提供资金。所有开发的算法将通过我们用于可达性分析的软件工具Cora(cora.in.um.de)和用于正式控制器综合的软件工具AROC(aroc.cps.in.tom.de)提供。

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.