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)
    41 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