Complete Proof Systems for Amortised Probabilistic Bisimulations  

作　　者：Li-Li Xu Hui-Min Lin 

机构地区：[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]Ecole P olytechnique, P alaiseau 91120, France

出　　处：《Journal of Computer Science & Technology》2016年第2期300-316,共17页计算机科学技术学报（英文版）

基　　金：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.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.

关 键 词：AXIOMATIZATION probabilistic calculus for communication systems （CCS） probabilistic automata amortisedbisimulation 

分 类 号：TP273[自动化与计算机技术—检测技术与自动化装置] TP301.6[自动化与计算机技术—控制科学与工程]