Model Checking Infinite-State Markov Chains

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

    Research output: Book/ReportReportOther research output

    547 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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages16
    Publication statusPublished - Dec 2004

    Publication series

    NameCTIT technical report series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-04-49

    Keywords

    • IR-56984
    • EWI-5757

    Cite this

    Remke, A. K. I., Haverkort, B. R. H. M., & Cloth, L. (2004). Model Checking Infinite-State Markov Chains. (CTIT technical report series; No. TR-CTIT-04-49). Enschede: Centre for Telematics and Information Technology (CTIT).