TY - GEN

T1 - Foundations for circular compositional reasoning

AU - Viswanathan, Mahesh

AU - Viswanathan, Ramesh

PY - 2001

Y1 - 2001

N2 - 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].

AB - 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].

UR - http://www.scopus.com/inward/record.url?scp=84879521374&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84879521374&partnerID=8YFLogxK

U2 - 10.1007/3-540-48224-5_68

DO - 10.1007/3-540-48224-5_68

M3 - Conference contribution

AN - SCOPUS:84879521374

SN - 3540422870

SN - 9783540422877

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 835

EP - 847

BT - Automata, Languages and Programming - 28th International Colloquium, ICALP 2001, Proceedings

A2 - Orejas, Fernando

A2 - Spirakis, Paul G.

A2 - van Leeuwen, Jan

PB - Springer

T2 - 28th International Colloquium on Automata, Languages and Programming, ICALP 2001

Y2 - 8 July 2001 through 12 July 2001

ER -