### Abstract

Expectation-based probabilistic predicate transformers [15] provide a logic for probabilistic sequential programs, giving access to expressions such as 'the probability that predicate A is achieved finally'. Using expectations more generally however, we can express μ-calculus formulae for the expected path-length of a computation tree. Moreover within an expectation-based μ-calculus such efficiency measures and more conventional (but probabilistic) temporal operators [14] can be related. This paper reports work carried out within a project supported by the EPSRC, whose other members are Carroll Morgan and Jeff Sanders. In particular Def. 3.1 was originally suggested by Carroll Morgan in the general context of probabilistic and nondeterministic programs.

Original language | English |
---|---|

Pages (from-to) | 138-155 |

Number of pages | 18 |

Journal | Electronic Notes in Theoretical Computer Science |

Volume | 22 |

DOIs | |

Publication status | Published - 1999 |

Externally published | Yes |

### Keywords

- Imperative programming
- Nondeterminism
- Predicate transformers
- Probabilistic semantics
- Refinement
- Time efficiency, complexity
- Verification