  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.
