闭包证书

屏障证书定义于动力系统的状态之上，是一个实值函数，其零水平集刻画了一个可归纳验证的状态不变式，将可达状态与不安全状态分离。当与平方和规划（SOS）或可满足性模理论求解器（SMT）等强大决策过程结合时，屏障证书实现了一种自动化的演绎安全验证方法。屏障证书方法已被扩展以反驳ω正则规范，通过分离ω自动机的连续转移来试图否定所有接受运行。不足为奇的是，此类策略必然保守，因为递归性质的否定需要对转移关系的传递闭包的良好基性进行推理。本文引入闭包证书的概念，作为屏障证书从状态不变式到转移不变式的自然扩展。我们提供了基于SOS与SMT的刻画以自动化搜索闭包证书，并通过一个典型案例研究展示了其有效性。