@techreport{TR-IC-13-05,
   number = {IC-13-05},
   author = {Rachid Rebiha and Arnaldo V. Moura and Nadir Matringe},
   title = {Generating Invariants for Non-linear Hybrid Systems},
   month = {February},
   year = {2013},
   institution = {Institute of Computing, University of Campinas},
   note = {In English, 36 pages.
    \par\selectlanguage{english}\textbf{Abstract}
       We  describe  powerful  computational  techniques,  relying  on 
       linear  algebraic  methods, for generating ideals of non-linear
       invariants  of  algebraic  hybrid  systems.  We  show  that the
       preconditions  for discrete transitions and the Lie-derivatives
       for continuous evolution can be viewed as morphisms, and so can
       be  suitably represented by matrices. We reduce the non-trivial
       invariant   generation   problem  to  the  computation  of  the 
       associated   eigenspaces   by   encoding  the  new  consecution 
       requirements   as   specific   morphisms  represented  by  such 
       matrices.  More  specifically,  our  methods  are  the first to
       establish  very  general  sufficient  conditions  that show the
       existence  and  allow  the computation of invariant ideals. Our
       methods  also  embody  a  strategy  to  estimate certain degree
       bounds,  leading to the discovery of rich classes of inductive,
       i.e.  provable,  invariants. By reducing the problem to related
       linear  algebraic  manipulations we are able to address various
       deficiencies  of  other  state-of-the-art  invariant generation
       methods, including the efficient treatment of non-linear hybrid
       systems.    Our    approach   avoids   first-order   quantifier  
       elimination,   Grobner   basis  computation  or  direct  system 
       resolution,  thereby  circumventing  difficulties  met by other
       recent techniques.
  }
}