Approximating labelled Markov processes

AbstractLabelled 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 ω-continuous dcpo Proc (defined as the solution of the recursive domain equation Proc=∏LPPr(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