Abstract patterns of compositional reasoning

Abstract

Compositional Reasoning - reducing reasoning about a concurrent system to reasoning about its individual components - is an essential tool for managing proof complexity and state explosion in model checking. Typically, such reasoning is carried out in an assume-guarantee manner: each component guarantees its behavior based on assumptions about the behavior of other components. Restrictions imposed on such methods to avoid unsoundness usually also result in incompleteness - i.e., one is unable to prove certain properties. In this paper, we construct an abstract framework for reasoning about process composition, formulate an assume-guarantee method, and show that it is sound and semantically complete. We then show how to instantiate the framework for several common notions of process behavior and composition. For these notions, the instantiations result in the first methods known to be complete for mutually inductive, assume-guarantee reasoning. © Springer-Verlag Berlin Heidelberg 2003.