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

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\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
PublisherSpringer
Publication date2013
Pages209-224
ISBN (Print)978-3-642-40195-4
ISBN (Electronic)978-3-642-40196-1
DOIs
Publication statusPublished - 2013
Event10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013
http://www.qest.org/qest2013/

Conference

Conference10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)
Country/TerritoryArgentina
CityBuenos Aires
Period27/08/201330/08/2013
Internet address
SeriesLecture Notes in Computer Science
Volume8054
ISSN0302-9743

Fingerprint

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

Cite this