@article{van_breugel_domain_2005,
series = {Foundations of {Software} {Science} and {Computation} {Structures}},
title = {Domain theory, testing and simulation for labelled {Markov} processes},
volume = {333},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/S030439750400711X},
doi = {10/ft9vc5},
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.},
language = {en},
number = {1},
urldate = {2019-11-26},
journal = {Theoretical Computer Science},
author = {van Breugel, Franck and Mislove, Michael and Ouaknine, Joël and Worrell, James},
month = mar,
year = {2005},
note = {ZSCC: 0000058},
keywords = {Coalgebras, Denotational semantics, Probabilistic transition systems, Transition systems},
pages = {171--197}
}
@article{desharnais_bisimulation_2002,
title = {Bisimulation for {Labelled} {Markov} {Processes}},
volume = {179},
issn = {0890-5401},
url = {http://www.sciencedirect.com/science/article/pii/S0890540101929621},
doi = {10/fmp9vd},
abstract = {In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems. •Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.•We do not need any finite branching assumption, yet there is no need of infinitary conjunction. We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.},
language = {en},
number = {2},
urldate = {2019-11-26},
journal = {Information and Computation},
author = {Desharnais, Josée and Edalat, Abbas and Panangaden, Prakash},
month = dec,
year = {2002},
note = {ZSCC: 0000297},
keywords = {Coalgebras, Denotational semantics, Probabilistic transition systems, Symbolic logic, Transition systems},
pages = {163--193}
}