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)
    37 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