概率带测试克林代数操作语义的研究  

Research on the Operational Semantics of Probabilistic Kleene Algebra with Test

作　　者：乔瑞[1] 高新岩[1] 

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

出　　处：《武汉理工大学学报（信息与管理工程版）》2008年第4期509-513,共5页Journal of Wuhan University of Technology：Information & Management Engineering

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

摘　　要：为了增强带测试克林代数(KAT)的表达能力,提出了一种加概率的带测试克林代数(PKAT)的理论,并将其应用于对加概率正则程序的推演。将概率格局变迁系统作为操作语义的模型,它的每个状态是一个格局,格局是由一个PKAT表达式和一个数据状态组成的序列对。为了确立模型中的关系,定义自然语义和结构操作语义,均从行为和状态两方面进行刻画,证明两者在只考虑程序正常终止的情况下是等价的。To improve the expressiveness of Kleene algebra with tests （KAT）, a complete theory of probabilistic Kleene algebra with tests （PKAT） for reasoning about regular programs with probability was presented. A model termed probabilistic configuration transition systems was proposed, whose states are composed of a pair of a PKAT expression and a data-state. To determine the transition relation in the model, both natural semantics and structural operational semantics for PKAT were put forward. The results prove that the two are equivalent when proper termination was considered.

关 键 词：概率带测试克林代数 概率格局变迁系统 自然语义 结构操作语义 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]