[ZhangH07] Deciding Simulations on Probabilistic Automata Zhang, L. and Hermanns, H. In Automated Technology for Verification and Analysis, 5th International Symposium (ATVA), pages 207-222, Springer, Lecture Notes in Computer Science 4762, 2007.
Downloads: pdf, bibURL: Abstract. Probabilistic automata are a central model for concurrent systems exhibiting random phenomena. This paper presents, in a uniform setting, efficient decision algorithms for strong simulation on probabilistic automata, but with subtly different results. The algorithm for strong probabilistic simulation is shown to be of polynomial complexity via a reduction to LP problem, while the algorithm for strong simulation has complexity mathcalO(m^2n) . The former relation allows for convex combinations of transitions in the definition and is thus less discriminative than the latter. As a byproduct, we obtain minimisation algorithms with respect to strong simulation equivalences and – for Markov decision processes – also to strong bisimulation equivalences. When extending these algorithms to the continuous-time setting, we retain same complexities for both strong simulation and strong probabilistic simulations.