TY - GEN
T1 - Qualitative Controller Synthesis for Consumption Markov Decision Processes
AU - Blahoudek, František
AU - Brázdil, Tomáš
AU - Novotný, Petr
AU - Ornik, Melkior
AU - Thangeda, Pranay
AU - Topcu, Ufuk
N1 - Publisher Copyright:
© 2020, The Author(s).
PY - 2020
Y1 - 2020
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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85089213071&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85089213071&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-53291-8_22
DO - 10.1007/978-3-030-53291-8_22
M3 - Conference contribution
AN - SCOPUS:85089213071
SN - 9783030532901
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 421
EP - 447
BT - Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings
A2 - Lahiri, Shuvendu K.
A2 - Wang, Chao
PB - Springer
T2 - 32nd International Conference on Computer Aided Verification, CAV 2020
Y2 - 21 July 2020 through 24 July 2020
ER -