近似单计数器 MDP 与随机博弈的终止值

单计数器 MDP（OC-MDP）和单计数器简单随机博弈（OC-SSG）分别是 1 玩家和 2 玩家回合制零和随机博弈，它们运行在经典单计数器自动机（等价于具有单字母栈字母表的下推自动机）的转移图上。这些博弈的分析与验证的一个关键目标是终止目标，即玩家从给定的控制状态和给定的计数器值出发，分别旨在最大化（最小化）击中计数器值 0 的概率。最近，我们研究了 OC-MDP（和 OC-SSG）的定性决策问题（“最优终止值是否等于 1？”），并证明它们可在 P 时间内判定（分别在 NP 和 coNP 中）。然而，定量决策与近似问题（“最优终止值是否大于 p？”或“在 epsilon 内近似终止值”）则更具挑战性。部分原因在于最优策略可能不存在，且即使存在，它们也可能具有高度非平凡的结构。因此，即使这些定量终止问题是否可计算，此前也仍未解决。在本文中，我们证明了 OC-MDP 和 OC-SSG 终止值的所有定量近似问题都是可计算的。具体而言，给定一个 OC-SSG 和 epsilon > 0，我们可以计算出一个值 v，该值在加性误差 epsilon 内近似 OC-SSG 终止博弈的值，并且我们还可以为博弈中的双方玩家计算出 epsilon-最优策略。我们证明中的一个关键要素是一个精妙的鞅，它源自于求解某些可与最大化 OC-MDP 关联的线性规划。对这些鞅应用 Azuma 不等式，为 OC-MDP 得出了“富人策略”变为 epsilon-最优时的“财富”的可计算界限。