Extension of PRISM by Synthesis of Optimal Timeouts in
Fixed-Delay CTMC

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

Autoři

KORENČIAK, Ľuboš (703 Slovensko, domácí), Vojtěch ŘEHÁK (203 Česká republika, garant, domácí) a Adrian FARMADIN (703 Slovensko, domácí)

Vydání

Switzerland, Integrated Formal Methods, od s. 130-138, 9 s. 2016

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

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"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088084

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-33692-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-33693-0_9

UT WoS

000379291800009

Klíčová slova anglicky

CTMC; DSPN; synthesis; timeout; expected reward; PRISM model checker

Štítky

core_B, firank_B, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 19:23, RNDr. Pavel Šmerk, Ph.D.

Anotace

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

Citovat

KORENČIAK, Ľuboš, Vojtěch ŘEHÁK a Adrian FARMADIN. Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. In Erika Ábrahám, Marieke Huisman. Integrated Formal Methods. Switzerland: Springer International Publishing, 2016, s. 130-138. ISBN 978-3-319-33692-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-33693-0_9.

@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 a 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, s.~130-138. ISBN~978-3-319-33692-3. Dostupné z: https://dx.doi.org/10.1007/978-3-319-33693-0\_{}9.

Podrobný výpis o publikaci