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
Katoen, Joost P. ; Zapreev, I.S. / Safe on-the-fly steady-state detection for time-bounded reachability. Quantitative Evaluation of Systems (QEST). Los Alamitos : IEEE Computer Society Press, 2006. pp. 301-310
@inproceedings{9958d59925be417095e6e307be89bdb3,
title = "Safe on-the-fly steady-state detection for time-bounded reachability",
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",
keywords = "EWI-8233, IR-63705, METIS-237638",
author = "Katoen, {Joost P.} and I.S. Zapreev",
note = "10.1109/QEST.2006.47",
year = "2006",
month = "9",
doi = "10.1109/QEST.2006.47",
language = "Undefined",
isbn = "0-7695-2665-9",
publisher = "IEEE Computer Society Press",
number = "10",
pages = "301--310",
booktitle = "Quantitative Evaluation of Systems (QEST)",

}

Katoen, JP & Zapreev, IS 2006, Safe on-the-fly steady-state detection for time-bounded reachability. in Quantitative Evaluation of Systems (QEST)., 10.1109/QEST.2006.47, IEEE Computer Society Press, Los Alamitos, pp. 301-310, 3rd International Conference on Quantitative Evaluation of SysTems, QEST 2006, Riverside, United States, 11/09/06. https://doi.org/10.1109/QEST.2006.47

Safe on-the-fly steady-state detection for time-bounded reachability. / Katoen, Joost P.; Zapreev, I.S.

Quantitative Evaluation of Systems (QEST). Los Alamitos : IEEE Computer Society Press, 2006. p. 301-310 10.1109/QEST.2006.47.

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

TY - GEN

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

AU - Katoen, Joost P.

AU - Zapreev, I.S.

N1 - 10.1109/QEST.2006.47

PY - 2006/9

Y1 - 2006/9

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

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

KW - EWI-8233

KW - IR-63705

KW - METIS-237638

U2 - 10.1109/QEST.2006.47

DO - 10.1109/QEST.2006.47

M3 - Conference contribution

SN - 0-7695-2665-9

SP - 301

EP - 310

BT - Quantitative Evaluation of Systems (QEST)

PB - IEEE Computer Society Press

CY - Los Alamitos

ER -

Katoen JP, Zapreev IS. Safe on-the-fly steady-state detection for time-bounded reachability. In Quantitative Evaluation of Systems (QEST). Los Alamitos: IEEE Computer Society Press. 2006. p. 301-310. 10.1109/QEST.2006.47 https://doi.org/10.1109/QEST.2006.47