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 in PKAT was established. The soundness of the equations of PKAT was validated with respect to the bisimulation.
