CSL model checking algorithms for QBDs

Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, L. Cloth, A. Di Pierro (Editor), H. Wiklicky (Editor)

Research output: Contribution to journalArticleScientificpeer-review

Abstract

We present an in-depth treatment of model checking lgorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with epresentatives. By the use of an application-driven dynamic stopping criterion the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.
Original languageEnglish
Pages (from-to)24-41
Number of pages18
JournalTheoretical Computer Science
Volume382
Issue numberLNCS4549/1
DOIs
Publication statusPublished - 28 Aug 2007
Externally publishedYes

Fingerprint

Model checking
Model Checking
Birth-death Process
Time Operator
Uniformization
Stopping Criterion
Continuous-time Markov Chain
Bounded Operator
Markov processes
Mathematical operators
Express
Logic
Operator
Class
Model

Keywords

  • EWI-11188
  • IR-61957
  • METIS-241971

Cite this

Remke, A. K. I., Haverkort, B. R. H. M., Cloth, L., Di Pierro, A. (Ed.), & Wiklicky, H. (Ed.) (2007). CSL model checking algorithms for QBDs. Theoretical Computer Science, 382(LNCS4549/1), 24-41. https://doi.org/10.1016/j.tcs.2007.05.007
Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. ; Cloth, L. ; Di Pierro, A. (Editor) ; Wiklicky, H. (Editor). / CSL model checking algorithms for QBDs. In: Theoretical Computer Science. 2007 ; Vol. 382, No. LNCS4549/1. pp. 24-41.
@article{1732fe429603490b9c7bca6f52823fd3,
title = "CSL model checking algorithms for QBDs",
abstract = "We present an in-depth treatment of model checking lgorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with epresentatives. By the use of an application-driven dynamic stopping criterion the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.",
keywords = "EWI-11188, IR-61957, METIS-241971",
author = "Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and L. Cloth and {Di Pierro}, A. and H. Wiklicky",
note = "10.1016/j.tcs.2007.05.007",
year = "2007",
month = "8",
day = "28",
doi = "10.1016/j.tcs.2007.05.007",
language = "English",
volume = "382",
pages = "24--41",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "LNCS4549/1",

}

Remke, AKI, Haverkort, BRHM, Cloth, L, Di Pierro, A (ed.) & Wiklicky, H (ed.) 2007, 'CSL model checking algorithms for QBDs', Theoretical Computer Science, vol. 382, no. LNCS4549/1, pp. 24-41. https://doi.org/10.1016/j.tcs.2007.05.007

CSL model checking algorithms for QBDs. / Remke, Anne Katharina Ingrid; Haverkort, Boudewijn R.H.M.; Cloth, L.; Di Pierro, A. (Editor); Wiklicky, H. (Editor).

In: Theoretical Computer Science, Vol. 382, No. LNCS4549/1, 28.08.2007, p. 24-41.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - CSL model checking algorithms for QBDs

AU - Remke, Anne Katharina Ingrid

AU - Haverkort, Boudewijn R.H.M.

AU - Cloth, L.

A2 - Di Pierro, A.

A2 - Wiklicky, H.

N1 - 10.1016/j.tcs.2007.05.007

PY - 2007/8/28

Y1 - 2007/8/28

N2 - We present an in-depth treatment of model checking lgorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with epresentatives. By the use of an application-driven dynamic stopping criterion the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.

AB - We present an in-depth treatment of model checking lgorithms for a class of infinite-state continuous-time Markov chains known as quasi-birth death processes. The model class is described in detail, as well as the logic CSL to express properties of interest. Using a new property-independency concept, we provide model checking algorithms for all CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with epresentatives. By the use of an application-driven dynamic stopping criterion the algorithm stops whenever the property to be checked can be certified (or falsified). A comprehensive case study of a connection management system shows the versatility of our new algorithms.

KW - EWI-11188

KW - IR-61957

KW - METIS-241971

U2 - 10.1016/j.tcs.2007.05.007

DO - 10.1016/j.tcs.2007.05.007

M3 - Article

VL - 382

SP - 24

EP - 41

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - LNCS4549/1

ER -

Remke AKI, Haverkort BRHM, Cloth L, Di Pierro A, (ed.), Wiklicky H, (ed.). CSL model checking algorithms for QBDs. Theoretical Computer Science. 2007 Aug 28;382(LNCS4549/1):24-41. https://doi.org/10.1016/j.tcs.2007.05.007