On the completeness of compositional reasoning

Abstract

Several proof rules based on the assume-guarantee paradigm have been proposed for compositional reasoning about concurrent systems. Some of the rules are syntactically circular in nature, in that assumptions and guarantees appear to be circularly dependent. While these rules are sound, we show that several such rules are incomplete, i.e., there are true properties of a composition that cannot be deduced using these rules. We present a new sound and complete circular rule. We also show that circular and non-circular rules are closely related. For the circular rules defined here, proofs with circular rules can be efficiently transformed to proofs with non-circular rules and vice versa.