Time-bounded reachability in tree-structured QBDs by abstraction

Share/Save/Bookmark

Klink, Daniel and Remke, Anne and Haverkort, Boudewijn R. and Katoen, Joost-Pieter (2011) Time-bounded reachability in tree-structured QBDs by abstraction. Performance Evaluation, 68 (2). pp. 105-125. ISSN 0166-5316

[img] PDF
Restricted to UT campus only
: Request a copy
1MB
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.
Item Type:Article
Copyright:© 2011 Elsevier
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/72833
Official URL:http://dx.doi.org/10.1016/j.peva.2010.04.002
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 271008