Using probabilistic kleene algebra for protocol verification

A. K. McIver*, E. Cohen, C. C. Morgan

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

22 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationRelations 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
Place of PublicationBerlin; New York
PublisherSpringer, Springer Nature
Pages296-310
Number of pages15
Volume4136 LNCS
ISBN (Electronic)9783540378747
ISBN (Print)3540378731, 9783540378730
DOIs
Publication statusPublished - 2006
Event9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra, RelMiCS/AKA 2006 - Manchester, United Kingdom
Duration: 29 Aug 20062 Sep 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4136 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International Conference on Relational Methods in Computer Science and 4th International Workshop on Applications of Kleene Algebra, RelMiCS/AKA 2006
CountryUnited Kingdom
CityManchester
Period29/08/062/09/06

Fingerprint

Dive into the research topics of 'Using probabilistic kleene algebra for protocol verification'. Together they form a unique fingerprint.

Cite this