Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability

Joost P. Katoen, I.S. Zapreev

    Research output: Book/ReportReportProfessional

    40 Downloads (Pure)

    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherFormal Methods and Tools (FMT)
    Number of pages32
    Publication statusPublished - Nov 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-05-52
    ISSN (Print)1381-3625

    Keywords

    • IR-57041
    • METIS-248099
    • EWI-5724

    Cite this

    Katoen, J. P., & Zapreev, I. S. (2005). Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. (CTIT Technical Report Series; No. TR-CTIT-05-52). Enschede: Formal Methods and Tools (FMT).