{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T06:10:19Z","timestamp":1737094219607,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008972"},{"type":"electronic","value":"9783540365761"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36576-1_17","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T02:42:17Z","timestamp":1181616137000},"page":"267-281","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Cones and Foci for Protocol Verification Revisited"],"prefix":"10.1007","author":[{"given":"Wan","family":"Fokkink","sequence":"first","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"T. Arts and I.A. van Langevelde. Correct performance of transaction capabilities. In Proc. 2nd Conference on Application of Concurrency to System Design, pp. 35\u201342. IEEE Computer Society, June 2001.","DOI":"10.1109\/CSD.2001.981762"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0304-3975(87)90052-1","volume":"51","author":"J.C.M. Baeten","year":"1987","unstructured":"J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. On the consistency of Koomen\u2019s fair abstraction rule. Theoretical Computer Science, 51:129\u2013176, 1987.","journal-title":"Theoretical Computer Science"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(96)00034-8","volume":"58","author":"T. Basten","year":"1996","unstructured":"T. Basten. Branching bisimilarity is an equivalence indeed! Information Processing Letters, 58:141\u2013147, 1996.","journal-title":"Information Processing Letters"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"J.A. Bergstra","year":"1985","unstructured":"J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77\u2013121, 1985.","journal-title":"Theoretical Computer Science"},{"key":"17_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BFb0015022","volume-title":"Invariants in process algebra with data","author":"M.A. Bezem","year":"1994","unstructured":"M.A. Bezem and J.F. Groote. Invariants in process algebra with data. In Proc. 5th Conference on Concurrency Theory, LNCS 836, pp. 401\u2013416. Springer, 1994."},{"key":"17_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"CRL: A toolset for analysing algebraic specifications","author":"S.C.C. Blom","year":"2001","unstructured":"S.C.C. Blom, W.J. Fokkink, J.F. Groote, I.A. van Langevelde, B. Lisser, and J.C. van de Pol. \u03bcCRL: A toolset for analysing algebraic specifications. In Proc. 13th Conference on Computer Aided Verification, LNCS 2102, pp. 250\u2013254. Springer, 2001."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"17_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-63166-6_21","volume-title":"A provably correct embedded verifier for the certification of safety critical software","author":"A. Cimatti","year":"1997","unstructured":"A. Cimatti, F. Giunchiglia, P. Pecchiari, B. Pietra, J. Profeta, D. Romano, P. Traverso, and B. Yu. A provably correct embedded verifier for the certification of safety critical software. In Proc. 9th Conference on Computer Aided Verification, LNCS 1254, pp. 202\u2013213. Springer, 1997."},{"key":"17_CR10","unstructured":"E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2000."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"B. Courcelle. Recursive applicative program schemes. In Handbook of Theoretical Computer Science, Volume B, Formal Methods and Semantics, pp. 459\u2013492. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50014-7"},{"key":"17_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"CADP-a protocol validation and verification toolbox","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and M. Sighireanu. CADP-a protocol validation and verification toolbox. In Proc. 8th Conference on Computer-Aided Verification, LNCS 1102, pp. 437\u2013440. Springer, 1997."},{"key":"17_CR13","unstructured":"W.J. Fokkink, J.F. Groote, and J. Pang. Verification of a sliding window protocol in \u03bcCRL. In preparation."},{"key":"17_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/BFb0029968","volume-title":"Simulation as a correct transformation of rewrite systems","author":"W.J. Fokkink","year":"1997","unstructured":"W.J. Fokkink and J.C. van de Pol. Simulation as a correct transformation of rewrite systems. In Proceedings of 22nd Symposium on Mathematical Foundations of Computer Science, LNCS 1295, pp. 249\u2013258. Springer, 1997."},{"key":"17_CR15","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1016\/S0304-3975(96)00256-3","volume":"177","author":"L.-\u00c5. Fredlund","year":"1997","unstructured":"L.-\u00c5. Fredlund, J.F. Groote, and H.P. Korver. Formal verification of a leader election protocol in process algebra. Theoretical Computer Science, 177:459\u2013486, 1997.","journal-title":"Theoretical Computer Science"},{"key":"17_CR16","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the ACM, 43:555\u2013600, 1996.","journal-title":"Journal of the ACM"},{"key":"17_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/10703260_4","volume-title":"Collaboration between Human and Artificial Societies, Coordination and Agent-Based Distributed Computing","author":"W. Goerigk","year":"1999","unstructured":"W. Goerigk and F. Simon. Towards rigorous compiler implementation verification. In Collaboration between Human and Artificial Societies, Coordination and Agent-Based Distributed Computing, LNCS 1624, pp. 62\u201373. Springer, 1999."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"J. F. Groote, J. Pang, and A.G. Wouters. Analysis of a distributed system for lifting trucks. Journal of Logic and Algebraic Programming, 2003. To appear.","DOI":"10.1016\/S1567-8326(02)00038-3"},{"key":"17_CR19","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S1567-8326(01)00005-4","volume":"48","author":"J. F. Groote","year":"2001","unstructured":"J. F. Groote, A. Ponse, and Y.S. Usenko. Linearization in parallel pCRL. Journal of Logic and Algebraic Programming, 48:39\u201372, 2001.","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"17_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"629","DOI":"10.1007\/BFb0055652","volume-title":"Checking verifications of protocols and distributed systems by computer","author":"J.F. Groote","year":"1998","unstructured":"J.F. Groote, F. Monin, and J.C. van de Pol. Checking verifications of protocols and distributed systems by computer. In Proc. 9th Conference on Concurrency Theory, LNCS 1466, pp. 629\u2013655. Springer, 1998."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse. The syntax and semantics of \u03bcCRL. In Proc. 1st Workshop on the Algebra of Communicating Processes, Workshops in Computing Series, pp. 26\u201362. Springer, 1995.","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/S1567-8326(01)00010-8","volume":"49","author":"J.F. Groote","year":"2001","unstructured":"J.F. Groote and J. Springintveld. Focus points and convergent process operators. A proof strategy for protocol verification. Journal of Logic and Algebraic Programming, 49:31\u201360, 2001.","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"17_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1007\/BFb0032063","volume-title":"An efficient algorithm for branching bisimulation and stuttering equivalence","author":"J.F. Groote","year":"1990","unstructured":"J.F. Groote and F.W. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In Proc. 17th Colloquium on Automata, Languages and Programming, LNCS 443, pp. 626\u2013638. Springer, 1990."},{"key":"17_CR24","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1016\/S0304-3975(00)00324-8","volume":"266","author":"J.F. Groote","year":"2001","unstructured":"J.F. Groote and J.J. van Wamel. The parallel composition of uniform processes with data. Theoretical Computer Science, 266:631\u2013652, 2001.","journal-title":"Theoretical Computer Science"},{"key":"17_CR25","unstructured":"B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Science, Uppsala University, 1987."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"C.P.J. Koymans and J.C. Mulder. A modular approach to protocol verification using process algebra. In Applications of Process Algebra, Cambridge Tracts in Theoretical Computer Science 17, pp. 261\u2013306. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511608841.012"},{"key":"17_CR27","unstructured":"J. Loeckx, H.-D. Ehrich, and M. Wolf. Specification of Abstract Data Types. Wiley\/Teubner, 1996."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symposium on Principles of Distributed Computing, pp. 137\u2013151. ACM, 1987.","DOI":"10.1145\/41840.41852"},{"key":"17_CR29","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N.A. Lynch","year":"1995","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations. Part I: Untimed systems. Information and Computation, 121:214\u2013233, 1995.","journal-title":"Information and Computation"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"G. Necula. Translation validation for an optimizing compiler. In Proc. 2000 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. SIGPLAN Notices 35:83\u201394. ACM, 2000.","DOI":"10.1145\/358438.349314"},{"key":"17_CR31","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/3-540-36103-0_40","volume-title":"Analysis of a security protocol in \u03bcCRL","author":"J. Pang","year":"2002","unstructured":"J. Pang. Analysis of a security protocol in \u03bcCRL. In Proc. 4th International Conference on Formal Engineering Methods, LNCS 2495, pp. 396\u2013400. Springer, 2002."},{"key":"17_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Translation validation","author":"A. Pnueli","year":"1998","unstructured":"A. Pnueli, M. Siegel, and E. Singerman. Translation validation. In Proc. 4th Conference on Tools and Algorithms for Construction and Analysis of Systems, LNCS 1384, pp. 151\u2013166. Springer, 1998."},{"key":"17_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1007\/3-540-46000-4_26","volume-title":"Formal specification of JavaspacesTM architecture using \u03bcCRL","author":"J.C. Pol van de","year":"2002","unstructured":"J.C. van de Pol and M. Valero Espada. Formal specification of JavaspacesTM architecture using \u03bcCRL. In Proc. 5th Conference on Coordination Models and Languages, LNCS 2315, pp. 274\u2013290. Springer, 2002."},{"key":"17_CR34","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/s001650050030","volume":"10","author":"C. Shankland","year":"1998","unstructured":"C. Shankland and M.B. van der Zwaag. The tree identify protocol of IEEE 1394 in \u03bcCRL. Formal Aspects of Computing, 10:509\u2013531, 1998.","journal-title":"Formal Aspects of Computing"},{"key":"17_CR35","unstructured":"Y.S. Usenko. Linearization of \u03bcCRL specifications (extended abstract). In Proc. 3rd International Workshop on Verification and Computational Logic (VCL2002), Technical Report DSSE-TR-2002-5. Department of Electronics and Computer Science, University of Southampton, 2002."},{"issue":"1","key":"17_CR36","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/S0020-0190(01)00215-0","volume":"80","author":"M.B. Zwaag van der","year":"2001","unstructured":"M.B. van der Zwaag. The cones and foci proof technique for timed transition systems. Information Processing Letters, 80(1):33\u201340, 2001.","journal-title":"Information Processing Letters"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36576-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T05:53:49Z","timestamp":1737093229000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36576-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008972","9783540365761"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-36576-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"28 February 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}