关于 LTL 目标 Bellman 方程解的唯一性

线性时序逻辑（LTL）目标的代理奖励通常用于 LTL 目标的规划问题中。在一种广泛采用的代理奖励方法中，使用两个折扣因子来确保期望回报近似于 LTL 目标的满足概率。随后，可以通过使用 Bellman 更新的方法（如强化学习）来估计期望回报。然而，具有两个折扣因子的 Bellman 方程解的唯一性尚未被明确讨论。我们通过一个示例证明，当其中一个折扣因子设为 1 时（正如以往许多工作所允许的那样），Bellman 方程可能存在多个解，从而导致期望回报的评估不准确。然后，我们提出了一个使 Bellman 方程将期望回报作为唯一解的条件，要求拒绝底部强连通分量（BSCC）内状态的解为 0。我们通过证明在该条件下，有折扣状态的解可以与无折扣状态的解分离，从而证明该条件是充分的。