Generating Polynomial Invariants for Hybrid Systems

Enric Rodriguez-Carbonell and Ashish Tiwari

To be presented at HSCC 2005, Swiss Federal Institute of Technology (ETH) Zurich, Switzerland March 9-11, 2005. © Springer-Verlag. The final version will appear at the Springer LNCS proceedings site or the Springer LNCS site.

Abstract

We present a powerful computational method for automatically generating polynomial invariants of hybrid systems with linear continuous dynamics. When restricted to linear continuous dynamical systems, our method generates a set of polynomial equations (algebraic set) that is the best such over-approximation of the reach set. This shows that the set of algebraic invariants of a linear system is computable. The extension to hybrid systems is achieved using the abstract interpretation framework over the lattice defined by algebraic sets. Algebraic sets are represented using canonical Groebner bases and the lattice operations are effectively computed via appropriate Groebner basis manipulations.

postscript or pdf or Springer link to the paper.

Slides

Slides of the presentation at HSCC'05 may be put up here later ...

BibTeX Entry


@inproceedings{CarbonellTiwari05:HSCC,
	author = "E. Rodriguez-Carbonell and A. Tiwari",
	title = "Generating polynomial invariants for hybrid systems",
	booktitle = "Hybrid Systems: Computation and Control, HSCC 2005",
	EDITOR = "Morari, M. and Thiele, L.",
	pages = "590--605",
	series = {LNCS},
	volume = 3414,
	PUBLISHER = {Springer},
	MONTH = mar,
	YEAR = 2005
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page