BiGKAT: an algebraic framework for relational verification of probabilistic programs

This work is devoted to formal reasoning on relational properties of probabilistic imperative programs. Relational properties are properties which relate the execution of two programs (possibly the same one) on two initial memories. We aim at extending the algebraic approach of Kleene Algebras with Tests (KAT) to relational properties of probabilistic programs. For that we consider the approach of Guarded Kleene Algebras with Tests (KAT), which can be used for representing probabilistic programs, and define a relational version of it, called Bi-guarded Kleene Algebras with Tests (BiGKAT). We show that the setting of BiGKAT is expressive enough to interprete probabilistic Relational Hoare Logic (pRHL), a program logic that has been introduced in the literature for the verification of relational properties of probabilistic programs