CMU-CS-14-122
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-14-122

Invariance of Conjunctions of Polynomial Equalities
for Algebraic Differential Equations

Khalil Ghorbal, Andrew Sogokon, André Platzer

July 2014

CMU-CS-14-122.pdf


To appear in the
Proceedings of the 21st International Static Analysis Symposium (SCS 2014),
11-13 September 2014, Munich, Germany.


Keywords: Algebraic invariant, high-order Lie derivation, differential equation, automated checking, proof rules, continuous dynamics, formal verification

In this paper we seek to provide greater automation for formal deductive verification tools working with continuous and hybrid dynamical systems. We present an efficient procedure to check invariance of conjunctions of polynomial equalities under the flow of polynomial ordinary differential equations. The procedure is based on a necessary and sufficient condition that characterizes invariant conjunctions of polynomial equalities. We contrast this approach to an alternative one which combines fast and sufficient (but not necessary) conditions using differential cuts for soundly restricting the system evolution domain.

37 pages

*University of Edinburgh, LFCS, School of Informatics, Edinburgh, Scotland

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu