Carroll Morgan and Annabelle McIver
April 1997, 20pp.
Generalising Boolean-valued predicates to expectations --- functions from the state space into [0,1] --- allows the definition of probabilistic temporal operators that treat explicit probabilities as well as demonic nondeterminism and divergence.
The conventional operational interpretation of the temporal operators does not generalise so easily: although one may speak of "satisfying a predicate" in the standard case, it is not meaningful to "satisfy an expectation". That difficulty is avoided by giving the operational interpretation of the operators for the probabilistic case in terms of various kinds of gambling game.