One-Counter Markov Decision Processes
Tom\'a\v{s} Br\'azdil, V\'aclav Bro\v{z}ek, Kousha Etessami, Anton\'in, Ku\v{c}era, Dominik Wojtczak

TL;DR
This paper investigates the computational complexity of analysis problems for One-Counter Markov Decision Processes, providing new bounds and algorithms for key questions like termination and limit behaviors.
Contribution
It introduces complexity bounds and algorithms for analysis problems in OC-MDPs, connecting them to queueing theory, automata, and stochastic models.
Findings
Polynomial-time algorithms for some problems.
PSPACE- and BH-hardness results for others.
EXPTIME upper bounds established.
Abstract
We study the computational complexity of central analysis problems for One-Counter Markov Decision Processes (OC-MDPs), a class of finitely-presented, countable-state MDPs. OC-MDPs are equivalent to a controlled extension of (discrete-time) Quasi-Birth-Death processes (QBDs), a stochastic model studied heavily in queueing theory and applied probability. They can thus be viewed as a natural ``adversarial'' version of a classic stochastic model. Alternatively, they can also be viewed as a natural probabilistic/controlled extension of classic one-counter automata. OC-MDPs also subsume (as a very restricted special case) a recently studied MDP model called ``solvency games'' that model a risk-averse gambling scenario. Basic computational questions about these models include ``termination'' questions and ``limit'' questions, such as the following: does the controller have a ``strategy'' (or…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPetri Nets in System Modeling · Formal Methods in Verification · Simulation Techniques and Applications
