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
会议名称	10th International Conference on Quantitative Evaluation of Systems, QEST 2013
页码	209-224
会议日期	August 27, 2013 - August 30, 2013
会议地点	Buenos Aires, Argentina
收录类别	EI
出版地	Springer Verlag, Tiergartenstrasse 17, Heidelberg, D-69121, Germany
ISSN	3029743
ISBN	9783642401954
部门归属	(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
摘要	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.
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16678
专题	中国科学院软件研究所
推荐引用方式 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.