Time-Bounded Reachability in Tree-Structured QBDs by Abstraction

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

1 Citation (Scopus)
61 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
Klink, Daniel ; Remke, Anne Katharina Ingrid ; Haverkort, Boudewijn R.H.M. ; Katoen, Joost P. / Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09). IEEE Computer Society, 2009. pp. 133-142
@inproceedings{db9f3fda88a248dfb33c0b52c515b487,
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, 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.",
keywords = "METIS-264128, EWI-16466, IR-68308",
author = "Daniel Klink and Remke, {Anne Katharina Ingrid} and Haverkort, {Boudewijn R.H.M.} and Katoen, {Joost P.}",
note = "10.1109/QEST.2009.9",
year = "2009",
month = "9",
doi = "10.1109/QEST.2009.9",
language = "Undefined",
isbn = "978-0-7695-3808-2",
publisher = "IEEE Computer Society",
pages = "133--142",
booktitle = "Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09)",
address = "United States",

}

Klink, D, Remke, AKI, Haverkort, BRHM & Katoen, JP 2009, Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. in Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09)., 10.1109/QEST.2009.9, IEEE Computer Society, pp. 133-142, 6th International Conference on Quantitative Evaluation of SysTems, QEST 2009, Budapest, Hungary, 13/09/09. https://doi.org/10.1109/QEST.2009.9

Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. / Klink, Daniel; Remke, Anne Katharina Ingrid; Haverkort, Boudewijn R.H.M.; Katoen, Joost P.

Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09). IEEE Computer Society, 2009. p. 133-142 10.1109/QEST.2009.9.

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

TY - GEN

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.1109/QEST.2009.9

PY - 2009/9

Y1 - 2009/9

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, 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.

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, 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.

KW - METIS-264128

KW - EWI-16466

KW - IR-68308

U2 - 10.1109/QEST.2009.9

DO - 10.1109/QEST.2009.9

M3 - Conference contribution

SN - 978-0-7695-3808-2

SP - 133

EP - 142

BT - Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09)

PB - IEEE Computer Society

ER -

Klink D, Remke AKI, Haverkort BRHM, Katoen JP. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. In Sixth International Conference on the Quantitative Evaluation of Systems, (QEST '09). IEEE Computer Society. 2009. p. 133-142. 10.1109/QEST.2009.9 https://doi.org/10.1109/QEST.2009.9