Model-checking large structured Markov chains

Buchholz, P. and Katoen, J.P. and Kemper, P. and Tepper, C. (2003) Model-checking large structured Markov chains. Journal of Logic and Algebraic Programming, 56 (1-2). pp. 69-97. ISSN 1567-8326

PDF
Restricted to UT campus only: Request a copy
364Kb

Abstract:	This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.
Item Type:	Article
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/63268
Official URL:	http://dx.doi.org/10.1016/S1567-8326(02)00067-X
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page