@techreport{TR-IC-12-14,
number = {IC-12-14},
author = {Rachid Rebiha and Nadir Matringe and Arnaldo V. Moura},
title = {{Transcendental Inductive Invariants Generation for
Non-linear Hybrid Systems}},
month = {January},
year = {2012},
institution = {Institute of Computing, University of Campinas},
note = {In English, 27 pages.
\par\selectlanguage{english}\textbf{Abstract}
We present the first verification methods that automatically
generate bases of inequality and equality invariants expressed
by multivariate formal power series and transcendental
functions. We also discuss their convergence over hybrid
systems that exhibit non linear models and parameters. We
reduce the invariant generation problem to linear algebraic
matrix systems, from which one can provide effective methods
for solving the original problem. We show that the
preconditions for discrete transitions, the Lie-derivatives for
continuous evolution and the newly introduced relaxed
consecution requirements can be viewed as morphisms and, thus,
can be represented by matrices. More specifically, we obtain
very general sufficient conditions for the existence and the
computation of formal power series invariants over multivariate
polynomial continuous differential systems. The formal power
series invariant generated are often composed by expansion of
some well-known transcendental functions (e.g. $log$, $exp$,...
) and has an analysable closed-form facilitating the use of the
invariants to verify safety properties. Our examples with non
linear continuous evolution similar to those present today in
many critical hybrid embedded systems, show the strength of our
results and prove that some of them are beyond the limits of
other recent approaches.
}
}