Safe on-the-fly steady-state detection for time-bounded reachability

Joost P. Katoen, I.S. Zapreev

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    18 Citations (Scopus)


    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
    Original languageUndefined
    Title of host publicationQuantitative Evaluation of Systems (QEST)
    Place of PublicationLos Alamitos
    PublisherIEEE Computer Society Press
    Number of pages10
    ISBN (Print)0-7695-2665-9
    Publication statusPublished - Sep 2006
    Event3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006 - University of California, Riverside, United States
    Duration: 11 Sep 200614 Sep 2006
    Conference number: 3

    Publication series

    PublisherIEEE Computer Society Press


    Conference3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
    Abbreviated titleQEST
    Country/TerritoryUnited States
    Internet address


    • EWI-8233
    • IR-63705
    • METIS-237638

    Cite this