马氏决策过程中的Skolem-硬点和饱和点
On Skolem-hardness and saturation points in Markov decision processes
摘要：
线性递归序列的Skolem问题及其相关的正性问题是一个重要的数论问题，其可判定性已经公开了几十年。在本文中，固有的数学困难的一系列优化问题的马尔可夫决策过程（MDP）是由减少从积极性问题相关联的决策问题，建立的问题也至少一样难的Skolem问题作为一个直接后果。所考虑的优化问题是随机最短路径问题（SSPP）在期望部分或条件累积权重方面的两个非经典变体，累积权重的条件风险值的优化，以及解决路径属性的长期满意度的两个问题，即正则共安全性质的长期概率优化和逻辑频率LTL的模型检验问题。为了证明积极性，因此Skolem硬度为后两个问题，一个新的辅助路径措施，称为加权长期频率，引入和相应的决策问题的积极性硬度显示为一个中间步骤。对于部分和条件SSPP与非负权重的MDP和约束可达性属性（a U b）的长期概率的优化，解决方案是已知的，依赖于识别的累计权重或连续访问某些状态的次数的界限，称为饱和点，从最佳的存储器行为memorylands。在本文中，它表明，也可以解决在伪多项式时间利用饱和点的存在下，经典SSPP的条件风险值和加权长期运行频率的MDP与非负权重的优化。
英文摘要：
The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic problems whose decidability has been open for many decades. In this paper, the inherent mathematical difficulty of a series of optimization problems on Markov decision processes (MDPs) is shown by a reduction from the Positivity problem to the associated decision problems which establishes that the problems are also at least as hard as the Skolem problem as an immediate consequence. The optimization problems under consideration are two non-classical variants of the stochastic shortest path problem (SSPP) in terms of expected partial or conditional accumulated weights, the optimization of the conditional value-at-risk for accumulated weights, and two problems addressing the long-run satisfaction of path properties, namely the optimization of long-run probabilities of regular co-safety properties and the model-checking problem of the logic frequency-LTL. To prove the Positivity- and hence Skolem-hardness for the latter two problems, a new auxiliary path measure, called weighted long-run frequency, is introduced and the Positivity-hardness of the corresponding decision problem is shown as an intermediate step. For the partial and conditional SSPP on MDPs with non-negative weights and for the optimization of long-run probabilities of constrained reachability properties (a U b), solutions are known that rely on the identification of a bound on the accumulated weight or the number of consecutive visits to certain sates, called a saturation point, from which on optimal schedulers behave memorylessly. In this paper, it is shown that also the optimization of the conditional value-at-risk for the classical SSPP and of weighted long-run frequencies on MDPs with non-negative weights can be solved in pseudo-polynomial time exploiting the existence of a saturation point.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
