Time-Bounded Reachability in Tree-Structured QBDs by Abstraction


Klink, Daniel and Remke, Anne and Haverkort, Boudewijn R. and Katoen, Joost-Pieter (2009) Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. In: Sixth International Conference on the Quantitative Evaluation of Systems, QEST, 13-16 Sept 2009, Budapest, Hungary (pp. pp. 133-142).

open access
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.
Item Type:Conference or Workshop Item
Copyright:© 2009 IEEE
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/68308
Official URL:https://doi.org/10.1109/QEST.2009.9
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page