概率带测试克林代数

Probabilistic Kleene Algebra with Tests

为了增强可形式刻画正则程序行为的带测试克林代数(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...