概率带测试克林代数  

Probabilistic Kleene Algebra with Tests

作　　者：乔瑞 吴尽昭 

机构地区：[1]中国科分院成都计算机应用研究所,四川成都610041

出　　处：《四川大学学报（工程科学版）》2009年第1期134-138,共5页Journal of Sichuan University (Engineering Science Edition)

基　　金：国家973计划资助项目(2004CB318000;2007CB310800);国家高技术发展计划(863计划)资助项目(2007AA01Z143)

摘　　要：为了增强可形式刻画正则程序行为的带测试克林代数(KAT)的表达能力,提出了一个加概率的带测试克林代数(PKAT)的完整理论用于对加概率正则程序的推演。提出了状态为PKAT表达式和数据状态组成的序列对的概率格局变迁系统。然后在概率格局变迁系统的基础上给出结构操作语义。并给出PKAT的基于操作语义的概率互模拟等价关系。最后证明了PKAT中等式关于互模拟等价的可靠性。In order to improve the expressiveness of Kleene algebra with tests(KAT),which formalizes the behavior of regular programs,a complete theory of probabilistic Kleene algebra with tests(PKAT) for reasoning regular programs with probability was proposed.A model termed probabilistic configuration transition systems was proposed,which are composed of a pair of a PKAT expression and a data-state.Operational semantics for PKAT based on the model was put forward,and a probabilistic bisimulation equivalence relation...

关 键 词：概率带测试克林代数 概率格局变迁系统 结构操作语义 互模拟等价 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]