Simulation-based CTMC Model Checking: An Empirical Evaluation

Joost P. Katoen; I.S. Zapreev

doi:10.1109/QEST.2009.25

Simulation-based CTMC Model Checking: An Empirical Evaluation

Joost P. Katoen, I.S. Zapreev

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

11 Citations (Scopus)

195 Downloads (Pure)

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.

Original language	Undefined
Title of host publication	Sixth International Conference on the Quantitative Evaluation of Systems
Place of Publication	Los Alamitos
Publisher	IEEE
Pages	31-40
Number of pages	10
ISBN (Print)	978-1-42444-942-2
DOIs	https://doi.org/10.1109/QEST.2009.25
Publication status	Published - Sept 2009
Event	6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary Duration: 13 Sept 2009 → 16 Sept 2009 Conference number: 6 http://www.qest.org/qest2009/

Publication series

Name
Publisher	IEEE Computer Society Press

Conference

Conference	6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
Abbreviated title	QEST
Country/Territory	Hungary
City	Budapest
Period	13/09/09 → 16/09/09
Internet address	http://www.qest.org/qest2009/

Keywords

METIS-264290
EWI-17103
IR-69307

Access to Document

10.1109/QEST.2009.25

Cite this

@inproceedings{118817bbec1d4bf49dc6c228c65e4a47,

title = "Simulation-based CTMC Model Checking: An Empirical Evaluation",

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.",

keywords = "METIS-264290, EWI-17103, IR-69307",

author = "Katoen, {Joost P.} and I.S. Zapreev",

note = "10.1109/QEST.2009.25 ; 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 ; Conference date: 13-09-2009 Through 16-09-2009",

year = "2009",

month = sep,

doi = "10.1109/QEST.2009.25",

language = "Undefined",

isbn = "978-1-42444-942-2",

publisher = "IEEE",

pages = "31--40",

booktitle = "Sixth International Conference on the Quantitative Evaluation of Systems",

address = "United States",

url = "http://www.qest.org/qest2009/",

}

TY - GEN

T1 - Simulation-based CTMC Model Checking: An Empirical Evaluation

AU - Katoen, Joost P.

AU - Zapreev, I.S.

N1 - Conference code: 6

PY - 2009/9

Y1 - 2009/9

N2 - 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.

AB - 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.

KW - METIS-264290

KW - EWI-17103

KW - IR-69307

U2 - 10.1109/QEST.2009.25

DO - 10.1109/QEST.2009.25

M3 - Conference contribution

SN - 978-1-42444-942-2

SP - 31

EP - 40

BT - Sixth International Conference on the Quantitative Evaluation of Systems

PB - IEEE

CY - Los Alamitos

T2 - 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009

Y2 - 13 September 2009 through 16 September 2009

ER -