A Set-Theoretic Framework for Assume-Guarantee Reasoning

abstract setting (of sets over a partially-ordered domain). The
rule has a mathematically concise side condition resolving the
circularity, and its soundness proof is simple. Now, in order to
establish an assume-guarantee rule in a concrete setting, all we
need to do is to is to instantiate the abstract setting and check
the side condition; we need not redo the notorious circularity
argument again. We use this framework to establish a new
assume-guarantee rule for the setting, where reactive systems are
modeled by first order Kripke structures.