Series of Abstractions for Hybrid Automata
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.
Abstract
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.
pdf
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
Slides of the presentation at HSCC'02 are available here in
postscript format.
BibTeX Entry
@inproceedings{TiwariKhanna02:HSCC,
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},
SERIES = {LNCS},
VOLUME = 2289,
MONTH = mar,
YEAR = 2002
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page