When do we not need complex assume-guarantee rules?

We study the need for complex circular assume-guarantee (AG) rules in formalisms that already provide the simple precongruence rule. We first investigate the question for two popular formalisms: Labeled Transition Systems (LTSs) with weak simulation and Interface Automata (IA) with alternating simulation. We observe that, in LTSs, complex circular AG rules cannot always be avoided, but, in the IA world, the simple precongruence rule is all we need. Based on these findings, we introduce modal IA with cut states, a novel formalism that not only generalizes IA and LTSs but also allows for compositional reasoning without complex AG rules.