Approximate parameter synthesis for probabilistic time-bounded reachability

Tingting Han; Joost P. Katoen; A. Mereacre

doi:10.1109/RTSS.2008.19

Approximate parameter synthesis for probabilistic time-bounded reachability

Tingting Han, Joost P. Katoen, A. Mereacre

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

52 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 language	Undefined
Title of host publication	Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)
Place of Publication	Los Alamitos
Publisher	IEEE
Pages	173-182
Number of pages	10
ISBN (Print)	978-0-7695-3477-0
DOIs	https://doi.org/10.1109/RTSS.2008.19
Publication status	Published - Dec 2008
Event	29th IEEE Real-Time Systems Symposium, RTSS 2008 - Barcelona, Spain Duration: 30 Nov 2008 → 3 Dec 2008 Conference number: 29

Publication series

Name
Publisher	IEEE Computer Society Press
Number	2008/16200

Conference

Conference	29th IEEE Real-Time Systems Symposium, RTSS 2008
Abbreviated title	RTSS
Country/Territory	Spain
City	Barcelona
Period	30/11/08 → 3/12/08

Keywords

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

Access to Document

10.1109/RTSS.2008.19

http://eprints.eemcs.utwente.nl/secure2/14721/01/rtss08.pdf

Cite this

@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 ; 29th IEEE Real-Time Systems Symposium, RTSS 2008 ; Conference date: 30-11-2008 Through 03-12-2008",

year = "2008",

month = dec,

doi = "10.1109/RTSS.2008.19",

language = "Undefined",

isbn = "978-0-7695-3477-0",

publisher = "IEEE",

number = "2008/16200",

pages = "173--182",

booktitle = "Proceedings of the IEEE Real-Time Systems Symposium (RTSS 2008)",

address = "United States",

}

TY - GEN

T1 - Approximate parameter synthesis for probabilistic time-bounded reachability

AU - Han, Tingting

AU - Katoen, Joost P.

AU - Mereacre, A.

N1 - Conference code: 29

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

CY - Los Alamitos

T2 - 29th IEEE Real-Time Systems Symposium, RTSS 2008

Y2 - 30 November 2008 through 3 December 2008

ER -