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

Abstract—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 I O. 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 ...

• Type: Journal
• Year: 2015
• Where: ACSD
• Authors: Antti Tapani Siirtola, Stavros Tripakis, Keijo Heljanko
• Keywords: ACSD 2015, Hardware