Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Convergence Guarantee of Dynamic Programming for LTL Surrogate Reward

Zetong Xuan, Yu Wang

TL;DR

This work addresses the challenge of computing the satisfaction probability for LTL objectives in MDPs using a surrogate reward with two state-dependent discounts, particularly when one discount can be set to 1. It proves a multi-step contraction exists, ensuring the DP-based approximate value function converges exponentially to the true probability, even in the absence of a one-step contraction. The authors establish a contractive mechanism by partitioning states into accepting and rejecting BSCCs and analyzing discounted transitions across layers, providing explicit bounds that depend on the reachability to accepting states. A case study corroborates the theoretical bounds, and the results have practical implications for model-free RL and policy evaluation in LTL-constrained planning. The work lays groundwork for future extensions to value iteration and Q-learning under changing BSCC structures during policy updates.

Abstract

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.

Convergence Guarantee of Dynamic Programming for LTL Surrogate Reward

TL;DR

This work addresses the challenge of computing the satisfaction probability for LTL objectives in MDPs using a surrogate reward with two state-dependent discounts, particularly when one discount can be set to 1. It proves a multi-step contraction exists, ensuring the DP-based approximate value function converges exponentially to the true probability, even in the absence of a one-step contraction. The authors establish a contractive mechanism by partitioning states into accepting and rejecting BSCCs and analyzing discounted transitions across layers, providing explicit bounds that depend on the reachability to accepting states. A case study corroborates the theoretical bounds, and the results have practical implications for model-free RL and policy evaluation in LTL-constrained planning. The work lays groundwork for future extensions to value iteration and Q-learning under changing BSCC structures during policy updates.

Abstract

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 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.
Paper Structure (15 sections, 5 theorems, 31 equations, 2 figures)

This paper contains 15 sections, 5 theorems, 31 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Modeling planning problems with LTL objectives as MDPs with Büchi objectives
  4. Policy evaluation for Büchi objective via reachability
  5. Surrogate reward that approximates the satisfaction probability
  6. Problem Formulation and main result
  7. Bellman equation and sufficient condition for the uniqueness of the solution
  8. Open question on the convergence of dynamic programming
  9. Overview on main result
  10. Multi-step contraction and proof of the main result
  11. Dynamic programming for states outside rejecting BSCCs
  12. Multi-step contraction
  13. Proof of Theorem \ref{['main result']}
  14. Case Study
  15. Conclusion and future work

Key Result

Lemma 1

The Bellman equation eqn:bellman has the value function as the unique solution, if and only if the solution for any state in a rejecting BSCC is zero xuan2024uniqueness.

Figures (2)

  • Figure 1: Example of a three-state Markov Chain. A discount factor $\gamma_B<1$ and a reward $1-\gamma_B$ hold at $s_a$. Meanwhile, no rewards are gained at $s_b$ and $s_c$. Discount $\gamma$ is applied to $s_b$ and $s_c$ but $\gamma$ can be set to $1$.
  • Figure 2: Exponential convergence of estimation error $\Vert D_{(k)} \Vert$ during dynamic programming updates. Our theorem yields an upper bound that shrinks $\gamma_B$ after every three dynamic programming updates. This upper bound captures the convergence in this example.

Theorems & Definitions (11)

  • Definition 1
  • Definition 2
  • Definition 3
  • Remark 1
  • Lemma 1
  • Theorem 1
  • Corollary 1
  • Lemma 2
  • proof
  • Lemma 3
  • ...and 1 more