CSL model checking algorithms for QBDs

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

Research output: Contribution to journalArticleAcademicpeer-review

18 Citations (Scopus)
32 Downloads (Pure)

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 languageUndefined
Article number10.1016/j.tcs.2007.05.007
Pages (from-to)24-41
Number of pages18
JournalTheoretical computer science
Volume382
Issue numberLNCS4549/1
DOIs
Publication statusPublished - 28 Aug 2007

Keywords

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

Cite this

Di Pierro, A. (Ed.), Remke, A. K. I., Haverkort, B. R. H. M., Wiklicky, H. (Ed.), & Cloth, L. (2007). CSL model checking algorithms for QBDs. Theoretical computer science, 382(LNCS4549/1), 24-41. [10.1016/j.tcs.2007.05.007]. https://doi.org/10.1016/j.tcs.2007.05.007
Di Pierro, A. (Editor) ; Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. ; Wiklicky, H. (Editor) ; Cloth, L. / CSL model checking algorithms for QBDs. In: Theoretical computer science. 2007 ; Vol. 382, No. LNCS4549/1. pp. 24-41.
@article{18853ae3b9eb4956a240e7eaf966fa19,
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 = "{Di Pierro}, A. and Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and H. Wiklicky and L. Cloth",
note = "10.1016/j.tcs.2007.05.007",
year = "2007",
month = "8",
day = "28",
doi = "10.1016/j.tcs.2007.05.007",
language = "Undefined",
volume = "382",
pages = "24--41",
journal = "Theoretical computer science",
issn = "0304-3975",
publisher = "Elsevier",
number = "LNCS4549/1",

}

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

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

In: Theoretical computer science, Vol. 382, No. LNCS4549/1, 10.1016/j.tcs.2007.05.007, 28.08.2007, p. 24-41.

Research output: Contribution to journalArticleAcademicpeer-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

M1 - 10.1016/j.tcs.2007.05.007

ER -

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