Computer Science Department
School of Computer Science, Carnegie Mellon University


Characterizing Algebraic Invariants by
Differential Radical Invariants

Khalil Ghorbal, André Platzer

November 2013

To appear in the
Proceedings of the 20th International Conference on
Tools and Algorithms for the Construction and Alayasis of Systems (TACAS 2014),
5-14 April 2014, Grenoble, France.


Keywords: Algebraic invariant, differential ideals, high-order Lie derivation, differential equation, automated generation, row reduction, abstraction, continuous dynamics, formal verification, hybrid system

We give a necessary and sufficient characterization of algebraic invariants of algebraic differential equations by a differential radical invariance criterion, i.e. an explicit equation on higher-order Lie derivatives. Differential radical invariants are computationally easy to check using polynomial arithmetic on higher-order Lie derivatives. The characterization makes it possible to generate invariants by solving for the coefficients in a parametrization by comparing coefficients. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation of algebraic invariants. The approach can, e.g., generate non-trivial algebraic invariants capturing the exact airplane behavior during take-off or landing in longitudinal motion.

24 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by