Quantitative Termination Approximation Analysis of One-Counter Markov Decision Processes

马尔可夫决策过程(MDP)是一个随机的、可控的、离散的过程，它在一个转移图上播放。玩家控制指定的状态子集，选择自己的策略来选择如何拾取过渡以及从这些状态移动到下一个位置。其余的状态由自然/不确定性控制，在传出跃迁上具有预定义的概率分布。增加一个在游戏的每一步最多变化1的无界计数器，建立一个计数器(OC)-MDPS的类。这个项目着眼于对这个游戏的所谓终止目标的分析，它是在任何状态下达到计数器值0的概率，给定状态和计数器&>0的开始配置。根据OC-MDP是最大化还是最小化，博弈者的目标分别是最大化或最小化这个概率。以往的研究证明，这个目标的定性决策部分，即“是最优概率1还是最优概率0？”，在多项式时间内是可判定的。至于定量部分，即“终止值是否至少p？”，已经证明了这类问题是否可计算的问题是开放的，并且计算最优博弈值和(？)最优策略的近似值可以在时间上以博弈的大小指数地完成。这项研究的重点是改善这类博弈的复杂性，从指数时间到多项式时间，以及终止逼近问题。实现这一点是有好处的，因为单计数器博弈也适用于其他地方。例如，离散时间拟生灭过程和偿付对策类被OC-MDP包含，这意味着这类过程在排队论和投资/赌博中得到了广泛的应用。作为里程碑，这个问题是第一年的焦点。在此之后，还有许多其他与博弈论相关和/或与MDP相关的问题可以分析。

A Markov Decision Process(MDP) is a stochastic, controlled, discrete-time process, which is played over a transition graph. A player controls a specified subset of states, choosing their own strategy on how to pick transitions and where to move to next from those states. The rest of the states fall under nature/uncertainty's possession, with pre-defined probability distributions over outgoing transitions. Adding an unbounded counter, that changes by at most 1 at each step of the game, builds the class of one-counter(OC)-MDPs.This project looks at the analysis of the so-called termination objective over this game, which is the probability of reaching counter value 0 at any state, provided a beginning configuration of given state and counter>0. Depending on whether it is a maximization or minimization OC-MDP, the goal of the player is to maximize or minimize, respectively, this probability.It has previously been proven that the qualitative decision part of this objective, i.e. "is optimal probability 1 or 0?", is decidable in polynomial time. As for the quantitative part, i.e. "is termination value at least p?", it has been shown that the question of whether such problems are computable is open and that computing an approximation of the optimal game value and (epsilon-)optimal strategies can be done in time exponential in the size of the game. The focus of this research aims at improving the complexity from exponential to polynomial time for such games and the termination approximation problem.Achieving this has its benefits, since one-counter games are applicable elsewhere. For example, the classes of discrete-time Quasi-Birth-Death processes and Solvency games are subsumed by OC-MDPs, meaning this type of process is widely used - in queueing theory and investment/gambling.As a milestone, this problem is the focus for this first year. After that, there are many other game-theory-related and/or MDP-related problems that could be analysed.