Strong and weak simulation relations have been proposed for Markov chains,while strong simulation and strong probabilistic simulation relations have beenproposed for probabilistic automata. However, decision algorithms for strongand weak simulation over Markov chains, and for strong simulation overprobabilistic automata are not efficient, which makes it as yet unclear whetherthey can be used as effectively as their non-probabilistic counterparts. Thispaper presents drastically improved algorithms to decide whether some(discrete- or continuous-time) Markov chain strongly or weakly simulatesanother, or whether a probabilistic automaton strongly simulates another. Thekey innovation is the use of parametric maximum flow techniques to amortizecomputations. We also present a novel algorithm for deciding strongprobabilistic simulation preorders on probabilistic automata, which haspolynomial complexity via a reduction to an LP problem. When extending thealgorithms for probabilistic automata to their continuous-time counterpart, weretain the same complexity for both strong and strong probabilisticsimulations.
展开▼
