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

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

23 Citationer (Scopus)

Abstrakt

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.
OriginalsprogEngelsk
TitelLogic for Programming, Artificial Intelligence, and Reasoning : 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings
Vol/bind7180
UdgivelsesstedBerlin
ForlagSpringer
Publikationsdato2012
Sider168-182
ISBN (Trykt)978-3-642-28716-9
ISBN (Elektronisk)978-3-642-28717-6
DOI
StatusUdgivet - 2012
Begivenhed18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. - Mérida, Venezuela
Varighed: 11 mar. 201215 mar. 2012
Konferencens nummer: 18th

Konference

Konference18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012.
Nummer18th
LandVenezuela
ByMérida
Periode11/03/201215/03/2012
NavnLecture Notes in Computer Science
Vol/bind7180
ISSN0302-9743

Fingeraftryk Dyk ned i forskningsemnerne om 'Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic'. Sammen danner de et unikt fingeraftryk.

Citationsformater