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...

Full description

Saved in:
Bibliographic Details
Published in:Logical methods in computer science 2007-11, Vol.3, Issue 4
Main Author: Kozen, Dexter
Format: Article
Language:English
Subjects:
computer science - logic in computer science
f.3.1
f.4.1
i.1.3
i.2.3
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
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
1860-5974
DOI:10.2168/LMCS-3(4:8)2007