Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm
Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm
复制标题
分段线性系统的控制器综合与归纳证明：基于 SMT 的算法
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Swarat Chaudhuri
中科院分区：
文献类型：
--
作者：
Zhenqi Huang;Yu Wang;S. Mitra;G. Dullerud;Swarat Chaudhuri
针对分段线性离散时间系统的到达回避问题，提出了一种控制器综合算法。我们的算法依赖于SMT求解器，在本文中，我们重点讨论分段恒定控制策略。我们的算法产生反馈控制律以及关于到达-避免集的无界时间安全性和进度性质的归纳证明。在合理的稳健性假设下，证明了算法的完备性。也就是说，它要么生成上述类型的控制器以及正确性证明，要么确定不可能存在这样的控制器。为了实现这一点，该算法迭代地尝试解决REACH-DOVE问题的SMT编码的弱化和强化版本。在原型实现的基础上，我们给出了应用该算法的初步实验结果。
We present a controller synthesis algorithm for reach-avoid problems for piecewise linear discrete-time systems. Our algorithm relies on SMT solvers and in this paper we focus on piecewise constant control strategies. Our algorithm generates feedback control laws together with inductive proofs of unbounded time safety and progress properties with respect to the reach-avoid sets. Under a reasonable robustness assumption, the algorithm is shown to be complete. That is, it either generates a controller of the above type along with a proof of correctness, or it establishes the impossibility of the existence of such controllers. To achieve this, the algorithm iteratively attempts to solve a weakened and strengthened versions of the SMT encoding of the reach-avoid problem. We present preliminary experimental results on applying this algorithm based on a prototype implementation.