Revisiting weak simulation for substochastic Markov chains

ISCAS OpenIR

	Revisiting weak simulation for substochastic Markov chains
	Jansen, David N. (1); Song, Lei (2); Zhang, Lijun (3)
	2013
Conference Name	10th International Conference on Quantitative Evaluation of Systems, QEST 2013
Pages	209-224
Conference Date	August 27, 2013 - August 30, 2013
Conference Place	Buenos Aires, Argentina
Indexed Type	EI
Publish Place	Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany
ISSN	3029743
ISBN	9783642401954
Department	(1) Radboud Universiteit, Model-Based System Development, Nijmegen, Netherlands; (2) Max-Planck-Institut für Informatik, Saarbrücken, Germany; (3) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (4) Technical University of Denmark, DTU Compute, Denmark; (5) Universität des Saarlandes, Saarbrücken, Germany
English 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 PCTLx, 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 PCTLx, and a variant that is both sound and complete. A long version of this article containing full proofs is available from [11]. © 2013 Springer-Verlag.; 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 PCTLx, 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 PCTLx, and a variant that is both sound and complete. A long version of this article containing full proofs is available from [11]. © 2013 Springer-Verlag.
Language	英语
Content Type	会议论文
URI	http://ir.iscas.ac.cn/handle/311060/16678
Collection	中国科学院软件研究所
Recommended Citation GB/T 7714	Jansen, David N. ,Song, Lei ,Zhang, Lijun . Revisiting weak simulation for substochastic Markov chains[C]. Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany,2013:209-224.

Files in This Item:
There are no files associated with this item.

If you have any objections to this item, please fill out the form below and the administrator will contact you as soon as possible.
Content:
Email：	*
Institution:
Verification Code:	Refresh

Any comments and suggestions are welcomed.
Title:	*
Content:
Email：	*
Verification Code:	Refresh

中国科学院软件研究所机构知识库