混合系统中 LTL 公式 p Until q 的验证

本文提出了保证混合系统满足形如 p Until q（记为 $p \mathcal{U} q$）的线性时序逻辑（LTL）公式的充分条件。粗略地说，满足公式 $p \mathcal{U} q$ 意味着初始满足命题 p 的解始终保持满足该命题，直到命题 q 被满足。为了验证此类公式，我们建立了其与条件不变性（CI）、最终条件不变性（ECI）以及有限时间吸引性（FTA）等不变性概念的联系。据此，推导出了涉及混合系统数据以及适当选取类李雅普诺夫函数（如障碍函数）的充分条件。所考虑的混合系统由微分包含和差分包含给出，分别刻画了同一系统中存在的连续与离散动态。文中通过实例说明了所得结果。