Using Probabilistic Kleene Algebra pKA for Protocol Verification

We propose a method for verification of probabilistic distributed systems in which a variation of Kozen’s Kleene Algebra with Tests [11] is used to take account of the well-known interaction of probability and “adversarial ” scheduling [17]. We describe pKA, a probabilistic Kleene-style algebra, based on a widely ac-cepted model of probabilistic/demonic computation [7,25,17]. Our technical aim is to express probabilistic versions of Cohen’s separation theorems[4]. Separation theorems simplify reasoning about distributed systems, where with purely algebraic reasoning they can reduce complicated interleaving behaviour to “separated ” behaviours each of which can be analysed on its own. Until now that has not been possible for probabilistic distributed systems. We present two case studies. The first treats a simple voting mechanism in the algebraic style, and the second — based on Rabin’s Mutual exclusion with bounded waiting [12] — is one where verification problems have already occurred: the original presentation was later shown to have subtle flaws [24]. It motivates our interest in algebras, where assumptions relating probability and secrecy are clearly exposed and, in some cases, can be given simple characterisations in spite of their intricacy. Finally we show how the algebraic proofs for these theorems can be automated using a modification of Kozen and Aboul-Hosn’s KAT-ML [3]