Qualitative controller synthesis for consumption Markov decision processes

DOI10.1007/978-3-030-53291-8_22MaRDI QIDQ2226753zbMATH OpenOpenAlexFDO

Authors František Blahoudek, Tomáš Brázdil, Petr Novotný, Melkior Ornik, Pranay Thangeda, Ufuk Topcu

Publication date 9 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2005.07227

Mathematics Subject Classification ID

Markov and semi-Markov decision processes (90C40) Synthesis problems (93B50) Stochastic systems in control theory (general) (93E03)

Abstract: 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"uchi 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.

Recommendations

• Quantitative controller synthesis for consumption Markov decision processes
• On the controller synthesis for finite-state Markov decision processes
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Synthesis of an optimal control for continuous Markov processes by semidefinite quality criteria
• Controller synthesis for reward collecting Markov processes in continuous space
• scientific article; zbMATH DE number 4203409
• Constrained Continuous-Time Markov Control Processes with Discounted Criteria
• AN OPTIMAL MARKOVIAN QUANTIZATION ALGORITHM FOR MULTI-DIMENSIONAL STOCHASTIC CONTROL PROBLEMS
• Quantitative model-checking of controlled discrete-time Markov processes

Cited in

(4)

• Quantitative controller synthesis for consumption Markov decision processes
• Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
• Reachability games and friends: a journey through the Lens of memory and complexity (invited talk)
• Simplicity lies in the eye of the beholder: a strategic perspective on controllers in reactive synthesis

This page was built for publication: Qualitative controller synthesis for consumption Markov decision processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2226753)