Quantitative Termination Approximation Analysis of One-Counter Markov Decision Processes

马尔可夫决策过程（MDP）是一个随机的、受控的、离散时间的过程，它是在一个过渡图上进行的。玩家控制特定的状态子集，选择自己的策略选择如何选择过渡以及从这些状态移动到下一个位置。其余的状态都在自然/不确定性的控制下，具有预定义的外向转换概率分布。添加一个无界计数器（游戏邦注：即在游戏的每一步中最多改变1个）便能够创造出一种单计数器(OC)- mdp。该项目着眼于分析所谓的终止目标，即在给定状态和计数器>的初始配置下，在任何状态下达到计数器值0的概率。取决于它是最大化还是最小化OC-MDP，玩家的目标分别是最大化或最小化这个概率。以前已经证明，这一目标的定性决策部分，即：“最优概率是1还是0?”，可以在多项式时间内确定。至于数量部分，即。“终止值是否至少为p?”，已经表明，这些问题是否可计算的问题是开放的，并且计算最优博弈值的近似值和（epsilon-）最优策略可以在博弈大小的时间指数中完成。本研究的重点是将这类对策的复杂度从指数时间提高到多项式时间以及终止逼近问题。实现这一点有其好处，因为单计数器游戏适用于其他地方。例如，离散时间拟生-死过程类和偿付博弈类被归入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.