Differential Invariants for Differential Equations

Table of Contents
  1. Overview
  2. Differential Invariants
  3. Differential Variants
  4. Differential Cuts
  5. Differential Ghosts
  6. Differential Equation Axiomatization
  7. Differential Radical Invariants
  8. Selected Publications
DownloadKeYmaera or
KeYmaera X or
Source

Overview

Differential invariants [1,4,5,13,21] provide induction principles for differential equations. They can be understood as the differential analogue of induction techniques but for differential equations rather than for discrete systems [11]. Discrete induction is used to prove a property of a loop by proving that the invariant is true initially and then that it is preserved every time the loop body executes once. Similarly, a differential invariant is proved to hold always after a differential equation by proving that it holds initially and by proving that it is preserved in the direction of the dynamics of the differential equation. Differential invariants can prove properties of differential equations without having to solve the equations, which makes them computationally attractive.

Differential Invariants

Differential invariants [1,4] define an induction principle for differential equations [11,21]. They make it possible to prove properties of differential equations without having to solve the equations. Differential invariants are formulas that remain true along the dynamics of the hybrid system and its differential equations. The central property of differential invariants for verification purposes is that they replace infeasible or impossible reachability analysis with feasible symbolic computation. Differential invariants are computationally attractive concepts, because their inductive conditions are formed by differentials or Lie derivatives, giving decidable first-order real arithmetic.

Differential invariants have been studied in a number of results [1,13,14,11,18,20,7,21]. Together with the other invariant principles for differential equations explained below, they make differential equation invariants decidable [23].

Differential invariants (and their companions below) have been implemented in the KeYmaera theorem prover, its successor KeYmaera X, in Isabelle/HOL, and the Coq proof assistant.

Differential Variants

The dual verification technique of differential variants can be used to prove liveness and progress properties of differential equations without having to solve them. Differential variants [1] are implemented in KeYmaera.

Differential Cuts

Differential cuts [1,4,13,21] allow the use of lemmas that have been proved for differential equations. Differential cuts work as follows. They first prove that a differential equation never leaves region C and then restrict the dynamics of the system to C. Restricting the dynamics of a system to a subregion C usually changes the behavior of the system, except that the first proof already showed a lemma that the system cannot leave region C anyhow, so that the restriction of the dynamics to C turns out to be a pseudo-restriction that does not change the actual dynamics even if it changes the description.

Illustration of differential cut that cuts a provably unreachable region from the state space

The no differential cut elimination theorem [13] has been proved, which implies that differential cuts cannot be eliminated but fundamentally add to the deductive power. Sometimes you crucially need to exploit differential cuts to be able to verify.

Differential Ghosts

Ghost variables (or auxiliary variables) are extra variables that remember intermediate states, which can be useful for proving properties of conventional discrete programs. Differential ghosts [13,21] are the differential counterpart. What differential ghosts do is that they introduce extra variables into extra dimensions of the system, which can further evolve according to extra differential equations that are made up solely for the purposes of the proof.

Illustration of differential ghost adding an auxiliary variable into the differential equation

Differential Equation Axiomatization

By crucially exploiting differential ghosts, it has been shown that invariance properties of differential equations are decidable [23] just by conducting a corresponding proof/disproof from these axiomatic reasoning principles for differential equations.
Illustration of vector field and invariant regions of a differential equation along with an illustration of the geometric intuition behind differential equation axiomatizations from LICS'18

We prove the completeness of an axiomatization for differential equation invariants. First, differential equation axioms in differential dynamic logic are shown to be complete for all algebraic invariants. The 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 enables its analysis.

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, the results are purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.

[23]

Differential Radical Invariants

A generalization of differential invariants to higher-order derivatives, called differential radical invariants, gives a decision procedure for algebraic invariants of algebraic differential equations. Differential radical invariants decide equational invariants p=0 for polynomials p. Differential radical invariants [16] are implemented in KeYmaera.

Differential Radical Invariants
Differential radical invariants also give rise to an efficient procedure for generating algebraic invariants for algebraic differential equations based on fast symbolic linear algebra [16].

Selected Publications

