LTL代理報酬に対する動的計画法の収束保証
Convergence Guarantee of Dynamic Programming for LTL Surrogate Reward
LTL目的を最大化する方策を動的計画法で求める際、割引率が1の場合でも近似価値関数が真値に指数的に収束することを示し、充足確率計算の保証を与えた。
著者: Zetong Xuan, Yu Wang
分類: cs.RO, cs.SY, eess.SY
原文アブストラクト
Linear Temporal Logic (LTL) is a formal way of specifying complex objectives for planning problems modeled as Markov Decision Processes (MDPs). The planning problem aims to find the optimal policy that maximizes the satisfaction probability of the LTL objective. One way to solve the planning problem is to use the surrogate reward with two discount factors and dynamic programming, which bypasses the graph analysis used in traditional model-checking. The surrogate reward is designed such that its value function represents the satisfaction probability. However, in some cases where one of the discount factors is set to $1$ for higher accuracy, the computation of the value function using dynamic programming is not guaranteed. This work shows that a multi-step contraction always exists during dynamic programming updates, guaranteeing that the approximate value function will converge exponentially to the true value function. Thus, the computation of satisfaction probability is guaranteed.
