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 language | English |
---|---|
Title of host publication | 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 |
Subtitle of host publication | Proceedings |
Place of Publication | Piscataway, NJ |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Pages | 63-70 |
Number of pages | 8 |
ISBN (Print) | 9780769537573 |
DOIs | |
Publication status | Published - 2009 |
Externally published | Yes |
Event | 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 - Tianjin, China Duration: 29 Jul 2009 → 31 Jul 2009 |
Other
Other | 2009 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2009 |
---|---|
Country/Territory | China |
City | Tianjin |
Period | 29/07/09 → 31/07/09 |