Logic in Computer Science (LICS 2000)

Paper: Approximating Labeled Markov Processes (at LICS 2000)

Authors: Josée Desharnais Prakash Panangaden Radha Jagadeesan Vineet Gupta

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 w-continuous dcpo Proc , defined as the solution of the recursive domain equation Proc = ?Labels PProb ( Proc )1.The correspondence between labeled Markov processes and Proc yields logic complete for reasoning about simulation for continuous-state processes.

BibTeX

  @InProceedings{DesharnaisPanangade-ApproximatingLabele,
    author = 	 {Josée Desharnais and Prakash Panangaden and Radha Jagadeesan and Vineet Gupta},
    title = 	 {Approximating Labeled Markov Processes},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {95--106},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }