Conservative Approximations of Hybrid Systems

Andrew K. Martin and Carl-Johan Seger
Publishing date
October 1994
29 pages
Systems that are modeled using both continuous and discrete mathematics are commonly called hybrid systems. Although much work has been done to develop frameworks in which both types of systems can be modeled at the same time, this is often a very difficult task. Verifying that desired properties hold in such hybrid models is even more daunting. In this paper we attack the problem from a different direction. First we make a distinction between two models of the system. A detailed model is developed as accurately as possible. Ultimately, one must trust in its correctness. An abstract model, which is typically less detailed, is actually used to verify properties of the system. The detailed model is typically defined in terms of both continuous and discrete mathematics, whereas the abstract one is typically discrete. We formally define the concept of conservative approximation, a relationship between models, that holds with respect to a translation between specification languages. We then progress by developing a theory that allows us to build a complicated detailed model by combining simple primitives. Simultaneously, we build a conservative approximation by similarly combining pre-defined parameterized approximations of those primitives.