Probabilistic choice in refinement algebra

Larissa Meinicke*, Ian J. Hayes

*Corresponding author for this work

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

3 Citations (Scopus)


The term refinement algebra refers to a set of abstract algebras, similar to Kleene algebra with tests, that are suitable for reasoning about programs in a total-correctness framework. Abstract algebraic reasoning also works well when probabilistic programs are concerned, and a general refinement algebra that is suitable for such programs has been defined previously. That refinement algebra does not contain features that are specific to probabilistic programs. For instance, it does not include a probabilistic choice operator, or probabilistic assertions and guards (tests), which may be used to represent correctness properties for probabilistic programs. In this paper we investigate how these features may be included in a refinement algebra. That is, we propose a new refinement algebra in which probabilistic choice, and probabilistic guards and assertions may be expressed. Two operators for modelling probabilistic enabledness and termination are also introduced.

Original languageEnglish
Title of host publicationMathematics of Program Construction - 9th International Conference, MPC 2008, Proceedings
EditorsPhilippe Audebaud, Christine Paulin-Mohring
Number of pages25
Volume5133 LNCS
Publication statusPublished - 2008
Event9th International Conference on Mathematics of Program Construction, MPC 2008 - Marseille, France
Duration: 15 Jul 200818 Jul 2008

Publication series

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


Other9th International Conference on Mathematics of Program Construction, MPC 2008


Dive into the research topics of 'Probabilistic choice in refinement algebra'. Together they form a unique fingerprint.

Cite this