{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,4,8]],"date-time":"2024-04-08T07:09:58Z","timestamp":1712560198800},"reference-count":34,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2006,4,1]],"date-time":"2006-04-01T00:00:00Z","timestamp":1143849600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":2700,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2006,4]]},"DOI":"10.1016\/j.tcs.2005.11.035","type":"journal-article","created":{"date-parts":[[2005,12,20]],"date-time":"2005-12-20T15:21:35Z","timestamp":1135092095000},"page":"421-440","source":"Crossref","is-referenced-by-count":25,"title":["Compositionality of Hennessy\u2013Milner logic by structural operational semantics"],"prefix":"10.1016","volume":"354","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Rob van","family":"Glabbeek","sequence":"additional","affiliation":[]},{"given":"Paulien","family":"de Wind","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2005.11.035_bib1","series-title":"Proc. 10th Ann. IEEE Symp. Logic in Computer Science","first-page":"398","article-title":"Partial model checking","author":"Andersen","year":"1995"},{"key":"10.1016\/j.tcs.2005.11.035_bib2","series-title":"Proc. Ninth Ann. IEEE Symp. Logic in Computer Science","first-page":"144","article-title":"A compositional proof system for the modal \u03bc-calculus","author":"Andersen","year":"1994"},{"issue":"4","key":"10.1016\/j.tcs.2005.11.035_bib3","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/BF00709155","article-title":"Compositional checking of satisfaction","volume":"1","author":"Andersen","year":"1992","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/j.tcs.2005.11.035_bib4","series-title":"ACM Symp. Theory of Computing (STOC \u201984)","first-page":"51","article-title":"Now you may compose temporal logic specifications","author":"Barringer","year":"1984"},{"issue":"1","key":"10.1016\/j.tcs.2005.11.035_bib5","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/963927.963929","article-title":"Precongruence formats for decorated trace semantics","volume":"5","author":"Bloom","year":"2004","journal-title":"ACM Trans. Comput. Logic"},{"issue":"1","key":"10.1016\/j.tcs.2005.11.035_bib6","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/200836.200876","article-title":"Bisimulation can\u2019t be traced","volume":"42","author":"Bloom","year":"1995","journal-title":"J. ACM"},{"issue":"5","key":"10.1016\/j.tcs.2005.11.035_bib7","doi-asserted-by":"crossref","first-page":"863","DOI":"10.1145\/234752.234756","article-title":"The meaning of negative premises in transition system specifications","volume":"43","author":"Bol","year":"1996","journal-title":"J. ACM"},{"issue":"3","key":"10.1016\/j.tcs.2005.11.035_bib8","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","article-title":"A theory of communicating sequential processes","volume":"31","author":"Brookes","year":"1984","journal-title":"J. ACM"},{"issue":"1","key":"10.1016\/j.tcs.2005.11.035_bib9","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1996.0030","article-title":"Ntyft\/ntyxt rules reduce to ntree rules","volume":"126","author":"Fokkink","year":"1996","journal-title":"Inform. Comput."},{"key":"10.1016\/j.tcs.2005.11.035_bib10","doi-asserted-by":"crossref","unstructured":"W.J. Fokkink, R.J. van Glabbeek, P. de Wind, Compositionality of Hennessy\u2013Milner logic through structural operational semantics, in: A. Lingas, B.J. Nilsson (Eds.), 14th Internat. Symp. Fundamentals of Computation Theory (FCT \u201903), Lecture Notes in Computer Science, Vol. 2751, Springer, Berlin, 2003, pp. 412\u2013422.","DOI":"10.1007\/978-3-540-45077-1_38"},{"key":"10.1016\/j.tcs.2005.11.035_bib11","series-title":"Handbook of Process Algebra","first-page":"3","article-title":"The linear time\u2014branching time spectrum I: the semantics of concrete, sequential processes","author":"van Glabbeek","year":"2001"},{"key":"10.1016\/j.tcs.2005.11.035_bib12","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.jlap.2004.03.007","article-title":"The meaning of negative premises in transition system specifications II","volume":"60\/61","author":"van Glabbeek","year":"2004","journal-title":"J. Logic Algebraic Programming"},{"issue":"2","key":"10.1016\/j.tcs.2005.11.035_bib13","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0304-3975(93)90111-6","article-title":"Transition system specifications with negative premises","volume":"118","author":"Groote","year":"1993","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"10.1016\/j.tcs.2005.11.035_bib14","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1016\/0890-5401(92)90013-6","article-title":"Structured operational semantics and bisimulation as a congruence","volume":"100","author":"Groote","year":"1992","journal-title":"Inform. Comput."},{"issue":"2","key":"10.1016\/j.tcs.2005.11.035_bib15","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1016\/0022-0000(82)90003-4","article-title":"Process logic: expressiveness, decidability, completeness","volume":"25","author":"Harel","year":"1982","journal-title":"J. Comput. System Sci."},{"issue":"1","key":"10.1016\/j.tcs.2005.11.035_bib16","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","article-title":"Algebraic laws for non-determinism and concurrency","volume":"32","author":"Hennessy","year":"1985","journal-title":"J. ACM"},{"key":"10.1016\/j.tcs.2005.11.035_bib17","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S0019-9958(85)80025-5","article-title":"The power of the future perfect in program logics","volume":"67","author":"Hennessy","year":"1985","journal-title":"Inform. Control"},{"issue":"3","key":"10.1016\/j.tcs.2005.11.035_bib18","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.11.035_bib19","doi-asserted-by":"crossref","unstructured":"F. Laroussinie, K.G. Larsen, Compositional model checking of real time systems, in: I. Lee, S.A. Smolka (Eds.), CONCUR \u201995: Concurrency Theory, Sixth Conference, Lecture Notes in Computer Science, Vol. 962, Springer, Berlin, 1995, pp. 27\u201341.","DOI":"10.1007\/3-540-60218-6_3"},{"key":"10.1016\/j.tcs.2005.11.035_bib20","unstructured":"K.G. Larsen, Context-dependent bisimulation between processes, Ph.D. Thesis, University of Edinburgh, Edinburgh, 1986."},{"issue":"6","key":"10.1016\/j.tcs.2005.11.035_bib21","doi-asserted-by":"crossref","first-page":"761","DOI":"10.1093\/logcom\/1.6.761","article-title":"Compositionality through an operational semantics of contexts","volume":"1","author":"Larsen","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/j.tcs.2005.11.035_bib22","doi-asserted-by":"crossref","unstructured":"R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science, Vol. 92, Springer, Berlin, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"10.1016\/j.tcs.2005.11.035_bib23","doi-asserted-by":"crossref","unstructured":"R. Milner, A modal characterization of observable machine-behaviour, in: E. Astesiano, C. B\u00f6hm (Eds.), CAAP \u201981: Trees in Algebra and Programming, Sixth Colloq., Lecture Notes in Computer Science, Vol. 112, Springer, Berlin, 1981, pp. 25\u201334.","DOI":"10.1007\/3-540-10828-9_52"},{"issue":"3","key":"10.1016\/j.tcs.2005.11.035_bib24","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","article-title":"Calculi for synchrony and asynchrony","volume":"25","author":"Milner","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.11.035_bib25","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.jlap.2004.03.009","article-title":"A structural approach to operational semantics","volume":"60\/61","author":"Plotkin","year":"2004","journal-title":"J. Logic Algebraic Programming"},{"key":"10.1016\/j.tcs.2005.11.035_bib26","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","article-title":"The temporal logic of concurrent programs","volume":"13","author":"Pnueli","year":"1981","journal-title":"Theoret. Comput. Sci."},{"issue":"3","key":"10.1016\/j.tcs.2005.11.035_bib27","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","article-title":"Higher-level synchronising devices in MEIJE\u2013SCCS","volume":"37","author":"de Simone","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.11.035_bib28","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/j.jlap.2004.03.004","article-title":"Sequent calculi for process verification: Hennessy\u2013Milner logic for an arbitrary GSOS","volume":"60\/61","author":"Simpson","year":"2004","journal-title":"J. Logic Algebraic Programming"},{"issue":"1","key":"10.1016\/j.tcs.2005.11.035_bib29","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(85)90129-X","article-title":"A proof-theoretic characterization of observational equivalence","volume":"39","author":"Stirling","year":"1985","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.11.035_bib30","doi-asserted-by":"crossref","unstructured":"C. Stirling, A complete modal proof system for a subset of SCCS, in: H. Ehrig, C. Floyd, M. Nivat, J.W. Thatcher (Eds.), Mathematical Foundations of Software Development: Proc. Joint Conf. Theory and Practice of Software Development (TAPSOFT), Vol. 1: Colloq. Trees in Algebra and Programming (CAAP \u201985), Lecture Notes in Computer Science, Vol. 185, Springer, Berlin, 1985, pp. 253\u2013266.","DOI":"10.1007\/3-540-15198-2_16"},{"key":"10.1016\/j.tcs.2005.11.035_bib31","doi-asserted-by":"crossref","unstructured":"C. Stirling, A complete compositional modal proof system for a subset of CCS, in: W. Brauer (Eds.), Automata, Languages and Programming, 12th Colloq. (ICALP \u201985), Lecture Notes in Computer Science, Vol. 194, Springer, Berlin, 1985, pp. 475\u2013486.","DOI":"10.1007\/BFb0015773"},{"issue":"2\u20133","key":"10.1016\/j.tcs.2005.11.035_bib32","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","article-title":"Modal logics for communicating systems","volume":"49","author":"Stirling","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/j.tcs.2005.11.035_bib33","doi-asserted-by":"crossref","unstructured":"G. Winskel, A complete proof system for SCCS with modal assertions. Fundamenta Informaticae IX, 1986, pp. 401\u2013420.","DOI":"10.3233\/FI-1986-9403"},{"key":"10.1016\/j.tcs.2005.11.035_bib34","doi-asserted-by":"crossref","unstructured":"G. Winskel, On the compositional checking of validity (extended abstract), in: J.C.M. Baeten, J.W. Klop (Eds.), CONCUR \u201990: Theories of Concurrency: Unification and Extension, Lecture Notes in Computer Science, Vol. 458, Springer, Berlin, 1990, pp. 481\u2013501.","DOI":"10.1007\/BFb0039079"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397505008819?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397505008819?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,7,21]],"date-time":"2021-07-21T19:05:18Z","timestamp":1626894318000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397505008819"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,4]]}},"alternative-id":["S0304397505008819"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2005.11.035","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2006,4]]}}}