Simulation-Based CTMC Model Checking: An Empirical Evaluation

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-intervalbased algorithms for verification of all main CSL formulae; Ymer – that allows for verification of time-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 requires the least number of observations to assess the model-checking problem, but MRMC is mostly the fastest. This implies that the tools’ efficiency does not, so much, depend on sampling but is rather determined by supplementary computations.

• Type: Conference
• Year: 2009
• Where: QEST
• Authors: Joost-Pieter Katoen, Ivan S. Zapreev
• Keywords: Continuous-time Markov Chains, Main Csl Formulae, QEST 2009, Quantitative Evaluation Of Systems, Simulation-based Model-checking Algorithms