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

    17 Citations (Scopus)

    Abstract

    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
    Pages301-310
    Number of pages10
    ISBN (Print)0-7695-2665-9
    DOIs
    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
    http://www.qest.org/qest2006/

    Publication series

    Name
    PublisherIEEE Computer Society Press
    Number10

    Conference

    Conference3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006
    Abbreviated titleQEST
    CountryUnited States
    CityRiverside
    Period11/09/0614/09/06
    Internet address

    Keywords

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

    Cite this

    Katoen, J. P., & Zapreev, I. S. (2006). Safe on-the-fly steady-state detection for time-bounded reachability. In Quantitative Evaluation of Systems (QEST) (pp. 301-310). [10.1109/QEST.2006.47] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/QEST.2006.47