基于信号时序逻辑规范的合成诊断与修复
系统与控制
2016-02-08 v1 计算机科学中的逻辑
摘要
我们处理混合系统基于信号时序逻辑（STL）形式化规范的诊断与修复问题。我们的焦点在于模型预测控制（MPC）框架中的控制器自动综合设置。我们建立在近期将控制器综合问题归约为求解一个或多个混合整数线性规划（MILP）的方法上，其中MILP的不可行性通常指示控制器综合问题的不可实现性。给定一个不可行的STL综合问题，我们提出算法，提供关于不可实现原因的反馈，以及使其可实现的建议。我们的算法是可靠且完整的，即它们提供正确诊断，并且总能在存在此类解时终止于一个使用所选综合方法可行的非平凡规范。我们在各种信息物理系统的控制器综合上展示了我们方法的有效性，包括一个自动驾驶应用和飞机电力系统。
引用
@article{arxiv.1602.01883,
title = {Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications},
author = {Shromona Ghosh and Dorsa Sadigh and Pierluigi Nuzzo and Vasumathi Raman and Alexandre Donze and Alberto Sangiovanni-Vincentelli and S. Shankar Sastry and Sanjit A. Seshia},
journal= {arXiv preprint arXiv:1602.01883},
year = {2016}
}