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

Research on the Operational Semantics of Probabilistic Kleene Algebra with Test

为了增强带测试克林代数(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.