@techreport{TR-IC-13-06,
number = {IC-13-06},
author = {Rachid Rebiha and Arnaldo V. Moura and Nadir Matringe},
title = {Transcendental Invariants Generation for Non-linear Hybrid
Systems},
month = {February},
year = {2013},
institution = {Institute of Computing, University of Campinas},
note = {In English, 26 pages.
\par\selectlanguage{english}\textbf{Abstract}
We present the first verification methods that automatically
generate bases of invariants expressed by multivariate formal
power series and transcendental functions. We discuss the
convergence of solutions generated over hybrid systems that
exhibit non-linear models augmented with 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 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 invariants
generated are often composed by the expansion of some
well-known transcendental functions like "log" or "exp" and
have an analysable closed-form. This facilitates their use to
verify safety properties. Moreover, we generate inequality and
equality invariants. Our examples, dealing 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.
}
}