Operational semantics of probabilistic Kleene algebra with tests

Kleene algebra with tests (KAT) is a prominent specification language used for formalizing the behavior of non-deterministic structured programs generally called regular programs. Regular programs with probabilistic information have richer and more powerful expressiveness than normal regular programs. However, KAT is incapable of specifying such recently widely used programs. We construct a complete theory of probabilistic Kleene algebra with tests (PKAT) for reasoning about regular programs with probability. We offer a model termed probabilistic configuration transition systems, whose states are configurations composed of a pair of a PKAT expression and a data-state. To determine the transition relation in the model, we define an operational semantics for PKAT, and establish a probabilistic bisimulation equivalence relation in PKAT. The soundness of the equations of PKAT is validated with respect to the bisimulation, to find equivalences without calculating the actual bisimulation relation.