06046610

a

06046610 Bulychev, Peter David, Alexandre Guldstrand Larsen, Kim Legay, Axel Li, Guangyuan B{\o}gsted Poulsen, Danny Stainer, Amelie Monitor-based statistical model checking for weighted metric temporal logic. Bj{\o}rner, Nikolaj (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 18th international conference, LPAR-18, M\'erida, Venezuela, March 11--15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-28716-9/pbk). Lecture Notes in Computer Science 7180, 168-182 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-28717-6_15

Summary: We present a novel approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric temporal logic $(WMTL_{ \leq })$. 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_{ \leq }$, 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.