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

Joost P. Katoen, I.S. Zapreev

Research output: Book/ReportReportProfessional

29 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).
Katoen, Joost P. ; Zapreev, I.S. / Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. Enschede : Formal Methods and Tools (FMT), 2005. 32 p. (CTIT Technical Report Series; TR-CTIT-05-52).
@book{a92aa3094eef44d695f5f568735890d3,
title = "Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability",
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.",
keywords = "IR-57041, METIS-248099, EWI-5724",
author = "Katoen, {Joost P.} and I.S. Zapreev",
note = "Imported from CTIT",
year = "2005",
month = "11",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Formal Methods and Tools (FMT)",
number = "TR-CTIT-05-52",

}

Katoen, JP & Zapreev, IS 2005, Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. CTIT Technical Report Series, no. TR-CTIT-05-52, Formal Methods and Tools (FMT), Enschede.

Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. / Katoen, Joost P.; Zapreev, I.S.

Enschede : Formal Methods and Tools (FMT), 2005. 32 p. (CTIT Technical Report Series; No. TR-CTIT-05-52).

Research output: Book/ReportReportProfessional

TY - BOOK

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

AU - Katoen, Joost P.

AU - Zapreev, I.S.

N1 - Imported from CTIT

PY - 2005/11

Y1 - 2005/11

N2 - 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.

AB - 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.

KW - IR-57041

KW - METIS-248099

KW - EWI-5724

M3 - Report

T3 - CTIT Technical Report Series

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

PB - Formal Methods and Tools (FMT)

CY - Enschede

ER -

Katoen JP, Zapreev IS. Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. Enschede: Formal Methods and Tools (FMT), 2005. 32 p. (CTIT Technical Report Series; TR-CTIT-05-52).