CSL Model Checking Algorithms for Infinite-state Structured Markov chains

Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)
    36 Downloads (Pure)

    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 languageUndefined
    Title of host publication5th International Conference, FORMATS 2007
    EditorsJ.-F. Raskin, P.S. Thiagarajan
    Place of PublicationLondon
    PublisherSpringer
    Pages336-351
    Number of pages16
    ISBN (Print)978-3-540-75453-4
    DOIs
    Publication statusPublished - 3 Oct 2007
    Event5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007 - Salzburg, Austria
    Duration: 3 Oct 20075 Oct 2007
    Conference number: 5

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberLNCS4549
    Volume4763

    Conference

    Conference5th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2007
    Abbreviated titleFORMATS
    CountryAustria
    CitySalzburg
    Period3/10/075/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