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 journalArticleScientificpeer-review

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 languageEnglish
Pages (from-to)105-125
Number of pages21
JournalPerformance Evaluation
Volume68
Issue number2
DOIs
Publication statusPublished - Feb 2011
Externally publishedYes

Fingerprint

Reachability
Markov processes
Model checking
Probabilistic Automata
Birth-death Process
Pushdown Automata
Uniformization
Continuous-time Markov Chain
Markov Decision Process
Direct Method
Model Checking
Performance Evaluation
Markov chain
State Space
Partition
Grid
Interval
Abstraction
Approximation

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{395763bd2f3d4765bf5ae39bc7c2d960,
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 = "English",
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 journalArticleScientificpeer-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 -