Authors: Dexter Kozen

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.

• 03B70 - Logic in computer science
• 60G07 - General theory of stochastic processes
• 68Q60 - Specification and verification (program logics, model checking, etc.)