CSL model checking algorithms for infinite-state structured Markov chains. (English) Zbl 1141.68355
Raskin, Jean-François (ed.) et al., Formal modeling and analysis of timed systems. 5th international conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75453-4/pbk). Lecture Notes in Computer Science 4763, 336-351 (2007).
Summary: 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.
For the entire collection see [Zbl 1138.68007].
For the entire collection see [Zbl 1138.68007].
MSC:
| 68M20 | Performance evaluation, queueing, and scheduling in the context of computer systems |
| 60K25 | Queueing theory (aspects of probability theory) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
