Programming Research Group
Technical Report TR-13-97
A probabilistic temporal calculus based on expectations
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.
- Keywords:
- Temporal logic, probability, formal
semantics, program correctness, weakest precondition.
See also An expectation-transformer model for probabilistic
temporal logic , PRG Technical Report
PRG-TR-20-97.
This paper is available as a 105,895 byte
gzipped PostScript file.
|
![[Oxford Spires]](/im/spires.gif){kind=small}
oucl