Model checking Infinite-State Markov Chains


Share/Save/Bookmark

Remke, Anne and Haverkort, Boudewijn R. and Cloth, Lucia (2005) Model checking Infinite-State Markov Chains. In: 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 4-8 April 2005, Edinburgh, UK.

[img]PDF
Restricted to UT campus only
: Request a copy
203Kb
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.
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).
Item Type:Conference or Workshop Item
Copyright:© 2005 Springer
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63633
Official URL:http://dx.doi.org/10.1007/b107194
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 225561