{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:53:16Z","timestamp":1725558796132},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405436"},{"type":"electronic","value":"9783540450771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45077-1_38","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:53:34Z","timestamp":1277499214000},"page":"412-422","source":"Crossref","is-referenced-by-count":3,"title":["Compositionality of Hennessy-Milner Logic through Structural Operational Semantics"],"prefix":"10.1007","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Rob","family":"van Glabbeek","sequence":"additional","affiliation":[]},{"given":"Paulien","family":"de Wind","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1109\/LICS.1994.316076","volume-title":"Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science","author":"H.R. Andersen","year":"1994","unstructured":"Andersen, H.R., Stirling, C., Winskel, G.: Compositional proof system for the modal \u03bc-calculus. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 144\u2013153. IEEE Computer Society Press, Paris (1994)"},{"issue":"4","key":"38_CR2","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/BF00709155","volume":"1","author":"H.R. Andersen","year":"1992","unstructured":"Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. Formal Methods in System Design\u00a01(4), 323\u2013354 (1992)","journal-title":"Formal Methods in System Design"},{"key":"38_CR3","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1145\/800057.808665","volume-title":"ACM Symposium on Theory of Computing (STOC 1984)","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Kuiper, R., Pnueli, A.: Now you may compose temporal logic specifications. In: ACM Symposium on Theory of Computing (STOC 1984), pp. 51\u201363. ACM Press, Baltimore (1984)"},{"key":"38_CR4","doi-asserted-by":"crossref","unstructured":"Bloom, B., Fokkink, W.J., van Glabbeek, R.J.:: Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic (2003) (to appear)","DOI":"10.1145\/963927.963929"},{"issue":"5","key":"38_CR5","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1145\/234752.234756","volume":"43","author":"R. Bol","year":"1996","unstructured":"Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. Journal of the ACM\u00a043(5), 863\u2013914 (1996)","journal-title":"Journal of the ACM"},{"issue":"3","key":"38_CR6","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM\u00a031(3), 560\u2013599 (1984)","journal-title":"Journal of the ACM"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/3-540-61440-0_154","volume-title":"Automata, Languages and Programming","author":"R.J. Glabbeek van","year":"1996","unstructured":"van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol.\u00a01099, pp. 502\u2013513. Springer, Heidelberg (1996)"},{"key":"38_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044482830-9\/50019-9","volume-title":"Handbook of Process Algebra","author":"R.J. Glabbeek van","year":"2001","unstructured":"van Glabbeek, R.J.: The linear time \u2013 branching time spectrum I: The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra,\u00a0ch. 1, pp. 3\u201399. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"38_CR9","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/0304-3975(93)90111-6","volume":"118","author":"J.F. Groote","year":"1993","unstructured":"Groote, J.F.: Transition system specifications with negative premises. Theoretical Computer Science\u00a0118(2), 263\u2013299 (1993)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"38_CR10","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0022-0000(82)90003-4","volume":"25","author":"D. Harel","year":"1982","unstructured":"Harel, D., Kozen, D., Parikh, R.: Process logic: Expressiveness, decidability, completeness. Journal of Computer and System Sciences\u00a025(2), 144\u2013170 (1982)","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"38_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M.C.B. Hennessy","year":"1985","unstructured":"Hennessy, M.C.B., Milner, R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM\u00a032(1), 137\u2013161 (1985)","journal-title":"Journal of the ACM"},{"issue":"1-3","key":"38_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/S0019-9958(85)80025-5","volume":"67","author":"M.C.B. Hennessy","year":"1985","unstructured":"Hennessy, M.C.B., Stirling, C.: The power of the future perfect in program logics. Information and Control\u00a067(1-3), 23\u201352 (1985)","journal-title":"Information and Control"},{"issue":"3","key":"38_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027(3), 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"38_CR14","unstructured":"Larsen, K.G.: Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, Edinburgh (1986)"},{"issue":"6","key":"38_CR15","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1093\/logcom\/1.6.761","volume":"1","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. Journal of Logic and Computation\u00a01(6), 761\u2013795 (1991)","journal-title":"Journal of Logic and Computation"},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"38_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/3-540-10828-9_52","volume-title":"CAAP \u201981","author":"R. Milner","year":"1981","unstructured":"Milner, R.: A modal characterization of observable machine-behaviour. In: Astesiano, E., B\u00f6hm, C. (eds.) CAAP 1981. LNCS, vol.\u00a0112, pp. 25\u201334. Springer, Heidelberg (1981)"},{"issue":"3","key":"38_CR18","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science\u00a025(3), 267\u2013310 (1983)","journal-title":"Theoretical Computer Science"},{"key":"38_CR19","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (1981)"},{"key":"38_CR20","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A. Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal logic of concurrent programs. Theoretical Computer Science\u00a013, 45\u201360 (1981)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"38_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","volume":"37","author":"R. Simone De","year":"1985","unstructured":"De Simone, R.: Higher-level synchronising devices in Meije\u2013SCCS. Theoretical Computer Science\u00a037(3), 245\u2013267 (1985)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"38_CR22","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(85)90129-X","volume":"39","author":"C. Stirling","year":"1985","unstructured":"Stirling, C.: A proof-theoretic characterization of observational equivalence. Theoretical Computer Science\u00a039(1), 27\u201345 (1985)","journal-title":"Theoretical Computer Science"},{"key":"38_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/BFb0015773","volume-title":"Automata, Languages and Programming","author":"C. Stirling","year":"1985","unstructured":"Stirling, C.: A complete compositional modal proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol.\u00a0194, pp. 475\u2013486. Springer, Heidelberg (1985)"},{"key":"38_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-15198-2_16","volume-title":"Mathematical Foundations of Software Development","author":"C. Stirling","year":"1985","unstructured":"Stirling, C.: A complete modal proof system for a subset of SCCS. In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol.\u00a0185, pp. 253\u2013266. Springer, Heidelberg (1985)"},{"issue":"2-3","key":"38_CR25","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. Stirling","year":"1987","unstructured":"Stirling, C.: Modal logics for communicating systems. Theoretical Computer Science\u00a049(2-3), 311\u2013347 (1987)","journal-title":"Theoretical Computer Science"},{"key":"38_CR26","doi-asserted-by":"crossref","first-page":"401","DOI":"10.3233\/FI-1986-9403","volume":"IX","author":"G. Winskel","year":"1986","unstructured":"Winskel, G.: A complete proof system for SCCS with modal assertions. Fundamenta Informaticae\u00a0IX, 401\u2013420 (1986)","journal-title":"Fundamenta Informaticae"},{"key":"38_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/BFb0039079","volume-title":"CONCUR \u201990","author":"G. Winskel","year":"1990","unstructured":"Winskel, G.: On the compositional checking of validity (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol.\u00a0458, pp. 481\u2013501. Springer, Heidelberg (1990)"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Computation Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45077-1_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T05:36:20Z","timestamp":1635572180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45077-1_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405436","9783540450771"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45077-1_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}