TY - GEN
T1 - Probabilistic choice in refinement algebra
AU - Meinicke, Larissa
AU - Hayes, Ian J.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=48949096614&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-70594-9_14
DO - 10.1007/978-3-540-70594-9_14
M3 - Conference proceeding contribution
AN - SCOPUS:48949096614
SN - 3540705937
SN - 9783540705932
VL - 5133 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 243
EP - 267
BT - Mathematics of Program Construction - 9th International Conference, MPC 2008, Proceedings
A2 - Audebaud, Philippe
A2 - Paulin-Mohring, Christine
T2 - 9th International Conference on Mathematics of Program Construction, MPC 2008
Y2 - 15 July 2008 through 18 July 2008
ER -