Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

Petr Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Li Guangyuan, Danny Bøgsted Poulsen, Amelie Stainer

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

32 Citations (Scopus)

Abstract

We present a novel approach and implementation for ana-
lysing weighted timed automata (WTA) with respect to the weighted
metric temporal logic (WMTL≤ ). 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 ap-
proach consists in generation of deterministic monitors for formulas in
WMTL≤ , allowing for efficient SMC by run-time evaluation of a given
formula. By necessity, the deterministic observers are in general approx-
imate (over- or under-approximations), but are most often exact and ex-
perimentally tight. The technique is implemented in the new tool Casaal
that we seamlessly connect to Uppaal-smc in a tool chain. We demon-
strate the applicability of our technique and the efficiency of our imple-
mentation through a number of case-studies.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings
Volume7180
Place of PublicationBerlin
PublisherSpringer
Publication date2012
Pages168-182
ISBN (Print)978-3-642-28716-9
ISBN (Electronic)978-3-642-28717-6
DOIs
Publication statusPublished - 2012
Event18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. - Mérida, Venezuela, Bolivarian Republic of
Duration: 11 Mar 201215 Mar 2012
Conference number: 18th

Conference

Conference18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012.
Number18th
Country/TerritoryVenezuela, Bolivarian Republic of
CityMérida
Period11/03/201215/03/2012
SeriesLecture Notes in Computer Science
Volume7180
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic'. Together they form a unique fingerprint.

Cite this