When do we not need complex assume-guarantee rules?
Research output: Contribution to journal › Article › Scientific › peer-review
- University of Oulu
- University of California at Berkeley
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.
|Journal||ACM Transactions on Embedded Computing Systems|
|Publication status||Published - 1 Jan 2017|
|MoE publication type||A1 Journal article-refereed|
- Circular assume-guarantee reasoning, Compositional reasoning, Cut state, Modal interface automata, Refinement checking