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 high...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2007-11-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1098/pdf |
| Summary: | 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. |
|---|---|
| ISSN: | 1860-5974 |