Probabilistic Modal Kleene Algebra and Hoare-Style Logic

Modal Kleene algebras (MKA) formalize the behavior of regular programs. However, MKA is incapable of verifying regular programs with probabilistic information, which have richer and more powerful expressiveness than normal regular programs. We define an extension of MKA, called probabilistic modal Kleene algebra (PMKA) for verifying the regular programs with probability in a purely algebraic approach. We give relational semantics for the regular programs with probability. Then, we modify the existent probabilistic Hoare-style logic in some sort to a proof system named PHL_np for probabilistic regular programs without iteration, and prove the soundness of the modified system in terms of the relational semantics. At last, we show that PHL_np is subsumed by PMKA.