用于保持可达性质的切换控制器反例引导综合
系统与控制
2015-09-24 v3
摘要
我们引入了一种反例引导的归纳综合（CEGIS）框架，用于综合连续时间切换控制器，以保证闭环系统的保持可达（RWS）性质。该解决方案基于为切换系统综合一类特殊定义的控制Lyapunov函数（CLFs），从而产生在每个模式中具有保证最小驻留时间的切换控制器。接下来，我们使用基于CEGIS的方法迭代求解由此产生的量化存在-全称约束，并找到CLF。我们引入了松弛以保证终止，以及启发式方法以提高收敛速度。最后，我们在一组具有二至六个状态变量的基准上评估了我们的方法。我们的评估包括与相关工具的初步比较。所提方法展示了非线性SMT求解器在可证明正确的切换控制律综合中的前景。
引用
@article{arxiv.1505.01180,
title = {Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties},
author = {Hadi Ravanbakhsh and Sriram Sankaranarayanan},
journal= {arXiv preprint arXiv:1505.01180},
year = {2015}
}