Mean-Payoff Optimization in Continuous-Time Markov Chains with
Parametric Alarms

D 2017

Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms

BAIER, Christel, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA, Vojtěch ŘEHÁK et. al.

Basic information

Original name

Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms

Authors

BAIER, Christel (276 Germany), Clemens DUBSLAFF (276 Germany), Ľuboš KORENČIAK (703 Slovakia, guarantor, belonging to the institution), Antonín KUČERA (203 Czech Republic, belonging to the institution) and Vojtěch ŘEHÁK (203 Czech Republic, belonging to the institution)

Edition

Cham, Quantitative Evaluation of Systems, p. 190-206, 17 pp. 2017

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/17:00095081

Organization unit

Faculty of Informatics

ISBN

978-3-319-66334-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-66335-7_12

UT WoS

000696692800012

Keywords in English

parameter synthesis; continuous-time Markov chains; non-Markovian distributions; Markov decision process; policy iteration; generalized semi-Markov process; Markov regenerative process

Abstract

V originále

Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events that can be non-exponentially distributed. Within parametric ACTMCs, the parameters of alarm-event distributions are not given explicitly and can be subject of parameter synthesis. An algorithm solving the epsilon-optimal parameter synthesis problem for parametric ACTMCs with long-run average optimization objectives is presented. Our approach is based on reduction of the problem to finding long-run average optimal strategies in semi-Markov decision processes (semi-MDPs) and sufficient discretization of parameter (i.e., action) space. Since the set of actions in the discretized semi-MDP can be very large, a straightforward approach based on explicit action-space construction fails to solve even simple instances of the problem. The presented algorithm uses an enhanced policy iteration on symbolic representations of the action space. The soundness of the algorithm is established for parametric ACTMCs with alarm-event distributions satisfying four mild assumptions that are shown to hold for uniform, Dirac, exponential, and Weibull distributions in particular, but are satisfied for many other distributions as well. An experimental implementation shows that the symbolic technique substantially improves the efficiency of the synthesis algorithm and allows to solve instances of realistic size.

Links

GA15-17564S, research and development project

Name: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů

Investor: Czech Science Foundation

MUNI/A/0992/2016, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

BAIER, Christel, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA and Vojtěch ŘEHÁK. Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms. In Nathalie Bertrand, Luca Bortolussi. Quantitative Evaluation of Systems. Cham: Springer, 2017, p. 190-206. ISBN 978-3-319-66334-0. Available from: https://dx.doi.org/10.1007/978-3-319-66335-7_12.

@inproceedings{1392972,
   author = {Baier, Christel and Dubslaff, Clemens and Korenčiak, Ľuboš and Kučera, Antonín and Řehák, Vojtěch},
   address = {Cham},
   booktitle = {Quantitative Evaluation of Systems},
   doi = {http://dx.doi.org/10.1007/978-3-319-66335-7_12},
   editor = {Nathalie Bertrand, Luca Bortolussi},
   keywords = {parameter synthesis; continuous-time Markov chains; non-Markovian distributions; Markov decision process; policy iteration; generalized semi-Markov process; Markov regenerative process},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-66334-0},
   pages = {190-206},
   publisher = {Springer},
   title = {Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms},
   year = {2017}
}

TY  - JOUR
ID  - 1392972
AU  - Baier, Christel - Dubslaff, Clemens - Korenčiak, Ľuboš - Kučera, Antonín - Řehák, Vojtěch
PY  - 2017
TI  - Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms
PB  - Springer
CY  - Cham
SN  - 9783319663340
KW  - parameter synthesis
KW  - continuous-time Markov chains
KW  - non-Markovian distributions
KW  - Markov decision process
KW  - policy iteration
KW  - generalized semi-Markov process
KW  - Markov regenerative process
N2  - Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events that can be non-exponentially distributed. Within parametric ACTMCs, the parameters of alarm-event distributions are not given explicitly and can be subject of parameter synthesis. An algorithm solving the epsilon-optimal parameter synthesis problem for parametric ACTMCs with long-run average optimization objectives is presented. Our approach is based on reduction of the problem to finding long-run average optimal strategies in semi-Markov decision processes (semi-MDPs) and sufficient discretization of parameter (i.e., action) space. Since the set of actions in the discretized semi-MDP can be very large, a straightforward approach based on explicit action-space construction fails to solve even simple instances of the problem. The presented algorithm uses an enhanced policy iteration on symbolic representations of the action space. The soundness of the algorithm is established for parametric ACTMCs with alarm-event distributions satisfying four mild assumptions that are shown to hold for uniform, Dirac, exponential, and Weibull distributions in particular, but are satisfied for many other distributions as well. An experimental implementation shows that the symbolic technique substantially improves the efficiency of the synthesis algorithm and allows to solve instances of realistic size.
ER  -

BAIER, Christel, Clemens DUBSLAFF, Ľuboš KORENČIAK, Antonín KUČERA and Vojtěch ŘEHÁK. Mean-Payoff Optimization in Continuous-Time Markov Chains with Parametric Alarms. In Nathalie Bertrand, Luca Bortolussi. \textit{Quantitative Evaluation of Systems}. Cham: Springer, 2017, p.~190-206. ISBN~978-3-319-66334-0. Available from: https://dx.doi.org/10.1007/978-3-319-66335-7\_{}12.

Detailed Information on Publication Record