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

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


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

    Cite this