### 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.

Original language | Undefined |
---|---|

Title of host publication | 5th International Conference, FORMATS 2007 |

Editors | J.-F. Raskin, P.S. Thiagarajan |

Place of Publication | London |

Publisher | Springer |

Pages | 336-351 |

Number of pages | 16 |

ISBN (Print) | 978-3-540-75453-4 |

DOIs | |

Publication status | Published - 3 Oct 2007 |

Event | 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007 - Salzburg, Austria Duration: 3 Oct 2007 → 5 Oct 2007 Conference number: 5 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Number | LNCS4549 |

Volume | 4763 |

### Conference

Conference | 5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007 |
---|---|

Abbreviated title | FORMATS |

Country | Austria |

City | Salzburg |

Period | 3/10/07 → 5/10/07 |

### Keywords

- EWI-11189
- METIS-241972
- IR-61958

## Cite this

Remke, A. K. I., & Haverkort, B. R. H. M. (2007). CSL Model Checking Algorithms for Infinite-state Structured Markov chains. In J-F. Raskin, & P. S. Thiagarajan (Eds.),

*5th International Conference, FORMATS 2007*(pp. 336-351). [10.1007/978-3-540-75454-1_24] (Lecture Notes in Computer Science; Vol. 4763, No. LNCS4549). London: Springer. https://doi.org/10.1007/978-3-540-75454-1_24