Complete Proof Systems for Amortised Probabilistic Bisimulations

作     者：Li-Li Xu Hui-Min Lin 

作者机构：State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing 100190 China University of Chinese Academy of Sciences Beijing 100049 China Ecole P olytechnique P alaiseau 91120 France 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2016年第31卷第2期

页      面：300-316页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0802[工学-机械工程] 080201[工学-机械制造及其自动化] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

主　　题：axiomatization probabilistic calculus for communication systems (CCS) probabilistic automata amortisedbisimulation 

摘      要：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.