monitor-based statistical model checking for weighted metric temporal logic

ISCAS OpenIR

	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
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	168-182
会议日期	March 11, 2012 - March 15, 2012
会议地点	Merida, Venezuela
收录类别	EI
ISSN	0302-9743
ISBN	9783642287169
部门归属	(1) Computer Science Aalborg University Denmark; (2) INRIA/IRISA Rennes Cedex France; (3) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China; (4) University of Rennes 1 Rennes France
摘要	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.
关键词	Artificial Intelligence Semantics
主办者	Microsoft Research
语种	英语
内容类型	会议论文
URI标识	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],2012:168-182.