Domain theory, testing and simulation for labelled Markov processes

Resource type
Authors/contributors
Title
Domain theory, testing and simulation for labelled Markov processes
Abstract
This paper presents a fundamental study of similarity and bisimilarity for labelled Markov processes (LMPs). The main results characterize similarity as a testing preorder and bisimilarity as a testing equivalence. In general, LMPs 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 LMPs can be constructed by solving a domain equation D≅V(D)Act, where V is the probabilistic powerdomain. Given an LMP whose state space is an analytic space, bisimilarity arises as the kernel of the unique map to the final LMP. We also show that the metric for approximate bisimilarity introduced by Desharnais, Gupta, Jagadeesan and Panangaden generates the Lawson topology on the domain D.
Publication
Theoretical Computer Science
Volume
333
Issue
1
Pages
171-197
Date
March 1, 2005
Series
Foundations of Software Science and Computation Structures
Journal Abbr
Theoretical Computer Science
Language
en
DOI
10/ft9vc5
ISSN
0304-3975
Accessed
2019-11-26T19:59:13Z
Library Catalog
ScienceDirect
Extra
ZSCC: 0000058
Citation
van Breugel, F., Mislove, M., Ouaknine, J., & Worrell, J. (2005). Domain theory, testing and simulation for labelled Markov processes. Theoretical Computer Science, 333(1), 171–197. https://doi.org/10/ft9vc5
Processing time: 0.01 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references