t-Barrier Certificates: A Continuous Analogy to k-Induction

Safety proofs of discrete and continuous systems often use related proof approaches, and insight can be obtained by comparing reasoning methods across domains. For example, proofs using inductive invariants in discrete systems are analogous to barrier certificate methods in continuous systems. In this paper, we present and prove the soundness of continuous and hybrid analogs to the k-induction proof rule, which we call t-barrier certificates. The method combines symbolic reasoning and time-bounded reachability along the barrier in order to prove system safety. Compared with traditional barrier certificates, a larger class of functions can be shown to be t-barrier certificates, so we expect them to be easier to find. Compared with traditional reachability analysis, t-barrier certificates can be computationally tractable in nonlinear settings despite large initial sets, and they prove time-unbounded safety. We demonstrate the feasibility of the approach with a nonlinear harmonic oscillator example, using sympy and Z3 for symbolic reasoning and Flow⁎ for reachability analysis.