MODEL CHECKING AND STATE MACHINES
Publication year

Bisimulation for Labelled Markov Processes

Resource type
Authors/contributors
Title
Bisimulation for Labelled Markov Processes
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.
Publication
Information and Computation
Volume
179
Issue
2
Pages
163-193
Date
December 15, 2002
Journal Abbr
Information and Computation
Language
en
DOI
10/fmp9vd
ISSN
0890-5401
Accessed
2019-11-26T21:27:24Z
Library Catalog
ScienceDirect
Extra
ZSCC: 0000297
Citation
Desharnais, J., Edalat, A., & Panangaden, P. (2002). Bisimulation for Labelled Markov Processes. Information and Computation, 179(2), 163–193. https://doi.org/10/fmp9vd
Processing time: 0.06 seconds

Graph of references

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