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）等强大的判定过程结合时，障碍证书能够为安全性提供自动演绎验证方法。为反驳 omega-正则规范，障碍证书方法通过分离 omega-自动机的连续转移以试图否定所有接受运行，从而得到扩展。不出所料，此类策略必然具有保守性，因为对递归性质的反驳需要推理转移关系传递闭包的良基性。本文提出闭包证书（closure certificates）的概念，将其作为障碍证书从状态不变量到转移不变量的自然推广。我们给出了基于SOS与SMT的自动化搜索闭包证书的形式化方法，并通过一个典型案例研究验证了其有效性。