Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction

Assume-guarantee reasoning (AGR) is recognized as a means to counter the state explosion problem in the verification of safety properties. We propose a novel assume-guarantee rule for hybrid systems based on simulation relations. This makes it possible to perform compositional reasoning that is conservative in the sense of over-approximating the composed behaviors. The framework is formally based on hybrid input/output automata and their labeled transition system semantics. In contrast to previous approaches that require global receptivity conditions, the 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, called PHAVer, for the class of linear hybrid I/O automata, and the approach is illustrated with a simple example.