This paper investigates a series of optimization problems for one-counter Markov decision processes (MDPs) and integer-weighted MDPs with finite state space. Specifically, it considers problems addressing termination probabilities and expected termination times for one-counter MDPs, as well as satisfaction probabilities of energy objectives, conditional and partial expectations, satisfaction probabilities of constraints on the total accumulated weight, the computation of quantiles for the accumulated weight, and the conditional value-at-risk for accumulated weights for integer-weighted MDPs. Although algorithmic results are available for some special instances, the decidability status of the decision versions of these problems is unknown in general. The paper demonstrates that these optimization problems are inherently mathematically difficult by providing polynomial-time reductions from the Positivity problem for linear recurrence sequences. This problem is a well-known number-theoretic problem whose decidability status has been open for decades and it is known that decidability of the Positivity problem would have far-reaching consequences in analytic number theory. So, the reductions presented in the paper show that an algorithmic solution to any of the investigated problems is not possible without a major breakthrough in analytic number theory. The reductions rely on the construction of MDP-gadgets that encode the initial values and linear recurrence relations of linear recurrence sequences. Interestingly, the reductions can also be extended to demonstrate the Positivity-hardness of two problems that address the long-run behavior of a system, namely the model-checking problem of frequency-LTL and the optimization of the long-run average probability to satisfy a path property. Both of these problems have been studied before on special instances, but are open in general.

翻译：本文研究了一类针对单计数器马尔可夫决策过程（MDP）和有限状态空间整数加权MDP的优化问题。具体而言，考虑了单计数器MDP的终止概率与期望终止时间、能量目标满足概率、条件期望与部分期望、总累计权重约束满足概率、累计权重分位数计算，以及整数加权MDP累计权重的条件风险值等问题。尽管某些特例已有算法结果，但这些问题的判定版本在一般情况下可判定性未知。本文通过从线性递归序列的正性问题进行多项式时间归约，证明了这些优化问题本质上的数学困难性。正性问题是数论中一个著名的未解决问题，其可判定性已开放数十年，且解决该问题将对解析数论产生深远影响。因此，本文的归约表明：除非在解析数论上取得重大突破，否则无法对这些研究问题给出算法解。归约依赖于构造编码线性递归序列初始值与递归关系的MDP-组件。有趣的是，这些归约还可扩展至证明两个涉及系统长期行为问题的正性困难性：频率LTL的模型检验问题与路径性质长期平均概率的优化问题。这两个问题此前仅在特例中被研究，但其一般情况尚待解决。