@book{99048290a8164fc3b26a086b9a137abe,

title = "Model Checking Infinite-State Markov Chains",

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.",

keywords = "IR-56984, EWI-5757",

author = "Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and L. Cloth",

note = "Imported from CTIT",

year = "2004",

month = dec,

language = "Undefined",

series = "CTIT technical report series",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "TR-CTIT-04-49",

address = "Netherlands",

}