Abstractions for Hybrid Systems
We present a procedure for constructing sound finite-state
discrete abstractions of hybrid systems. This procedure uses
ideas from predicate abstraction to abstract the discrete
dynamics and qualitative reasoning to abstract the continuous
dynamics of the hybrid system. It relies on the ability to
decide satisfiability of quantifier-free formulas in some theory
rich enough to encode the hybrid system.
We characterize the sets of predicates that can be used to create
high quality abstractions and
we present new approaches to discover such useful sets of predicates.
Under certain assumptions, the abstraction procedure can be applied
compositionally to abstract a hybrid system described as a composition
of two hybrid automata.
We show that the constructed abstractions are always sound, but
are relatively complete only under certain assumptions.
title = "Abstractions for hybrid systems",
author = "Tiwari, A.",
journal = "Formal Methods in Systems Design",
year = 2008,
volume = 32,
pages = "57--83",
publisher = "Springer",
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page