@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",
}