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 |
| _version_ | 1797268785283989504 |
|---|---|
| author | Dexter Kozen |
| author_facet | Dexter Kozen |
| author_sort | Dexter Kozen |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:38:00Z |
| format | Article |
| id | doaj.art-b5afb381591b4749abeb99cb92ee23c4 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:38:00Z |
| publishDate | 2007-11-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b5afb381591b4749abeb99cb92ee23c42024-03-08T08:49:28ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742007-11-01Volume 3, Issue 410.2168/LMCS-3(4:8)20071098Coinductive Proof Principles for Stochastic ProcessesDexter Kozenhttps://orcid.org/0000-0002-8007-4725We 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.https://lmcs.episciences.org/1098/pdfcomputer science - logic in computer sciencef.4.1f.3.1i.1.3i.2.3 |
| spellingShingle | Dexter Kozen Coinductive Proof Principles for Stochastic Processes Logical Methods in Computer Science computer science - logic in computer science f.4.1 f.3.1 i.1.3 i.2.3 |
| title | Coinductive Proof Principles for Stochastic Processes |
| title_full | Coinductive Proof Principles for Stochastic Processes |
| title_fullStr | Coinductive Proof Principles for Stochastic Processes |
| title_full_unstemmed | Coinductive Proof Principles for Stochastic Processes |
| title_short | Coinductive Proof Principles for Stochastic Processes |
| title_sort | coinductive proof principles for stochastic processes |
| topic | computer science - logic in computer science f.4.1 f.3.1 i.1.3 i.2.3 |
| url | https://lmcs.episciences.org/1098/pdf |
| work_keys_str_mv | AT dexterkozen coinductiveproofprinciplesforstochasticprocesses |