Reasoning about efficiency within a probabilistic μ-calculus
<p>Expectation-based probabilistic predicate transformers [15] provide a logic for probabilistic sequential programs, giving access to expressions such as &apos;the probability that predicate <em>A</em> is achieved finally&apos;. Using expectations more generally ho...
| Main Author: | |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
1999
|
| Subjects: |
| Summary: | <p>Expectation-based probabilistic predicate transformers [15] provide a logic for probabilistic sequential programs, giving access to expressions such as &apos;the probability that predicate <em>A</em> is achieved finally&apos;. 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.</p> |
|---|