Help Privacy Policy Disclaimer
  Advanced SearchBrowse




Conference Paper

A Set-Theoretic Framework for Assume-Guarantee Reasoning


Maier,  Patrick
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

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

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-31E2-E
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.