loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Third International Conference on the Quantitative Evaluation of Systems - (QEST'06)
Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability
Riverside, California
September 11-September 14
ISBN: 0-7695-2665-9
Joost-Pieter Katoen, RWTH Aachen, Software Modeling and Verification Group, D-52056 Aachen, Germany
Ivan S. Zapreev, University of Twente, P.O. Box 217, 7500 AE Enschede, The Netherlands
The time-bounded reachability problem for continuoustime Markov chains (CTMCs) amounts to determine the probability to reach a (set of) goal state(s) within a given time span, such that prior to reaching the goal certain states are avoided. Efficient algorithms for time-bounded reachability are at the heart of probabilistic model checkers such as PRISM and ETMCC. For large time spans, on-the-fly steady-state detection is commonly applied. To obtain correct results (up to a given accuracy), it is essential to avoid detecting premature stationarity. This paper gives a detailed account of criteria for steady-state detection in the setting of time-bounded reachability. This is done for forward and backward reachability algorithms. As a spin-off of this study, new results for on-the-fly steady-state detection during CTMC transient analysis are reported. Based on these results, a precise procedure for steady-state detection for time-bounded reachability is obtained. Experiments show the impact of these results in probabilistic model checking.
Citation:
Joost-Pieter Katoen, Ivan S. Zapreev, "Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability," qest, pp.301-310, Third International Conference on the Quantitative Evaluation of Systems - (QEST'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.