[JansenSZ13] Revisiting Weak Simulation for Substochastic Markov Chains Jansen, D. N.; Song, L. and Zhang, L. In Quantitative Evaluation of Systems - 10th International Conference (QEST), pages 209-224, Springer, Lecture Notes in Computer Science 8054, 2013.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-40196-1_18 Abstract. The spectrum of branching-time relations for probabilistic systems has been investigated thoroughly by Baier, Hermanns, Katoen and Wolf (2003, 2005), including weak simulation for systems involving substochastic distributions. Weak simulation was proven to be sound w.r.t. the liveness fragment of the logic PCTL_setminus mathcalX , and its completeness was conjectured. We revisit this result and show that soundness does not hold in general, but only for Markov chains without divergence. It is refuted for some systems with substochastic distributions. Moreover, we provide a counterexample to completeness. In this paper, we present a novel definition that is sound for live PCTL_setminus mathcalX , and a variant that is both sound and complete.
A long version of this article containing full proofs is available from [11].