Time-bounded reachability in tree-structured QBDs by abstraction

Daniel Klink, Anne Katharina Ingrid Remke, Boudewijn R.H.M. Haverkort, Joost P. Katoen

    Research output: Contribution to journalArticleAcademicpeer-review

    4 Citations (Scopus)
    14 Downloads (Pure)

    Abstract

    This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performance evaluation. We determine time-bounded reachability probabilities in these processes–which with direct methods, i.e., uniformization, result in an exponential blow-up–by applying abstraction. We contrast abstraction based on Markov decision processes (MDPs) and interval-based abstraction; study various schemes to partition the state space, and empirically show their influence on the accuracy of the obtained reachability probabilities. Results show that grid-like schemes, in contrast to chain- and tree-like ones, yield extremely precise approximations for rather coarse abstractions.
    Original languageUndefined
    Pages (from-to)105-125
    Number of pages21
    JournalPerformance evaluation
    Volume68
    Issue number2
    DOIs
    Publication statusPublished - Feb 2011

    Keywords

    • EWI-18354
    • Queueing Theory
    • Reachability
    • IR-72833
    • Markov chains
    • Probabilistic simulation
    • METIS-271008
    • Abstraction

    Cite this

    Klink, Daniel ; Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. ; Katoen, Joost P. / Time-bounded reachability in tree-structured QBDs by abstraction. In: Performance evaluation. 2011 ; Vol. 68, No. 2. pp. 105-125.
    @article{d38caa99de7e47e7a5b781233a15fe3a,
    title = "Time-bounded reachability in tree-structured QBDs by abstraction",
    abstract = "This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performance evaluation. We determine time-bounded reachability probabilities in these processes–which with direct methods, i.e., uniformization, result in an exponential blow-up–by applying abstraction. We contrast abstraction based on Markov decision processes (MDPs) and interval-based abstraction; study various schemes to partition the state space, and empirically show their influence on the accuracy of the obtained reachability probabilities. Results show that grid-like schemes, in contrast to chain- and tree-like ones, yield extremely precise approximations for rather coarse abstractions.",
    keywords = "EWI-18354, Queueing Theory, Reachability, IR-72833, Markov chains, Probabilistic simulation, METIS-271008, Abstraction",
    author = "Daniel Klink and Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and Katoen, {Joost P.}",
    note = "10.1016/j.peva.2010.04.002",
    year = "2011",
    month = "2",
    doi = "10.1016/j.peva.2010.04.002",
    language = "Undefined",
    volume = "68",
    pages = "105--125",
    journal = "Performance evaluation",
    issn = "0166-5316",
    publisher = "Elsevier",
    number = "2",

    }

    Time-bounded reachability in tree-structured QBDs by abstraction. / Klink, Daniel; Remke, Anne Katharina Ingrid; Haverkort, Boudewijn R.H.M.; Katoen, Joost P.

    In: Performance evaluation, Vol. 68, No. 2, 02.2011, p. 105-125.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Time-bounded reachability in tree-structured QBDs by abstraction

    AU - Klink, Daniel

    AU - Remke, Anne Katharina Ingrid

    AU - Haverkort, Boudewijn R.H.M.

    AU - Katoen, Joost P.

    N1 - 10.1016/j.peva.2010.04.002

    PY - 2011/2

    Y1 - 2011/2

    N2 - This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performance evaluation. We determine time-bounded reachability probabilities in these processes–which with direct methods, i.e., uniformization, result in an exponential blow-up–by applying abstraction. We contrast abstraction based on Markov decision processes (MDPs) and interval-based abstraction; study various schemes to partition the state space, and empirically show their influence on the accuracy of the obtained reachability probabilities. Results show that grid-like schemes, in contrast to chain- and tree-like ones, yield extremely precise approximations for rather coarse abstractions.

    AB - This paper studies quantitative model checking of infinite tree-like (continuous-time) Markov chains. These tree-structured quasi-birth death processes are equivalent to probabilistic pushdown automata and recursive Markov chains and are widely used in the field of performance evaluation. We determine time-bounded reachability probabilities in these processes–which with direct methods, i.e., uniformization, result in an exponential blow-up–by applying abstraction. We contrast abstraction based on Markov decision processes (MDPs) and interval-based abstraction; study various schemes to partition the state space, and empirically show their influence on the accuracy of the obtained reachability probabilities. Results show that grid-like schemes, in contrast to chain- and tree-like ones, yield extremely precise approximations for rather coarse abstractions.

    KW - EWI-18354

    KW - Queueing Theory

    KW - Reachability

    KW - IR-72833

    KW - Markov chains

    KW - Probabilistic simulation

    KW - METIS-271008

    KW - Abstraction

    U2 - 10.1016/j.peva.2010.04.002

    DO - 10.1016/j.peva.2010.04.002

    M3 - Article

    VL - 68

    SP - 105

    EP - 125

    JO - Performance evaluation

    JF - Performance evaluation

    SN - 0166-5316

    IS - 2

    ER -