Series of Abstractions for Hybrid Automata

Ashish Tiwari and Gaurav Khanna

Presented at HSCC 2002, Stanford University, March 25--27 2002, Springer-Verlag. The final version will appear in LNCS 2289 and will be available at the Springer LNCS site.


We present a technique based on the use of the quantifier elimination decision procedure for real closed fields and simple theorem proving to construct a series of successively finer qualitative abstractions of hybrid automata. The resulting abstractions are always discrete transition systems which can then be used by any traditional analysis tool. The constructed abstractions are conservative and can be used to establish safety properties of the original system. Our technique works on linear and non-linear polynomial hybrid systems, that is, the guards on discrete transitions and the continuous flows in all modes can be specified using arbitrary polynomial expressions over the continuous variables. We have a prototype tool in the SAL environment which is built over the theorem prover PVS. The technique promises to scale well to large and complex hybrid systems.


Errata: On page 7, Case (a4) ... either p < 0 or p = 0 is a conjunct in psi_2; Case (c4) ... either p > 0 or p = 0 is a conjunct in psi_2.
I have corrected this in the version available on this page.


Slides of the presentation at HSCC'02 are available here in postscript format.

BibTeX Entry

	TITLE = {Series of Abstractions for Hybrid Automata},
	AUTHOR = {Tiwari, A. and Khanna, G.},
	BOOKTITLE = {Hybrid Systems: Computation and Control HSCC},
	EDITOR = "Tomlin, C. J. and Greenstreet, M. R.",
	PAGES = {465--478},
	PUBLISHER = {Springer},
	VOLUME = 2289,
	MONTH = mar,
	YEAR = 2002

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page