Faster and symbolic CTMC model checking

Joost P. Katoen, Marta Kwiatkowska, Gethin Norman, David Parker

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

47 Citations (Scopus)

Abstract

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 includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.
Original languageUndefined
Title of host publicationProcess Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001
EditorsS. Gilmore, L. de Alfaro
Place of PublicationBerlin
PublisherSpringer
Pages23-38
Number of pages16
ISBN (Print)3-540-42556-X
DOIs
Publication statusPublished - 2001

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2165
ISSN (Print)0302-9743

Keywords

  • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
  • FMT-BDD: BINARY DECISION DIAGRAMS
  • FMT-PM: PROBABILISTIC METHODS
  • FMT-MC: MODEL CHECKING
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • FMT-TOOLS
  • EWI-6449
  • IR-63281
  • METIS-203851

Cite this

Katoen, J. P., Kwiatkowska, M., Norman, G., & Parker, D. (2001). Faster and symbolic CTMC model checking. In S. Gilmore, & L. de Alfaro (Eds.), Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 (pp. 23-38). (Lecture Notes in Computer Science; Vol. 2165). Berlin: Springer. https://doi.org/10.1007/3-540-44804-7_2
Katoen, Joost P. ; Kwiatkowska, Marta ; Norman, Gethin ; Parker, David. / Faster and symbolic CTMC model checking. Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. editor / S. Gilmore ; L. de Alfaro. Berlin : Springer, 2001. pp. 23-38 (Lecture Notes in Computer Science).
@inproceedings{f9ce3196db8a4f98b88c847c25d44bd1,
title = "Faster and symbolic CTMC model checking",
abstract = "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 includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.",
keywords = "FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, FMT-BDD: BINARY DECISION DIAGRAMS, FMT-PM: PROBABILISTIC METHODS, FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-TOOLS, EWI-6449, IR-63281, METIS-203851",
author = "Katoen, {Joost P.} and Marta Kwiatkowska and Gethin Norman and David Parker",
year = "2001",
doi = "10.1007/3-540-44804-7_2",
language = "Undefined",
isbn = "3-540-42556-X",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "23--38",
editor = "S. Gilmore and {de Alfaro}, L.",
booktitle = "Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001",

}

Katoen, JP, Kwiatkowska, M, Norman, G & Parker, D 2001, Faster and symbolic CTMC model checking. in S Gilmore & L de Alfaro (eds), Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. Lecture Notes in Computer Science, vol. 2165, Springer, Berlin, pp. 23-38. https://doi.org/10.1007/3-540-44804-7_2

Faster and symbolic CTMC model checking. / Katoen, Joost P.; Kwiatkowska, Marta; Norman, Gethin; Parker, David.

Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. ed. / S. Gilmore; L. de Alfaro. Berlin : Springer, 2001. p. 23-38 (Lecture Notes in Computer Science; Vol. 2165).

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

TY - GEN

T1 - Faster and symbolic CTMC model checking

AU - Katoen, Joost P.

AU - Kwiatkowska, Marta

AU - Norman, Gethin

AU - Parker, David

PY - 2001

Y1 - 2001

N2 - 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 includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.

AB - 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 includes the means to express both transient and steady-state performance measures. We show that all CSL operators can be treated using standard operations on MTBDDs, thus allowing a rather straightforward implementation of symbolic CSL model checking on existing MTBDD-based platforms such as the verifier PRISM. The main result of the paper is an improvement of O(N)]]> in the time complexity of checking time-bounded until-formulas, where N is the number of states in the CTMC under consideration. This result yields a drastic speed-up in the verification time of model checking CTMCs, both in the symbolic and non-symbolic case.

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-TOOLS

KW - EWI-6449

KW - IR-63281

KW - METIS-203851

U2 - 10.1007/3-540-44804-7_2

DO - 10.1007/3-540-44804-7_2

M3 - Conference contribution

SN - 3-540-42556-X

T3 - Lecture Notes in Computer Science

SP - 23

EP - 38

BT - Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001

A2 - Gilmore, S.

A2 - de Alfaro, L.

PB - Springer

CY - Berlin

ER -

Katoen JP, Kwiatkowska M, Norman G, Parker D. Faster and symbolic CTMC model checking. In Gilmore S, de Alfaro L, editors, Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. Berlin: Springer. 2001. p. 23-38. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-44804-7_2