Qualitative Controller Synthesis for Consumption Markov
Decision Processes

D 2020

Qualitative Controller Synthesis for Consumption Markov Decision Processes

BLAHOUDEK, František, Tomáš BRÁZDIL, Petr NOVOTNÝ, Melkior ORNIK, Pranay THANGEDA et. al.

Základní údaje

Originální název

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Autoři

BLAHOUDEK, František (203 Česká republika), Tomáš BRÁZDIL (203 Česká republika, domácí), Petr NOVOTNÝ (203 Česká republika, garant, domácí), Melkior ORNIK (191 Chorvatsko), Pranay THANGEDA (356 Indie) a Ufuk TOPCU (792 Turecko)

Vydání

Cham, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}, od s. 421-447, 27 s. 2020

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

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"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/20:00114617

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-53290-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-53291-8_22

UT WoS

000695272500022

Klíčová slova anglicky

decision making; Markov decision processes; controller synthesis; resource constraints

Štítky

core_A, firank_1, formela-ver

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 29. 4. 2021 08:12, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. In a CMDP, the controller possesses a certain amount of a critical resource, such as electric power. Each action of the controller can consume some amount of the resource. Resource replenishment is only possible in special reload states, in which the resource level can be reloaded up to the full capacity of the system. The task of the controller is to prevent resource exhaustion, i.e. ensure that the available amount of the resource stays non-negative, while ensuring an additional linear-time property. We study the complexity of strategy synthesis in consumption MDPs with almost-sure Büchi objectives. We show that the problem can be solved in polynomial time. We implement our algorithm and show that it can efficiently solve CMDPs modelling real-world scenarios.

Návaznosti

GA19-15134Y, interní kód MU

Název: Verifikace a analýza pravděpodobnostních programů

Investor: Grantová agentura ČR, Verifikace a analýza pravděpodobnostních programů

GJ19-15134Y, projekt VaV

Název: Verifikace a analýza pravděpodobnostních programů

Citovat

BLAHOUDEK, František, Tomáš BRÁZDIL, Petr NOVOTNÝ, Melkior ORNIK, Pranay THANGEDA a Ufuk TOPCU. Qualitative Controller Synthesis for Consumption Markov Decision Processes. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}. Cham: Springer, 2020, s. 421-447. ISBN 978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8_22.

@inproceedings{1718417,
   author = {Blahoudek, František and Brázdil, Tomáš and Novotný, Petr and Ornik, Melkior and Thangeda, Pranay and Topcu, Ufuk},
   address = {Cham},
   booktitle = {Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}},
   doi = {http://dx.doi.org/10.1007/978-3-030-53291-8_22},
   keywords = {decision making; Markov decision processes; controller synthesis; resource constraints},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-030-53290-1},
   pages = {421-447},
   publisher = {Springer},
   title = {Qualitative Controller Synthesis for Consumption Markov Decision Processes},
   year = {2020}
}

TY  - JOUR
ID  - 1718417
AU  - Blahoudek, František - Brázdil, Tomáš - Novotný, Petr - Ornik, Melkior - Thangeda, Pranay - Topcu, Ufuk
PY  - 2020
TI  - Qualitative Controller Synthesis for Consumption Markov Decision Processes
PB  - Springer
CY  - Cham
SN  - 9783030532901
KW  - decision making
KW  - Markov decision processes
KW  - controller synthesis
KW  - resource constraints
N2  - Consumption Markov Decision Processes (CMDPs) are probabilistic decision-making models of resource-constrained systems. In a CMDP, the controller possesses a certain amount of a critical resource, such as electric power. Each action of the controller can consume some amount of the resource. Resource replenishment is only possible in special reload states, in which the resource level can be reloaded up to the full capacity of the system. The task of the controller is to prevent resource exhaustion, i.e. ensure that the available amount of the resource stays non-negative, while ensuring an additional linear-time property. We study the complexity of strategy synthesis in consumption MDPs with almost-sure Büchi objectives. We show that the problem can be solved in polynomial time. We implement our algorithm and show that it can efficiently solve CMDPs modelling real-world scenarios.
ER  -

BLAHOUDEK, František, Tomáš BRÁZDIL, Petr NOVOTNÝ, Melkior ORNIK, Pranay THANGEDA a Ufuk TOPCU. Qualitative Controller Synthesis for Consumption Markov Decision Processes. In \textit{Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part $\{$II$\}$}. Cham: Springer, 2020, s.~421-447. ISBN~978-3-030-53290-1. Dostupné z: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}22.

Podrobný výpis o publikaci