The Structure of Differential Invariants and Differential Cut Elimination

The biggest challenge in hybrid systems verification is the handling ofdifferential equations. Because computable closed-form solutions only exist forvery simple differential equations, proof certificates have been proposed formore scalable verification. Search procedures for these proof certificates arestill rather ad-hoc, though, because the problem structure is only understoodpoorly. We investigate differential invariants, which define an inductionprinciple for differential equations and which can be checked for invariancealong a differential equation just by using their differential structure,without having to solve them. We study the structural properties ofdifferential invariants. To analyze trade-offs for proof search complexity, weidentify more than a dozen relations between several classes of differentialinvariants and compare their deductive power. As our main results, we analyzethe deductive power of differential cuts and the deductive power ofdifferential invariants with auxiliary differential variables. We refute thedifferential cut elimination hypothesis and show that, unlike standard cuts,differential cuts are fundamental proof principles that strictly increase thedeductive power. We also prove that the deductive power increases further whenadding auxiliary differential variables to the dynamics