Article

Monitor-Based statistical model checking for weighted metric temporal logic

Authors:

Peter Bulychev,

Alexandre David,

Kim Guldstrand Larsen,

Danny Bøgsted Poulsen,

Amelie StainerAuthors Info & Claims

LPAR'12: Proceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

Pages 168 - 182

https://doi.org/10.1007/978-3-642-28717-6_15

Published: 11 March 2012 Publication History

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.

References

[1]

Agha, G., Meseguer, J., Sen, K.: Pmaude: Rewrite-based specification language for probabilistic object systems. Electronic Notes in Theoretical Computer Science 153(2), 213-239 (2006)

Digital Library

[2]

Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3-34 (1995)

Digital Library

[3]

Alur, R., Feder, T., Henzinger, T. A.: The benefits of relaxing punctuality. J. ACM 43, 116-146 (1996)

Digital Library

[4]

Alur, R., La Torre, S., Pappas, G. J.: Optimal Paths in Weighted Timed Automata. In: Di Benedetto, M. D., Sangiovanni-Vincentelli, A. L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49-62. Springer, Heidelberg (2001)

Digital Library

[5]

Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC Model Checking of Linear Real-Time Objectives. In: Abdulla, P. A., Leino, K. R. M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128-142. Springer, Heidelberg (2011)

Digital Library

[6]

Behrmann, G., Fehnker, A., Hune, T., Larsen, K. G., Pettersson, P., Romijn, J., Vaandrager, F. W.: Minimum-Cost Reachability for Priced Timed Automata. In: Di Benedetto, M. D., Sangiovanni-Vincentelli, A. L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147-161. Springer, Heidelberg (2001)

Digital Library

[7]

Bouyer, P., Larsen, K. G., Markey, N.: Model checking one-clock priced timed automata. Logical Methods in Computer Science 4(2) (2008)

[8]

Cassez, F., Larsen, K. G.: The Impressive Power of Stopwatches. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 138-152. Springer, Heidelberg (2000)

Digital Library

[9]

Couvreur, J.-M.: On-the-Fly Verification of Linear Temporal Logic. In:Wing, J. M., Woodcock, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253-271. Springer, Heidelberg (1999)

Digital Library

[10]

David, A., Larsen, K. G., Legay, A., Mikučionis, M., Poulsen, D. B., van Vliet, J., Wang, Z.: Statistical Model Checking for Networks of Priced Timed Automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80-96. Springer, Heidelberg (2011)

Digital Library

[11]

David, A., Larsen, K. G., Legay, A., Mikučionis, M., Wang, Z.: Time for Statistical Model Checking of Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349-355. Springer, Heidelberg (2011)

Digital Library

[12]

Geilen, M.: An Improved On-the-Fly Tableau Construction for a Real-Time Temporal Logic. In: Hunt Jr., W. A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 394-406. Springer, Heidelberg (2003)

[13]

Geilen, M., Dams, D. R.: An On-the-fly Tableau Construction for a Real-Time Temporal Logic. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 276-290. Springer, Heidelberg (2000)

Digital Library

[14]

Clarke Jr., E. M., Grumberg, O., Peled, D. A.:ModelChecking. TheMITPress (1999)

Digital Library

[15]

Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2, 255-299 (1990)

Digital Library

[16]

Maler, O., Ničkovic, D., Pnueli, A.: From MITL to Timed Automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274-289. Springer, Heidelberg (2006)

Digital Library

[17]

Ničkovic, D., Piterman, N.: From Mtl to Deterministic Timed Automata. In: Chatterjee, K., Henzinger, T. A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 152-167. Springer, Heidelberg (2010)

Digital Library

[18]

Sen, K., Viswanathan, M., Agha, G.: On Statistical Model Checking of Stochastic Systems. In: Etessami, K., Rajamani, S. K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 266-280. Springer, Heidelberg (2005)

Digital Library

[19]

Younes, H. L. S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon University (2005)

Digital Library

[20]

Zuliani, P., Platzer, A., Clarke, E. M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC 2010, pp. 243-252. ACM, New York (2010)

Digital Library

Cited By

Kumar RNarra BKela RSingh S(2022)AFMTComputers in Industry10.1016/j.compind.2021.103584136:COnline publication date: 6-May-2022
https://dl.acm.org/doi/10.1016/j.compind.2021.103584
Grosen TKauffman SLarsen KZimmermann M(2022)Monitoring Timed Properties (Revisited)Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_3(43-62)Online publication date: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_3
Fernandes HGomes Gde Oliveira ACampos S(2020)Statistical Model Checking in Drug Repurposing for Alzheimer’s DiseaseFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_5(64-80)Online publication date: 25-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-63882-5_5
Show More Cited By

Monitor-Based statistical model checking for weighted metric temporal logic
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
2. Theory of computation
  1. Logic

Recommendations

Model checking temporal metric specifications with Trio2Promela
FSEN'07: Proceedings of the 2007 international conference on Fundamentals of software engineering

We present Trio2Promela, a tool for model checking TRIO specifications by means of Spin. TRIO is a linear-time temporal logic with both future and past operators and a quantitative metric on time. Our approach is based on the translation of TRIO ...
From model checking to a temporal proof
SPIN '01: Proceedings of the 8th international SPIN workshop on Model checking of software

Model checking is used to automatically verify temporal properties of finite state systems. It is usually considered to be `sucessful', when an error, in the form of a counterexample to the checked property, is found. We present the dual approach, where,...
Statistical model checking of Timed Rebeca models

The actor-based language, Timed Rebeca, was introduced to model distributed and asynchronous systems with timing constraints and message passing communication. A toolset was developed for automated translation of Timed Rebeca models to Erlang. The ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

LPAR'12: Proceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning

March 2012

444 pages

ISBN:9783642287169

Editors:
Nikolaj Bjørner
Microsoft Research, One Microsoft Way, Redmond, WA
,
Andrei Voronkov
School of computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, WA, UK

Sponsors

Microsoft Research: Microsoft Research

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 March 2012

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kumar RNarra BKela RSingh S(2022)AFMTComputers in Industry10.1016/j.compind.2021.103584136:COnline publication date: 6-May-2022
https://dl.acm.org/doi/10.1016/j.compind.2021.103584
Grosen TKauffman SLarsen KZimmermann M(2022)Monitoring Timed Properties (Revisited)Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_3(43-62)Online publication date: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_3
Fernandes HGomes Gde Oliveira ACampos S(2020)Statistical Model Checking in Drug Repurposing for Alzheimer’s DiseaseFormal Methods: Foundations and Applications10.1007/978-3-030-63882-5_5(64-80)Online publication date: 25-Nov-2020
https://dl.acm.org/doi/10.1007/978-3-030-63882-5_5
Foughali MIngrand FSeceleanu C(2019)Statistical Model Checking of Complex Robotic SystemsModel Checking Software10.1007/978-3-030-30923-7_7(114-134)Online publication date: 15-Jul-2019
https://dl.acm.org/doi/10.1007/978-3-030-30923-7_7
Li GJensen PLarsen KLegay APoulsen DErdogmus HHavelund K(2017)Practical controller synthesis for MTL0,∞Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software10.1145/3092282.3092303(102-111)Online publication date: 13-Jul-2017
https://dl.acm.org/doi/10.1145/3092282.3092303
Banks CStark I(2014)A logic of behaviour in contextInformation and Computation10.1016/j.ic.2014.01.009236:C(3-18)Online publication date: 1-Aug-2014
https://dl.acm.org/doi/10.1016/j.ic.2014.01.009
Althoff MBelta CIvančić F(2013)Reachability analysis of nonlinear systems using conservative polynomialization and non-convex setsProceedings of the 16th international conference on Hybrid systems: computation and control10.1145/2461328.2461358(173-182)Online publication date: 8-Apr-2013
https://dl.acm.org/doi/10.1145/2461328.2461358
Fahrenberg ULarsen KLegay A(2013)Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time SystemsUnifying Theories of Programming and Formal Engineering Methods10.1007/978-3-642-39721-9_2(67-108)Online publication date: 26-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-642-39721-9_2
Larsen K(2012)Statistical model checking, refinement checking, optimization, … for stochastic hybrid systemsProceedings of the 10th international conference on Formal Modeling and Analysis of Timed Systems10.5555/2413866.2413869(7-10)Online publication date: 18-Sep-2012
https://dl.acm.org/doi/10.5555/2413866.2413869

View Options

View options

Media

Figures

Other

Tables

View Table of Contents