@inproceedings{10.1007/978-3-642-54862-8_19,
    Abstract = {We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This so-called differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over real-closed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NP-hard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during take-off or landing in longitudinal motion.},
    Address = {Berlin, Heidelberg},
    Author = {Ghorbal, Khalil and Platzer, Andr{\'e}},
    BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems},
    Editor = {{\'A}brah{\'a}m, Erika and Havelund, Klaus},
    File = {Characterizing Algebraic Invariants by Differential Radical Invariants - 978-3-642-54862-8\_19.pdf},
    ISBN = {978-3-642-54862-8},
    Pages = {279--294},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Characterizing Algebraic Invariants by Differential Radical Invariants},
    Year = {2014},
    date-added = {2023-02-21 20:50:54 +0100},
    date-modified = {2023-02-21 20:50:54 +0100},
    file-2 = {Characterizing Algebraic Invariants by Differential Radical Invariants - CMU-CS-13-129.pdf},
    doi = {10.1007/978-3-642-54862-8_19}
}

@inproceedings{10.1007/978-3-642-54862-8_19, Abstract = {We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This so-called differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over real-closed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NP-hard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during take-off or landing in longitudinal motion.}, Address = {Berlin, Heidelberg}, Author = {Ghorbal, Khalil and Platzer, Andr{\'e}}, BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems}, Editor = {{\'A}brah{\'a}m, Erika and Havelund, Klaus}, File = {Characterizing Algebraic Invariants by Differential Radical Invariants - 978-3-642-54862-8_19.pdf}, ISBN = {978-3-642-54862-8}, Pages = {279--294}, Publisher = {Springer Berlin Heidelberg}, Title = {Characterizing Algebraic Invariants by Differential Radical Invariants}, Year = {2014}, date-added = {2023-02-21 20:50:54 +0100}, date-modified = {2023-02-21 20:50:54 +0100}, file-2 = {Characterizing Algebraic Invariants by Differential Radical Invariants - CMU-CS-13-129.pdf}, doi = {10.1007/978-3-642-54862-8_19} }