Back to University of Twente portal
Model Checking Infinite-State Markov Chains
Remke, Anne and Haverkort, Boudewijn R. and Cloth, Lucia (2004) Model Checking Infinite-State Markov Chains. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 215Kb |
| 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. |
| Item Type: | Report |
| Copyright: | ©2004 CTIT |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/56984 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page