Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations

Strong and weak simulation relations have been proposed for Markov chains, while strong simulation and strong probabilistic simulation relations have been proposed for probabilistic automata. This paper investigates whether they can be used as effectively as their non-probabilistic counterparts. It presents drastically improved algorithms to decide whether some (discrete- or continuous-time) Markov chain strongly or weakly simulates another, or whether a probabilistic automaton strongly simulates another. The key innovation is the use of parametric maximum flow techniques to amortize computations. We also present a novel algorithm for deciding strong probabilistic simulation preorders on probabilistic automata, which has polynomial complexity via a reduction to an LP problem. When extending the algorithms for probabilistic automata to their continuous-time counterpart, we retain the same complexity for both strong and strong probabilistic simulations.

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen
• Keywords: CORR 2008, Education, Probabilistic, Probabilistic Automata, Strong Probabilistic Simulations