Simulation-based CTMC Model Checking: An Empirical Evaluation


Katoen, Joost-Pieter and Zapreev, Ivan S. (2009) Simulation-based CTMC Model Checking: An Empirical Evaluation. In: Sixth International Conference on the Quantitative Evaluation of Systems, QEST, 13-16 Sept 2009, Budapest, Hungary (pp. pp. 31-40).

open access
Abstract: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 all main CSL formulae; Ymer - that allows for verification oftime-bounded and time-interval until using sequential acceptance sampling; and VESTA - that can verify time-bounded and unbounded until by means of simple hypothesis testing. The study shows that MRMC provides the most accurate verification results. Ymer and VESTA, unlike MRMC, have almost constant memory consumption. Ymer requiresthe least number of observations to assess the model-checking problem, but MRMC is mostly the fastest. This indicates that the tools' efficiency does not so muchdepend on sampling but is rather determined by extra computations.
Item Type:Conference or Workshop Item
Copyright:© 2009 IEEE
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page