Coinductive Proof Principles for Stochastic Processes
Logic in Computer Science
2015-07-01 v2
Abstract
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.
Cite
@article{arxiv.0711.0194,
title = {Coinductive Proof Principles for Stochastic Processes},
author = {Dexter Kozen},
journal= {arXiv preprint arXiv:0711.0194},
year = {2015}
}
Comments
16 pages, 2 figures. Preliminary version appeared in: Rajeev Alur, ed., Proc. 21st Symp. Logic in Computer Science (LICS'06), pages 359-366. IEEE, August 2006