lpar2012

P. Bulychev, D. David, K. Larsen, A. Legay, G. Li, D. Poulsen, A. Stainer. Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. In The 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning, LNCS, Volume 7180, Pages 168-182, Mérida, Venezuela, March 2012.

Download [help]

Download paper: Doi page

Download paper: Adobe portable document (pdf)

Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
This page is automatically generated by bib2html v216, © INRIA 2002-2007, Projet Lagadic

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

Contact

Amélie Stainer http://www.irisa.fr/prive/amelie.stainer/

BibTex Reference

@InProceedings{lpar2012,
   Author = {Bulychev, P. and David, D. and Larsen, K. and Legay, A. and Li, G. and Poulsen, D. and Stainer, A.},
   Title = {Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic},
   BookTitle = {The 18th International Conference on Logic for Programming Artificial Intelligence and Reasoning},
   Volume = {7180},
   Pages = {168--182},
   Series = {LNCS},
   Address = {Mérida, Venezuela},
   Month = {March},
   Year = {2012}
}

EndNote Reference [help]

Get EndNote Reference (.ref)