Decision Algorithms for Probabilistic Bisimulation Stefano Cattani and Roberto Segala
We propose decision algorithms for bisimulation relations defined on
probabilistic automata, a model for concurrent nondeterministic
systems with randomization. The algorithms decide both strong and weak
bisimulation relations based on deterministic as well as randomized
schedulers. These algorithms extend and complete other known
algorithms for simpler relations and models. The algorithm we present
for strong probabilistic bisimulation has polynomial time complexity,
while the algorithm for weak probabilistic bisimulation is
exponential; however we argue that the latter is feasible in
practice.
|
concur02@fi.muni.cz |