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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    1 Citation (Scopus)
    84 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, results 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
    Title of host publicationSixth International Conference on the Quantitative Evaluation of Systems, (QEST '09)
    PublisherIEEE Computer Society
    Pages133-142
    Number of pages10
    ISBN (Print)978-0-7695-3808-2
    DOIs
    Publication statusPublished - Sep 2009
    Event6th International Conference on Quantitative Evaluation of SysTems, QEST 2009 - Technical University of Budapest, Budapest, Hungary
    Duration: 13 Sep 200916 Sep 2009
    Conference number: 6
    http://www.qest.org/qest2009/

    Publication series

    Name
    PublisherIEEE Computer Society

    Conference

    Conference6th International Conference on Quantitative Evaluation of SysTems, QEST 2009
    Abbreviated titleQEST
    CountryHungary
    CityBudapest
    Period13/09/0916/09/09
    Internet address

    Keywords

    • METIS-264128
    • EWI-16466
    • IR-68308

    Cite this

    Klink, D., Remke, A. K. I., Haverkort, B. R. H. M., & Katoen, J. P. (2009). Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. In Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09) (pp. 133-142). [10.1109/QEST.2009.9] IEEE Computer Society. https://doi.org/10.1109/QEST.2009.9