{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:07:12Z","timestamp":1725548832487},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540241010"},{"type":"electronic","value":"9783540317944"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31794-4_1","type":"book-chapter","created":{"date-parts":[[2010,2,28]],"date-time":"2010-02-28T19:11:12Z","timestamp":1267384272000},"page":"1-17","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Equivalences for Open Systems"],"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","reference":[{"key":"1_CR1","first-page":"160","volume-title":"Proc. 14th IEEE Computer Security Foundations Workshop","author":"M. Abadi","year":"2001","unstructured":"Abadi, M., Fiore, M.P.: Computing symbolic models for verifying cryptographic protocols. In: Proc. 14th IEEE Computer Security Foundations Workshop, pp. 160\u2013173. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/B978-044482830-9\/50021-7","volume-title":"Handbook of Process Algebra","author":"L. Aceto","year":"2001","unstructured":"Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, pp. 197\u2013292. Elsevier Science, Amsterdam (2001)"},{"issue":"6","key":"1_CR3","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/258077.258078","volume":"3","author":"R. Allen","year":"1997","unstructured":"Allen, R., Garlan, D.: A formal basis for architectural connectors. ACM Transactions on Software Engineering and Methodology\u00a03(6), 213\u2013249 (1997)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-46000-4_4","volume-title":"Coordination Models and Languages","author":"L.F. Andrade","year":"2002","unstructured":"Andrade, L.F., Fiadeiro, J.L., Gouveia, L., Koutsoukos, G., Wermelinger, M.: Coordination for orchestration. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol.\u00a02315, pp. 5\u201313. Springer, Heidelberg (2002)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-45719-4_18","volume-title":"Algebraic Methodology and Software Technology","author":"P. Baldan","year":"2002","unstructured":"Baldan, P., Bracciali, A., Bruni, R.: Bisimulation by unification. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 254\u2013270. Springer, Heidelberg (2002)"},{"key":"1_CR6","unstructured":"Baldan, P., Bracciali, A., Bruni, R.: Symbolic equivalences for open systems. Technical Report TR-03-16, Department of Computer Science, University of Pisa (2003)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/3-540-48224-5_55","volume-title":"Automata, Languages and Programming","author":"M. Boreale","year":"2001","unstructured":"Boreale, M.: Symbolic trace analysis of cryptographic protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 667\u2013681. Springer, Heidelberg (2001)"},{"key":"1_CR8","unstructured":"Caires, L.: A Model for Declarative Programming and Specification with Concurrency and Mobility. PhD thesis, Departamento de Inform\u00e1tica, Faculdade de Ci\u00eancias e Tecnologia, Universidade Nova de Lisboa (1999)"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45500-0_1","volume-title":"Theoretical Aspects of Computer Software","author":"L. Caires","year":"2001","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 1\u201337. Springer, Heidelberg (2001)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45694-5_15","volume-title":"CONCUR 2002 - Concurrency Theory","author":"L. Caires","year":"2002","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (part II). In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 209\u2013225. Springer, Heidelberg (2002)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/BFb0053547","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Cardelli","year":"1998","unstructured":"Cardelli, L., Gordon, A.D.: Mobile ambients. In: Nivat, M. (ed.) ETAPS 1998 and FOSSACS 1998. LNCS, vol.\u00a01378, pp. 140\u2013155. Springer, Heidelberg (1998)"},{"key":"1_CR12","first-page":"365","volume-title":"Proc. POPL 2000","author":"L. Cardelli","year":"2000","unstructured":"Cardelli, L., Gordon, A.D.: Anytime, anywhere. modal logics for mobile ambients. In: Proc. POPL 2000, pp. 365\u2013377. ACM, New York (2000)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Jha, S., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proc. PROCOMET 1998. Chapmann & Hall, Sydney (1998)","DOI":"10.1007\/978-0-387-35358-6_10"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., L\u00fcttgen, G.: A logical process calculus. ENTCS (2002)","DOI":"10.1016\/S1571-0661(05)80362-7"},{"key":"1_CR15","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(92)90087-V","volume":"103","author":"A. Corradini","year":"1992","unstructured":"Corradini, A., Montanari, U.: An algebraic semantics for structured transition systems and its application to logic programs. Theoret. Comput. Sci.\u00a0103, 51\u2013106 (1992)","journal-title":"Theoret. Comput. Sci."},{"issue":"5","key":"1_CR16","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1109\/32.685256","volume":"24","author":"R. Nicola De","year":"1998","unstructured":"De Nicola, R., Ferrari, G., Pugliese, R.: KLAIM: a kernel language for agents interaction and mobility. IEEE Transactions on Software Engineering\u00a024(5), 315\u2013330 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR17","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 synchronizing devices in MEIJE\u2013SCCS. Theoret. Comput. Sci.\u00a037, 245\u2013267 (1985)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/978-3-540-44616-3_25","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J.L. Fiadeiro","year":"2000","unstructured":"Fiadeiro, J.L., Maibaum, T., Mart\u00ed-Oliet, N., Meseguer, J., Pita, I.: Towards a verification logic for rewriting logic. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 438\u2013458. Springer, Heidelberg (2000)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of Security Analysis and Design","author":"R. Focardi","year":"2001","unstructured":"Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol.\u00a02171, pp. 331\u2013396. Springer, Heidelberg (2001)"},{"key":"1_CR20","doi-asserted-by":"crossref","first-page":"133","DOI":"10.7551\/mitpress\/5641.003.0010","volume-title":"Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"F. Gadducci","year":"2000","unstructured":"Gadducci, F., Montanari, U.: The tile model. In: Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 133\u2013166. MIT Press, Cambridge (2000)"},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/3-540-57182-5_39","volume-title":"Proc. MFCS 1993","author":"R. Glabbeek van","year":"1993","unstructured":"van Glabbeek, R.: A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In: MFCS 1993. LNCS, vol.\u00a0711, pp. 473\u2013484. Springer, Heidelberg (1993)"},{"key":"1_CR22","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","volume":"138","author":"M. Hennessy","year":"1995","unstructured":"Hennessy, M., Lin, H.: Symbolic bisimulations. Theoret. Comput. Sci.\u00a0138, 353\u2013389 (1995)","journal-title":"Theoret. Comput. Sci."},{"key":"1_CR23","volume-title":"On the Construction of Programs","author":"C.A.R. Hoare","year":"1980","unstructured":"Hoare, C.A.R.: A model for communicating sequential processes. In: On the Construction of Programs. Cambridge University Press, Cambridge (1980)"},{"key":"1_CR24","first-page":"203","volume-title":"Proceedings of LICS","author":"K.G. Larsen","year":"1988","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of LICS, pp. 203\u2013210. IEEE, Los Alamitos (1988)"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1007\/BFb0032056","volume-title":"Proc. ICALP 1990","author":"K.G. Larsen","year":"1990","unstructured":"Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. In: ICALP 1990. LNCS, vol.\u00a0443, pp. 526\u2013539. Springer, Heidelberg (1990)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-44618-4_19","volume-title":"CONCUR 2000 - Concurrency Theory","author":"J.J. Leifer","year":"2000","unstructured":"Leifer, J.J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 243\u2013258. Springer, Heidelberg (2000)"},{"key":"1_CR27","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/0890-5401(89)90070-9","volume":"81","author":"R. Milner","year":"1989","unstructured":"Milner, R.: A complete axiomatisation for observational congruence of finite-state behaviours. Information and Computation\u00a081, 227\u2013247 (1989)","journal-title":"Information and Computation"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Miller, D., Nadathur, G.: Higher-order logic programming. In: Handbook of Logics for Artificial Intelligence and Logic Programming, vol.\u00a05, pp. 499\u2013590. Clarendon Press, Oxford (1998)","DOI":"10.1093\/oso\/9780198537922.003.0011"},{"issue":"1","key":"1_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, J.: A calculus of mobile processes, I and II. Inform. and Comput.\u00a0100(1), 1\u201340, 41\u201377 (1992)","journal-title":"Inform. and Comput."},{"key":"1_CR30","unstructured":"Nunziato, R.: Sviluppo dell\u2019applicazione SEA per la verifica di sistemi aperti. Master Thesis, Department of Computer Science, University of Pisa (2003) (in Italian)"},{"key":"1_CR31","unstructured":"Plotkin, G.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, Computer Science Department (1981)"},{"issue":"1-2","key":"1_CR32","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1006\/inco.1999.2818","volume":"156","author":"A. Rensink","year":"2000","unstructured":"Rensink, A.: Bisimilarity of open terms. Inform. and Comput.\u00a0156(1-2), 345\u2013385 (2000)","journal-title":"Inform. and Comput."},{"key":"1_CR33","unstructured":"Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, LFCS, University of Edinburgh, CST-99-93 (also published as ECS-LFCS-93-266) (1993)"},{"key":"1_CR34","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s002360050036","volume":"33","author":"D. Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: A theory of bisimulation for the \u03c0-calculus. Acta Inform.\u00a033, 69\u201397 (1996)","journal-title":"Acta Inform."},{"key":"1_CR35","doi-asserted-by":"crossref","unstructured":"Sassone, V., Sobocinski, P.: Deriving bisimulation congruences using 2-categories. Nordic Journal of Computing\u00a010 (2002)","DOI":"10.7146\/brics.v10i1.21772"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BFb0055628","volume-title":"CONCUR \u201998 Concurrency Theory","author":"P. Sewell","year":"1998","unstructured":"Sewell, P.: From rewrite rules to bisimulation congruences. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 269\u2013284. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Global Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31794-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,24]],"date-time":"2024-03-24T09:57:54Z","timestamp":1711274274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31794-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540241010","9783540317944"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31794-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}