Sciweavers

Share
HYBRID
2010
Springer

Automatic invariant generation for hybrid systems using ideal fixed points

10 years 16 days ago
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 ...
Sriram Sankaranarayanan
Added 18 May 2010
Updated 18 May 2010
Type Conference
Year 2010
Where HYBRID
Authors Sriram Sankaranarayanan
Comments (0)
books