Compositional Reasoning --- reducing reasoning about a concurrent system to reasoning about its individual components --- is an essential tool for managing 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 may also result in incompleteness --- that is, one is unable to prove certain properties. We construct a general 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 common notions of process behavior and composition. For these notions, the instantiations result in complete, mutually inductive, assume-guarantee reasoning methods.
Joint work with Nina Amla, E. Allen Emerson, and Kedar Namjoshi.