{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T05:00:40Z","timestamp":1648530040136},"reference-count":62,"publisher":"Springer Science and Business Media LLC","issue":"9","license":[{"start":{"date-parts":[[2005,7,8]],"date-time":"2005-07-08T00:00:00Z","timestamp":1120780800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2005,10]]},"DOI":"10.1007\/s00236-005-0168-0","type":"journal-article","created":{"date-parts":[[2005,7,22]],"date-time":"2005-07-22T15:57:09Z","timestamp":1122047829000},"page":"525-593","source":"Crossref","is-referenced-by-count":9,"title":["\u03c0-calculus with noisy channels"],"prefix":"10.1007","volume":"41","author":[{"given":"Mingsheng","family":"Ying","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,7,8]]},"reference":[{"key":"168_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1\u201370 (1999). An extended version appeared as Digital Equipment Corporation Systems Research Center Report No. 149 (1998)","DOI":"10.1006\/inco.1998.2740"},{"key":"168_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Annichini, A., Bouajjani, A.: Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In: Tools and Algorithms for the Construction and Analysis of Systems, Proceedings, LNCS 1579, pp. 208\u2013222. Springer (1999)","DOI":"10.1007\/3-540-49059-0_15"},{"key":"168_CR3","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Boasson, L., Bouajjani, A.: Effective lossy queue languages. In: Automata, Languages and Programming, Proceedings, LNCS 2076, pp. 639\u2013651. Springer (2001)","DOI":"10.1007\/3-540-48224-5_53"},{"key":"168_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-the-fly analysis of systems with unbounded, lossy FIFO channels. In: Computer-Aided Verification, Proceedings, LNCS 1427, pp. 305\u2013318. Springer (1998)","DOI":"10.1007\/BFb0028754"},{"key":"168_CR5","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1023\/B:FORM.0000033962.51898.1a","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods in System Design 25, 39\u201365 (2004)","journal-title":"Formal Methods in System Design"},{"key":"168_CR6","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channel. Information and Computation 127, 91\u2013101 (1996)","journal-title":"Information and Computation"},{"key":"168_CR7","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130, 71\u201390 (1996)","journal-title":"Information and Computation"},{"key":"168_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Rabinovich, A.: Verification of probabilistic systems with faulty communication. In: Foundations of Software Science and Computation Structures, Proceedings, LNCS 2620, pp. 39\u201353. Springer (2003)","DOI":"10.1007\/3-540-36576-1_3"},{"key":"168_CR9","volume-title":"Information Dover","author":"R.B. Ash","year":"1990","unstructured":"Ash, R.B.: Information Theory. Dover, New York (1990)"},{"key":"168_CR10","doi-asserted-by":"crossref","unstructured":"Baeten, J., Bergstra, J., Smolka, S.: Axiomatizing probabilistic processes: ACP with generative probability. Information and Computation 122, 234\u2013255 (1995) (Preliminary version appeared in: CONCUR\u201992, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24\u201327, 1992, Proceedings, LNCS 630, pp. 472\u2013485). Springer (1992)","DOI":"10.1007\/BFb0084810"},{"key":"168_CR11","doi-asserted-by":"crossref","unstructured":"Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems. In: Katoen, J.-P. (ed.), Formal Methods for Real-Time and Probabilistic Systems: 5th International AMAST Workshop, ARTS\u201999, Bamberg, Germany, May 1999. Proceedings, LNCS 1601, pp. 34\u201353. Springer (1999)","DOI":"10.1007\/3-540-48778-6_3"},{"key":"168_CR12","doi-asserted-by":"crossref","unstructured":"Berger, M.: Basic theory of reduction congruence for two timed asynchronous \u03c0-calculi. In: Gardner, P., Yoshida, N. (eds.), CONCUR 2004 - Concurrency Theory: 15th International Conference, London, UK, August 31 \u2013 September 3, 2004. Proceedings, LNCS 3170, pp. 115\u2013130. Springer (2004)","DOI":"10.1007\/978-3-540-28644-8_8"},{"key":"168_CR13","unstructured":"Berger, M.: Towards Abstractions for Distributed Systems. Ph.D. Thesis, Imperial College, London (2002)"},{"key":"168_CR14","unstructured":"Berger, M., Honda, K.: The two-phase commit protocol in an extended \u03c0-calculus. In: Proc. EXPRESS\u201900, 7th International Workshop on Expressiveness in Concurrency. Penn State University, USA (2000)"},{"key":"168_CR15","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"33","author":"J.A. Bergstra","year":"1985","unstructured":"Bergstra, J.A. Klop, J.-W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 33, 77\u2013121 (1985)","journal-title":"Theoretical Computer Science"},{"key":"168_CR16","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0304-3975(97)00125-4","volume":"198","author":"M. Boreale","year":"1998","unstructured":"Boreale, M., Sangiorgi, D.: Some congruence properties for \u03c0-calculus bisimilarities. Theoretical Computer Science 198, 159\u2013176 (1998)","journal-title":"Theoretical Computer Science"},{"key":"168_CR17","unstructured":"Boudol, G.: Asynchrony and the \u03c0-calculus. Rapport de Recherche 1702, INRIA, Sophia-Antipolis (1992)"},{"key":"168_CR18","doi-asserted-by":"crossref","first-page":"433","DOI":"10.3233\/FI-1988-11406","volume":"11","author":"G. Boudol","year":"1988","unstructured":"Boudol, G., Castellani, I.: A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae 11, 433\u2013452 (1988)","journal-title":"Fundamenta Informaticae"},{"key":"168_CR19","doi-asserted-by":"crossref","unstructured":"van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Proceedings of the 23th International Colloquium on Automata, Languages and Programming, LNCS 2076, pp. 421\u2013432. Springer, Berlin (2001)","DOI":"10.1007\/3-540-48224-5_35"},{"key":"168_CR20","volume-title":"Lectures on Formal Methods and Performance Analysis. LNCS 2090","year":"2001","unstructured":"Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.): Lectures on Formal Methods and Performance Analysis. LNCS 2090, Springer, Berlin (2001)"},{"key":"168_CR21","doi-asserted-by":"crossref","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31, 560\u2013599 (1984)","journal-title":"Journal of the ACM"},{"key":"168_CR22","unstructured":"Chang, C.C., Keisler, H.J.: Model Theory (3rd edition), Studies in Logic and the Foundations of Mathematics 73. North-Holland, Amsterdam (1990)"},{"key":"168_CR23","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1006\/inco.1999.2808","volume":"154","author":"R. Cleaveland","year":"1999","unstructured":"Cleaveland, R., Dayar, Z., Smolka, S.A., Yuen, S.: Testing preorders for probabilistic processes. Information and Computation 154, 93\u2013148 (1999)","journal-title":"Information and Computation"},{"key":"168_CR24","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., Smolka, S.A., Zwarico, A.E.: Testing preorders for probabilistic processes. In: Kuich, W. (ed.), Automata, Languages and Programming (ICALP\u201992), Viena, Proceedings, LNCS 623, pp. 708\u2013719. Springer (1992)","DOI":"10.1007\/3-540-55719-9_116"},{"key":"168_CR25","doi-asserted-by":"crossref","unstructured":"Desharnais, D., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov systems. In: Proceedings of the 10th International Conference on Concurrency Theory, LNCS 1664, pp. 258\u2013273. Springer (1999)","DOI":"10.1007\/3-540-48320-9_19"},{"key":"168_CR26","doi-asserted-by":"crossref","unstructured":"Engberg, U., Nielsen, M.: A calculus of communicating systems with label passing. Report DAIMI PB-208, Computer Science Department, University of Aarhus (1986)","DOI":"10.7146\/dpb.v15i208.7559"},{"key":"168_CR27","unstructured":"Feng, Y., Zhang, S.Y.: Approximate bisimilarity in probabilistic process algebras. unpublished note (2002)"},{"key":"168_CR28","volume-title":"Program Verification","author":"N. Francez","year":"1992","unstructured":"Francez, N.: Program Verification. Addison-Wesley, Wokingham (1992)"},{"key":"168_CR29","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1006\/inco.1995.1123","volume":"121","author":"R.J. van Glabbeek","year":"1995","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative, and stratified models of probabilistic processes. Information and Computation 121, 59\u201380 (1995)","journal-title":"Information and Computation"},{"key":"168_CR30","doi-asserted-by":"crossref","unstructured":"van Glabbeek, R.J., Smolka, S.A., Steffen, B., Tofts, C.M.N.: Reactive, generative, and stratified models of probabilistic processes. In: Proc. 5th Annual IEEE Symposium on Logic in Computer Science, pp. 130\u2013141. Philadelphia (1990)","DOI":"10.1109\/LICS.1990.113740"},{"key":"168_CR31","doi-asserted-by":"crossref","unstructured":"Hansson, H.A., Jonsson, B.: A calculus for communicating systems with time and probability. In: Proceedings of the 11th IEEE Symposium on Real-Time Systems, Lake Buena Vista, Florida, USA, pp. 278\u2013287. IEEE Computer Societ Press (1990)","DOI":"10.1109\/REAL.1990.128759"},{"key":"168_CR32","doi-asserted-by":"crossref","unstructured":"Herescu, O.M., Palamidessi, C.: Probabilistic asynchronous pi-calculus. In: Tiuryn, J. (ed.), Proceedings of the Third International Conference on Foundations of Software Science and Computation Structures. Held as Part of the Joint European Conferences on Theory and Practice of Software, LNCS 1784, pp. 146\u2013160. Springer (2000)","DOI":"10.1007\/3-540-46432-8_10"},{"key":"168_CR33","unstructured":"Herescu, The Probabilistic Asynchronous PI-Calculus. Ph.D. Thesis, The Pennsylvania State University (2002)"},{"key":"168_CR34","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Communications of the ACM 21, 666\u2013677 (1978)","journal-title":"Communications of the ACM"},{"key":"168_CR35","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, New York (1985)"},{"key":"168_CR36","doi-asserted-by":"crossref","unstructured":"Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.), Proceedings of the European Conference on Object-Oriented Programming, LNCS 512, pp. 133\u2013147. Springer-Verlag Heidelberg (1991)","DOI":"10.1007\/BFb0057019"},{"key":"168_CR37","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/0304-3975(95)00074-7","volume":"151","author":"K. Honda","year":"1995","unstructured":"Honda, K., Yoshida, N.: On reduction-based process semantics. Theoretical Computer Science 151, 437\u2013486 (1995)","journal-title":"Theoretical Computer Science"},{"key":"168_CR38","doi-asserted-by":"crossref","unstructured":"Iyer, P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.), TAPSOFT\u201997, Theory and Practice of Software Development, Proceedings, LNCS 1214, pp. 667\u2013681. Springer (1997)","DOI":"10.1007\/BFb0030633"},{"key":"168_CR39","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Information and Computation 94, 371\u2013384 (1991)","journal-title":"Information and Computation"},{"key":"168_CR40","unstructured":"Lu, R.Q., Wei, Z.C.: Truly Probabilistic Pi-Calculus and Risk Semantics. Technical Report, Mathematical Institute, Academia Sinica (2004)"},{"key":"168_CR41","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems, Lecture Notes in Computer Science 92","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems, Lecture Notes in Computer Science 92. Springer-Verlag, Berlin (1980)"},{"key":"168_CR42","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ (1989)"},{"key":"168_CR43","unstructured":"Milner, R.: The polyadic \u03c0-calculus: a tutorial. Technical Report ECS-LFCS-91-180, University of Edinburgh (1991)"},{"key":"168_CR44","doi-asserted-by":"crossref","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Technical Report ECS-LFCS-89-85 and 86, University of Edinburgh, 1989; also see Information and Computation 100, 1\u201377 (1992)","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"168_CR45","doi-asserted-by":"crossref","unstructured":"Milner, R., Sangiorgi, D.: Barbed bisimulation. In: ICALP\u201992, Automata, Languages and Programming, LNCS 623, pp. 685\u2013695. Springer (1992)","DOI":"10.1007\/3-540-55719-9_114"},{"key":"168_CR46","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S1567-8326(02)00069-3","volume":"56","author":"M. N\u00fa\u00f1ez","year":"2003","unstructured":"N\u00fa\u00f1ez, M.: Algebraic theory of probabilistic processes. Journal of Logic and Algebraic Programming 56, 117\u2013177 (2003)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"168_CR47","unstructured":"Petri, C.A.: Kommunikation mit Automaten. Schriften des Rheinisch-Westfaelischen, Institutes fuer instrumentelle Mathematik an der Universitaet, Nr. 2, Bonn (1962)"},{"key":"168_CR48","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1093\/comjnl\/38.7.578","volume":"38","author":"C. Priami","year":"1995","unstructured":"Priami, C.: Stochastic \u03c0-calculus. The Computer Journal 38, 578\u2013589 (1995)","journal-title":"The Computer Journal"},{"key":"168_CR49","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1006\/inco.1996.0096","volume":"131","author":"D. Sangiorgi","year":"1996","unstructured":"Sangiorgi, D.: Bisimulation for higher-order process calculi. Information and Computation 131, 141\u2013178 (1996)","journal-title":"Information and Computation"},{"key":"168_CR50","volume-title":"The \u03c0-calculus: A Theory of Mobile Processes","author":"D. Sangiorgi","year":"2001","unstructured":"Sangiorgi, D., Walker, D.: The \u03c0-calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)"},{"key":"168_CR51","doi-asserted-by":"crossref","unstructured":"Schnoebelen, P.: The verification of probabilistic lossy channel systems. In: Christel Baier et al. (eds.), Validation of Stochastic Systems: A Guide to Current Research BibEditorNames, LNCS 2925, pp. 445\u2013465. Springer (2004)","DOI":"10.1007\/978-3-540-24611-4_13"},{"key":"168_CR52","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/0304-3975(94)00286-0","volume":"152","author":"K. Seidel","year":"1995","unstructured":"Seidel, K.: Probabilistic communicating processes. Theoretical Computer Science 152, 219\u2013249 (1995)","journal-title":"Theoretical Computer Science"},{"key":"168_CR53","doi-asserted-by":"crossref","unstructured":"Shannon, C.E.: A mathematical theory of communication, I, II. Bell System Technical Journal 27, 379\u2013423; 623\u2013656 (1948)","DOI":"10.1002\/j.1538-7305.1948.tb01338.x"},{"key":"168_CR54","doi-asserted-by":"crossref","unstructured":"Thomsen, B.: Calculi for Higher Order Communicating Systems. Ph.D. Thesis, Dept. of Computing, Imperial College (1990)","DOI":"10.1145\/75277.75290"},{"key":"168_CR55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01200262","volume":"30","author":"B. Thomsen","year":"1993","unstructured":"Thomsen, B.: Plain CHOCS, a second generation calculus for higher-order process. Acta Informatica 30, 1\u201359 (1993)","journal-title":"Acta Informatica"},{"key":"168_CR56","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-3472-7","volume-title":"Statistical Reasoning with Imprecise Probabilities","author":"P. Walley","year":"1991","unstructured":"Walley, P.: Statistical Reasoning with Imprecise Probabilities. Chapman and Hall, London (1991)"},{"key":"168_CR57","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-0123-3","volume-title":"Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs","author":"M.S. Ying","year":"2001","unstructured":"Ying, M.S.: Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs. Springer-Verlag, New York (2001)"},{"key":"168_CR58","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(01)00124-4","volume":"275","author":"M.S. Ying","year":"2002","unstructured":"Ying, M.S.: Bisimulation indexes and their applications. Theoretical Computer Science 275, 1\u201368 (2002)","journal-title":"Theoretical Computer Science"},{"key":"168_CR59","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1016\/S0304-3975(01)00294-8","volume":"275","author":"M.S. Ying","year":"2002","unstructured":"Ying, M.S.: Additive models of probabilistic processes. Theoretical Computer Science 275, 481\u2013519 (2002)","journal-title":"Theoretical Computer Science"},{"key":"168_CR60","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1007\/s00236-003-0113-z","volume":"39","author":"M.S. Ying","year":"2003","unstructured":"Ying, M.S.: Reasoning about probabilistic sequential programs in a probabilistic logic. Acta Informatica 39, 315\u2013389 (2003)","journal-title":"Acta Informatica"},{"key":"168_CR61","doi-asserted-by":"crossref","unstructured":"Ying, M.S., Wirsing, M.: Approximate bisimilarity. In: Rus, T. (ed.), Algebraic Methodology and Software Technology, 8th International Conference, AMAST 2000, Iowa City, USA. Proceedings, Lecture Notes in Computer Science 1816, pp. 309\u2013321. Springer-Verlag, Berlin (2000)","DOI":"10.1007\/3-540-45499-3_23"},{"key":"168_CR62","doi-asserted-by":"crossref","first-page":"839","DOI":"10.1016\/S0304-3975(00)00378-9","volume":"266","author":"M.S. Ying","year":"2001","unstructured":"Ying, M.S., Wirsing, M.: Recursive equations in higher-order process calculi. Theoretical Computer Science 266, 839\u2013852 (2001)","journal-title":"Theoretical Computer Science"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-005-0168-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-005-0168-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-005-0168-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T22:06:32Z","timestamp":1626213992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-005-0168-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,7,8]]},"references-count":62,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["168"],"URL":"https:\/\/doi.org\/10.1007\/s00236-005-0168-0","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,7,8]]}}}