微分不变式结构与微分切割消除

混合系统验证中最大的挑战是处理微分方程。由于仅对非常简单的微分方程存在可计算的解析解，因此人们提出了用于更具可扩展性验证的证明证书。然而，这些证明证书的搜索过程仍然相当临时，因为对该问题的结构理解非常不足。我们研究了微分不变式，它定义了微分方程的归纳原理，并且只需利用其微分结构即可验证其沿微分方程的不变性，而无需求解它们。我们研究了微分不变式的结构性质。为了分析证明搜索复杂度的权衡，我们识别了若干类微分不变式之间的十多种关系，并比较了它们的演绎能力。作为我们的主要结果，我们分析了微分切割的演绎能力以及带有辅助微分变量的微分不变式的演绎能力。我们反驳了微分切割消除假说，并表明与标准切割不同，微分切割是严格增强演绎能力的基本证明原理。我们还证明了，当向动力学系统添加辅助微分变量时，其演绎能力会进一步增强。