A Set-Theoretic Framework for Assume-Guarantee Reasoning

Patrick Maier

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

8 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages821-834
Number of pages14
DOIs
Publication statusPublished - 2001
Event28th International Colloquium on Automata, Languages and Programming - Crete, Greece
Duration: 8 Jul 200112 Jul 2001

Conference

Conference28th International Colloquium on Automata, Languages and Programming
Abbreviated titleICALP 2001
CountryGreece
CityCrete
Period8/07/0112/07/01

Keywords

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

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

Cite this