{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:51Z","timestamp":1725574611877},"publisher-location":"Berlin, Heidelberg","reference-count":84,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253884"},{"type":"electronic","value":"9783540319825"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31982-5_1","type":"book-chapter","created":{"date-parts":[[2011,1,14]],"date-time":"2011-01-14T07:29:02Z","timestamp":1294990142000},"page":"1-24","source":"Crossref","is-referenced-by-count":5,"title":["Model Checking for Nominal Calculi"],"prefix":"10.1007","author":[{"given":"Gian Luigi","family":"Ferrari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ugo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"1_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. Inf. and Comp.\u00a0148(1), 1\u201370 (1999)","journal-title":"Inf. and Comp."},{"key":"1_CR2","series-title":"ENTCS","volume-title":"WISP","author":"G. Baldi","year":"2004","unstructured":"Baldi, G., Bracciali, A., Ferrari, G., Tuosto, E.: A Coordination-based Methodology for Security Protocol Verification. In: WISP, Bologna, Italy. ENTCS. Elsevier, Amsterdam (2004) (to appear)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"issue":"5","key":"1_CR4","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/1018203.1018205","volume":"26","author":"N. Benton","year":"2004","unstructured":"Benton, N., Cardelli, L., Fournet, C.: Modern Concurrency Abstractions for C#. TOPLAS\u00a026(5), 269\u2013304 (2004)","journal-title":"TOPLAS"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/3-540-45694-5_32","volume-title":"CONCUR 2002 - Concurrency Theory","author":"M. Boreale","year":"2002","unstructured":"Boreale, M., Buscemi, M.: A Framework for the Analysis of Security Protocols. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 483\u2013498. Springer, Heidelberg (2002)"},{"issue":"1","key":"1_CR6","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1006\/inco.1996.0032","volume":"126","author":"M. Boreale","year":"1996","unstructured":"Boreale, M., De Nicola, R.: A Symbolic Semantics for the \u03c0-calculus. Inf. and Comp.\u00a0126(1), 34\u201352 (1996)","journal-title":"Inf. and Comp."},{"key":"1_CR7","first-page":"207","volume":"54","author":"A. Bouali","year":"1994","unstructured":"Bouali, A., Gnesi, S., Larosa, S.: The Integration Project for the JACK Environment. EATCS Bull.\u00a054, 207\u2013223 (1994) Centrum voor Wiskunde en Informatica (CWI)","journal-title":"EATCS Bull"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/3-540-61474-5_98","volume-title":"Computer Aided Verification","author":"A. Bouali","year":"1996","unstructured":"Bouali, A., Ressouche, A., Roy, V., de Simone, R.: The FC2TOOLS Set. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 441\u2013445. Springer, Heidelberg (1996)"},{"key":"1_CR9","series-title":"ENTCS","volume-title":"ConCoord: International Workshop on Concurrency and Coordination","author":"A. Bracciali","year":"2001","unstructured":"Bracciali, A., Brogi, A., Ferrari, G., Tuosto, E.: Security Issues in Component Based Design. In: Montanari, U., Sassone, V. (eds.) ConCoord: International Workshop on Concurrency and Coordination, Lipari Island - Italy. ENTCS, vol.\u00a054. Elsevier, Amsterdam (2001)"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"G. Brat","year":"2003","unstructured":"Brat, G., Havelund, K., Park, S., Visser, W.: Model Checking Programs. Automated Software Engineering\u00a010(2), 203\u2013232 (2003)","journal-title":"Automated Software Engineering"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-45694-5_22","volume-title":"CONCUR 2002 - Concurrency Theory","author":"R. Bruni","year":"2002","unstructured":"Bruni, R., Laneve, C., Montanari, U.: Orchestrating Transactions in Join Calculus. In: Brim, L., Jancar, P., Kretinsky, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 321\u2013336. Springer, Heidelberg (2002)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Bruni, R., Melgratti, H., Montanari, U.: Theoretical Foundations for Compensations in Flow Composition Languages. In: POPL (2005) (to appear)","DOI":"10.1145\/1040305.1040323"},{"issue":"6","key":"1_CR13","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1017\/S1471068401000035","volume":"1","author":"R. Bruni","year":"2001","unstructured":"Bruni, R., Montanari, U., Rossi, F.: An Interactive Semantics of Logic Programming. Theory and Practice of Logic Programming\u00a01(6), 647\u2013690 (2001)","journal-title":"Theory and Practice of Logic Programming"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-24634-3_9","volume-title":"Coordination Models and Languages","author":"M. Butler","year":"2004","unstructured":"Butler, M., Ferreira, C.: An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions. In: De Nicola, R., Ferrari, G.-L., Meredith, G. (eds.) COORDINATION 2004. LNCS, vol.\u00a02949, pp. 87\u2013104. Springer, Heidelberg (2004)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Caires, L., Cardelli, L.: A Spatial Logic for Concurrency (Part I). Inf. and Comp.\u00a0186 (2003)","DOI":"10.1016\/S0890-5401(03)00137-8"},{"issue":"3","key":"1_CR16","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1016\/j.tcs.2003.10.041","volume":"322","author":"L. Caires","year":"2004","unstructured":"Caires, L., Cardelli, L.: A Spatial Logic for Concurrency II. TCS\u00a0322(3), 517\u2013565 (2004)","journal-title":"TCS"},{"issue":"2","key":"1_CR17","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.ic.2003.12.003","volume":"190","author":"G. Cattani","year":"2004","unstructured":"Cattani, G., Sewell, P.: Models for Name-Passing Processes: Interleaving and Causal (Extended Abstract). Inf. and Comp.\u00a0190(2), 136\u2013178 (2004)","journal-title":"Inf. and Comp."},{"key":"1_CR18","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"1_CR19","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Wing, J.: Formal Methods: State of the Art and Future Directions. ACM Computing Surveys\u00a028(4), 626\u2013643 (1996)","journal-title":"ACM Computing Surveys"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Clarke, S., Jha, E.M., Marrero, W.: Using State Space Exploration and a Nautural Deduction Style Message Derivation Engine to Verify Security Protocols. In: Proc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET) (1998)","DOI":"10.1007\/978-0-387-35358-6_10"},{"issue":"1","key":"1_CR21","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems. TOPLAS\u00a015(1), 36\u201372 (1993)","journal-title":"TOPLAS"},{"key":"1_CR22","first-page":"22","volume-title":"International Symposium on Agent Systems and Applications","author":"S. Conchon","year":"1999","unstructured":"Conchon, S., Le Fessant, F.: Jocaml: Mobile Agents for Objective-Caml. In: International Symposium on Agent Systems and Applications, Palm Springs, California, pp. 22\u201329 (1999)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Corina, S., Robby, J., Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: International Conference on Software Engineering, Limerick, Ireland, June 2000, pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"issue":"10","key":"1_CR24","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1145\/944217.944234","volume":"46","author":"F. Curbera","year":"2003","unstructured":"Curbera, F., Khalaf, R., Mukhi, N., Tai, S., Weerawarana, S.: The Next Step in Web Services. CACM\u00a046(10), 29\u201334 (2003)","journal-title":"CACM"},{"issue":"1","key":"1_CR25","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1996.0072","volume":"129","author":"M. Dam","year":"1996","unstructured":"Dam, M.: Model Checking Mobile Processes. Inf. and Comp.\u00a0129(1), 35\u201351 (1996)","journal-title":"Inf. and Comp."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Dam, M.: Proof Systems for \u03c0-Calculus Logics. Logic for concurrency and synchronisation, 145\u2013212 (2003)","DOI":"10.1007\/0-306-48088-3_4"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Denker, G., Millen, J.: CAPSL Integrated Protocol Environment. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (1999)","DOI":"10.1109\/DISCEX.2000.824980"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-24727-2_12","volume-title":"Foundations of Software Science and Computation Structures","author":"H. Ehrig","year":"2004","unstructured":"Ehrig, H., K\u00f6nig, B.: Deriving Bisimulation Congruences in the DPO Approach to Graph Rewriting. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 151\u2013166. Springer, Heidelberg (2004)"},{"issue":"2\u20133","key":"1_CR29","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0167-6423(90)90071-K","volume":"13","author":"J. Fernandez","year":"1990","unstructured":"Fernandez, J.: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming\u00a013(2\u20133), 219\u2013236 (1990)","journal-title":"Science of Computer Programming"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-55179-4_18","volume-title":"Computer Aided Verification","author":"J. Fernandez","year":"1992","unstructured":"Fernandez, J., Mounier, L.: On-the-fly Verification of Behavioural Equivalences and Preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol.\u00a0575, pp. 181\u2013191. Springer, Heidelberg (1992)"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0035394","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Ferrari","year":"1997","unstructured":"Ferrari, G., Ferro, G., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: An Automata Based Verification Environment for Mobile Processes. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 275\u2013289. Springer, Heidelberg (1997)"},{"issue":"4","key":"1_CR32","first-page":"1","volume":"12","author":"G. Ferrari","year":"2004","unstructured":"Ferrari, G., Gnesi, S., Montanari, U., Pistore, M.: A Model Checking Verification Environment for Mobile Processes. TOPLAS\u00a012(4), 1\u201334 (2004)","journal-title":"TOPLAS"},{"key":"1_CR33","unstructured":"Ferrari, G., Gnesi, S., Montanari, U., Raggi, R., Trentanni, G., Tuosto, E.: Verification on the WEB. In: Augusto, J., Ultes-Nitsche, U. (eds.) VVEIS, Porto, Portugal, April 2004, pp. 72\u201374. INSTICC Press (2004)"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-45931-6_10","volume-title":"Foundations of Software Science and Computation Structures","author":"G. Ferrari","year":"2002","unstructured":"Ferrari, G., Montanari, U., Pistore, M.: Minimizing Transition Systems for Name Passing Calculi: A Co-algebraic Formulation. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol.\u00a02303, pp. 129\u2013143. Springer, Heidelberg (2002)"},{"key":"1_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-39656-7_13","volume-title":"Formal Methods for Components and Objects","author":"G. Ferrari","year":"2003","unstructured":"Ferrari, G., Montanari, U., Tuosto, E.: From Co-algebraic Specifications to Implementation: The Mihda toolkit. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol.\u00a02852, pp. 319\u2013338. Springer, Heidelberg (2003)"},{"key":"1_CR36","unstructured":"Ferrari, G., Montanari, U., Tuosto, E.: Coalgebraic Minimisation of HD-automata for the \u03c0-Calculus in a Polymorphic \u03bb-Calculus. TCS (2004) (to appear)"},{"key":"1_CR37","first-page":"193","volume-title":"LICS","author":"M. Fiore","year":"1999","unstructured":"Fiore, M., Plotkin, G., Turi, D.: Abstract Syntax and Variable Binding (Extended Abstract). In: LICS, Trento, Italy, pp. 193\u2013202. IEEE, Los Alamitos (1999)"},{"key":"1_CR38","first-page":"160","volume-title":"Computer Security Foundations Workshop, CSFW","author":"P. Fiore","year":"2001","unstructured":"Fiore, P., Abadi, M.: Computing Symbolic Models for Verifying Cryptographic Protocols. In: Computer Security Foundations Workshop, CSFW, Cape Breton, Nova Scotia, Canada, pp. 160\u2013173. IEEE, Los Alamitos (2001)"},{"key":"1_CR39","doi-asserted-by":"crossref","unstructured":"Focardi, R., Gorrieri, R.: A Classification of Security Properties. J. of Computer Security\u00a03(1) (1995)","DOI":"10.3233\/JCS-1994\/1995-3103"},{"key":"1_CR40","first-page":"214","volume-title":"LICS","author":"M. Gabbay","year":"1999","unstructured":"Gabbay, M., Pitts, A.: A New Approach to Abstract Syntax Involving Binders. In: Longo, G. (ed.) LICS, Trento, Italy, pp. 214\u2013224. IEEE, Los Alamitos (1999)"},{"key":"1_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45608-2_5","volume-title":"Foundations of Security Analysis and Design","author":"A. Gordon","year":"2001","unstructured":"Gordon, A.: Notes on Nominal Calculi for Security and Mobility. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol.\u00a02171, pp. 262\u2013330. Springer, Heidelberg (2001)"},{"issue":"2","key":"1_CR42","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. TCS\u00a0138(2), 353\u2013389 (1995)","journal-title":"TCS"},{"key":"1_CR43","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL","author":"T. Henzinger","year":"2002","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy Abstraction. In: POPL, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"1_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/3-540-49059-0_20","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"D. Hirschkoff","year":"1999","unstructured":"Hirschkoff, D.: On the Benefits of Using the up-to Techniques for Bisimulation Verification. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 285\u2013299. Springer, Heidelberg (1999)"},{"issue":"5","key":"1_CR45","first-page":"279","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The Model Checker Spin. TSE\u00a023(5), 279\u2013295 (1997)","journal-title":"TSE"},{"key":"1_CR46","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"issue":"5","key":"1_CR47","first-page":"617","volume":"10","author":"K. Honda","year":"2000","unstructured":"Honda, K.: Elementary Structures in Process Theory (1): Sets with Renaming. MSCS\u00a010(5), 617\u2013663 (2000)","journal-title":"MSCS"},{"key":"1_CR48","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/604131.604135","volume-title":"POPL","author":"O. Jensen","year":"2003","unstructured":"Jensen, O., Milner, R.: Bigraphs and Transitions. In: POPL, pp. 38\u201349. ACM Press, New York (2003)"},{"issue":"1","key":"1_CR49","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/0890-5401(90)90025-D","volume":"86","author":"P. Kanellakis","year":"1990","unstructured":"Kanellakis, P., Smolka, S.: CCS Expressions, Finite State Processes and Three Problem of Equivalence. Inf. and Comp.\u00a086(1), 272\u2013302 (1990)","journal-title":"Inf. and Comp."},{"key":"1_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-24727-2_20","volume-title":"Foundations of Software Science and Computation Structures","author":"S. Lack","year":"2004","unstructured":"Lack, S., Soboci\u0144ski, P.: Adhesive Categories. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 273\u2013288. Springer, Heidelberg (2004)"},{"key":"1_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-540-31982-5_18","volume-title":"Foundations of Software Science and Computational Structures","author":"C. Laneve","year":"2005","unstructured":"Laneve, C., Zavattaro, G.: Foundations of Web Transactions. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol.\u00a03441, pp. 282\u2013298. Springer, Heidelberg (2005)"},{"key":"1_CR52","unstructured":"Leifer, J.: Operational Congruences for Reactive Systems. PhD thesis, Computer Laboratory, University of Cambridge, Cambridge, UK (2001)"},{"key":"1_CR53","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. Leifer","year":"2000","unstructured":"Leifer, J., Milner, R.: Deriving Bisimulation Congruences for Reactive Systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 243\u2013258. Springer, Heidelberg (2000)"},{"issue":"1","key":"1_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0890-5401(02)00014-7","volume":"180","author":"H. Lin","year":"2003","unstructured":"Lin, H.: Complete Inference Systems for Weak Bisimulation Equivalences in the \u03c0-Calculus. Inf. and Comp.\u00a0180(1), 1\u201329 (2003)","journal-title":"Inf. and Comp."},{"key":"1_CR55","volume-title":"CSFW","author":"G. Lowe","year":"1998","unstructured":"Lowe, G.: Towards a Completeness Result for Model Checking of Security Protocols. In: CSFW. IEEE, Los Alamitos (1998)"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"Marrero, W., Clarke, E., Jha, S.: Model Checking for Security Protocols. In: Formal Verification of Security Protocols (1997)","DOI":"10.21236\/ADA327281"},{"key":"1_CR57","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"McMillan, K.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"1_CR58","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"issue":"1","key":"1_CR59","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, D.: A Calculus of Mobile Processes, I and II. Inf. and Comp.\u00a0100(1), 1\u201340, 41\u201377 (1992)","journal-title":"Inf. and Comp."},{"key":"1_CR60","first-page":"141","volume-title":"CSFW","author":"J. Mitchell","year":"1997","unstructured":"Mitchell, J., Mitchell, M., Ster, U.: Automated analysis of cryptographic protocols using mur\u03c6. In: CSFW, pp. 141\u2013151. IEEE, Los Alamitos (1997)"},{"key":"1_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/3-540-45694-5_30","volume-title":"CONCUR 2002 - Concurrency Theory","author":"U. Montanari","year":"2002","unstructured":"Montanari, U., Buscemi, M.: A First Order Coalgebraic Model of \u03c0-Calculus Early Observational Equivalence. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 449\u2013465. Springer, Heidelberg (2002)"},{"key":"1_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/3-540-60218-6_4","volume-title":"CONCUR \u201995 Concurrency Theory","author":"U. Montanari","year":"1995","unstructured":"Montanari, U., Pistore, M.: Checking Bisimilarity for Finitary \u03c0-Calculus. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 42\u201356. Springer, Heidelberg (1995)"},{"key":"1_CR63","unstructured":"Montanari, U., Pistore, M.: History Dependent Automata. Technical report, Computer Science Department, Universit\u00e0 di Pisa, TR-11-98 (1998)"},{"key":"1_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/3-540-44612-5_52","volume-title":"Mathematical Foundations of Computer Science 2000","author":"U. Montanari","year":"2000","unstructured":"Montanari, U., Pistore, M.: \u03c0-calculus, structured coalgebras and minimal HD-automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, p. 569. Springer, Heidelberg (2000)"},{"key":"1_CR65","doi-asserted-by":"crossref","first-page":"171","DOI":"10.3233\/FI-1992-16206","volume":"16","author":"U. Montanari","year":"1992","unstructured":"Montanari, U., Sassone, V.: Dynamic Congruence vs. Progressing Bisimulation for CCS. Fundamenta Informaticae\u00a016, 171\u2013196 (1992)","journal-title":"Fundamenta Informaticae"},{"key":"1_CR66","volume-title":"Names","author":"R. Needham","year":"1989","unstructured":"Needham, R.: Names. Mullender (ed.) Addison-Wesley, Reading (1989)"},{"issue":"6","key":"1_CR67","doi-asserted-by":"publisher","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.: Three Partition Refinement Algorithms. SIAM Journal on Computing\u00a016(6), 973\u2013989 (1987)","journal-title":"SIAM Journal on Computing"},{"key":"1_CR68","series-title":"LNCS","first-page":"3","volume-title":"Web Information Systems Engineering (WISE 2003)","author":"M. Papazoglou","year":"2003","unstructured":"Papazoglou, M.: Service-Oriented Computing: Concepts, Characteristics and Directions. In: Web Information Systems Engineering (WISE 2003). LNCS, pp. 3\u201312. Springer, Heidelberg (2003)"},{"key":"1_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and Automata on Infinite Sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol.\u00a0104, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"1_CR70","volume-title":"LICS","author":"J. Parrow","year":"1998","unstructured":"Parrow, J., Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In: LICS. IEEE, Los Alamitos (1998)"},{"key":"1_CR71","unstructured":"Pistore, M.: History Dependent Automata. PhD thesis, Computer Science Department, Universit\u00e0 di Pisa (1999)"},{"issue":"2","key":"1_CR72","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1006\/inco.2000.2895","volume":"164","author":"M. Pistore","year":"2001","unstructured":"Pistore, M., Sangiorgi, D.: A Partition Refinement Algorithm for the \u03c0-Calculus. Inf. and Comp.\u00a0164(2), 467\u2013509 (2001)","journal-title":"Inf. and Comp."},{"key":"1_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/3-540-60246-1_153","volume-title":"Mathematical Foundations of Computer Science 1995","author":"D. Sangiorgi","year":"1995","unstructured":"Sangiorgi, D.: On the Bisimulation Proof Method (Extended Abstract). In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 479\u2013488. Springer, Heidelberg (1995)"},{"issue":"1","key":"1_CR74","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 Informatica\u00a033(1), 69\u201397 (1996)","journal-title":"Acta Informatica"},{"key":"1_CR75","volume-title":"The \u03c0-Calculus: a Theory of Mobile Processes","author":"D. Sangiorgi","year":"2002","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-Calculus: a Theory of Mobile Processes. Cambridge University Press, Cambridge (2002)"},{"key":"1_CR76","doi-asserted-by":"crossref","unstructured":"Sassone, V., Soboci\u0144ski, P.: Deriving Bisimulation Congruences using 2-categories. Nordic J. of Computing\u00a010(2) (2003)","DOI":"10.7146\/brics.v10i1.21772"},{"key":"1_CR77","doi-asserted-by":"crossref","unstructured":"Sassone, V., Soboci\u0144ski, P.: Congruences for Contextual Graph-Rewriting. Technical Report RS-14, BRICS (June 2004)","DOI":"10.7146\/brics.v11i11.21836"},{"key":"1_CR78","doi-asserted-by":"crossref","unstructured":"Sassone, V., Soboci\u0144ski, P.: Locating Reaction with 2-Categories. TCS (2004) (to appear)","DOI":"10.1016\/S0304-3975(04)00137-9"},{"key":"1_CR79","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)"},{"key":"1_CR80","unstructured":"Sewell, P.: Applied \u03c0 \u2013 A Brief Tutorial. Technical Report 498, Computer Laboratory, University of Cambridge (August 2000)"},{"key":"1_CR81","unstructured":"Smith, H., Fingar, P.: Workflow is Just a Pi process (2003), Available at http:\/\/www.bpm3.com\/picalculus"},{"key":"1_CR82","unstructured":"Vanack\u00e9re, V.: The TRUST protocol analyser. Automatic and Efficient Verification of Cryptographic Protocols. In: VERIFY 2002 (2002)"},{"key":"1_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/3-540-58179-0_73","volume-title":"Computer Aided Verification","author":"B. Victor","year":"1994","unstructured":"Victor, B., Moller, F.: The Mobility Workbench \u2014 A Tool for the \u03c0-Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 428\u2013440. Springer, Heidelberg (1994)"},{"issue":"1","key":"1_CR84","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/s10009-003-0136-3","volume":"6","author":"P. Yang","year":"2004","unstructured":"Yang, P., Ramakrishnan, C., Smolka, S.: A Logical Encoding of the \u03c0-Calculus: Model Checking Mobile Processes Using Tabled Resolution. STTT\u00a06(1), 38\u201366 (2004)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31982-5_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,4]],"date-time":"2023-06-04T21:30:37Z","timestamp":1685914237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31982-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253884","9783540319825"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31982-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}