{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214893},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_25","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T04:26:08Z","timestamp":1187238368000},"page":"312-324","source":"Crossref","is-referenced-by-count":4,"title":["A Semantic Theory for Heterogeneous System Design"],"prefix":"10.1007","author":[{"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"issue":"1","key":"25_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. TOPLAS, 15(1):73\u2013132, 1993. See also: Conjoining Specifications, TOPLAS, 17(3):507-534, 1995.","journal-title":"TOPLAS"},{"key":"25_CR2","unstructured":"J. A. Bergstra, A. Ponse, and S.A. Smolka. Handbook of Process Algebra. Elsevier Science, 2000."},{"key":"25_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/3-540-60218-6_23","volume-title":"CONCUR\u2019 95","author":"E. Brinksma","year":"1995","unstructured":"E. Brinksma, A. Rensink, and W. Vogler. Fair testing. In CONCUR\u2019 95, volume 962 of LNCS, pages 313\u2013328. Springer-Verlag, 1995."},{"issue":"3","key":"25_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S. D. Brookes","year":"1984","unstructured":"S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. of the ACM, 31(3):560\u2013599, 1984.","journal-title":"J. of the ACM"},{"key":"25_CR5","unstructured":"E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In LICS\u2019 89, pages 353\u2013362. IEEE Computer Society Press, 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"25_CR7","unstructured":"R. Cleaveland and G. L\u00fcttgen. Model checking is refinement: Relating B\u00fcchi testing and linear-time temporal logic. Technical Report 2000\u201314, Institute for Computer Applications in Science and Engineering, March 2000."},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(84)90113-0","volume":"34","author":"R. Nicola De","year":"1983","unstructured":"R. DeNicola and M. C. B. Hennessy. Testing equivalences for processes. TCS, 34:83\u2013133, 1983.","journal-title":"TCS"},{"issue":"2","key":"25_CR9","doi-asserted-by":"publisher","first-page":"458","DOI":"10.1145\/201019.201032","volume":"42","author":"R. Nicola De","year":"1995","unstructured":"R. DeNicola and F. Vaandrager. Three logics for branching bisimulation. J. of the ACM, 42(2):458\u2013487, 1995.","journal-title":"J. of the ACM"},{"issue":"3","key":"25_CR10","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. TOPLAS, 16(3):843\u2013871, 1994.","journal-title":"TOPLAS"},{"issue":"1","key":"25_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. C. B. Hennessy","year":"1985","unstructured":"M. C. B. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. of the ACM, 32(1):137\u2013161, 1985.","journal-title":"J. of the ACM"},{"key":"25_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BFb0084793","volume-title":"CONCUR\u2019 92","author":"R. Kaivola","year":"1992","unstructured":"R. Kaivola and A. Valmari. The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In CONCUR\u2019 92, volume 630 of LNCS, pages 207\u2013221. Springer-Verlag, 1992."},{"key":"25_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Compositionality: The Significant Difference","author":"O. Kupferman","year":"1997","unstructured":"O. Kupferman and M. Y. Vardi. Modular model checking. In Compositionality: The Significant Difference, volume 1536 of LNCS. Springer-Verlag, 1997."},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"issue":"3","key":"25_CR15","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. TOPLAS, 16(3):872\u2013923, 1994.","journal-title":"TOPLAS"},{"issue":"1","key":"25_CR16","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0304-3975(93)90155-M","volume":"114","author":"K. G. Larsen","year":"1993","unstructured":"K. G. Larsen. The expressive power of implicit specifications. TCS, 114(1):119\u2013147, 1993.","journal-title":"TCS"},{"key":"25_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"The glory of the past","author":"O. Lichtenstein","year":"1985","unstructured":"O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In Workshop on Logics of Programs, volume 193 of LNCS, pages 196\u2013218. Springer-Verlag, 1985."},{"issue":"5","key":"25_CR18","first-page":"383","volume":"16","author":"M. G. Main","year":"1987","unstructured":"M. G. Main. Trace, failure and testing equivalences for communicating processes. J. of Par. Comp., 16(5):383\u2013400, 1987.","journal-title":"J. of Par. Comp."},{"key":"25_CR19","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"25_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-540-49382-2_19","volume-title":"FSTTCS\u2019 98","author":"K. N. Kumar","year":"1998","unstructured":"K. Narayan Kumar, R. Cleaveland, and S. A. Smolka. Infinite probabilistic and nonprobabilistic testing. In FSTTCS\u2019 98, volume 1530 of LNCS, pages 209\u2013220. Springer-Verlag, 1998."},{"key":"25_CR21","series-title":"Lect Notes Comput Sci","first-page":"684","volume-title":"ICALP\u2019 95","author":"V. Natarajan","year":"1995","unstructured":"V. Natarajan and R. Cleaveland. Divergence and fair testing. In ICALP\u2019 95, volume 944 of LNCS, pages 684\u2013695. Springer-Verlag, 1995."},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In FOCS\u2019 77, pages 46\u201357. IEEE Computer Society Press, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"25_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"510","DOI":"10.1007\/3-540-48320-9_35","volume-title":"CONCUR\u2019 99","author":"A. Puhakka","year":"1999","unstructured":"A. Puhakka and A. Valmari. Weakest-congruence results for livelock-preserving equivalences. In CONCUR\u2019 99, volume 1664 of LNCS, pages 510\u2013524. Springer-Verlag, 1999."},{"issue":"1","key":"25_CR24","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1006\/inco.1994.1028","volume":"110","author":"B. Steffen","year":"1994","unstructured":"B. Steffen and A. Ing\u00f3lfsd\u00f3ttir. Characteristic formulae for CCS with divergence. Inform. & Comp., 110(1):149\u2013163, 1994.","journal-title":"Inform. & Comp."},{"key":"25_CR25","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. Stirling","year":"1987","unstructured":"C. Stirling. Modal logics for communicating systems. TCS, 49:311\u2013347, 1987.","journal-title":"TCS"},{"issue":"4","key":"25_CR26","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211218","volume":"7","author":"A. Valmari","year":"1995","unstructured":"A. Valmari and M. Tiernari. Compositional failure-based semantics models for basic LOTOS. FAC, 7(4):440\u2013468, 1995.","journal-title":"FAC"},{"key":"25_CR27","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS\u2019 86, pages 332\u2013344. IEEE Computer Society Press, 1986."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T00:17:23Z","timestamp":1556756243000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}