{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,5]],"date-time":"2024-12-05T05:30:49Z","timestamp":1733376649421,"version":"3.30.1"},"reference-count":29,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2001,11,1]],"date-time":"2001-11-01T00:00:00Z","timestamp":1004572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4276,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2001,11]]},"DOI":"10.1016\/s0167-6423(01)00008-9","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T17:02:32Z","timestamp":1027616552000},"page":"241-275","source":"Crossref","is-referenced-by-count":5,"title":["Unique fixpoint induction for message-passing process calculi"],"prefix":"10.1016","volume":"41","author":[{"given":"M.","family":"Hennessy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Rathke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S0167-6423(01)00008-9_BIB1","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1093\/comjnl\/37.4.289","article-title":"A correctness proof of a one bit sliding window protocol in \u03bcCRL","volume":"37","author":"Bezem","year":"1994","journal-title":"The Comput. J."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB2","series-title":"A complete inference system for regular processes with silent moves, in Proc. Logic Colloquium\u201986","first-page":"21","author":"Bergstra","year":"1988"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB3","series-title":"Model checking and abstraction, in POPL\u201992","first-page":"343","author":"Clarke","year":"1992"},{"year":"1989","series-title":"A semantics based verification tool for finite state systems, in Proc. of the 9th Internat. Symp. on Protocol Specification, Testing and Verification","author":"Cleaveland","key":"10.1016\/S0167-6423(01)00008-9_BIB4"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB5","series-title":"Testing-based abstractions for value-passing systems, in CONCUR\u201994, No. 836 in Lecture Notes in Computer Science","first-page":"417","author":"Cleaveland","year":"1994"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB6","unstructured":"G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, B. Werner, The Coq proof assistant user's guide, version 5.8, Report, INRIA-Rocquencourt and CNRS-ENS Lyon, 1993."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB7","series-title":"Proc. of the Internat. Workshop on Semantics of Specification Languages, Workshops in Computing Series","first-page":"231","article-title":"Proof theory for \u03bcCRL","author":"Groote","year":"1994"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB8","series-title":"Algebra of Communicating Processes \u201994, Workshops in Computing Series","first-page":"26","article-title":"The syntax and semantics of \u03bc CRL.","author":"Groote","year":"1995"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB9","series-title":"Technical Report SEN-R9830","article-title":"A complete axiomatisation of branching bisimulation for process algebras with alternative quantification over data","author":"Groote","year":"1998"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB10","series-title":"Technical Report SEN-R9806","article-title":"Undecidability and completeness results for process algebras with alternative quantification over data","author":"Groote","year":"1998"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB11","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1016\/0304-3975(94)00172-F","article-title":"Symbolic bisimulations","volume":"138","author":"Hennessy","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB12","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1007\/BF01213531","article-title":"Proof systems for message-passing process algebras","volume":"8","author":"Hennessy","year":"1996","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB13","unstructured":"M. Hennessy, H. Lin, Unique fixpoint induction for message-passing process calculi. in Proc. CATS\u201997, Australia Computer Science Communications, 1997, pp. 122\u2013131."},{"year":"1993","series-title":"A verification tool for value-passing processes, in Proc. of 13th Internat. Symp. on Protocol Specification, Testing and Verification, IFIP Transactions","author":"Lin","key":"10.1016\/S0167-6423(01)00008-9_BIB14"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB15","series-title":"Unique fixpoint induction for mobile processes, in CONCUR\u201995, Vol. 962 of Lecture Notes in Computer Science","first-page":"88","author":"Lin","year":"1995"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB16","unstructured":"H. Lin, On implementing unique fixpoint induction for value-passing processes, in Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, May 1995, pp. 104\u2013118."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB17","series-title":"Symbolic graphs with assignment, in CONCUR\u201996, Pisa, Vol. 1119 of Lecture Notes in Computer Science","first-page":"50","author":"Lin","year":"1996"},{"year":"1999","series-title":"Complete axiomatisations of weak-, delay- and \u03b7-bisimulation for process algebras with alternative quantification over data, Technical Report SEN-R9914","author":"Luttik","key":"10.1016\/S0167-6423(01)00008-9_BIB18"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB19","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1016\/0022-0000(84)90023-0","article-title":"A complete inference system for a class of regular behaviours","volume":"28","author":"Milner","year":"1984","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB20","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0890-5401(89)90070-9","article-title":"A complete axiomatisation for observational congruence of finite-state behaviours","volume":"81","author":"Milner","year":"1989","journal-title":"Inform. Comput."},{"year":"1989","series-title":"Communication and Concurrency","author":"Milner","key":"10.1016\/S0167-6423(01)00008-9_BIB21"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB22","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A calculus of mobile processes, Part I,II","volume":"100","author":"Milner","year":"1992","journal-title":"Inform. Comput."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB23","unstructured":"P. Paczkowski, Characterising bisimilarity of value-passing parameterised processes, in Proc. Infinity Workshop on Verification of Infinite State Systems, Pisa, 1996, pp. 47\u201355."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB24","series-title":"Isabelle: a generic theorem prover, Vol. 828 of Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","author":"Paulson","year":"1994"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB25","unstructured":"J. Parrow, D. Sangiorgi, Algebraic theories for name-passing calculi, Report ECS-LFCS-93-262, LFCS, University of Edinburgh, 1993."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB26","doi-asserted-by":"crossref","unstructured":"J. Rathke, Symbolic techniques for value-passing calculi, Thesis, University of Sussex 1997, available as a Technical Report.","DOI":"10.1109\/LICS.1997.614942"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB27","doi-asserted-by":"crossref","unstructured":"J. Rathke, Unique fixpoint induction for value-passing processes, in Proc. LICS\u201997, 12th Ann. Symp. on Logic in Computer Science, 1997, pp. 140\u2013148.","DOI":"10.1109\/LICS.1997.614942"},{"key":"10.1016\/S0167-6423(01)00008-9_BIB28","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0304-3975(88)90149-1","article-title":"Substitution revisited","volume":"59","author":"Stoughton","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0167-6423(01)00008-9_BIB29","doi-asserted-by":"crossref","unstructured":"W.J. Yeh, M. Young, Compositional reachability analysis using process algebra, in TAV\u201991, ACM SIGSOFT, ACM Press, 1991, New York, pp. 49\u201359.","DOI":"10.1145\/120807.120812"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000089?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642301000089?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,4]],"date-time":"2024-12-04T17:12:47Z","timestamp":1733332367000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642301000089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,11]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2001,11]]}},"alternative-id":["S0167642301000089"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(01)00008-9","relation":{},"ISSN":["0167-6423"],"issn-type":[{"type":"print","value":"0167-6423"}],"subject":[],"published":{"date-parts":[[2001,11]]}}}