Approximating labelled Markov processes

Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. In this paper, we study approximation techniques for continuous-state labelled Markov processes. We show that the collection of labelled Markov processes carries a Polish-space structure with a countable basis given by finite-state Markov chains with rational probabilities; thus permitting the approximation of quantitative observations (e.g., an integral of a continuous function) of a continuous-state labelled Markov process by the observations on finite-state Markov chains. The primary technical tools that we develop to reach these results are A variant of a finite-model theorem for the modal logic used to characterize bisimulation, and an isomorphism between the poset of Markov processes (ordered by simulation) with the omega-continuous dcpo Proc (defined as the solution of the recursive domain equation Proc = Pi(L) P-Pr(Proc)). The isomorphism between labelled Markov processes and Proc can be independently viewed as a full-abstraction result relating an operational (labelled Markov process) and a denotational (Proc) model and yields a logic complete for reasoning about simulation for continuous-state processes. (C) 2003 Elsevier Science (USA). All rights reserved.