Carroll Morgan and Annabelle McIver
April 1997, 25pp.
We reinterpret the modal mu-calculus {16} to act over expectations rather than predicates, where expectations generalise predicates by taking states into the interval [0,1] rather than the two-point set {0,1}; our interest is in the idioms of the mu-calculus that correspond to operators of temporal logic, in particular in establishing reasoning principles for them.
Our model includes both probabilistic and demonic choice, and the interpretation exploits the characterisation [20] of probabilistic healthiness for expectation transformers to determine the algebraic properties of probabilistic next and thence those of the other probabilistic temporal operators.
The results confirm that many nonprobabilistic temporal axioms have close probabilistic analogues, and that they can indeed be use for quantitive reasoning about probabilistic behaviour. Often the proofs are just generalisations of the original nonprobabilistic versions. In the mu-calculus more generally the new interpretation may be useful for describing 'gambling games' containing demonic, angelic and probablistic choice.
Keywords: Temporal logic, probability, formal semantics, program correctness, weakest precondition. See also A probabilistic temporal calculus based on expectations, PRG Technical Report PRG-TR-13-97.