Finite Axiomatization for Symbolic Probabilistic π-Calculus  

作　　者：宋磊 邓玉欣 

机构地区：[1]Department of Computer Science and Engineering,Shanghai Jiaotong University

出　　处：《Journal of Shanghai Jiaotong university(Science)》2009年第5期536-541,共6页上海交通大学学报（英文版）

基　　金：the National Basic Research Program (973) of China (No.2003CB317005);the National Nature Science Foundation of China (Nos.60573002 and 60703033)

摘　　要：This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu,Palamidessi and Lin.We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness.This is the first work,to our knowledge,that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.This paper focuses on the problem of seeking complete axiomatization for finite processes in the process calculus called symbolic probabilistic π-calculus introduced by Wu, Palamidessi and Lin. We provide inference systems for both strong and weak symbolic probabilistic bisimulations and also prove their soundness and completeness. This is the first work, to our knowledge, that provides complete axiomatization for symbolic probabilistic bisimulations in the presence of both nondeterministic and probabilistic choice.

关 键 词：probabilistic process calculus AXIOMATIZATION symbolic bisimulation 

分 类 号：O1-0[理学—数学] TP301.6[理学—基础数学]