KORENČIAK, Ľuboš, Antonín KUČERA a Vojtěch ŘEHÁK. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. Online. In 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems. London: IEEE Computer Society, 2016. s. 367-372. ISBN 978-1-5090-3431-4. Dostupné z: https://dx.doi.org/10.1109/MASCOTS.2016.34. [citováno 2024-04-24]
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration
Autoři KORENČIAK, Ľuboš (703 Slovensko, domácí), Antonín KUČERA (203 Česká republika, domácí) a Vojtěch ŘEHÁK (203 Česká republika, garant, domácí)
Vydání London, 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, od s. 367-372, 6 s. 2016.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy
Utajení není předmětem státního či obchodního tajemství
Forma vydání tištěná verze "print"
WWW URL
Kód RIV RIV/00216224:14330/16:00088476
Organizační jednotka Fakulta informatiky
ISBN 978-1-5090-3431-4
ISSN 2375-0227
Doi http://dx.doi.org/10.1109/MASCOTS.2016.34
UT WoS 000390937800046
Klíčová slova anglicky Clocks: Protocols; Markov processes; Delays; Standards; Computational modeling
Štítky core_A, firank_A, formela-conference
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 12. 5. 2017 07:03.
Anotace
We consider the fixed-delay synthesis problem for continuous-time Markov chains extended with fixed-delay transitions (fdCTMC). The goal is to synthesize concrete values of the fixed-delays (timeouts) that minimize the expected total cost incurred before reaching a given set of target states. The same problem has been considered and solved in previous works by computing an optimal policy in a certain discrete-time Markov decision process (MDP) with a huge number of actions that correspond to suitably discretized values of the timeouts. In this paper, we design a symbolic fixed-delay synthesis algorithm which avoids the explicit construction of large action spaces. Instead, the algorithm computes a small sets of "promising" candidate actions on demand. The candidate actions are selected by minimizing a certain objective function by computing its symbolic derivative and extracting a univariate polynomial whose roots are precisely the points where the derivative takes zero value. Since roots of high degree univariate polynomials can be isolated very efficiently using modern mathematical software, we achieve not only drastic memory savings but also speedup by three orders of magnitude compared to the previous methods.
Návaznosti
GA15-17564S, projekt VaVNázev: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
Investor: Grantová agentura ČR, Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
MUNI/A/0945/2015, interní kód MUNá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
VytisknoutZobrazeno: 24. 4. 2024 00:06