一类用于保证切换系统可达且停留的控证

在本文中,我们考虑通过简单原语可达且停留(RWS)性质的组合来综合用于时序性质的切换控制器的问题。可达且停留性质规定:从初始集合 I 出发的系统状态必须在有限时间内到达目标集合 G,同时始终保持在安全集合 S 内。我们的方法综合在有限多个模式间进行选择的切换控制器,以满足给定的 RWS 规范。为此,我们考虑控证,即表示实现期望规范的控制策略的类 Lyapunov 函数。然而,对于 RWS 问题,控制类 Lyapunov 函数通常难以以简单多项式形式综合。因此,我们将控制障碍函数与 Lyapunov 函数结合,并附加它们之间的相容条件。使用该方法,控制器综合问题归约为求解量化非线性约束问题,这些问题通过 SMT 求解器的组合来处理。控制器的综合通过一组来自相关工作的有趣数值例子予以展示,并与最先进工具 SCOTS 进行比较。我们的评估表明,我们的方法在计算上可行,并为日益增长的控制器形式化综合方法体系做出了补充。