›› 2016, Vol. 31 ›› Issue (2): 300-316.doi: 10.1007/s11390-016-1628-4

Special Issue: Theory and Algorithms

• Theory and Algorithms • Previous Articles     Next Articles

Complete Proof Systems for Amortised Probabilistic Bisimulations

Li-Li Xu(许丽丽)1,2,3, and Hui-Min Lin(林惠民)1, Fellow, CCF   

  1. 1 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;
    2 University of Chinese Academy of Sciences, Beijing 100049, China;
    3 École Polytechnique, Palaiseau 91120, France
  • Received:2014-09-17 Revised:2015-03-20 Online:2016-03-05 Published:2016-03-05
  • About author:Li-Li Xu received her B.S. degree in computer science and technology from Xiamen University, Xiamen, in 2008, and her Ph.D. degree in computer software and theory from the University of Chinese Academy of Sciences (CAS), Beijing, in 2015. She was selected by the 2011 Joint Doctoral Promotion Program between the CAS, and the French National Institute for Research in Computer Science and Control (INRIA). She is now an assistant professor in the Institute of Information Engineering, CAS, Beijing.
  • Supported by:

    This work was supported by the National Natural Science Foundation of China under Grant No. 60833001.

The notion of amortisation has been integrated in quantitative bisimulations to make long-term behavioral comparisons between nondeterministic systems. In this paper, we present sound and complete proof systems for amortised strong probabilistic bisimulation and its observational congruence on a process algebra with probability and nondeterminism, and prove their soundness and completeness. Our results make it possible to reason about long-term (observable) probabilistic behaviors by syntactic manipulations.

[1] Milner R. Communication and Concurrency. Upper Saddle River, NJ, USA: Prentice Hall, 1989.

[2] Lin H. PAM: A process algebra manipulator. Formal Methods in System Design, 1995, 7(3): 243-259.

[3] Larsen K G, Skou A. Bisimulation through probabilistic testing. Information and Computation, 1991, 94(1): 1-28.

[4] Kiehn A, Arun-Kumar S. Amortised bisimulations. In Proc. the 25th FORTE, Oct. 2005, pp.320-334.

[5] de Frutos-Escrig D, Rosa-Velardo F, Gregorio-Rodríguez C. New bisimulation semantics for distributed systems. In Proc. the 27th FORTE, June 2007, pp.143-159.

[6] Xu L, Chatzikokolakis K, Lin H. Metrics for differential privacy in concurrent systems. In Proc. the 34th FORTE, June 2014, pp.199-215.

[7] Dwork C. Differential privacy. In Proc. the 33rd ICALP, July 2006, pp.1-12.

[8] Chatzikokolakis K, Andrés M E, Bordenabe N E, Palamidessi C. Broadening the scope of differential privacy using metrics. In Proc. the 13th Int. Symp. Privacy Enhancing Technologies, July 2013, pp.82-102.

[9] Bandini E, Segala R. Axiomatizations for probabilistic bisimulation. In Proc. the 28th ICALP, July 2001, pp.370- 381.

[10] Hennessy M. A calculus for costed computations. Logical Methods in Computer Science, 2011, 7(1): 7:1-7:35.

[11] Deng Y, Hennessy M. Compositional reasoning for weighted Markov decision processes. Science of Computer Programming, 2013, 78(12): 2537-2579.

[12] Desharnais J, Laviolette F, Tracol M. Approximate analysis of probabilistic processes: Logic, simulation and games. In Proc. the 5th International Conference on Quantitative Evaluation of Systems, Sept. 2008, pp.264-273.

[13] Tracol M, Desharnais J, Zhioua A. Computing distances between probabilistic automata. In Proc. the 9th QAPL, April 2011, pp.148-162.

[14] Deng Y, Palamidessi C, Pang J. Compositional reasoning for probabilistic finite-state behaviors. In Lecture Notes in Computer Science 3838, Middeldorp A, van Oostrom V, van Raamsdonk F, de Vrijer (eds.), Spring-Verlag, 2005, pp.309–337.

[15] Deng Y, Palamidessi C. Axiomatizations for probabilistic finite-state behaviors. In Proc. the 8th FoSSaCS, April 2005, pp.110–124.

[16] Segala R. Modeling and verification of randomized distributed real-time systems [Ph.D. Thesis]. Massachusetts Institute of Technology, 1995.

[17] Segala R, Lynch N. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 1995, 2(2): 250-273.

[18] Hennessy M, Lin H. Proof systems for message-passing process algebras. In Proc. the 4th CONCUR, August 1993, pp.202-216.

[19] Desharnais J, Jagadeesan R, Gupta V, Panangaden P. The metric analogue of weak bisimulation for probabilistic processes. In Proc. the 17th LICS, July 2002, pp.413-422.

[20] D'Argenio P R, Gebler D, Lee M D. Axiomatizing bisimulation equivalences and metrics from probabilistic SOS rules. In Proc. the 17th FoSSaCS, April 2014, pp.289-303.

[21] Chatzikokolakis K, Gebler D, Palamidessi C, Xu L. Generalized bisimulation metrics. In Proc. the 25th CONCUR, Sept. 2014, pp.32-46.
No related articles found!
Full text



[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Chen Shihua;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] Chen Zhaoxiong; Gao Qingshi;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] Huang Heyan;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Zhang Bo; Zhang Ling;. Statistical Heuristic Search[J]. , 1987, 2(1): 1 -11 .
[10] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved