{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:57Z","timestamp":1761611217691,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540654933"},{"type":"electronic","value":"9783540492139"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49213-5_14","type":"book-chapter","created":{"date-parts":[[2007,12,9]],"date-time":"2007-12-09T12:03:39Z","timestamp":1197201819000},"page":"381-401","source":"Crossref","is-referenced-by-count":31,"title":["Modular Model Checking"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,5,21]]},"reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"M. Abadi and L. Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(1):73\u2013132, 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-58179-0_65","volume-title":"Proc. 6th Conf. on Computer Aided Verification","author":"A. Aziz","year":"1994","unstructured":"A. Aziz, T.R. Shiple, V. Singhal, and A.L. Sangiovanni-Vincentelli. Formula-dependent equivalence for compositional CTL model checking. In Proc. 6th Conf. on Computer Aided Verification, volume 818 of Lecture Notes in Computer Science, pages 324\u2013337, Stanford, CA, June 1994. Springer-Verlag."},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th Symposium on Logic in Computer Science, pages 428\u2013439, Philadelphia, June 1990.","DOI":"10.1109\/LICS.1990.113767"},{"issue":"2","key":"14_CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, January 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1146\/annurev.cs.02.060187.001413","volume":"2","author":"E.M. Clarke","year":"1987","unstructured":"E.M. Clarke and O. Grumberg. Research on automatic verification of finitestate concurrent systems. In Annual Review of Computer Science, volume 2, pages 269\u2013290, 1987.","journal-title":"Annual Review of Computer Science"},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/BFb0028174","volume-title":"Decade of Concurrency-Refections and Perspectives (Proceedings of REX School)","author":"E.M. Clarke","year":"1993","unstructured":"E.M. Clarke, O. Grumberg, and D. Long. Verification tools for finitestate concurrent systems. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Decade of Concurrency-Refections and Perspectives (Proceedings of REX School), volume 803 of Lecture Notes in Computer Science, pages 124\u2013175. Springer-Verlag, 1993."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In R. Parikh, editor, Proc. 4th IEEE Symposium on Logic in Computer Science, pages 353\u2013362. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"14_CR8","series-title":"Lect Notes Comput Sci","first-page":"180","volume-title":"Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop)","author":"W. Damm","year":"1989","unstructured":"W. Damm, G. D.ohmen, V. Gerstner, and B. Josko. Modular verification of Petri nets: the temporal logic approach. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop), volume 430 of Lecture Notes in Computer Science, pages 180\u2013207, Mook, The Netherlands, May\/June 1989. Springer-Verlag."},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"479","DOI":"10.1007\/3-540-56922-7_39","volume-title":"Proc. 5th Conf. on Computer Aided Verification","author":"D. Dams","year":"1993","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Generation of reduced models for checking fragments of CTL. In Proc. 5th Conf. on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 479\u2013490. Springer-Verlag, June 1993."},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and J.Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of Computer and System Sciences, 30:1\u201324, 1985.","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"14_CR11","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. Sometimes and not never revisited: On branching versus linear time. Journal of the ACM, 33(1):151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proc. 29th IEEE Symposium on Foundations of Computer Science, pages 368\u2013377, White Plains, October 1988.","DOI":"10.1109\/SFCS.1988.21949"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. In Proc. 20th ACM Symposium on Principles of Programming Languages, pages 84\u201396, New Orleans, January 1985.","DOI":"10.1145\/318593.318620"},{"key":"14_CR14","unstructured":"E.A. Emerson and C.-L. Lei. Temporal model checking under generalized fairness constraints. In Proc. 18th Hawaii International Conference on System Sciences, North Holywood, 1985. Western Periodicals Company."},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C.-L. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"14_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-54430-5_93","volume-title":"Proc. 2nd Conferance on Concurrency Theory","author":"O. Grumberg","year":"1991","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. In Proc. 2nd Conferance on Concurrency Theory, volume 527 of Lecture Notes in Computer Science, pages 250\u2013265. Springer-Verlag, 1991."},{"issue":"3","key":"14_CR17","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. ACM Trans. on Programming Languages and Systems, 16(3):843\u2013871, 1994.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"14_CR18","first-page":"321","volume-title":"Information Processing 83: Proc. IFIP 9th World Congress","author":"C.B. Jones","year":"1983","unstructured":"C.B. Jones. Specification and design of (parallel) programs. In R.E.A. Mason, editor, Information Processing 83: Proc. IFIP 9th World Congress, pages 321\u2013332. IFIP, North-Holland, 1983."},{"key":"14_CR19","series-title":"Lect Notes Comput Sci","first-page":"165","volume-title":"Temporal Logic in Specification, Proceedings","author":"B. Josko","year":"1987","unstructured":"B. Josko. MCTL-an extension of CTL for modular verification of concurrent systems. In Temporal Logic in Specification, Proceedings, volume 398 of Lecture Notes in Computer Science, pages 165\u2013187, Altrincham, UK, April 1987. Springer-Verlag."},{"key":"14_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/3-540-18088-5_23","volume-title":"Proc. 14th Colloq. on Automata, Programming, and Languages (ICALP)","author":"B. Josko","year":"1987","unstructured":"B. Josko. Model checking of CTL formulae under liveness assumptions. In Proc. 14th Colloq. on Automata, Programming, and Languages (ICALP), volume 267 of Lecture Notes in Computer Science, pages 280\u2013289. Springer-Verlag, July 1987."},{"key":"14_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"386","DOI":"10.1007\/3-540-52559-9_72","volume-title":"Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop)","author":"B. Josko","year":"1990","unstructured":"B. Josko. Verifying the correctness of AADL modules using model chekcing. In Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (Proceedings of REX Workshop), volume 430 of Lecture Notes in Computer Science, pages 386\u2013400, Mook, The Netherlands, May\/June 1989. Springer-Verlag."},{"key":"14_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-59293-8_200","volume-title":"TAPSOFT\u2019 95: Theory and Practice of Software Development","author":"B. Jonsson","year":"1995","unstructured":"B. Jonsson and Y.-K. Tsay. Assumption\/guarantee specifications in lineartime temporal logic. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, TAPSOFT\u2019 95: Theory and Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 262\u2013276, Aarhus, Denmark, May 1995. Springer-Verlag."},{"key":"14_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-60218-6_31","volume-title":"Proc. 6th Conferance on Concurrency Theory","author":"O. Kupferman","year":"1995","unstructured":"O. Kupferman and M.Y. Vardi. On the complexity of branching modular model checking. In Proc. 6th Conferance on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 408\u2013422, Philadelphia, August 1995. Springer-Verlag."},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"L. Lamport. Sometimes is sometimes \u201cnot never\u201d-on the temporal logic of programs. In Proc. 7th ACM Symposium on Principles of Programming Languages, pages 174\u2013185, January 1980.","DOI":"10.1145\/567446.567463"},{"key":"14_CR25","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"L. Lamport. Specifying concurrent program modules. ACM Trans. on Programming Languages and Systenms, 5:190\u2013222, 1983.","journal-title":"ACM Trans. on Programming Languages and Systenms"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th ACM Symposium on Principles of Programming Languages, pages 97\u2013107, New Orleans, January 1985.","DOI":"10.1145\/318593.318622"},{"key":"14_CR27","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"B. Misra","year":"1981","unstructured":"B. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Trans. on Software Engineering, 7:417\u2013426, 1981.","journal-title":"IEEE Trans. on Software Engineering"},{"key":"14_CR28","unstructured":"R. Milner. An algebraic definition of simulation between programs. In Proc. 2nd International Joint Conference onArtificial Intelligence, pages 481\u2013489. British Computer Society, September 1971."},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proc. 18th IEEE Symposium on Foundation of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR30","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13:45\u201360, 1981.","journal-title":"Theoretical Computer Science"},{"key":"14_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/BFb0027047","volume-title":"Proc. Advanced School on Current Trends in Concurrency","author":"A. Pnueli","year":"1985","unstructured":"A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In Proc. Advanced School on Current Trends in Concurrency, pages 510\u2013584, Berlin, 1985. Volume 224, LNCS, Springer-Verlag."},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"A. Pnueli. In transition from global to modular temporal reasoning about programs. In K. Apt, editor, Logics and Models of Concurrent Systems, volume F-13 of NATO Advanced Summer Institutes, pages 123\u2013144. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"14_CR33","series-title":"Lect Notes Comput Sci","first-page":"337","volume-title":"Proc. 5th International Symp. on Programming","author":"J.P. Queille","year":"1981","unstructured":"J.P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In Proc. 5th International Symp. on Programming, volume 137, pages 337\u2013351. Springer-Verlag, Lecture Notes in Computer Science, 1981."},{"key":"14_CR34","series-title":"PhD thesis","volume-title":"Complexity of automata on infinite objects","author":"S. Safra","year":"1989","unstructured":"S. Safra. Complexity of automata on infinite objects. PhD thesis, Weizmann Institute of Science, Rehovot, Israel, 1989."},{"key":"14_CR35","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal ACM, 32:733\u2013749, 1985.","journal-title":"Journal ACM"},{"key":"14_CR36","doi-asserted-by":"crossref","unstructured":"M.Y. Vardi and L. Stockmeyer. Improved upper and lower bounds for modal logics of programs. In Proc 17th ACM Symp. on Theory of Computing, pages 240\u2013251, 1985.","DOI":"10.1145\/22145.22173"},{"key":"14_CR37","unstructured":"M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. First Symposium on Logic in Computer Science, pages 322\u2013331, Cambridge, June 1986."},{"issue":"1","key":"14_CR38","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1\u201337, November 1994.","journal-title":"Information and Computation"},{"key":"14_CR39","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-51803-7_23","volume-title":"Proc. Temporal Logic in Specification","author":"P. Wolper","year":"1989","unstructured":"P. Wolper. On the relation of programs and computations to models of temporal logic. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proc. Temporal Logic in Specification, volume 398, pages 75\u2013123. Lecture Notes in Computer Science, Springer-Verlag, 1989."}],"container-title":["Lecture Notes in Computer Science","Compositionality: The Significant Difference"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49213-5_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T13:14:19Z","timestamp":1737638059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49213-5_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540654933","9783540492139"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-49213-5_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}