{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,8]],"date-time":"2026-09-08T12:49:14Z","timestamp":1788871754317,"version":"build-2803163510"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2010,5,1]],"date-time":"2010-05-01T00:00:00Z","timestamp":1272672000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-0341658"],"award-info":[{"award-number":["CCR-0341658"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2010,5]]},"abstract":"<jats:p>\n                    Hardware systems and reactive software systems can be described as the composition of several concurrently active processes. Automated reasoning based on model checking algorithms can substantially increase confidence in the overall reliability of a system. Direct methods for model checking a concurrent composition, however, usually suffer from the explosion in the number of program states that arises from concurrency. Reasoning compositionally about individual processes helps mitigate this problem. A number of rules have been proposed for compositional reasoning, typically based on an assume-guarantee reasoning paradigm. Reasoning with these rules can be delicate, as some are syntactically circular in nature, in that assumptions and guarantees are mutually dependent. This is known to be a source of unsoundness. In this article, we investigate rules for compositional reasoning from the viewpoint of\n                    <jats:italic>completeness<\/jats:italic>\n                    . We show that several rules are incomplete: that is, there are properties whose validity cannot be established using (only) these rules. We derive a new, circular, reasoning rule and show it to be sound and complete. We show that the auxiliary assertions needed for completeness need be defined only on the interface of the component processes. We also show that the two main paradigms of circular and noncircular reasoning are closely related, in that a proof of one type can be transformed in a straightforward manner to one of the other type. These results give some insight into the applicability of compositional reasoning methods.\n                  <\/jats:p>","DOI":"10.1145\/1740582.1740584","type":"journal-article","created":{"date-parts":[[2010,5,18]],"date-time":"2010-05-18T09:46:22Z","timestamp":1274175982000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["On the completeness of compositional reasoning methods"],"prefix":"10.1145","volume":"11","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[{"name":"Bell Laboratories, Murray Hill, NJ"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, ON, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2010,5,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of IEEE LICS. 207--218","author":"Alur R.","unstructured":"Alur , R. and Henzinger , T . 1996. Reactive modules . In Proceedings of IEEE LICS. 207--218 . Alur, R. and Henzinger, T. 1996. Reactive modules. In Proceedings of IEEE LICS. 207--218."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_52"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 2001 European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems.","author":"Amla N.","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R. J . 2001. Assume-guarantee based compositional reasoning for synchronous timing diagrams . In Proceedings of the 2001 European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems. Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. J. 2001. Assume-guarantee based compositional reasoning for synchronous timing diagrams. In Proceedings of the 2001 European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the IFIP TC6 WG 6.1 Joint International Conference on Formal Techniques for Networked and Distributed Systems.","author":"Amla N.","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R. J . 2002. Visual specifications for modular reasoning about asynchronous systems . In Proceedings of the IFIP TC6 WG 6.1 Joint International Conference on Formal Techniques for Networked and Distributed Systems. Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. J. 2002. Visual specifications for modular reasoning about asynchronous systems. In Proceedings of the IFIP TC6 WG 6.1 Joint International Conference on Formal Techniques for Networked and Distributed Systems."},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 14th International Conference on Concurrency Theory (CONCUR).","author":"Amla N.","unstructured":"Amla , N. , Emerson , E. A. , Namjoshi , K. S. , and Trefler , R. J . 2003. Abstract patterns of compositional reasoning . In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR). Amla, N., Emerson, E. A., Namjoshi, K. S., and Trefler, R. J. 2003. Abstract patterns of compositional reasoning. In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR)."},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the Second Workshop on Specification and Verification of Component-Based Systems.","author":"Barringer H.","unstructured":"Barringer , H. , Giannakopoulou , D. , and P\u0103s\u0103reanu , C . 2003. Proof rules for automated compositional verification through learning . In Proceedings of the Second Workshop on Specification and Verification of Component-Based Systems. Barringer, H., Giannakopoulou, D., and P\u0103s\u0103reanu, C. 2003. Proof rules for automated compositional verification through learning. In Proceedings of the Second Workshop on Specification and Verification of Component-Based Systems."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1123058.1123060"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_51"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2006.8"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the Workshop on Logics of Programs.","author":"Clarke E.","unstructured":"Clarke , E. and Emerson , E. A . 1981. Design and synthesis of synchronization skeletons using branching time temporal logic . In Proceedings of the Workshop on Logics of Programs. Clarke, E. and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of the Workshop on Logics of Programs."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77387"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems.","author":"Cobleigh J. M.","unstructured":"Cobleigh , J. M. , Giannakopoulou , D. , and P\u0103s\u0103reanu , C. S . 2003. Learning assumptions for compositional verification . In Proceedings of the European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems. Cobleigh, J. M., Giannakopoulou, D., and P\u0103s\u0103reanu, C. S. 2003. Learning assumptions for compositional verification. In Proceedings of the European Joint Conferences on Theory and Practice of Software, Tools and Algorithms for the Construction and Analysis of Systems."},{"key":"e_1_2_1_15_1","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods","author":"de Roever W.-P.","year":"2001","unstructured":"de Roever , W.-P. , de Boer , F. , Hannemann , U. , Hooman , J. , Lakhnech , Y. , Poel , M. , and Zwiers , J . 2001 . Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods . Cambridge University Press , Cambridge, U.K. de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., and Zwiers, J. 2001. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, Cambridge, U.K."},{"key":"e_1_2_1_16_1","volume-title":"Eds","author":"de Roever W.-P.","year":"1997","unstructured":"de Roever , W.-P. , Langmaack , H. , and Pnueli , A. , Eds . 1997 . Compositionality : The Significant Difference. Lecture Notes in Computer Science, vol. 1536 . Springer , Berlin, Germany. de Roever, W.-P., Langmaack, H., and Pnueli, A., Eds. 1997. Compositionality: The Significant Difference. Lecture Notes in Computer Science, vol. 1536. Springer, Berlin, Germany."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of ICALP 280--289","author":"Josko B.","year":"1987","unstructured":"Josko , B. 1987 . Model checking of CTL formulae under liveness assumptions . In Proceedings of ICALP 280--289 . Josko, B. 1987. Model checking of CTL formulae under liveness assumptions. In Proceedings of ICALP 280--289."},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Control and Information Sciences","volume-title":"Discrete Event Systems: Models and Applications","author":"Kurshan R.","unstructured":"Kurshan , R. 1988. Reducibility in analysis of coordination . In Discrete Event Systems: Models and Applications . Lecture Notes in Control and Information Sciences , vol. 103 . Springer , Berlin, Germany , 19--39. Kurshan, R. 1988. Reducibility in analysis of coordination. In Discrete Event Systems: Models and Applications. Lecture Notes in Control and Information Sciences, vol. 103. Springer, Berlin, Germany, 19--39."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the Conference on Logics of Programs.","author":"Lichtenstein O.","unstructured":"Lichtenstein , O. , Pnueli , A. , and Zuck , L . 1985. The glory of the past . In Proceedings of the Conference on Logics of Programs. Lichtenstein, O., Pnueli, A., and Zuck, L. 1985. The glory of the past. In Proceedings of the Conference on Logics of Programs."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag Berlin Germany.   Manna Z. and Pnueli A. 1995. Temporal Verification of Reactive Systems: Safety. Springer-Verlag Berlin Germany.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733598"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647767.733764"},{"key":"e_1_2_1_28_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods","author":"McMillan K.","unstructured":"McMillan , K. 1999. Circular compositional reasoning about liveness . In Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods . Lecture Notes in Computer Science , vol. 1703 . Springer, Berlin , Germany , 342--345. McMillan, K. 1999. Circular compositional reasoning about liveness. In Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science, vol. 1703. Springer, Berlin, Germany, 342--345."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02311231"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Pnueli A. 1985. In transition from global to modular reasoning about programs. In Logics and Models of Concurrent Systems. NATO ASI Series. NATO Brussels Belgium.   Pnueli A. 1985. In transition from global to modular reasoning about programs. In Logics and Models of Concurrent Systems. NATO ASI Series. NATO Brussels Belgium.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_1_35_1","volume-title":"Proceedings of the 5th International Symposium on Programming.","author":"Queille J.","unstructured":"Queille , J. and Sifakis , J . 1982. Specification and verification of concurrent systems in CESAR . In Proceedings of the 5th International Symposium on Programming. Queille, J. and Sifakis, J. 1982. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/646823.706907"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics J. van Leeuwen ed. Elsevier Amsterdam The Netherlands and MIT Press Cambridge MA.   Thomas W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics J. van Leeuwen ed. Elsevier Amsterdam The Netherlands and MIT Press Cambridge MA.","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science.","author":"Vardi M.","unstructured":"Vardi , M. and Wolper , P . 1986. An automata-theoretic approach to automatic program verification . In Proceedings of the IEEE Symposium on Logic in Computer Science. Vardi, M. and Wolper, P. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of the IEEE Symposium on Logic in Computer Science."},{"key":"e_1_2_1_39_1","volume-title":"Concurrency and Partial Correctness","author":"Zwiers J.","unstructured":"Zwiers , J. 1989. Compositionality , Concurrency and Partial Correctness . Springer-Verlag , Berlin, Germany . Zwiers, J. 1989. Compositionality, Concurrency and Partial Correctness. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_40_1","volume-title":"Compositionality and concurrent networks: Soundness and completeness of a proof system. Tech. rep","author":"Zwiers J.","unstructured":"Zwiers , J. , de Roever , W. , and van EmdeBoas , P. 1984. Compositionality and concurrent networks: Soundness and completeness of a proof system. Tech. rep . University of Nijmegen , Nijmegen, The Netherlands. Zwiers, J., de Roever, W., and van EmdeBoas, P. 1984. Compositionality and concurrent networks: Soundness and completeness of a proof system. Tech. rep. University of Nijmegen, Nijmegen, The Netherlands."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1740582.1740584","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1740582.1740584","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:40:55Z","timestamp":1750236055000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1740582.1740584"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,5]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1145\/1740582.1740584"],"URL":"https:\/\/doi.org\/10.1145\/1740582.1740584","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,5]]},"assertion":[{"value":"2007-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-05-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}