Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1351805,
author = {Korenčiak, Ľuboš and Řehák, Vojtěch and Farmadin, Adrian},
address = {Switzerland},
booktitle = {Integrated Formal Methods},
doi = {http://dx.doi.org/10.1007/978-3-319-33693-0_9},
editor = {Erika Ábrahám, Marieke Huisman},
keywords = {CTMC; DSPN; synthesis; timeout; expected reward; PRISM model checker},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Switzerland},
isbn = {978-3-319-33692-3},
pages = {130-138},
publisher = {Springer International Publishing},
title = {Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC},
url = {http://link.springer.com/chapter/10.1007/978-3-319-33693-0_9},
year = {2016}
}
TY - JOUR
ID - 1351805
AU - Korenčiak, Ľuboš - Řehák, Vojtěch - Farmadin, Adrian
PY - 2016
TI - Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
PB - Springer International Publishing
CY - Switzerland
SN - 9783319336923
KW - CTMC
KW - DSPN
KW - synthesis
KW - timeout
KW - expected reward
KW - PRISM model checker
UR - http://link.springer.com/chapter/10.1007/978-3-319-33693-0_9
L2 - http://link.springer.com/chapter/10.1007/978-3-319-33693-0_9
N2 - We present a practically appealing extension of the probabilistic model checker PRISM rendering it to handle fixed-delay continuous-time Markov chains (fdCTMCs) with rewards, the equivalent formalism to the deterministic and stochastic Petri nets (DSPNs). fdCTMCs allow transitions with fixed-delays (or timeouts) on top of the traditional transitions with exponential rates. Our extension supports an evaluation of expected reward until reaching a given set of target states. The main contribution is that, considering the fixed-delays as parameters, we implemented a synthesis algorithm that computes the epsilon-optimal values of the fixed-delays minimizing the expected reward. We provide a performance evaluation of the synthesis on practical examples.
ER -
KORENČIAK, Ľuboš, Vojtěch ŘEHÁK and Adrian FARMADIN. Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. In Erika Ábrahám, Marieke Huisman. \textit{Integrated Formal Methods}. Switzerland: Springer International Publishing, 2016, p.~130-138. ISBN~978-3-319-33692-3. Available from: https://dx.doi.org/10.1007/978-3-319-33693-0\_{}9.
|
