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\x, 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\x, and a variant that is both sound and complete. A long version of this article containing full proofs is available from .
Lecture Notes in Computer Science: 10th International Conference, Qest 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, 2013, p. 209-224
Main Research Area:
Lecture Notes in Computer Science
10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)