Qualitative Controller Synthesis for Consumption Markov Decision Processes

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Qualitative Controller Synthesis for Consumption Markov Decision Processes
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verification and Analysis of Probabilistic Programs</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

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

Article name in the collection
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
—
Number of pages
27
Pages from-to
421-447
Publisher name
Springer
Place of publication
Cham
Event location
Los Angeles, USA
Event date
Jan 1, 2020
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
000695272500022

Similar results(10)