A barrier certificate, defined over the states of a dynamical system, is a real-valued function whose zero level set characterizes an inductively verifiable state invariant separating reachable states from unsafe ones. When combined with powerful decision procedures such as sum-of-squares programming (SOS) or satisfiability-modulo-theory solvers (SMT) barrier certificates enable an automated deductive verification approach to safety. The barrier certificate approach has been extended to refute omega-regular specifications by separating consecutive transitions of omega-automata in the hope of denying all accepting runs. Unsurprisingly, such tactics are bound to be conservative as refutation of recurrence properties requires reasoning about the well-foundedness of the transitive closure of the transition relation. This paper introduces the notion of closure certificates as a natural extension of barrier certificates from state invariants to transition invariants. We provide SOS and SMT based characterization for automating the search of closure certificates and demonstrate their effectiveness via a paradigmatic case study.

翻译：摘要：定义在动力系统状态空间上的障碍证书是一种实值函数，其零水平集刻画了一个可归纳验证的状态不变量，将可达状态与不安全状态分离开来。当与平方和规划或可满足性模理论求解器等强大判定过程结合时，障碍证书能够实现安全性的自动化演绎验证方法。通过分离ω自动机的连续转移以否定所有接受路径，障碍证书方法已被扩展用于反驳ω-正则规范。然而，这种策略必然具有保守性，因为反驳循环性质需要关于转移关系传递闭包的良基性推理。本文提出闭包证书的概念，将其作为从状态不变量到转移不变量的自然拓展。我们给出了基于SOS和SMT的自动化闭包证书搜索方法，并通过一个典型案例研究验证了其有效性。