|
CMU-CS-13-129
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-13-129
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.
CMU-CS-13-129.pdf
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
|