On the Completeness of Compositional Reasoning

Several proof rules based on the assume-guarantee paradigm have been proposed for compositional realsoning about concurrent systems. Some of the rules are syntacticaly 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 noncircular rules are closely related. Proofs with circular rules can be efficiently transformed to proofs with noncircular rules and vice versa, for the circular rules defined here.