model checking conditional csl for continuous-time markov chains

ISCAS OpenIR

	model checking conditional csl for continuous-time markov chains
	Gao Yang; Xu Ming; Zhan Naijun; Zhang Lijun
	2013
发表期刊	Information Processing Letters
ISSN	0020-0190
卷号	113 期号:1-2 页码:44-50
摘要	In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity. Crown Copyright © 2012 Elsevier B.V. All rights reserved.; In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000) [1] to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity. Crown Copyright © 2012 Elsevier B.V. All rights reserved.
收录类别	EI
关键词	Automata Theory Formal Methods Stochastic Systems
部门归属	(1) State Key Lab. of Comp. Sci. Institute of Software Chinese Academy of Sciences China; (2) Department of Computer Science and Technology East China Normal University China; (3) Technical University of Denmark DTU Informatics Denmark
语种	英语
WOS记录号	WOS:000312175200009
引用统计
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15206
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Gao Yang,Xu Ming,Zhan Naijun,et al. model checking conditional csl for continuous-time markov chains[J]. Information Processing Letters,2013,113(1-2):44-50.
APA	Gao Yang,Xu Ming,Zhan Naijun,&Zhang Lijun.(2013).model checking conditional csl for continuous-time markov chains.Information Processing Letters,113(1-2),44-50.
MLA	Gao Yang,et al."model checking conditional csl for continuous-time markov chains".Information Processing Letters 113.1-2(2013):44-50.