When do we not need complex assume-guarantee rules?

Antti Siirtola, Stavros Tripakis, Keijo Heljanko

Research output: Contribution to journalArticleScientificpeer-review


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
JournalACM Transactions on Embedded Computing Systems
Issue number2
Pages (from-to)1-25
Publication statusPublished - 2017
Externally publishedYes
MoE publication typeA1 Journal article-refereed

Fields of Science

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

Cite this