monitor-based statistical model checking for weighted metric temporal logic

CORC > 软件研究所 > 软件所图书馆 > 会议论文

	monitor-based statistical model checking for weighted metric temporal logic
	Bulychev Peter ; David Alexandre ; Guldstrand Larsen Kim ; Legay Axel ; Li Guangyuan ; Bgsted Poulsen Danny ; Stainer Amelie
	2012
会议名称	18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
会议日期	March 11, 2012 - March 15, 2012
会议地点	Merida, Venezuela
关键词	Artificial intelligence Semantics
页码	168-182
中文摘要	We present a novel approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric temporal logic (WMTL &le). Based on a stochastic semantics of WTAs, we apply statistical model checking (SMC) to estimate and test probabilities of satisfaction with desired levels of confidence. Our approach consists in generation of deterministic monitors for formulas in WMTL&le, allowing for efficient SMC by run-time evaluation of a given formula. By necessity, the deterministic observers are in general approximate (over- or under-approximations), but are most often exact and experimentally tight. The technique is implemented in the new tool Casaal. that we seamlessly connect to Uppaal-smc. in a tool chain. We demonstrate the applicability of our technique and the efficiency of our implementation through a number of case-studies. © 2012 Springer-Verlag.
英文摘要	We present a novel approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric temporal logic (WMTL &le). Based on a stochastic semantics of WTAs, we apply statistical model checking (SMC) to estimate and test probabilities of satisfaction with desired levels of confidence. Our approach consists in generation of deterministic monitors for formulas in WMTL&le, allowing for efficient SMC by run-time evaluation of a given formula. By necessity, the deterministic observers are in general approximate (over- or under-approximations), but are most often exact and experimentally tight. The technique is implemented in the new tool Casaal. that we seamlessly connect to Uppaal-smc. in a tool chain. We demonstrate the applicability of our technique and the efficiency of our implementation through a number of case-studies. © 2012 Springer-Verlag.
收录类别	EI
会议主办者	Microsoft Research
会议录	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
语种	英语
ISSN号	0302-9743
ISBN号	9783642287169
内容类型	会议论文
源URL	[http://ir.iscas.ac.cn/handle/311060/15719]
专题	软件研究所_软件所图书馆_会议论文
推荐引用方式 GB/T 7714	Bulychev Peter,David Alexandre,Guldstrand Larsen Kim,et al. monitor-based statistical model checking for weighted metric temporal logic[C]. 见:18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18. Merida, Venezuela. March 11, 2012 - March 15, 2012.