Refinement Algebra for Probabilistic Programs
2010 (English)In: Formal Aspects of Computing, ISSN 0934-5043, E-ISSN 1433-299X, Vol. 22, no 1, 3-31 p.Article in journal (Refereed) Published
We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.
Place, publisher, year, edition, pages
London: Springer International , 2010. Vol. 22, no 1, 3-31 p.
IdentifiersURN: urn:nbn:se:uu:diva-119862DOI: 10.1007/s00165-009-0111-1ISI: 000273979400002OAI: oai:DiVA.org:uu-119862DiVA: diva2:301075