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.

翻译：闭包证书（barrier certificate）定义在动力学系统状态空间上，是一种实值函数，其零水平集刻画了从可达状态到不安全状态的可归纳验证状态不变量。当与平方和规划（SOS）或可满足性模理论求解器（SMT）等强大判定程序结合时，闭包证书为安全性提供了自动化演绎验证方法。通过分离ω自动机连续转移以否定所有接收运行，闭包证书方法已扩展至反驳ω正则规约。不意外的是，此类策略必然具有保守性，因为对递归性质的证伪需要推理转移关系传递闭包的良基性。本文提出闭包证书的概念，作为从状态不变量到转移不变量的自然推广。我们基于SOS和SMT给出自动化搜索闭包证书的刻划方法，并通过典型实例验证其有效性。