Algebraic reasoning for probabilistic action systems and while-loops

Larissa Meinicke*, Ian J. Hayes

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)321-382
Number of pages62
JournalActa Informatica
Issue number5
Publication statusPublished - Jul 2008

Cite this