When do we not need complex assume-guarantee rules?

Antti Siirtola, Stavros Tripakis, Keijo Heljanko

Research output: Contribution to journalArticleScientificpeer-review

1 Citation (Scopus)

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.

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

Keywords

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

Cite this