Approximating Continuous Markov Processes

Josee Desharnais, Vineet Gupta, Radha Jagadeesan, Prakash Panangaden

Abstract

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are

A finite-model theorem for the modal logic used to characterize bisimulation
A categorical equivalence between the category of Markov processes (with simulation morphisms) with the omega-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc = ∏_(Labels) P_(Prob)(Proc), where P_(Prob)(D) is the probabilistic powerdomain of Jones and Plotkin.

The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.

@InProceedings{approx-lics2000,
  title =        "Approximating Continuous Markov Processes",
  author =       "Josee Desharnais and Vineet Gupta and Radha
Jagadeesan and Prakash Panangaden"
  booktitle =    "Proceedings, Fifteenth Annual {IEEE} Symposium on Logic in
                 Computer Science",
  year =         "2000",
  pages =	 "95-106",
  address =      "Santa Barbara, USA",
  organization = "IEEE Computer Society Press"
}

Postscript file of extended abstract (220K)