We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in $O(n^3 \log n)$ time via a generic partition refinement algorithm.

翻译：我们引入概率保护型带测试克林代数（ProbGKAT），这是GKAT的一种扩展，允许对具有概率分支的无解释命令式程序进行推理。我们通过一类特殊的概率自动机给出其操作语义。我们给出了ProbGKAT表达式双相似性的一个完备且可靠的Salomaa式公理化体系。最后，我们证明ProbGKAT表达式的双相似性可通过通用分区细化算法在$O(n^3 \log n)$时间内判定。