Algebraic reasoning for probabilistic action systems and while-loops

Meinicke, Larissa and Hayes, Ian J. (2008) Algebraic reasoning for probabilistic action systems and while-loops. Acta Informatica, 45 5: 321-382. doi:10.1007/s00236-008-0073-4

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

Author Meinicke, Larissa
Hayes, Ian J.
Title Algebraic reasoning for probabilistic action systems and while-loops
Journal name Acta Informatica   Check publisher's open access policy
ISSN 0001-5903
Publication date 2008-07-01
Sub-type Article (original research)
DOI 10.1007/s00236-008-0073-4
Open Access Status
Volume 45
Issue 5
Start page 321
End page 382
Total pages 62
Place of publication Berlin, Germany
Publisher Springer
Language eng
Subject C1
890299 Computer Software and Services not elsewhere classified
080309 Software Engineering
Abstract Back and von Wright have developed algebraic laws for reasoning about loops in a total correctness framework using the refinement calculus. We extend their work to reasoning about probabilistic loops in the probabilistic refinement calculus. We apply our algebraic reasoning to derive transformation rules for probabilistic action systems and probabilistic while-loops. In particular we focus on developing data refinement rules for these two constructs. Our extension is interesting since some well known transformation rules that are applicable to standard programs are not applicable to probabilistic ones: we identify some of these important differences and we develop alternative rules where possible.
Q-Index Code C1
Q-Index Status Confirmed Code
Institutional Status UQ

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 3 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 17 Apr 2009, 04:30:13 EST by Ms Kimberley Nunes on behalf of School of Information Technol and Elec Engineering