基于信号时间逻辑规范的诊断与修复
Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications
AI总结：
本文研究了混合系统在信号时间逻辑规范下的诊断与修复问题，提出基于模型预测控制框架的控制器综合方法，通过混合整数线性规划解决不可行性问题，并提供修复建议。
摘要：
我们研究了混合系统在信号时间逻辑（STL）规范下的诊断与修复问题。我们的重点是自动综合控制器的模型预测控制（MPC）框架。我们基于最近的方法，将控制器综合问题减少为求解一个或多个混合整数线性规划（MILP）问题，其中MILP的不可行性通常表明控制器综合问题的不可实现性。给定一个不可行的STL综合问题，我们提出算法以提供关于不可实现性的反馈，并提供使其可行的建议。我们的算法是准确且完整的，即它们提供正确的诊断，并在存在可行解时始终终止于一个非平凡的规范，该规范可以使用所选综合方法实现。我们通过各种嵌入式物理系统控制器的综合展示了方法的有效性，包括自主驾驶应用和飞机电力系统。
英文摘要：
We address the problem of diagnosing and repairing specifications for hybrid systems formalized in signal temporal logic (STL). Our focus is on the setting of automatic synthesis of controllers in a model predictive control (MPC) framework. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of a MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete, i.e., they provide a correct diagnosis, and always terminate with a non-trivial specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on the synthesis of controllers for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
