@inproceedings{63bf355f50ea45eb94882ac19d21a740,

title = "Using probabilistic kleene algebra for protocol verification",

abstract = "We describe pKA, a probabilistic Kleene-style algebra, based on a well known model of probabilistic/demonic computation [3,16,10]. Our technical aim is to express probabilistic versions of Cohen's separation theorems[1]. 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. Algebraic reasoning in general is very robust, and easy to check: thus an algebraic approach to probabilistic distributed systems is attractive because in that {"}doubly hostile{"} environment (probability and interleaving) the opportunities for subtle error abound. Especially tricky is the interaction of probability and the demonic or {"}adversarial{"} scheduling implied by concurrency. Our case study - based on Rabin's Mutual exclusion with bounded waiting [6] - is one where just such problems have already occurred: the original presentation was later shown to have subtle flaws [15]. 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.",

author = "McIver, {A. K.} and E. Cohen and Morgan, {C. C.}",

year = "2006",

doi = "10.1007/11828563_20",

language = "English",

isbn = "3540378731",

volume = "4136 LNCS",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Springer Nature",

pages = "296--310",

booktitle = "Relations and Kleene Algebra in Computer Science - 9th Int. Conf. on Relational Methods in Computer Science and 4th Int. Workshop on Applications of Kleene Algebra, RelMiCS/AKA 2006, Proceedings",

address = "United States",

}