CSL Model Checking Algorithms for Infinite-state Structured Markov chains

Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, J.-F. Raskin (Editor), P.S. Thiagarajan (Editor)

Research output: Other contribution

6 Citations (Scopus)

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 languageEnglish
PublisherSpringer Verlag
Number of pages16
Place of PublicationLondon
ISBN (Print)978-3-540-75453-4
DOIs
Publication statusPublished - 3 Oct 2007
Externally publishedYes

Keywords

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

Fingerprint Dive into the research topics of 'CSL Model Checking Algorithms for Infinite-state Structured Markov chains'. Together they form a unique fingerprint.

  • Cite this

    Remke, A. K. I., Haverkort, B. R. H. M., Raskin, J-F. (Ed.), & Thiagarajan, P. S. (Ed.) (2007, Oct 3). CSL Model Checking Algorithms for Infinite-state Structured Markov chains. London: Springer Verlag. https://doi.org/10.1007/978-3-540-75454-1_24