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

为了增强带测试克林代数(KAT）的表达能力,提出了一种加概率的带测试克林代数(PKAT）的理论,并将其应用于对加概率正则程序的推演。将概率格局变迁系统作为操作语义的模型,它的每个状态是一个格局,格局是由一个PKAT表达式和一个数据状态组成的序列对。为了确立模型中的关系,定义自然语义和结构操作语义,均从行为和状态两方面进行刻画,证明两者在只考虑程序正常终止的情况下是等价的。