基于 BDD 的带输入线性系统安全违例的完整刻画

线性系统的控制设计工具通常涉及极点配置与计算 Lyapunov 函数，这些有助于确保稳定性。但在对控制设计有更高要求时，设计者还需满足安全性或时序逻辑规范等其他规范，而朴素的控制设计可能无法满足此类规范。控制设计者可采用模型检测作为安全检查工具，并在发生安全违例时获得反例。尽管针对线性动力学系统的安全性验证已开发出若干可扩展技术，此类工具仅作为评估系统安全性的判定过程，因此将反例作为安全违例的证据。然而这些模型检测方法并不旨在发现极端情况，或复用验证产物以用于另一亚最优安全规范。在本文中，我们描述一种用于获取线性系统安全违例反例完整刻画的技术。所提技术利用安全性验证期间针对给定时序逻辑公式计算的可达集，执行约束传播，并使用二元决策图（BDD）表示反例的所有模态。我们引入一种动态确定同构节点的方法，以获得尺寸显著缩减的决策图。在各种基准上的详尽实验评估表明，该缩减技术使节点数量减少多达 $67\%$，决策图宽度减少 $75\%$。