Coinductive Proof Principles for Stochastic Processes

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.

• Type: Conference
• Year: 2006
• Where: LICS
• Authors: Dexter Kozen
• Keywords: Computer Science, Explicit Coinduction Principle, LICS 2006, Low-level Analytic Arguments, Recursively-defined Stochastic Processes