Weak bisimulation for probabilistic systems
Date
2000Author
Philippou, AnnaLee, I.
Sokolsky, O.
ISSN
0302-9743Source
11th International Conference on Concurrency Theory, CONCUR 2000Volume
1877 LNCSPages
334-349Google Scholar check
Keyword(s):
Metadata
Show full item recordAbstract
In this paper, we introduce weak bisimulation in the framework of Labeled Concurrent Markov Chains, that is, probabilistic transition systems which exhibit both probabilistic and nondeterministic behavior. By resolving the nondeterminism present, these models can be decomposed into a possibly infinite number of computation trees. We show that in order to compute weak bisimulation it is sufficient to restrict attention to only a finite number of these computations. Finally, we present an algorithm for deciding weak bisimulation which has polynomial-time complexity in the number of states of the transition system. © Springer-Verlag Berlin Heidelberg 2000.