Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic

Abstract : We present a novel approach and implementation for analysing 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 approach 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 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.
Type de document :
Communication dans un congrès
Nikolaj Bjørner, Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Mar 2012, Merida, Venezuela. Springer, 7180, pp.168-182, 2012, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00744100
Contributeur : Amélie Stainer <>
Soumis le : lundi 22 octobre 2012 - 12:24:22
Dernière modification le : mercredi 16 mai 2018 - 11:23:02
Document(s) archivé(s) le : samedi 17 décembre 2016 - 03:12:15

Fichier

lpar18_submission_20-1.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00744100, version 1

Citation

Peter Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, et al.. Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. Nikolaj Bjørner, Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning, Mar 2012, Merida, Venezuela. Springer, 7180, pp.168-182, 2012, Lecture Notes in Computer Science. 〈hal-00744100〉

Partager

Métriques

Consultations de la notice

475

Téléchargements de fichiers

135