Paper: Coinductive Proof Principles for Stochastic Processes (at LICS 2006)

Authors: Dexter C. Kozen

Abstract

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.

BibTeX

  @InProceedings{Kozen-CoinductiveProofPri,
    author = 	 {Dexter C. Kozen},
    title = 	 {Coinductive Proof Principles for Stochastic Processes},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {359--366},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }