Article

Efficient CTMC model checking of linear real-time objectives

Authors:

Benoît Barbot,

Joost-Pieter Katoen,

Alexandru MereacreAuthors Info & Claims

TACAS'11/ETAPS'11: Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software

Pages 128 - 142

Published: 26 March 2011 Publication History

Abstract

This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.

References

[1]

PRISM website, http://www.prismmodelchecker.org

[2]

Alur, R., Dill, D.L.: A theory of timed automata. TCS 126(2), 183-235 (1994)

Digital Library

[3]

Amparore, E.G., Donatelli, S.: Model checking CSL^TA with deterministic and stochastic Petri Nets. In: Dependable Systems and Networks (DSN), pp. 605-614 (2010)

[4]

Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Grösser, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: LICS, pp. 217-226 (2008)

Digital Library

[5]

Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE TSE 33(4), 209-224 (2007)

Digital Library

[6]

Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29(6), 524-541 (2003)

Digital Library

[7]

Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. of the ACM 53(9), 74-85 (2010)

Digital Library

[8]

Bérard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fund. Inf. 36(2-3), 145-182 (1998)

Digital Library

[9]

Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST, pp. 55-64 (2008)

Digital Library

[10]

Blom, S., Haverkort, B.R., Kuntz, M., van de Pol, J.: Distributed Markovian bisimulation reduction aimed at CSL model checking. ENTCS 220(2), 35-50 (2008)

Digital Library

[11]

Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., Ř ehák, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207-221. Springer, Heidelberg (2010)

Digital Library

[12]

Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuoustime Markov chains against timed automata specification. In: LICS, pp. 309-318 (2009)

Digital Library

[13]

Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309-315 (2003)

Digital Library

[14]

Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSL^TA. IEEE TSE 35(2), 224-240 (2009)

Digital Library

[15]

Goldstein, B., Faeder, J.R., Hlavacek, W.S.: Mathematical and computational models of immune-receptor signalling. Nat. Reviews Immunology 4, 445-456 (2004)

[16]

Haverkort, B.R.: Performance evaluation of polling-based communication systems using SPNs. In: Appl. of Petri Nets to Comm. Networks, pp. 176-209 (1999)

Digital Library

[17]

Katoen, J.-P., Hahn, E.M., Hermanns, H., Jansen, D.N., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: QEST, pp. 167-176 (2009)

Digital Library

[18]

Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87-101. Springer, Heidelberg (2007)

Digital Library

[19]

Valmari, A., Franceschinis, G.: Simple O(mlogn) time markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 38-52. Springer, Heidelberg (2010)

Digital Library

[20]

Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327-338 (1985)

Digital Library

Cited By

Katoen JKoskinen EGrohe MShankar N(2016)The Probabilistic Model Checking LandscapeProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934574(31-45)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934574
Soeanu ADebbabi MAlhadidi DMakkawi MAllouche MBélanger MLéchevin N(2015)Transportation risk analysis using probabilistic model checkingExpert Systems with Applications: An International Journal10.1016/j.eswa.2014.12.05242:9(4410-4421)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1016/j.eswa.2014.12.052
Chen TDiciolla MKwiatkowska MMereacre A(2013)Verification of linear duration properties over continuous-time markov chainsACM Transactions on Computational Logic10.1145/252893514:4(1-35)Online publication date: 28-Nov-2013
https://dl.acm.org/doi/10.1145/2528935
Show More Cited By

Recommendations

Simulation-Based CTMC Model Checking: An Empirical Evaluation
QEST '09: Proceedings of the 2009 Sixth International Conference on the Quantitative Evaluation of Systems

This paper provides an experimental study of the efficiency of simulation-based model-checking algorithms for continuous-time Markov chains by comparing:MRMC -- the only tool that implements (new) confidence-interval-based algorithms for verification of ...
Faster and Symbolic CTMC Model Checking
PAPM-PROBMIV '01: Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification

This paper reports on the implementation and the experiments with symbolic model checking of continuous-time Markov chains using multi-terminal binary decision diagrams (MTBDDs). Properties are expressed in Continuous Stochastic Logic (CSL) [7] which ...
An Efficient Algorithm for Real-Time Symbolic Model Checking
EDTC '96: Proceedings of the 1996 European conference on Design and Test

The verification of real-time properties requires model checking techniques for quantitative temporal structures and real-time temporal logics. However, up to now, most of those problems were solved by a translation into a standard CTL model checking ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

TACAS'11/ETAPS'11: Proceedings of the 17th international conference on Tools and algorithms for the construction and analysis of systems: part of the joint European conferences on theory and practice of software

March 2011

392 pages

ISBN:9783642198342

Editors:
Parosh Aziz Abdulla
University of Uppsala, Dept. of Information Technology, Uppsala, Sweden
,
K. Rustan M. Leino
Microsoft Research, Redmond,WA

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 26 March 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
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

Katoen JKoskinen EGrohe MShankar N(2016)The Probabilistic Model Checking LandscapeProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934574(31-45)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934574
Soeanu ADebbabi MAlhadidi DMakkawi MAllouche MBélanger MLéchevin N(2015)Transportation risk analysis using probabilistic model checkingExpert Systems with Applications: An International Journal10.1016/j.eswa.2014.12.05242:9(4410-4421)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1016/j.eswa.2014.12.052
Chen TDiciolla MKwiatkowska MMereacre A(2013)Verification of linear duration properties over continuous-time markov chainsACM Transactions on Computational Logic10.1145/252893514:4(1-35)Online publication date: 28-Nov-2013
https://dl.acm.org/doi/10.1145/2528935
Fu HBelta CIvančić F(2013)Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automataProceedings of the 16th international conference on Hybrid systems: computation and control10.1145/2461328.2461376(323-332)Online publication date: 8-Apr-2013
https://dl.acm.org/doi/10.1145/2461328.2461376
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
Eisentraut CHermanns HSchuster JTurrini AZhang L(2013)The quest for minimal quotients for probabilistic automataProceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-36742-7_2(16-31)Online publication date: 16-Mar-2013
https://dl.acm.org/doi/10.1007/978-3-642-36742-7_2
Chen TDiciolla MKwiatkowska MMereacre ADang TMitchell I(2012)Verification of linear duration properties over continuous-time markov chainsProceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control10.1145/2185632.2185672(265-274)Online publication date: 17-Apr-2012
https://dl.acm.org/doi/10.1145/2185632.2185672
Bulychev PDavid AGuldstrand Larsen KLegay ALi GBøgsted Poulsen DStainer A(2012)Monitor-Based statistical model checking for weighted metric temporal logicProceedings of the 18th international conference on Logic for Programming, Artificial Intelligence, and Reasoning10.1007/978-3-642-28717-6_15(168-182)Online publication date: 11-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28717-6_15
Chen THan TKatoen JMereacre A(2011)Observing continuous-time MDPs by 1-clock timed automataProceedings of the 5th international conference on Reachability problems10.5555/2045343.2045345(2-25)Online publication date: 28-Sep-2011
https://dl.acm.org/doi/10.5555/2045343.2045345
Brázdil TKrčál JKřetínský JŘehák V(2011)Fixed-delay events in generalized semi-Markov processes revisitedProceedings of the 22nd international conference on Concurrency theory10.5555/2040235.2040248(140-155)Online publication date: 6-Sep-2011
https://dl.acm.org/doi/10.5555/2040235.2040248
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents