{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:35Z","timestamp":1762458575482,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540441441"},{"type":"electronic","value":"9783540457190"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45719-4_18","type":"book-chapter","created":{"date-parts":[[2007,10,9]],"date-time":"2007-10-09T14:55:00Z","timestamp":1191941700000},"page":"254-270","source":"Crossref","is-referenced-by-count":6,"title":["Bisimulation by Unification*"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Bracciali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,2]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and M. P. Fiore. Computing symbolic models for verifying cryptographic protocols. In Proc. 14th IEEE Computer Security Foundations Workshop, pp. 160\u2013173. IEEE, 2001.","DOI":"10.1109\/CSFW.2001.930144"},{"issue":"3","key":"18_CR2","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/258077.258078","volume":"6","author":"R. Allen","year":"1997","unstructured":"R. Allen and D. Garlan. A Formal Basis for Architectural Connectors. ACM TOSEM, 6(3), pp. 213\u2013249, 1997.","journal-title":"ACM TOSEM"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"L. F. Andrade, J. L. Fiadeiro, J. Gouveia, G. Koutsoukos and M. Wermelinger. Coordination for Orchestration. In Coordination Models and Languages, 5th Int. Conference COORDINATION. Lect. Notes in Comput. Sci. 2315 pp. 5\u201313. Springer 2002.","DOI":"10.1007\/3-540-46000-4_4"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"F. Baader and W. Snyder. Unification theory. In Handbook of Automated Reasoning. Elsevier Science, 2000.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"M. Boreale. Symbolic trace analysis of cryptographic protocols. In Proc. ICALP\u201901, Lect. Notes in Comput. Sci. 2076, pp. 667\u2013681. Springer, 2001.","DOI":"10.1007\/3-540-48224-5_55"},{"key":"18_CR6","unstructured":"R. Bruni, D. de Frutos-Escrig, N. Mart\u00ed-Oliet, and U. Montanari. Bisimilarity congruences for open terms and term graphs via tile logic. In Proc. CONCUR 2000, Lect. Notes in Comput. Sci. 1877, pp. 259\u2013274. Springer, 2000."},{"issue":"6","key":"18_CR7","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1017\/S1471068401000035","volume":"1","author":"R. Bruni","year":"2001","unstructured":"R. Bruni, U. Montanari, and F. Rossi. An interactive semantics of logic programming. Theory and Practice of Logic Programming, 1(6):647\u2013690, 2001.","journal-title":"Theory and Practice of Logic Programming"},{"key":"18_CR8","unstructured":"L. Caires. A Model for Declarative Programming and Specification with Concurrency and Mobility. PhD thesis, Departamento de Inform\u00e1tica, Universidade Nova de Lisboa, 1999."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"L. Caires and L. Cardelli. A spatial logic for concurrency (part I). In Proc. TACS 2001, Lect. Notes in Comput. Sci. 2215, pp. 1\u201337. Springer, 2001.","DOI":"10.1007\/3-540-45500-0_1"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"L. Caires and L. Cardelli. A spatial logic for concurrency (part II). In Proc. CONCUR 2002. Lect. Notes in Comput. Sci., Springer, 2002. To appear.","DOI":"10.1007\/3-540-45694-5_15"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"L. Cardelli and A. D. Gordon. Anytime, anywhere. modal logics for mobile ambients. In Proc. POPL 2000, pp. 365\u2013377. ACM, 2000.","DOI":"10.1145\/325694.325742"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"L. Cardelli and A. D. Gordon. Mobile ambients. In Proc. FoSSaCS\u201998, Lect. Notes in Comput. Sci. 1378, pp. 140\u2013155. Springer, 1998.","DOI":"10.1007\/BFb0053547"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, S. Jha, and W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In Proc. PROCOMET\u201998. Chapmann & Hall, 1998.","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/0304-3975(85)90093-3","volume":"37","author":"R. Simone De","year":"1985","unstructured":"R. De Simone. Higher level synchronizing devices in MEIJE-SCCS. TCS, 37:245\u2013267, 1985.","journal-title":"TCS"},{"key":"18_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-540-44616-3_25","volume-title":"Towards a verification logic for rewriting logic","author":"J. L. Fiadeiro","year":"2000","unstructured":"J. L. Fiadeiro, T. Maibaum, N. Mart\u00ed-Oliet, J. Meseguer, and I. Pita. Towards a verification logic for rewriting logic. In Proc. WADT\u201999, LNCS 1827, pp. 438\u2013458. Springer, 2000."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"F. Gadducci and U. Montanari. The tile model. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000.","DOI":"10.7551\/mitpress\/5641.003.0010"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M. Hennessy","year":"1995","unstructured":"M. Hennessy and H. Lin. Symbolic bisimulations. Theoret. Comp. Sci., 138:353\u2013389, 1995.","journal-title":"Theoret. Comp. Sci."},{"issue":"3","key":"18_CR18","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/BF00243791","volume":"3","author":"A. Herold","year":"1987","unstructured":"A. Herold and J. Siekmann. Unification in abelian semi-groups. Journal of Automated Reasoning, 3(3):247\u2013283, 1987.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"K. G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts. In Proc. ICALP\u201990, Lect. Notes in Comput. Sci. 443, pp. 526\u2013539. Springer, 1990.","DOI":"10.1007\/BFb0032056"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"J. J. Leifer and R. Milner. Deriving bisimulation congruences for reactive systems. In Proc. CONCUR 2000, Lect. Notes in Comput. Sci. 1877, pp. 243\u2013258. Springer, 2000.","DOI":"10.1007\/3-540-44618-4_19"},{"key":"18_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A Calculus of Communicating Systems, LNCS 92. Springer, 1980."},{"key":"18_CR22","doi-asserted-by":"crossref","first-page":"171","DOI":"10.3233\/FI-1992-16206","volume":"16","author":"U. Montanari","year":"1992","unstructured":"U. Montanari and V. Sassone. Dynamic congruence vs. progressing bisimulation for CCS. Fundamenta Informaticae, 16:171\u2013196, 1992.","journal-title":"Fundamenta Informaticae"},{"key":"18_CR23","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Computer Science Department, 1981."},{"issue":"1","key":"18_CR24","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/inco.1999.2818","volume":"156","author":"A. Rensink","year":"2000","unstructured":"A. Rensink. Bisimilarity of open terms. Inform. and Comput., 156(1\u20132):345\u2013385, 2000.","journal-title":"Inform. and Comput."},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"P. Sewell. From rewrite rules to bisimulation congruences. In Proc. CONCUR\u201998, Lect. Notes in Comput. Sci. 1466, pp. 269\u2013284. Springer, 1998.","DOI":"10.1007\/BFb0055628"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45719-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T13:58:35Z","timestamp":1737467915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45719-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540441441","9783540457190"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45719-4_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}