Reasoning about efficiency within a probabilistic μ-calculus

Research output: Contribution to journalArticlepeer-review

3 Citations (Scopus)


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 languageEnglish
Pages (from-to)138-155
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 1999
Externally publishedYes


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


Dive into the research topics of 'Reasoning about efficiency within a probabilistic μ-calculus'. Together they form a unique fingerprint.

Cite this