CMU-CS-17-117Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-17-117
André Platzer, Yong Kiam Tan August 2017
Keywords:
Differential dynamic logic, algebraic and semialgebraic invariants
This report shows that differential ghosts prove all algebraic invariants of algebraic differential equations by proving that differential radical invariants derive from differential ghosts. Differential ghosts add differential equations to a differential equation system, which, if cleverly chosen, simplify proofs, because they make it possible to relate the change in the quantities of interest to additional variables that can be chosen to evolve freely. A fractional generalization of Darboux's principle for proving invariance of (polynomial) equations along polynomial differential equations is shown to derive from differential ghosts. Differential adjoints are identified as the missing link to derive a vectorial formulation of Darboux's principle from vectorial differential ghosts, from which differential radical invariants follow. These ideas are subsequently generalized from equalities to inequalities, ultimately covering proofs of all true semialgebraic invariants. 40 pages
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |