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 | |
| 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/Territory | Argentina |
| City | Buenos Aires |
| Period | 27/08/2013 → 30/08/2013 |
| Internet address |
| Series | Lecture Notes in Computer Science |
|---|---|
| Volume | 8054 |
| ISSN | 0302-9743 |