## 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 | China |

City | Tianjin |

Period | 29/07/09 → 31/07/09 |