A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

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

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

    67 Downloads (Pure)

    Abstract

    We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.
    Original languageUndefined
    Title of host publicationThe 6th International Conference on Formal Modelling and Analysis of Timed Systems
    Place of PublicationBerlin
    PublisherSpringer
    Pages188-202
    Number of pages15
    DOIs
    Publication statusPublished - 15 Sep 2008
    Event6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008 - Palais du grand Large, St. Malo, France
    Duration: 15 Sep 200817 Sep 2008
    Conference number: 6
    http://formats08.inria.fr/index.html

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Number302
    ISSN (Print)0302-9743

    Conference

    Conference6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008
    Abbreviated titleFORMATS
    CountryFrance
    CitySt. Malo
    Period15/09/0817/09/08
    Internet address

    Keywords

    • EWI-12928
    • IR-64827
    • METIS-251031

    Cite this

    Remke, A. K. I., & Haverkort, B. R. H. M. (2008). A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. In The 6th International Conference on Formal Modelling and Analysis of Timed Systems (pp. 188-202). [10.1007/978-3-540-85778-5_14] (Lecture Notes in Computer Science; No. 302). Berlin: Springer. https://doi.org/10.1007/978-3-540-85778-5_14
    Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. / A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. The 6th International Conference on Formal Modelling and Analysis of Timed Systems. Berlin : Springer, 2008. pp. 188-202 (Lecture Notes in Computer Science; 302).
    @inproceedings{44cb2bc98b24429eaf2d72657d5a5947,
    title = "A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks",
    abstract = "We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.",
    keywords = "EWI-12928, IR-64827, METIS-251031",
    author = "Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.}",
    year = "2008",
    month = "9",
    day = "15",
    doi = "10.1007/978-3-540-85778-5_14",
    language = "Undefined",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "302",
    pages = "188--202",
    booktitle = "The 6th International Conference on Formal Modelling and Analysis of Timed Systems",

    }

    Remke, AKI & Haverkort, BRHM 2008, A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. in The 6th International Conference on Formal Modelling and Analysis of Timed Systems., 10.1007/978-3-540-85778-5_14, Lecture Notes in Computer Science, no. 302, Springer, Berlin, pp. 188-202, 6th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2008, St. Malo, France, 15/09/08. https://doi.org/10.1007/978-3-540-85778-5_14

    A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. / Remke, Anne Katharina Ingrid; Haverkort, Boudewijn R.H.M.

    The 6th International Conference on Formal Modelling and Analysis of Timed Systems. Berlin : Springer, 2008. p. 188-202 10.1007/978-3-540-85778-5_14 (Lecture Notes in Computer Science; No. 302).

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

    TY - GEN

    T1 - A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks

    AU - Remke, Anne Katharina Ingrid

    AU - Haverkort, Boudewijn R.H.M.

    PY - 2008/9/15

    Y1 - 2008/9/15

    N2 - We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.

    AB - We present a model checking procedure for the CSL until operator on the CTMCs that underlie Jackson queueing networks. The key issue lies in the fact that the underlying CTMC is infinite in as many dimension as there are queues in the JQN. We need to compute the transient state probabilities for all goal states and for all possible starting states. However, for these transient probabilities no computational procedures are readily available. The contribution of this paper is the proposal of a new uniformization-based approach to compute the transient state probabilities. Furthermore, we show how the highly structured state space of JQNs allows us to compute the possible infinite satisfaction set for until formulas. A case study on an e-business site shows the feasibility of our approach.

    KW - EWI-12928

    KW - IR-64827

    KW - METIS-251031

    U2 - 10.1007/978-3-540-85778-5_14

    DO - 10.1007/978-3-540-85778-5_14

    M3 - Conference contribution

    T3 - Lecture Notes in Computer Science

    SP - 188

    EP - 202

    BT - The 6th International Conference on Formal Modelling and Analysis of Timed Systems

    PB - Springer

    CY - Berlin

    ER -

    Remke AKI, Haverkort BRHM. A uniformization-based algorithm for model checking the CSL until operator on labeled queueing networks. In The 6th International Conference on Formal Modelling and Analysis of Timed Systems. Berlin: Springer. 2008. p. 188-202. 10.1007/978-3-540-85778-5_14. (Lecture Notes in Computer Science; 302). https://doi.org/10.1007/978-3-540-85778-5_14