Revisiting Weak Simulation for Substochastic Markov Chains

David N. Jansen, Lei Song, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


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 [11].
Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems : 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings
Publication date2013
ISBN (Print)978-3-642-40195-4
ISBN (Electronic)978-3-642-40196-1
Publication statusPublished - 2013
Event10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013


Conference10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)
CityBuenos Aires
Internet address
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Revisiting Weak Simulation for Substochastic Markov Chains'. Together they form a unique fingerprint.

Cite this