Automatic invariant generation for hybrid systems using ideal fixed points

We present computational techniques for automatically generating algebraic (polynomial equality) invariants for algebraic hybrid systems. Such systems involve ordinary differential equations with multivariate polynomial right-hand sides. Our approach casts the problem of generating invariants for differential equations as the greatest fixed point of a monotone operator over the lattice of ideals in a polynomial ring. We provide an algorithm to compute this monotone operator using basic ideas from commutative algebraic geometry. However, the resulting iteration sequence does not always converge to a fixed point, since the lattice of ideals over a polynomial ring does not satisfy the descending chain condition. We then present a bounded-degree relaxation based on the concept of “pseudo ideals”, due to Colón, that restricts ideal membership using multipliers with bounded degrees. We show that the monotone operator on bounded degree pseudo ideals is convergent and generates fixed ...

• Type: Conference
• Year: 2010
• Where: HYBRID
• Authors: Sriram Sankaranarayanan
• Keywords: HYBRID 2010, Hybrid Systems, Monotone Operator, Polynomial, Pseudo Ideals