Transformations for compositional verification of assumption-commitment properties

Abstract

This paper presents a transformation-based compositional verification approach for verifying assumption-commitment properties. Our approach improves the verification process by pruning the state space of the model where the assumption is violated. This exclusion is performed by transformation functions which are defined based on a new notion of edges supporting a property. Our approach applies to all computational models where an automaton syntax with locations and edges induces a transition system semantics in a consistent way which is the case for hybrid, timed, B¨uchi, and finite automata. We have successfully applied our approach to Fischer's protocol.