When Do We (Not) Need Complex Assume-Guarantee Rules?

Assume-guarantee (AG) reasoning is a compositional verification method where a verification task involving many processes is broken into multiple verification tasks involving fewer and/or simpler processes. Unfortunately, AG verification rules, and especially circular rules are often complex and hence hard to reason about. This raises the question whether complex rules are really necessary, especially in view of formalisms that already enable compositional reasoning via simple rules based on precongruence. This paper investigates this question for two formalisms: (1) labelled transition systems (LTS) with parallel composition and weak simulation, and (2) interface automata (IA) with composition and alternating simulation ^>_<;O^I. In (1), not all AG rules are sound and the precongruence rule cannot replace all sound ones, but we can provide a generic and sound AG rule that complements the precongruence rule. We show that in (2) all AG rules are sound and can be replaced by a simple rule where all premisses are of the form P_i^>_<;O^I Q_t. Moreover, we show that proofs in the LTS AG rule can be converted into proofs in the simple IA rule. This suggests that circular reasoning is a built-in feature of the IA formalism, and provided system components can be modelled as IA, complex assume-guarantee rules are not needed.