Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy
Iteration

D 2016

Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration

KORENČIAK, Ľuboš, Antonín KUČERA a Vojtěch ŘEHÁK

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

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"

Odkazy

URL

Kód RIV

RIV/00216224:14330/16:00088476

Organizační jednotka

Fakulta informatiky

ISBN

978-1-5090-3431-4

ISSN

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ěněno: 12. 5. 2017 07:03, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 VaV

Ná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 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

Přiložené soubory

MASCOTS16_TO_Synthesis_in_fdCTMC_policy_iter_Kucera.pdf

Požádat o autorskou verzi souboru

Citovat

KORENČIAK, Ľuboš, Antonín KUČERA a Vojtěch ŘEHÁK. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. 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.

@inproceedings{1365671,
   author = {Korenčiak, Ľuboš and Kučera, Antonín and Řehák, Vojtěch},
   address = {London},
   booktitle = {2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems},
   doi = {http://dx.doi.org/10.1109/MASCOTS.2016.34},
   keywords = {Clocks: Protocols; Markov processes; Delays; Standards; Computational modeling},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {London},
   isbn = {978-1-5090-3431-4},
   pages = {367-372},
   publisher = {IEEE Computer Society},
   title = {Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration},
   url = {http://ieeexplore.ieee.org/document/7774605/},
   year = {2016}
}

TY  - JOUR
ID  - 1365671
AU  - Korenčiak, Ľuboš - Kučera, Antonín - Řehák, Vojtěch
PY  - 2016
TI  - Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration
PB  - IEEE Computer Society
CY  - London
SN  - 9781509034314
KW  - Clocks: Protocols
KW  - Markov processes
KW  - Delays
KW  - Standards
KW  - Computational modeling
UR  - http://ieeexplore.ieee.org/document/7774605/
L2  - http://ieeexplore.ieee.org/document/7774605/
N2  - 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.
ER  -

KORENČIAK, Ľuboš, Antonín KUČERA a Vojtěch ŘEHÁK. Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration. In \textit{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.

Podrobný výpis o publikaci