中国科学院机构知识库网格
Chinese Academy of Sciences Institutional Repositories Grid
首页 机构 成果 学者
  
  1. CAS IR Grid
  2. 软件研究所
  3. 软件所图书馆
  4. 会议论文
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.

入库方式： OAI收割

来源：软件研究所

浏览0
下载0
收藏0
其他版本

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。