# Item

ITEM ACTIONSEXPORT

Released

Conference Paper

#### A Set-Theoretic Framework for Assume-Guarantee Reasoning

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Maier, P. (2001). A Set-Theoretic Framework for Assume-Guarantee Reasoning. In F. Orejas,
P. G. Spirakis, & J. van Leeuwen (*Proceedings of
the 28th International Colloquium on Automata, Languages and Programming (ICALP-2001)* (pp. 821-834). Berlin, Germany:
Springer.

Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-31E2-E

##### 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 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.