21st Annual IEEE Symposium on Logic in Computer Science (LICS'06)
Coinductive Proof Principles for Stochastic Processes
Seattle, Washington
August 12-August 15
ISBN: 0-7695-2631-4
We give an explicit coinduction principle for recursivelydefined 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.