Sciweavers

Share
FORMATS
2007
Springer

CSL Model Checking Algorithms for Infinite-State Structured Markov Chains

10 years 5 months ago
CSL Model Checking Algorithms for Infinite-State Structured Markov Chains
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.
Anne Remke, Boudewijn R. Haverkort
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where FORMATS
Authors Anne Remke, Boudewijn R. Haverkort
Comments (0)
books