Approximating quotient transition systems for hybrid systems

This paper concerns the theory for computational methods to construct finite-state approximations for hybrid systems for verification and supervisory control synthesis. The theory of bisimulation is extended to the case when the reachable-state mappings can only be approximated. New results for the flow pipe approximation method for computing approximations to reachable states for continuous dynamics are also presented. A previous technique for reducing the computational burden for linear systems is extended to the affine case and the approximation error is analyzed for the general case. In the concluding section, the reader is pointed to a Web site containing a complete implementation of the techniques described in this paper