Probabilistic Choice in Refinement Algebra

Meinicke, L. and Hayes, I. J. (2008). Probabilistic Choice in Refinement Algebra. In: P. Audebaud and C. Paulin-Mohring, Lecture Notes in Computer ScienceProceedings of the 9th international conference on Mathematics of Program Construction. 9th International Conference on Mathematics of Program Construction [MPC], Marseille, France, (243-267). 15-18 July 2008. doi:10.1007/978-3-540-70594-9_14

Attached Files (Some files may be inaccessible until you login with your UQ eSpace credentials)
Name Description MIMEType Size Downloads

Author Meinicke, L.
Hayes, I. J.
Title of paper Probabilistic Choice in Refinement Algebra
Conference name 9th International Conference on Mathematics of Program Construction [MPC]
Conference location Marseille, France
Conference dates 15-18 July 2008
Proceedings title Lecture Notes in Computer ScienceProceedings of the 9th international conference on Mathematics of Program Construction   Check publisher's open access policy
Journal name Mathematics of Program Construction, Proceedings   Check publisher's open access policy
Place of Publication Berlin, Heidelberg
Publisher Springer Verlag
Publication Year 2008
Sub-type Fully published paper
DOI 10.1007/978-3-540-70594-9_14
Open Access Status
ISBN 9783540705932
3540705937
ISSN 0302-9743
Editor P. Audebaud
C. Paulin-Mohring
Volume 5133
Start page 243
End page 267
Total pages 25
Collection year 2009
Language eng
Abstract/Summary 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.
Subjects E1
890299 Computer Software and Services not elsewhere classified
080309 Software Engineering
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ

 
Versions
Version Filter Type
Citation counts: TR Web of Science Citation Count  Cited 3 times in Thomson Reuters Web of Science Article | Citations
Scopus Citation Count Cited 2 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 17 Apr 2009, 10:34:14 EST by Ms Kimberley Nunes on behalf of School of Information Technol and Elec Engineering