Simulation-based CTMC Model Checking: An Empirical Evaluation

Joost P. Katoen, I.S. Zapreev

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

10 Citations (Scopus)
57 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 languageUndefined
Title of host publicationSixth International Conference on the Quantitative Evaluation of Systems
Place of PublicationLos Alamitos
PublisherIEEE Computer Society Press
Pages31-40
Number of pages10
ISBN (Print)978-1-42444-942-2
DOIs
Publication statusPublished - Sep 2009
Event6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary
Duration: 13 Sep 200916 Sep 2009
Conference number: 6
http://www.qest.org/qest2009/

Publication series

Name
PublisherIEEE Computer Society Press

Conference

Conference6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
Abbreviated titleQEST
CountryHungary
CityBudapest
Period13/09/0916/09/09
Internet address

Keywords

  • METIS-264290
  • EWI-17103
  • IR-69307

Cite this

Katoen, J. P., & Zapreev, I. S. (2009). Simulation-based CTMC Model Checking: An Empirical Evaluation. In Sixth International Conference on the Quantitative Evaluation of Systems (pp. 31-40). [10.1109/QEST.2009.25] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/QEST.2009.25
Katoen, Joost P. ; Zapreev, I.S. / Simulation-based CTMC Model Checking: An Empirical Evaluation. Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos : IEEE Computer Society Press, 2009. pp. 31-40
@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",
year = "2009",
month = "9",
doi = "10.1109/QEST.2009.25",
language = "Undefined",
isbn = "978-1-42444-942-2",
publisher = "IEEE Computer Society Press",
pages = "31--40",
booktitle = "Sixth International Conference on the Quantitative Evaluation of Systems",

}

Katoen, JP & Zapreev, IS 2009, Simulation-based CTMC Model Checking: An Empirical Evaluation. in Sixth International Conference on the Quantitative Evaluation of Systems., 10.1109/QEST.2009.25, IEEE Computer Society Press, Los Alamitos, pp. 31-40, 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009, Budapest, Hungary, 13/09/09. https://doi.org/10.1109/QEST.2009.25

Simulation-based CTMC Model Checking: An Empirical Evaluation. / Katoen, Joost P.; Zapreev, I.S.

Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos : IEEE Computer Society Press, 2009. p. 31-40 10.1109/QEST.2009.25.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

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

AU - Katoen, Joost P.

AU - Zapreev, I.S.

N1 - 10.1109/QEST.2009.25

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 Computer Society Press

CY - Los Alamitos

ER -

Katoen JP, Zapreev IS. Simulation-based CTMC Model Checking: An Empirical Evaluation. In Sixth International Conference on the Quantitative Evaluation of Systems. Los Alamitos: IEEE Computer Society Press. 2009. p. 31-40. 10.1109/QEST.2009.25 https://doi.org/10.1109/QEST.2009.25