@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.
  }
}