Differential equation axiomatization. The impressive power of differential ghosts

DOI10.1145/3209108.3209147MaRDI QIDQ5145359zbMATH OpenOpenAlexFDO

Authors André Platzer, Yong Kiam Tan

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1802.01226

zbMATH Keywords

differential dynamic logicdifferential equation axiomatizationdifferential ghosts

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Hybrid systems of ordinary differential equations (34A38) Other applications of logic (03B80)

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.

Recommendations

• Differential equation invariance axiomatization
• A differential operator approach to equational differential invariants (invited paper)
• A complete uniform substitution calculus for differential dynamic logic
• An axiomatic approach to existence and liveness for differential equations
• The structure of differential invariants and differential cut elimination

Cited in

(15)

• An axiomatic approach to existence and liveness for differential equations
• Differential equation invariance axiomatization
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• Relational differential dynamic logic
• Vector barrier certificates and comparison systems
• A differential operator approach to equational differential invariants (invited paper)
• Characterizing positively invariant sets: inductive and topological methods
• On induction principles for partial orders
• Symbolic computation of differential equivalences
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Towards physical hybrid systems
• An axiomatic approach to liveness for differential equations
• Pegasus: a framework for sound continuous invariant generation
• Parallel composition and modular verification of computer controlled systems in differential dynamic logic

This page was built for publication: Differential equation axiomatization. The impressive power of differential ghosts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145359)