| Title: | monitor-based statistical model checking for weighted metric temporal logic |
| Author: | Bulychev Peter
; David Alexandre
; Guldstrand Larsen Kim
; Legay Axel
; Li Guangyuan
; Bgsted Poulsen Danny
; Stainer Amelie
|
| Source: | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
|
| Conference Name: | 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
|
| Conference Date: | March 11, 2012 - March 15, 2012
|
| Issued Date: | 2012
|
| Conference Place: | Merida, Venezuela
|
| Keyword: | Artificial intelligence
; Semantics
|
| 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
|
| Sponsorship: | Microsoft Research
|
| 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. |
| 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. |
| Language: | 英语
|
| Content Type: | 会议论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/15719
|
| Appears in Collections: | 软件所图书馆_会议论文
|
|
There are no files associated with this item.
|
| Recommended Citation: | |
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.
|
|
|
