CSL model checking algorithms for QBDs

    Research output: Contribution to journalArticleAcademicpeer-review

    20 Citations (Scopus)
    62 Downloads (Pure)


    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 number1
    Publication statusPublished - 28 Aug 2007


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

    Cite this