Foundations for circular compositional reasoning

Mahesh Viswanathan, Ramesh Viswanathan

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


Compositional proofs about systems of many components require circular reasoning principles in which properties of other components need to be assumed in proving the properties of each individual component. A number of such circular assume-guarantee rules have been proposed for different concurrency models and different forms of property specifications. In this paper, we provide a framework that unifies and extends these results. We define an assume-guarantee semantics for properties expressible as least or greatest fixed points, and a circular compositional rule that is sound with respect to this semantics. We demonstrate the utility of this general rule by applying it to trace semantics with linear temporal logic specifications, and trace tree semantics with automata refinement specifications. For traces, we derive a new assume-guarantee rule for the weakly until operator of linear temporal logic and show that previously proposed assume-guarantee rules can be seen as special instances of our rule. For trace trees, we derive a rule for parallel composition of Moore machines, and show that the rule of [7] is a special instance thus yielding an alternate proof of the results in [7].

Original languageEnglish (US)
Title of host publicationAutomata, Languages and Programming - 28th International Colloquium, ICALP 2001, Proceedings
EditorsFernando Orejas, Paul G. Spirakis, Jan van Leeuwen
Number of pages13
ISBN (Print)3540422870, 9783540422877
StatePublished - 2001
Externally publishedYes
Event28th International Colloquium on Automata, Languages and Programming, ICALP 2001 - Crete, Greece
Duration: Jul 8 2001Jul 12 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2076 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other28th International Colloquium on Automata, Languages and Programming, ICALP 2001

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Foundations for circular compositional reasoning'. Together they form a unique fingerprint.

Cite this