BLAHOUDEK, František, Tomáš BRÁZDIL, Petr NOVOTNÝ, Melkior ORNIK, Pranay THANGEDA and 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, p. 421-447. ISBN 978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8_22. |
Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~421-447. ISBN~978-3-030-53290-1. Available from: https://dx.doi.org/10.1007/978-3-030-53291-8\_{}22.
|