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 [Dexter Kozen, Kleene algebra with tests, ACM Trans. Programming Lang. Syst. 19(3) (1997) 427–443] is used to take account of the well known interaction of probability and “adversarial” scheduling [Annabelle McIver, Carroll Morgan, Abstraction, Refinement and Proof for Probabilistic Systems, Technical Monographs in Computer Science, Springer-Verlag, New York, 2004]. We describe pKA, a probabilistic Kleene-style algebra, based on a widely accepted model of probabilistic/demonic computation [Jifeng He, K. Seidel, A.K. McIver, Probabilistic models for the guarded command language, Sci. Comput. Programming 28 (1997) 171–192; Roberto Segala, Modeling and verification of randomized distributed real-time systems, Ph.D. thesis, MIT, 1995; Roberto Segala, Modeling and Verification of Randomized Distributed Real-Time Systems, PhD thesis, MIT, 1995; Annabelle McIver, Carroll Morgan, Abstraction, Refinement and Proof for Probabilistic Systems, Technical Monographs in Computer Science, Springer-Verlag, New York, 2004]. Our technical aim is to express probabilistic versions of Cohen’s separation theorems [E. Cohen, Separation and reduction, in: Mathematics of Program Construction, 5th International Conference, LNCS, vol. 1837, Springer-Verlag, July 2000, pp. 45–59]. 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 [Eyal Kushilevitz, M.O. Rabin, Randomized mutual exclusion algorithms revisited, in: Proceedings of the 11th Annual ACM Symposium on Principles of Distributed Computing, 1992, pp. 275–283]—is one where verification problems have already occurred: the original presentation [M.O. Rabin, N-process mutual exclusion with bounded waiting by 4 log 2n-valued shared variable, Journal of Computer and System Sciences, 25(1) (1982) 66–75] was later shown to have subtle flaws [I. Saias, Proving probabilistic correctness statements: the case of Rabin’s algorithm for mutual exclusion, in: Proceedings of the 11th Annual ACM Symposium on Principles of Distributed Computing, 1992]. 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 Aboul-Hosn and Kozen’s KAT-ML [Kamal Aboul-Hosn, Dexter Kozen, KAT-ML: An interactive theorem prover for Kleene algebra with tests, J. Appl. Non-Classical Logics 1 (2006)].22 page(s