Joint work with Zhi Han and Bruce Krogh.

Abstract: The verification of hybrid systems suffers from the state explosion problem when increasing the number of composed subsystems as well as the number of continuous variables. Assume-guarantee reasoning (AGR) provides a remedy in suitable cases by splitting the analysis into several abstracted sub-problems. We extend AGR to hybrid dynamic systems that interact through continuous state variables on the basis of simulation relations for timed transition systems. This makes it possible to perform compositional reasoning that is conservative in the sense of over approximating the composed behaviors. In contrast to previous approaches that require global receptivity conditions, circularity is broken in our approach by a state-based nonblocking condition that can be checked in the course of computing the AGR simulation relations. The proposed procedures for AGR are implemented in a computational tool for the case of linear hybrid I/O automata, and the approach is illustrated with a simple example.

CV: Goran Frehse is a PhD student from the Process Control Laboratory at the Department of Biochemical and Chemical Engineering of Dortmund University, Germany. His research interests are in the compositional verification of hybrid automata and in applying simulation relations in modeling and verification. He is also interested in the optimal control of hybrid systems. He holds a diploma in Electrical Engineering and Information Technology from the University of Karlsruhe, Germany. He can be contacted on goran.frehse@gmx.de.