Weak Bisimulation for Probabilistic Systems

Abstract. 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 nondeterminismpresent, these models can be decomposed into a possibly in nite number of computation trees. We show that in order to compute weak bisimulation it is su cient to restrict attention to only a nite 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.

• Type: Conference
• Year: 2000
• Where: CONCUR
• Authors: Anna Philippou, Insup Lee, Oleg Sokolsky
• Keywords: CONCUR 2000, Distributed And Parallel Computing, Nite Number, Probabilistic Transition Systems, Weak Bisimulation