状态空间物理被控对象的数字控制器自动化形式化综合
系统与控制
2017-05-09 v2 计算机科学中的逻辑
摘要
我们提出了一种可靠且自动化的方法，用于为表示为线性时不变模型的物理被控对象综合安全的数字反馈控制器。模型以带输入的动力学方程给出，在连续状态空间上演化，并考虑由控制器信号数字化引起的误差。我们的方法分为两个阶段，利用反例引导归纳综合（CEGIS）和可达性分析。CEGIS 综合一个静态反馈控制器，在可达空间安全性所给限制下稳定系统。安全性通过 BMC 或抽象加速验证；如果验证步骤失败，我们通过泛化反例来精化控制器。我们为数字控制文献中复杂的物理被控对象模型综合了稳定且安全的控制器。
引用
@article{arxiv.1705.00981,
title = {Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants},
author = {Alessandro Abate and Iury Bessa and Dario Cattaruzza and Lucas Cordeiro and Cristina David and Pascal Kesseli and Daniel Kroening and Elizabeth Polgreen},
journal= {arXiv preprint arXiv:1705.00981},
year = {2017}
}