Faster and symbolic CTMC model checking

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

doi:10.1007/3-540-44804-7_2

Faster and symbolic CTMC model checking

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

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

50 Citations (Scopus)

1 Downloads (Pure)

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 language	English
Title of host publication	Process Algebra and Probabilistic Methods, Performance Modeling and Verification
Subtitle of host publication	Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings
Editors	S. Gilmore, L. de Alfaro
Place of Publication	Berlin
Publisher	Springer
Pages	23-38
Number of pages	16
ISBN (Print)	3-540-42556-X
DOIs	https://doi.org/10.1007/3-540-44804-7_2
Publication status	Published - 2001
Event	Process Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001 - Aachen, Germany Duration: 12 Sept 2001 → 14 Sept 2001

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2165
ISSN (Print)	0302-9743

Conference

Conference	Process Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001
Country/Territory	Germany
City	Aachen
Period	12/09/01 → 14/09/01

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

Access to Document

10.1007/3-540-44804-7_2

http://link.springer.de/link/service/series/0558/bibs/2165/21650023.htm

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 Aachen, Germany, September 12–14, 2001 Proceedings (pp. 23-38). (Lecture Notes in Computer Science; Vol. 2165). Springer. https://doi.org/10.1007/3-540-44804-7_2

Katoen, Joost P. ; Kwiatkowska, Marta ; Norman, Gethin et al. / Faster and symbolic CTMC model checking. Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. 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 = "English",

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

address = "Germany",

note = "Process Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001 ; Conference date: 12-09-2001 Through 14-09-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 Aachen, Germany, September 12–14, 2001 Proceedings. Lecture Notes in Computer Science, vol. 2165, Springer, Berlin, pp. 23-38, Process Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001, Aachen, Germany, 12/09/01. https://doi.org/10.1007/3-540-44804-7_2

Faster and symbolic CTMC model checking. / Katoen, Joost P.; Kwiatkowska, Marta; Norman, Gethin et al.
Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001 Aachen, Germany, September 12–14, 2001 Proceedings. 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 proceeding › Conference contribution › Academic › peer-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

A2 - Gilmore, S.

A2 - de Alfaro, L.

PB - Springer

CY - Berlin

T2 - Process Algebra and Probabilistic Methods - Performance Modelling in Verification, PAPM-PROBMIV 2001

Y2 - 12 September 2001 through 14 September 2001

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 Aachen, Germany, September 12–14, 2001 Proceedings. Berlin: Springer. 2001. p. 23-38. (Lecture Notes in Computer Science). doi: 10.1007/3-540-44804-7_2

Faster and symbolic CTMC model checking

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this