We generalise the classical notion of stationary distributions of Markov processes to a model of probabilistic programs which includes demonic nondeterminism. As well as removing some of the conditions normally required for stationarity, our generalisation allows the development of a complete theory linking stationary behaviour to long-term average behaviour - the latter being an important property that lies outside the expressive range of standard logics for probabilistic programs.
- Demonic nondeterminism
- Markov decision processes
- Markov process
- Probabilistic program semantics
- Stationary distribution