Qualitative Controller Synthesis for Consumption Markov Decision Processes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00114617" target="_blank" >RIV/00216224:14330/20:00114617 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-53291-8_22" target="_blank" >http://dx.doi.org/10.1007/978-3-030-53291-8_22</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-53291-8_22" target="_blank" >10.1007/978-3-030-53291-8_22</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Qualitative Controller Synthesis for Consumption Markov Decision Processes

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verifikace a analýza pravděpodobnostních programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part {II}

ISBN

9783030532901

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

27

Strana od-do

421-447

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Los Angeles, USA

Datum konání akce

1. 1. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000695272500022