Composing hybrid systems

Hybrid systems are useful abstractions of embedded controllers. However, they are notoriously very difficult to verify as computation complexity grows quickly with the size of the hybrid system. We address the problem of building in a systematic way a compact representation of a hybrid system obtained by composing hybrid subsystems. This technique can be used as a front-end to any hybrid formal verification tool thus freeing the designer from the cumbersome and error-prone manual calculation of the composition and of its reduction. Critical to the efficiency of the method are: i) hiding the internal signals and synchronization events between components; ii) eliminating locations that result in empty invariant conditions as well as non reachable locations; iii) using the notion of equivalent locations for a labeled transition system associated to the hybrid system to compute an equivalent minimal realization of the composed hybrid system.