KORENČIAK, Ľuboš, Antonín KUČERA and 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. p. 367-372, 6 pp. ISBN 978-1-5090-3431-4. doi:10.1109/MASCOTS.2016.34.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Efficient Timeout Synthesis in Fixed-Delay CTMC Using Policy Iteration
Authors KORENČIAK, Ľuboš (703 Slovakia, belonging to the institution), Antonín KUČERA (203 Czech Republic, belonging to the institution) and Vojtěch ŘEHÁK (203 Czech Republic, guarantor, belonging to the institution).
Edition London, 2016 IEEE 24th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, p. 367-372, 6 pp. 2016.
Publisher IEEE Computer Society
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/16:00088476
Organization unit Faculty of Informatics
ISBN 978-1-5090-3431-4
ISSN 2375-0227
Doi http://dx.doi.org/10.1109/MASCOTS.2016.34
UT WoS 000390937800046
Keywords in English Clocks: Protocols; Markov processes; Delays; Standards; Computational modeling
Tags formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 12/5/2017 07:03.
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.
GA15-17564S, research and development projectName: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
Investor: Czech Science Foundation, Standard Projects
MUNI/A/0945/2015, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
Type Name Uploaded/Created by Uploaded/Created Rights
MASCOTS16_TO_Synthesis_in_fdCTMC_policy_iter_Kucera.pdf   File version Řehák, V. 21/12/2016


Right to read
Right to upload
Right to administer:
  • a concrete person Mgr. Ľuboš Korenčiak, učo 208317
  • a concrete person prof. RNDr. Antonín Kučera, Ph.D., učo 2508
  • a concrete person doc. RNDr. Vojtěch Řehák, Ph.D., učo 3721
  • a concrete person RNDr. Pavel Šmerk, Ph.D., učo 3880
Ask the author for author copy Displayed: 27/9/2020 10:38