Time-bounded reachability in tree-structured QBDs by abstraction

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)
7 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

@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 -