## Domain theory, testing and simulation for labelled Markov
processes

*Franck van Breugel*,
*Michael W. Mislove*,
*Joël
Ouaknine*, and
*James Worrell*
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.

Imprint / Data Protection