On some equivalence relations for probabilistic processes. (English) Zbl 0766.68099

Summary: We investigate several equivalence relations for probabilistic labeled transition systems: bisimulation equivalence, readiness equivalence, failure equivalence, trace equivalence, maximal trace equivalence and finite trace equivalence. We formally prove the inclusions (equalities) among these equivalences. We also show that readiness, failure, trace, maximum trace and finite trace equivalences for finite probabilistic labeled transition systems are decidable in polynomial time. This should be contrasted with the PSPACE completeness of the same equivalences for classical labeled transition systems. Moreover, we derive an efficient polynomial time algorithm for deciding bisimulation equivalence for finite probabilistic labeled transition systems. The special case of initiated probabilistic transition systems will be considered. We show that the isomorphism problem for finite initiated labeled probabilistic transition systems is \(NC^{(1)}\) equivalent to graph isomorphism.


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)