André Platzer: Differential Equation Invariance Axiomatization

This talk proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis.

An extended axiomatization with existence and uniqueness axioms is complete for all local progress properties, and, with a real induction axiom, is complete for all semianalytic invariants. This parsimonious axiomatization serves as the logical foundation for reasoning about invariants of differential equations where properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case. Moreover, the approach is purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.

This talk is based on joint work with Yong Kiam Tan, LICS 2018, JACM 2020.