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

20 Citations (Scopus)


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
Issue numberLNCS4549/1
Publication statusPublished - 28 Aug 2007
Externally publishedYes


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


Dive into the research topics of 'CSL model checking algorithms for QBDs'. Together they form a unique fingerprint.

Cite this