Time-bounded reachability in tree-structured QBDs by abstraction
conference paper
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 performanceevaluation.Wedeterminetime-boundedreachabilityprobabilitiesinthese processes– which with direct methods, i.e., uniformization, result in an exponential blowup–byapplyingabstraction. We contrast abstraction based on Markov decision processes (MDPs) andinterval-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.
TNO Identifier
954287
ISSN
01665316
Publisher
Elsevier
Source title
Performance Evaluation
Pages
105-125
Files
To receive the publication files, please send an e-mail request to TNO Repository.