A set-theoretic framework for assume-guarantee reasoning

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 assumeguarantee 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. © 2011 Springer-Verlag Berlin Heidelberg.