Refinement algebra with explicit probabilism

T. M. Rabehaja, J. W. Sanders

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

1 Citation (Scopus)

Abstract

Refinement algebra provides axioms for the stepwise removal of abstraction, in the form of demonic nondeterminism, in a first-order system that supports reasoning about loops. It has been extended by Solin and Meinecke to computations involving implicit probabilistic choices: demonic nondeterminismthen satisfies weaker properties. In this paper their axiom system is extended to capture explicit probabilistic choices. The first form is an unquantified probabilistic choice; the second is a partial quantified probabilistic choice (from which the usual binary probabilistic choice can be recovered). The new refinement algebra is sound with respect to 1-bounded expectation transformers, the premier model of probabilistic computations, but also with respect to a new model introduced here to capture more directly partial quantified computations. In this setting a 'normal form' result of Kozen is proved, replacing multiple loops with a single loop that does the same job; and the extent to which the two forms of loop have the same expected number of steps to termination is considered. Being entirely first-order, the new refinement algebra is targetted to automation.

Original languageEnglish
Title of host publication2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
Subtitle of host publicationProceedings
Place of PublicationPiscataway, NJ
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages63-70
Number of pages8
ISBN (Print)9780769537573
DOIs
Publication statusPublished - 2009
Externally publishedYes
Event2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 - Tianjin, China
Duration: 29 Jul 200931 Jul 2009

Other

Other2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009
CountryChina
CityTianjin
Period29/07/0931/07/09

Fingerprint Dive into the research topics of 'Refinement algebra with explicit probabilism'. Together they form a unique fingerprint.

Cite this