| 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
|
| Conference Name | 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
|
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
| Pages | 168-182
|
| Conference Date | March 11, 2012 - March 15, 2012
|
| Conference Place | Merida, Venezuela
|
| Indexed Type | EI
|
| ISSN | 0302-9743
|
| ISBN | 9783642287169
|
| Department | (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
|
| English Abstract | 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. |
| Keyword | Artificial Intelligence
Semantics
|
| Sponsorship | Microsoft Research
|
| Language | 英语
|
| Content Type | 会议论文
|
| URI | http://ir.iscas.ac.cn/handle/311060/15719
|
| Collection | 中国科学院软件研究所
|
Recommended Citation
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.
|
| Files in This Item: |
|
There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment