D
2016
Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
KORENČIAK, Ľuboš, Vojtěch ŘEHÁK a Adrian FARMADIN
Základní údaje
Originální název
Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC
Vydání
Switzerland, Integrated Formal Methods, od s. 130-138, 9 s. 2016
Nakladatel
Springer International Publishing
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Švýcarsko
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/16:00088084
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
CTMC; DSPN; synthesis; timeout; expected reward; PRISM model checker
Příznaky
Mezinárodní význam, Recenzováno
V originále
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.
Návaznosti
GBP202/12/G061, projekt VaV | Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI) | Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky |
|
MUNI/A/0935/2015, interní kód MU | Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU) | Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
MUNI/A/0945/2015, interní kód MU | Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V. | Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty |
|
Zobrazeno: 11. 11. 2024 00:38