Conservative Approximations of Hybrid Systems?

Andrew K. Martin
Carl-Johan H. Seger
Integrated Systems Design Laboratory
University of British Columbia
Vancouver, B.C. V6T 1Z4 Canada

October 25, 1994

Abstract

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.

1 Introduction

In our research laboratory we have a computer controlled model train set consisting of about 35 feet of track, 13 computer controlled switches, three remotely controlled trains and approximately 60 position sensors. Although it was built to provide a test bed for designing mixed hardware/software systems, the train set has become a source of many challenging research questions related to hybrid systems. While some of the problems encountered are specific to our particular model train set, it is clear that others, such as old sensor data, noise, unreliable sensors and actuators are typical of other real systems as well.

One particularly challenging problem has been the development of a control system that guarantees freedom from collisions. Of course, there is a trivial solution to this task:

?This research was supported by a Killam pre-doctoral fellowship, by a postgraduate scholarship and by operating grant OGPO 109688 from the Natural Sciences and Engineering Research Council of Canada and by a fellowship from the B. C. Advanced Systems Institute.