Approximate parameter synthesis for probabilistic time-bounded reachability

Tingting Han, Joost P. Katoen, A. Mereacre

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

40 Citations (Scopus)

Abstract

This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity ofbounded reachability properties. This algorithm is based ondiscretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.
Original languageUndefined
Title of host publicationProceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)
Place of PublicationLos Alamitos
PublisherIEEE Computer Society Press
Pages173-182
Number of pages10
ISBN (Print)978-0-7695-3477-0
DOIs
Publication statusPublished - Dec 2008
Event29th IEEE Real-Time Systems Symposium, RTSS 2008 - Barcelona, Spain
Duration: 30 Nov 20083 Dec 2008
Conference number: 29

Publication series

Name
PublisherIEEE Computer Society Press
Number2008/16200

Conference

Conference29th IEEE Real-Time Systems Symposium, RTSS 2008
Abbreviated titleRTSS
CountrySpain
CityBarcelona
Period30/11/083/12/08

Keywords

  • EWI-14721
  • METIS-255051
  • IR-62645
  • FMT-MC: MODEL CHECKING

Cite this

Han, T., Katoen, J. P., & Mereacre, A. (2008). Approximate parameter synthesis for probabilistic time-bounded reachability. In Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008) (pp. 173-182). [10.1109/RTSS.2008.19] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/RTSS.2008.19
Han, Tingting ; Katoen, Joost P. ; Mereacre, A. / Approximate parameter synthesis for probabilistic time-bounded reachability. Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008). Los Alamitos : IEEE Computer Society Press, 2008. pp. 173-182
@inproceedings{f355064aaa8941c6ab7800f9abd8b0e5,
title = "Approximate parameter synthesis for probabilistic time-bounded reachability",
abstract = "This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity ofbounded reachability properties. This algorithm is based ondiscretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.",
keywords = "EWI-14721, METIS-255051, IR-62645, FMT-MC: MODEL CHECKING",
author = "Tingting Han and Katoen, {Joost P.} and A. Mereacre",
note = "10.1109/RTSS.2008.19",
year = "2008",
month = "12",
doi = "10.1109/RTSS.2008.19",
language = "Undefined",
isbn = "978-0-7695-3477-0",
publisher = "IEEE Computer Society Press",
number = "2008/16200",
pages = "173--182",
booktitle = "Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)",

}

Han, T, Katoen, JP & Mereacre, A 2008, Approximate parameter synthesis for probabilistic time-bounded reachability. in Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)., 10.1109/RTSS.2008.19, IEEE Computer Society Press, Los Alamitos, pp. 173-182, 29th IEEE Real-Time Systems Symposium, RTSS 2008, Barcelona, Spain, 30/11/08. https://doi.org/10.1109/RTSS.2008.19

Approximate parameter synthesis for probabilistic time-bounded reachability. / Han, Tingting; Katoen, Joost P.; Mereacre, A.

Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008). Los Alamitos : IEEE Computer Society Press, 2008. p. 173-182 10.1109/RTSS.2008.19.

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

TY - GEN

T1 - Approximate parameter synthesis for probabilistic time-bounded reachability

AU - Han, Tingting

AU - Katoen, Joost P.

AU - Mereacre, A.

N1 - 10.1109/RTSS.2008.19

PY - 2008/12

Y1 - 2008/12

N2 - This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity ofbounded reachability properties. This algorithm is based ondiscretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.

AB - This paper proposes a technique to synthesize parametric rate values in continuous-time Markov chains that ensure the validity of bounded reachability properties. Rate expressions over variables indicate the average speed of state changes and are expressed using the polynomials over reals. The key contribution is an algorithm that approximates the set of parameter values for which the stochastic real-time system guarantees the validity ofbounded reachability properties. This algorithm is based ondiscretizing parameter ranges together with a refinement technique. This paper describes the algorithm, analyzes its time complexity, and shows its applicability by deriving parameter constraints for a real-time storage system with probabilistic error checking facilities.

KW - EWI-14721

KW - METIS-255051

KW - IR-62645

KW - FMT-MC: MODEL CHECKING

U2 - 10.1109/RTSS.2008.19

DO - 10.1109/RTSS.2008.19

M3 - Conference contribution

SN - 978-0-7695-3477-0

SP - 173

EP - 182

BT - Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)

PB - IEEE Computer Society Press

CY - Los Alamitos

ER -

Han T, Katoen JP, Mereacre A. Approximate parameter synthesis for probabilistic time-bounded reachability. In Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008). Los Alamitos: IEEE Computer Society Press. 2008. p. 173-182. 10.1109/RTSS.2008.19 https://doi.org/10.1109/RTSS.2008.19