Dexter Kozen. Coinductive proof principles for stochastic processes. Logical Methods in Computer Science, 3(4:8), 2007. DOI: 10.2168/LMCS-3 (4:8) 2007.

We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.