
CMUCS13129
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS13129
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),
514 April 2014, Grenoble, France.
CMUCS13129.pdf
Keywords:
Algebraic invariant, differential ideals, highorder 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 higherorder Lie derivatives. Differential radical invariants are computationally easy to check using polynomial arithmetic on higherorder 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 nontrivial algebraic invariants capturing the exact airplane behavior during takeoff or landing in longitudinal motion.
24 pages
