Model checking Infinite-State Markov Chains

Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, L. Cloth, Nicolas Halbwachs (Editor), Lenore D. Zuck (Editor)

Research output: Other contribution

24 Citations (Scopus)


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 languageEnglish
PublisherSpringer Verlag
Number of pages16
Place of PublicationBerlin / Heidelberg, Germany
ISBN (Print)9783540253334
Publication statusPublished - 2005
Externally publishedYes


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


Dive into the research topics of 'Model checking Infinite-State Markov Chains'. Together they form a unique fingerprint.

Cite this