A Set-Theoretic Framework for Assume-Guarantee Reasoning

Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

9 Citations (Scopus)


We present a circular assume-guarantee rule in an abstract setting (of sets over a partially-ordered domain). The rule has a mathematically concise side condition. Now, in order to prove an assume-guarantee rule in a concrete setting, all we need to do is to instantiate the abstract setting and check the side condition; i.e., we need not redo the notorious circularity argument again. We use this framework to prove a new assume-guarantee rule for Kripke structures. That rule generalizes existing assume-guarantee rules for other settings such as Reactive Modules or Mealy machines.
Original languageEnglish
Title of host publicationAutomata, Languages and Programming
Subtitle of host publication28th International Colloquium, ICALP 2001; Crete, Greece, July 8–12, 2001; Proceedings
Number of pages14
Publication statusPublished - 2001
Event28th International Colloquium on Automata, Languages and Programming - Crete, Greece
Duration: 8 Jul 200112 Jul 2001


Conference28th International Colloquium on Automata, Languages and Programming
Abbreviated titleICALP 2001


  • compositional verification
  • assume-guarantee reasoning
  • Kripke structures
  • trace semantics


Dive into the research topics of 'A Set-Theoretic Framework for Assume-Guarantee Reasoning'. Together they form a unique fingerprint.

Cite this