Differential Equation Axiomatization: The Impressive Power of Differential Ghosts

Abstract

We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof 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. We then show that extending the axiomatization with existence and uniqueness axioms makes it complete for all local progress properties, and further extension with a real induction axiom makes it complete for all real arithmetic invariants. This yields a parsimonious axiomatization, which serves as the logical foundation for reasoning about invariants of differential equations. Moreover, our results are purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.

arXiv commentLICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9-12, 2018, Oxford, United Kingdom, ACM ISBN 978-1-4503-5583-4/18/07

References in corpus (3)

• A Complete Uniform Substitution Calculus for Differential Dynamic Logic
• Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
• A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems

Cited by in corpus (11)

• Differential Equation Invariance Axiomatization
• Differential Equation Axiomatization: The Impressive Power of Differential Ghosts
• Parallel Composition and Modular Verification of Computer Controlled Systems in Differential Dynamic Logic
• An Axiomatic Approach to Liveness for Differential Equations
• Characterizing Positively Invariant Sets: Inductive and Topological Methods
• Uniform Substitution for Differential Refinement Logic
• Axiomatization of Compact Initial Value Problems: Open Properties
• Adaptive Shielding via Parametric Safety Proofs
• Towards Physical Hybrid Systems
• Relational Differential Dynamic Logic
• Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements