Revisiting Weak Simulation for Substochastic Markov Chains

David N. Jansen; Lei Song; Lijun Zhang

doi:10.1007/978-3-642-40196-1_18

Revisiting Weak Simulation for Substochastic Markov Chains

David N. Jansen, Lei Song, Lijun Zhang

Department of Applied Mathematics and Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Quantitative Evaluation of Systems : 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings
Publisher	Springer
Publication date	2013
Pages	209-224
ISBN (Print)	978-3-642-40195-4
ISBN (Electronic)	978-3-642-40196-1
DOIs	https://doi.org/10.1007/978-3-642-40196-1_18
Publication status	Published - 2013
Event	10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) - Buenos Aires, Argentina Duration: 27 Aug 2013 → 30 Aug 2013 http://www.qest.org/qest2013/

Conference

Conference	10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)
Country	Argentina
City	Buenos Aires
Period	27/08/2013 → 30/08/2013
Internet address	http://www.qest.org/qest2013/

Series	Lecture Notes in Computer Science
Volume	8054
ISSN	0302-9743

Access to Document

10.1007/978-3-642-40196-1_18

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

Cite this

@inproceedings{d010129f187140d383df979ab9b2b80f,

title = "Revisiting Weak Simulation for Substochastic Markov Chains",

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].",

author = "Jansen, {David N.} and Lei Song and Lijun Zhang",

year = "2013",

doi = "10.1007/978-3-642-40196-1_18",

language = "English",

isbn = "978-3-642-40195-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "209--224",

booktitle = "Quantitative Evaluation of Systems",

note = "10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) ; Conference date: 27-08-2013 Through 30-08-2013",

url = "http://www.qest.org/qest2013/",

}

Jansen, DN, Song, L & Zhang, L 2013, Revisiting Weak Simulation for Substochastic Markov Chains. in Quantitative Evaluation of Systems: 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Springer, Lecture Notes in Computer Science, vol. 8054, pp. 209-224, 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013) , Buenos Aires, Argentina, 27/08/2013. https://doi.org/10.1007/978-3-642-40196-1_18

Revisiting Weak Simulation for Substochastic Markov Chains. / Jansen, David N.; Song, Lei; Zhang, Lijun.

Quantitative Evaluation of Systems: 10th International Conference, QEST 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Springer, 2013. p. 209-224 (Lecture Notes in Computer Science, Vol. 8054).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Revisiting Weak Simulation for Substochastic Markov Chains

AU - Jansen, David N.

AU - Song, Lei

AU - Zhang, Lijun

PY - 2013

Y1 - 2013

N2 - 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].

AB - 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].

U2 - 10.1007/978-3-642-40196-1_18

DO - 10.1007/978-3-642-40196-1_18

M3 - Article in proceedings

SN - 978-3-642-40195-4

T3 - Lecture Notes in Computer Science

SP - 209

EP - 224

BT - Quantitative Evaluation of Systems

PB - Springer

T2 - 10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)

Y2 - 27 August 2013 through 30 August 2013

ER -