基于凸优化的可达-避免验证

本文提出基于优化的新方法，用于验证由常微分方程建模的连续时间系统的可达-避免（或称事件性）性质。给定系统、初始集、安全集与目标状态集，若初始集中的所有初始条件出发的系统轨迹最终（即无界但有限时间内）进入目标集，且在此首次命中目标前始终停留在安全集内，则称可达-避免性质成立。基于折扣值函数，推导出两组量化约束，用于通过计算指数/渐近引导-障碍函数（它们构成以指数或渐近速率安全护送系统至目标集的障碍）来验证可达-避免性质。有趣的是，发现其中一组约束的解称为指数引导-障碍函数，恰为基于矩方法导出的已有约束的简化版本，而另一组约束的解称为渐近引导-障碍函数则是全新的。此外，基于这组新约束，我们推导出一组更具表达力的约束，它将前述两组约束作为特例包含在内，为成功验证可达-避免性质提供了更多可能。当所涉及的数据为多项式时，即初始集、安全集与目标集为半代数集，且系统具有多项式动力学，则求解这些约束的问题可借助平方和分解技术化为半定优化问题，从而可通过内点法在多项式时间内高效求解。最后，若干示例展示了理论进展与所提方法的性能。