Scalable Controller Synthesis with Formal Guarantees

具有正式保证的可扩展控制器综合

• 批准号: 511538378
• 负责人: Professor Dr.-Ing. Matthias Althoff
• 金额: --
• 依托单位: Lehrstuhl für Informatik VI: Robotik, Künstliche Intelligenz und Echtzeitsysteme
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/511538378?language=en
• 关键词: Scalable; Controller; Synthesis; 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.

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