Issue No.09 - Sept. (2012 vol.61)
pp: 1217-1230
Yongzhi Cao , Peking University, Beijing
To model the behavior of channels in real-world mobile systems, Ying introduced an extension of the \pi-calculus by taking channel noise into account. Unfortunately, this extension is not faithful in the sense that its semantics does not coincide with the standard one for the \pi-calculus in the noise-free case. In this paper, we consider a simple variant of the \pi-calculus, the asynchronous \pi-calculus (A\pi), which has been used for modeling some concurrent systems with asynchronous communication. To model these systems with noisy channels, we propose a faithful extension of A\pi, called the A\pi_n-calculus. After giving a probabilistic transitional semantics of A\pi_n, we introduce bisimilarity in A\pi_n and show that it is a partial input congruence. If a specification of a system is described as a process P in A\pi and we view the behavior of P in A\pi_n as an implementation of the specification, then it is interesting to measure how far the behavior in A\pi_n is from that in A\pi. We thus introduce the notion of reliability degree, which is based upon a new approximate bisimulation. We find that bisimilar agents may have different reliability degrees and even the agent with the greatest reliability degree may not be satisfactory. We thus appeal to Shannon's noisy channel coding theorem and show that reliability degrees can be improved by employing coding techniques.
Approximate bisimulation, asynchronous \pi-calculus, bisimilarity, noisy channel, reliability.
Yongzhi Cao, "Reliability of Mobile Processes with Noisy Channels", IEEE Transactions on Computers, vol.61, no. 9, pp. 1217-1230, Sept. 2012, doi:10.1109/TC.2011.147
[1] R. Milner, J. Parrow, and D. Walker, "A Calculus of Mobile Processes, Parts I and II," Information and Computation, vol. 100, pp. 1-77, 1992.
[2] R. Milner, Communicating and Mobile Systems: The $\pi$ -Calculus. Cambridge Univ. Press, 1999.
[3] D. Sangiorgi and D. Walker, The $\pi$ -Calculus: A Theory of Mobile Processes. Cambridge Univ. Press, 2001.
[4] P.A. Abdulla, N. Bertrand, A.M. Rabinovich, and P. Schnoebelen, "Verification of Probabilistic Systems with Faulty Communication," Information and Computation, vol. 202, no. 2, pp. 141-165, 2005.
[5] P.A. Abdulla, A. Annichini, and A. Bouajjani, "Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol," Proc. Fifth Int'l Conf. Tools and Algorithms for Construction and Analysis of Systems (TACAS '99), pp. 208-222, 1999.
[6] P.A. Abdulla, L. Boasson, and A. Bouajjani, “Effective Lossy Queue Languages,” Proc. 28th Int'l Colloquium Automata, Languages and Programming (ICALP '01), pp. 639-651, 2001.
[7] P.A. Abdulla, A. Bouajjani, and B. Jonsson, “On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels,” Proc. 10th Int'l Conf. Computer Aided Verification (CAV '98), pp. 305-318, 1998.
[8] P.A. Abdulla and B. Jonsson, “Undecidable Verification Problems for Programs with Unreliable Channels,” Information and Computation, vol. 130, no. 1, pp. 71-90, 1996.
[9] P.A. Abdulla and B. Jonsson, “Verifying Programs with Unreliable Channels,” Information and Computation, vol. 127, no. 2, pp. 91-101, 1996.
[10] S.P. Iyer and M. Narasimha, “Probabilistic Lossy Channel Systems,” Proc. Seventh Int'l Joint Conf. Theory and Practice of Software Development (TAPSOFT '97), pp. 667-681, 1997.
[11] M. Berger and K. Honda, “The Two-Phase Commitment Protocol in an Extended $\pi$ -Calculus,” Electrical Notes in Theoretical Computer Science, vol. 39, pp. 21-46, 2003.
[12] M. Berger, “Basic Theory of Reduction Congruence for Two Timed Asynchronous $\pi$ -Calculi,” Proc. Int'l Conf. Concurrency Theory (CONCUR '04), pp. 115-130, 2004.
[13] M. Berger and N. Yoshida, “Timed, Distributed, Probabilistic, Typed Processes,” Proc. Fifth Asian Conf. Programming Languages and Systems (APLAS '07), pp. 158-174, 2007.
[14] M. Ying, “$\pi$ -Calculus with Noisy Channels,” Acta Informatica, vol. 41, pp. 525-593, 2005.
[15] M. Ying, Topology of Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent. Springer-Verlag, 2001.
[16] M. Ying, “Bisimulation Indexes and Their Applications,” Theoretical Computer Science, vol. 275, pp. 1-68, 2002.
[17] M. Ying, “Reasoning about Probabilistic Sequential Programs in a Probabilistic Logic,” Acta Informatica, vol. 39, pp. 315-389, 2003.
[18] Y. Cao, “A Hierarchy of Behavioral Equivalences in the $\pi$ -Calculus with Noisy Channels,” Computer J., vol. 53, no. 1, pp. 3-20, 2010.
[19] G. Boudol, “Asynchrony and the $\pi$ -Calculus (Note),” INRIA Sophia-Antipolis, Rapport de Recherche 1702, May 1992.
[20] K. Honda and M. Tokoro, “An Object Calculus for Asynchronous Communication,” Proc. European Conf. Object-Oriented Programming (ECOOP '91), pp. 133-147, 1991.
[21] C.E. Shannon, “A Mathematical Theory of Communication, I, II,” Bell System Technical J., vol. 27, pp. 379-423, 623-656, July-Oct. 1948.
[22] K. Honda and N. Yoshida, “On Reduction-Based Process Semantics,” Theoretical Computer Science, vol. 151, no. 2, pp. 437-486, 1995.
[23] K.G. Larsen and A. Skou, “Bisimulation through Probabilistic Testing,” Information and Computation, vol. 94, pp. 1-28, 1991.
[24] A. Giacalone, C. Jou, and S. Smolka, “Algebraic Reasoning for Probabilistic Concurrent Systems,” Proc. IFIP TC2 Working Conf. Programming Concepts and Methods, pp. 453-459, 1990.
[25] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden, “Metrics for Labeled Markov Systems,” Proc. 10th Int'l Conf. Concurrency Theory (CONCUR '99), pp. 258-273, 1999.
[26] F. van Breugel and J. Worrell, “Towards Quantitative Verification of Probabilistic Transition Systems,” Proc. 28th Int'l Colloquium Automata, Languages and Programming (ICALP '01), pp. 421-432, 2001.
[27] Y. Deng, T. Chothia, C. Palamidessi, and J. Pang, “Metrics for Action-Labelled Quantitative Transition Systems,” Electrical Notes in Theoretical Computer Science, vol. 153, no. 2, pp. 79-96, 2006.
[28] S. Tini, “Non Expansive $\epsilon$ -Bisimulations,” Proc. 12th Int'l Conf. Algebric, Methodology and Software Technology (AMAST '08), pp. 362-376, 2008.
[29] S. Tini, “Non-Expansive $\epsilon$ -Bisimulations for Probabilistic Processes,” Theoretical Computer Science, vol. 411, nos. 22-24, pp. 2202-2222, 2010.
[30] M. Ying and M. Wirsing, “Approximate Bisimilarity,” Proc. Eighth Int'l Conf. Algebric, Methodology and Software Technology (AMAST '00), pp. 309-322, 2000.
[31] J. Zhang and Z. Zhu, “A Behavioural Pseudometric Based on $\lambda$ -Bisimilarity,” Electrical Notes in Theoretical Computer Science, vol. 220, no. 3, pp. 115-127, 2008.
[32] J. Zhang and Z. Zhu, “Characterize Branching Distance in Terms of ($\eta$ , $\alpha$ )-Bisimilarity,” Information and Computation, vol. 206, no. 8, pp. 953-965, 2008.
[33] R.M. Amadio, I. Castellani, and D. Sangiorgi, “On Bisimulations for the Asynchronous $\pi$ -Calculus,” Theoretical Computer Science, vol. 195, no. 2, pp. 291-324, 1998.
[34] J. Desharnais, R. Jagadeesan, V. Gupta, and P. Panangaden, “The Metric Analogue of Weak Bisimulation for Probabilistic Processes,” Proc. 17th Ann. IEEE Symp. Logic in Computer Science (LICS '02), pp. 413-422, 2002.
[35] F. van Breugel and J. Worrell, “A Behavioural Pseudometric for Probabilistic Transition Systems,” Theoretical Computer Science, vol. 331, no. 1, pp. 115-142, 2005.
[36] A. Aldini, M. Bravetti, and R. Gorrieri, “A Process-Algebraic Approach for the Analysis of Probabilistic Noninterference,” J. Computer Security, vol. 12, no. 2, pp. 191-245, 2004.
[37] A. Aldini, M. Bravetti, A. Di Pierro, R. Gorrieri, C. Hankin, and H. Wiklicky, “Two Formal Approaches for Approximating Noninterference Properties,” Foundations of Security Analysis and Design II: FOSAD 2001/2002, pp. 1-43, 2004.
[38] A. Girard and G. Pappas, “Approximation Metrics for Discrete and Continuous Systems,” IEEE Trans. Automatic Control, vol. 52, no. 5, pp. 782-798, May 2007.