Abstract

Dexter Kozen: Coinductive Proof Principles for Stochastic Processes

Coinduction (or "baseless induction") has been shown to be a useful tool in functional programming. Streams, automata, concurrent and stochastic processes, and recursive types have been successfully analyzed using coinductive methods.

Most approaches emphasize the relationship between coinduction and bisimulation. There is a coinduction principle that states that under certain conditions, two bisimilar processes must be equal. For example, to prove the equality of infinite streams s=merge(split(s)), where merge and split satisfy the familiar coinductive definitions

merge(a::s,t) = a::merge(t,s)

#1(split(a::b::r)) = a::#1(split(r))

#2(split(a::b::r)) = b::#2(split(r)),

it suffices to show that the two streams are bisimilar. An alternative view is that certain systems of recursive equations over a certain algebraic structure have unique solutions.

Desharnais et al. (2002,2004) study bisimulation in a probabilistic context. They are primarily interested in the approximation of one process with another. Again, they focus on bisimulation, but do not formulate an explicit coinduction rule.

In this talk I will describe an explicit coinduction principle for recursively-defined stochastic processes and dynamical systems. I will illustrate the use of the rule in deriving some properties of a simple coin-flip process.