This paper presents a fundamental study of similarity and bisimilarity for labelled Markov processes. The main results characterize similarity as a testing preorder and bisimilarity as a testing equivalence. In general, labelled Markov processes are not required to satisfy a finite-branching condition -- indeed the state space may be a continuum, with the transitions given by arbitrary probability measures. Nevertheless we show that to characterize bisimilarity it suffices to use finitely-branching labelled trees as tests. Our results involve an interaction between domain theory and measure theory. One of the main technical contributions is to show that a final object in a suitable category of labelled Markov processes can be constructed by solving a domain equation D = V(D)Act, where V is the probabilistic powerdomain. Given a labelled Markov process whose state space is an analytic space, bisimilarity arises as the kernel of the unique map to the final labelled Markov process. We also show that the metric for approximate bisimilarity introduced by Desharnais, Gupta, Jagadeesan and Panangaden generates the Lawson topology on the domain D.
Theoretical Computer Science 333(1-2), 2005. 32 pages.
PostScript /
PDF
© 2004 Elsevier B.V.