@techreport{TR-IC-09-48,
   number = {IC-09-48},
   author = {Nadir Matringe and Arnaldo V. Moura and Rachid Rebiha},
   title = {Multivariate Formal Power Series Invariants Generation for
                   Non Linear Hybrid Systems},
   month = {December},
   year = {2009},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 22 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       We  present  the  first  automatic  verification  methods  that 
       automatically   generate   invariants   which   are  assertions 
       expressed  by  \emph{multivariate formal power series}. We also
       discuss  their  convergence  analysis  over hybrid systems that
       exhibit  highly  non  linear models. As far as we know, this is
       the  first  approach that can deal with this type of systems or
       that  can  automatically  generate  this type of invariants. 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 suitably represented by matrices. By
       doing  so, we reduce the invariant generation problem to linear
       algebraic  matrix  systems,  from  which  one  can provide very
       effective  methods  for  solving  the  original  problem.  Such 
       methods have much lower time complexities than other approaches
       based  on  Grobner basis computations, quantifier eliminations,
       cylindrical    algebraic   decompositions,   directly   solving  
       non-linear  systems  or  abstract  operators,  or even the more
       recent constraint-based approaches. More specifically, we bring
       necessary  and  sufficient  conditions that allow existence and
       completeness  proofs  for  our  formal  power  series invariant
       generation   methods.  We  illustrate  the  efficiency  of  our 
       computational  methods  by  dealing  with highly non linear and
       complex hybrid systems.
  }
}