Behavioural equivalences of a probabilistic pi-calculus  

作　　者：CHEN WeiEn CAO YongZhi WANG HanPin 

机构地区：[1]Key Laboratory of High Confidence Software Technologies,Ministry of Education of China,Institute of Software,School of Electronics Engineering and Computer Science,Peking University,Beijing 100871,China

出　　处：《Science China(Information Sciences)》2012年第9期2031-2043,共13页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 60973004,61170299,70890080);National Basic Research Program of China (Grant Nos. 2009CB320701,2010CB328103)

摘　　要：Although different kinds of probabilistic π-calculus have been introduced and found their place in quantitative verification and evaluation, their behavioural equivalences still lack a deep investigation. We propose a simple probabilistic extension of the π-calculus, πp, which is inspired by Herescu and Palamidessi＇s probabilistic asynchronous π-calculus. An early semantics of our π-p is presented. We generalise several classic behavioural equivalences to probabilistic versions, obtaining the probabilistic （strong） barbed equivalence and probabilistic bisimulation for πp. Then we prove that the coincidence between the barbed equivalence and bisimilarity in the π-calculus is preserved in the probabilistic setting.Although different kinds of probabilistic π-calculus have been introduced and found their place in quantitative verification and evaluation, their behavioural equivalences still lack a deep investigation. We propose a simple probabilistic extension of the π-calculus, πp, which is inspired by Herescu and Palamidessi＇s probabilistic asynchronous π-calculus. An early semantics of our π-p is presented. We generalise several classic behavioural equivalences to probabilistic versions, obtaining the probabilistic （strong） barbed equivalence and probabilistic bisimulation for πp. Then we prove that the coincidence between the barbed equivalence and bisimilarity in the π-calculus is preserved in the probabilistic setting.

关 键 词：probabilistic pi-calculus behavioural equivalence probabilistic bisimulation probabilistic barbed bisimulation 

分 类 号：O211[理学—概率论与数理统计] O171[理学—数学]