Differential Equation Invariance Axiomatization

Abstract

This article 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. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case.

arXiv commentSignificantly extended version of arXiv:1802.01226

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 (21)

• Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI
• Pegasus: Sound Continuous Invariant Generation
• Verifying Switched System Stability With Logic
• An Axiomatic Approach to Existence and Liveness for Differential Equations
• Characterizing Positively Invariant Sets: Inductive and Topological Methods
• Implicit and Explicit Proof Management in KeYmaera X
• Switched Systems as Hybrid Programs
• Deductive Stability Proofs for Ordinary Differential Equations
• Implicit Definitions with Differential Equations for KeYmaera X (System Description)
• CESAR: Control Envelope Synthesis via Angelic Refinements
• Structured Proofs for Adversarial Cyber-Physical Systems
• Uniform Substitution for Differential Refinement Logic
• Constructive Hybrid Games
• Axiomatization of Compact Initial Value Problems: Open Properties
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• A Real-Analytic Approach to Differential-Algebraic Dynamic Logic
• Differential Elimination and Algebraic Invariants of Polynomial Dynamical Systems
• Semi-Competitive Differential Game Logic
• Heterogeneous Dynamic Logic: Provability Modulo Program Theories
• Complete Robust Hybrid Systems Reachability
• A Deductive Refinement Calculus for Differential-Algebraic Programs