Back to University of Twente portal
Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability
Katoen, Joost-Pieter and Zapreev, Ivan S. (2005) Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 203Kb |
| Abstract: | The time-bounded reachability problemfor continuous-timeMarkov 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 technical report 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. |
| Item Type: | Report |
| Copyright: | ©2005 CTIT |
| Link to this item: | http://purl.utwente.nl/publications/57041 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page