The canonical reference on differential invariants is the article in the Journal of Logic and Computation [1] that appeared in 2008. Differential invariants were later used for a fixpoint procedure that computes differential invariants and verifies some interesting hybrid systems automatically , which appeared at CAV'08 [3] and in a special issue of FMSD for selected CAV papers [5]. An elegant axiomatic formulation of differential invariants, differential cuts, and differential ghosts has been reported at CADE'15 [19] and JAR [21], which was subsequently exploited for a differential equation axiomatization at LICS'18 [23]. Also see publications on differential invariants and the publication reading guide.
  1. André Platzer and Yong Kiam Tan.
    Differential equation axiomatization:
       The impressive power of differential ghosts.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018. © The authors
    [bib | pdf | doi | arXiv | abstract]

  2. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | doi | book | web | abstract]

  3. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning, 59(2), pp. 219-265, 2017. © The author
    [bib | pdf | doi | arXiv | abstract]

  4. Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer.
    A method for invariant generation for polynomial continuous systems.
    In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 17-19, 2016, Proceedings, volume 9583 of LNCS, pp. 268-288. Springer, 2016. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  5. André Platzer.
    A uniform substitution calculus for differential dynamic logic.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467-481. Springer, 2015. © Springer-Verlag
    [bib | pdf | doi | slides | arXiv | abstract]

  6. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    A hierarchy of proof rules for checking differential invariance of algebraic sets.
    In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015, Proceedings, volume 8931 of LNCS, pp. 431-448. Springer, 2015. © Springer-Verlag
    [bib | pdf | doi | slides | study | ComLan'17 | abstract]

  7. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    Invariance of conjunctions of polynomial equalities for algebraic differential equations.
    In Markus Müller-Olm and Helmut Seidl, editors, 21st International Static Analysis Symposium, SAS 2014, volume 8723 of LNCS, pp. 151-167. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  8. Khalil Ghorbal and André Platzer.
    Characterizing algebraic invariants by differential radical invariants.
    In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp. 279-294. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  9. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv:1205.4788, May 2012.
    [bib | pdf | arXiv | abstract]

  10. André Platzer.
    A differential operator approach to equational differential invariants.
    In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 28-48. Springer, 2012. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  11. André Platzer.
    The structure of differential invariants and differential cut elimination.
    Logical Methods in Computer Science, 8(4), pp. 1-38, 2012. © The author
    [bib | pdf | doi | eprint | arXiv | abstract]

  12. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | pdf | doi | slides | abstract]

  13. André Platzer.
    The complete proof theory of hybrid systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541-550. IEEE 2012. © IEEE
    [bib | pdf | doi | slides | TR | abstract]

  14. André Platzer.
    The Complete Proof Theory of Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-144, November 2011.
    [bib | pdf | LICS'12]

  15. André Platzer.
    Logic and compositional verification of hybrid systems.
    In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pp. 28-43. Springer, 2011. © Springer-Verlag
    Invited tutorial.
    [bib | pdf | doi | slides | abstract]

  16. André Platzer.
    Quantified differential invariants.
    In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
    [bib | pdf | doi | slides | abstract]

  17. André Platzer.
    Logical Analysis of Hybrid Systems:
       Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 pages. ISBN 978-3-642-14508-7.
    [bib | doi | book | web | abstract]

  18. André Platzer and Edmund M. Clarke.
    Formal verification of curved flight collision avoidance maneuvers: A case study.
    In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547-562. Springer, 2009. © Springer-Verlag
    This paper was awarded the FM Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

  19. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    Formal Methods in System Design, 35(1), pp. 98-120, 2009.
    Special issue for selected papers from CAV'08. © Springer-Verlag
    [bib | pdf | doi | study | CAV'08 | abstract]

  20. André Platzer.
    Differential Dynamic Logics:
       Automated Theorem Proving for Hybrid Systems.
    PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
    ACM Doctoral Dissertation Honorable Mention Award in 2009.
    Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
    [bib | pdf | slides | book | eprint | ebook | abstract]

  21. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176-189, Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | FMSD'09 | abstract]

  22. André Platzer and Edmund M. Clarke.
    Computing Differential Invariants of Hybrid Systems as Fixedpoints.
    School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
    [bib | pdf | CAV'08]

  23. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pp. 309-352, 2010.
    Special issue for selected papers from TABLEAUX'07. © The author.
    [bib | pdf | doi | study | abstract]

For full details, please see my List of Publications.

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.