Model checking Infinite-State Markov Chains

Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, L. Cloth

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    23 Citations (Scopus)
    10 Downloads (Pure)

    Abstract

    In this paper algorithms for model checking CSL (continuous stochastic logic) against infinite-state continuous-time Markov chains of so-called quasi birth-death type are developed. In doing so we extend the applicability of CSL model checking beyond the recently proposed case for finite-state continuous-time Markov chains, to an important class of infinite-state Markov chains. We present syntax and semantics for CSL and develop efficient model checking algorithms for the steady-state operator and the time-bounded next and until operator. For the former, we rely on the so-called matrix-geometric solution of the steady-state probabilities of the infinite-state Markov chain. For the time-bounded until operator we develop a new algorithm for the transient analysis of infinite-state Markov chains, thereby exploiting the quasi birth-death structure. A case study shows the feasibility of our approach. The work presented in this paper has been performed in the context of the MC=MC project (612.000.311), financed by the Netherlands Organization for Scientific Research (NWO) and is based on the diploma thesis [18], supported by the German Academic Exchange Service (DAAD).
    Original languageUndefined
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005)
    EditorsNicolas Halbwachs, Lenore D. Zuck
    Place of PublicationBerlin / Heidelberg, Germany
    PublisherSpringer
    Pages237-252
    Number of pages16
    ISBN (Print)9783540253334
    DOIs
    Publication statusPublished - 2005
    Event11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005 - Edinburgh, United Kingdom
    Duration: 4 Apr 20058 Apr 2005
    Conference number: 11

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume3440
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005
    Abbreviated titleTACAS
    CountryUnited Kingdom
    CityEdinburgh
    Period4/04/058/04/05

    Keywords

    • EWI-7894
    • METIS-225561
    • IR-63633

    Cite this

    Remke, A. K. I., Haverkort, B. R. H. M., & Cloth, L. (2005). Model checking Infinite-State Markov Chains. In N. Halbwachs, & L. D. Zuck (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005) (pp. 237-252). (Lecture Notes in Computer Science; Vol. 3440). Berlin / Heidelberg, Germany: Springer. https://doi.org/10.1007/978-3-540-31980-1_16, https://doi.org/10.1007/b107194