CSL Model Checking Algorithms for Infinite-state Structured Markov chains

Remke, Anne and Haverkort, Boudewijn R. (2007) CSL Model Checking Algorithms for Infinite-state Structured Markov chains. In: 5th International Conferenceon Formal Modeling and Analysis of Timed Systems, FORMATS 2007, October 3-5, 2007, Salzburg, Austria.

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

Abstract:	Jackson queueing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the continuous-time Markov chain (CTMC) that underlies such a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues. We present CSL model checking algorithms for labeled JQNs. To do so, we rely on well-known product-form results for the steady-state probabilities in (stable) JQNs. The transient probabilities are computed using an uniformization-based approach. We develop a new notion of property independence that allows us to define model checking algorithms for labeled JQNs.
Item Type:	Conference or Workshop Item
Copyright:	© 2007 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Design and Analysis of Communication Systems (DACS)
Link to this item:	http://purl.utwente.nl/publications/61958
Official URL:	http://dx.doi.org/10.1007/978-3-540-75454-1_24
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 241972