Differential Invariants for Differential Equations

Table of Contents
  1. Overview
  2. Differential Invariants
  3. Differential Variants
  4. Differential Radical Invariants
  5. Differential Cuts
  6. Differential Ghosts
  7. Abstract
  8. Selected Publications
Download or
WebstartKeYmaera or
Source

Overview

Differential invariants [1,4,3,5,13,14,22] 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 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. They play an important role in verifying properties of advanced hybrid systems such as aircraft and robots.

Differential Invariants

Advanced verification technology for differential dynamic logics is further based on differential invariants [1,4] that have been subsequently refined to a procedure that computes differential invariants in a fixed-point loop [3,5]. Differential invariants define an induction principle for differential equations [11,22]. 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 just polynomial constraints, which are formulas of first-order real arithmetic, and are thus decidable by quantifier elimination in real-closed fields.

Several results about the theory of differential invariants can be found in the literature [1,13,14,11,19,21,7,22].

There also is an implementation of differential invariants in the KeYmaera theorem prover and its successor KeYmaera X.

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 as well.

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 have been introduced in 2014 [17] and are implemented in KeYmaera as well.

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 [17].

Differential Cuts

Differential cuts [1,4,13,22] 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 restricts the dynamics of the system to C. Restricting the dynamics of a system to a subregion C usually changes the behavior of the system around, except that the first prove 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.

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

It has been shown that there is no differential cut elimination theorem [13].

Differential Ghosts

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

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

Abstract

The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather ad-hoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze trade-offs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.

Keywords: proof theory, differential equations, differential invariants, differential cut elimination, differential dynamic logic, hybrid systems, logics of programs, real differential semialgebraic geometry

[13]

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 [20] and JAR [22]. Also see publications on differential invariants and the publication reading guide.
  1. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning, 2016. © The author
    [bib | pdf | doi | arXiv | abstract]

  2. 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 | abstract]

  3. 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]

  4. 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'16 | abstract]

  5. 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, volume 8723 of LNCS, pp. 151-167. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  6. 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 | TR | abstract]

  7. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2013.
    [bib | pdf | course | abstract]

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

  9. 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]

  10. 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]

  11. 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]

  12. 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]

  13. 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]

  14. 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]

  15. 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]

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

  17. 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]

  18. 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]

  19. 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 | eprint | book | doi | web | abstract | slides]

  20. 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]

  21. 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]

  22. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pp. 309-352, 2010. © The author
    Special issue for selected papers from TABLEAUX'07. Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

For full details, please see my List of Publications.