When do we not need complex assume-guarantee rules?

Research output: Contribution to journalArticleScientificpeer-review

Researchers

Research units

  • University of Oulu
  • University of California at Berkeley

Abstract

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.

Details

Original languageEnglish
Article number48
Pages (from-to)1-25
JournalACM Transactions on Embedded Computing Systems
Volume16
Issue number2
Publication statusPublished - 1 Jan 2017
MoE publication typeA1 Journal article-refereed

    Research areas

  • Circular assume-guarantee reasoning, Compositional reasoning, Cut state, Modal interface automata, Refinement checking

ID: 10515527