Convergence Guarantee of Dynamic Programming for LTL Surrogate Reward

We propose our model called Markov decision processes with Büchi objective. It augments general MDPs [2] with a set of accepting states.

A path of the MDP $\mathcal{M}$ is an infinite state sequence $\sigma=s_{0}s_{1}s_{2}\cdots$ such that for all $i\geq 0$, there exists $a_{i}\in A(s)$ and $s_{i},s_{i+1}\in S$ with $P(s_{i},a_{i},s_{i+1})>0$. Given a path $\sigma$, the $i$th state is denoted by $\sigma[i]=s_{i}$. We denote the prefix by $\sigma[{:}i]=s_{0}s_{1}\cdots s_{i}$ and suffix by $\sigma[i{+}1{:}]=s_{i+1}s_{i+2}\cdots$. We say a path $\sigma$ satisfies the Büchi objective $\varphi_{B}$ if $\mathrm{inf}(\sigma)\cap B\neq\emptyset$. Here, $\mathrm{inf}(\sigma)$ denotes the set of states visited infinitely many times on $\sigma$.

Our model is valid as the LTL objective can be translated into a Büchi objective. The translation is done by constructing a product MDP from the original MDP and a limit-deterministic Büchi automaton [15] generated from the LTL objective. Instead of looking for the optimal memory-dependent policy for the LTL objective, one can find the optimal memoryless policy on the product MDP [15]. Since the maximum satisfaction probability of Büchi objective can be achieved by a memoryless deterministic policy.

We change an LTL planning problem into seeking the policy that maximizes the satisfaction probability of the Büchi objective. Evaluation of the policy requires the calculation of the satisfaction probability, which can be done by calculating the reachability probability.

Under the policy $\pi$, for a path $\sigma$ starting at state $s$, its satisfaction probability of the Büchi objective $\varphi_{B}$ is defined as

The calculation of the satisfaction probability can be done by calculating the reachability probability. The probability of a path under the policy $\pi$ satisfying the Büchi objective equals the probability of a path entering the accepting bottom strongly connected component (BSCC) of the induced MC $\mathcal{M}_{\pi}$.

Any path on the MC will eventually enter a BSCC and stay there. Any path entering an accepting BSCC will visit accepting states infinitely many times, therefore satisfying the Büchi objective.

The calculation of the reachability probability can be done via dynamic programming after one detects all the BSCCs. This approach is adopted by probabilistic model-checking and requires complete model knowledge.

A surrogate reward allows one to calculate the satisfaction probability even without knowledge of BSCCs. This equivalent representation of the Büchi objective allows one to transfer an LTL objective as a discounted reward.

We study the surrogate reward for Büchi objective proposed in [8], which is also widely used in [10, 11, 12, 13, 16]. This surrogate reward is designed in a way that its value function approximates the satisfaction probability. It consists of a reward function $R:S\to\mathbb{R}$ and a state-dependent discount factor function $\Gamma:S\to(0,1]$ with two discount factors $0<\gamma_{B}<\gamma\leq 1$,

A positive reward is collected only when an accepting state is visited along the path. For this surrogate reward, the $K$-step return ($K\in\mathbb{N}$ or $K=\infty$) of a path from time $t\in\mathbb{N}$ is

Here, the definition follows a standard discounted reward setting [17] but allows state-dependent discounting. Suppose the discount factor $\gamma=1$. If a path satisfies the Büchi objective, its return shall be a summation of a geometric series as $\sum_{i=0}^{\infty}(1-\gamma_{B})\gamma_{B}^{i}=\frac{1-\gamma_{B}}{1-\gamma_{B}}=1$.

The value function $V_{\pi}(s)$ is the expected return conditional on the path starting at $s$ under the policy $\pi$. And it is related to Büchi objective as follows,

where $1-\mathbb{P}_{\pi}(s,B)$ stands for the probability of a path not satisfying the Büchi objective conditional on the path starting at $s$. As $\gamma_{B}$, $\gamma$ close to $1$, the value function becomes close to $\pi(s,B)$ as

The setting $\gamma_{B}$ and $\gamma$ is critical for solving an discounted reward problem using the value iteration, or Q-learning. These methods are guaranteed to find the optimal policy for the surrogate reward when $\gamma<1$. To make sure the optimal policy for the surrogate reward is the optimal policy for the LTL objective, one has to take $\gamma$, $\gamma_{B}$ as close to $1$ as possible to reduce the error between the value function and the satisfaction probability. For $\gamma_{B}$, one can never take $\gamma_{B}=1$ as $1-\gamma_{B}=0$ can not serve as a positive reward. Setting $\gamma=1$ seems to work in several works. However, [14] exposes setting $\gamma=1$ would break the uniqueness of the solution of the Bellman equation, thus hindering a correct evaluation of the satisfaction probability.

Given a policy, the value function satisfies the Bellman equation.²²2We call $V_{\pi}(s)=R(s)+\Gamma(s)\sum_{s^{\prime}\in S}P_{\pi}(s,s^{\prime})V_{\pi}(s^{\prime})$ as the Bellman equation and $V_{\pi}^{*}(s)=\max_{a\in A(s)}\{R(s)+\Gamma(s)\sum_{s^{\prime}\in S}P(s,a,s^{\prime})V_{\pi}^{*}(s^{\prime})\}$ as the Bellman optimality equation. The Bellman equation is derived from the fact that the value of the current state is equal to the expectation of the current reward plus the discounted value of the next state. For the surrogate reward in the equation (2), the Bellman equation is given as follows:

Previous work [10, 13, 11] allows $\gamma=1$. However, setting $\gamma=1$ yields multiple solutions of the Bellman equations, raising concerns about applying dynamic programming or RL. A sufficient condition to restrict the uniqueness of the solution is proposed in [14].

Based on Lemma 1, dynamic programming is a way to compute the value function using the Bellman equation. Given an initialization of the approximate value function $U_{(0)}$ and the Bellman equation (6), we shall iteratively do the dynamic programming update as

where $m=|B|$ is the number of accepting states, $n=|\neg B|$ is the number of rejecting states. $\mathbb{I}$ and $\mathbb{O}$ are column vectors with all $1$ and $0$ elements, respectively. We expect the approximate value function $U_{(k)}$ to converge to the value function $V$ during updates.

Suppose we initialize $U_{(0)}$ as a zero vector. The sufficient condition for the uniqueness of the solution holds for all $U_{(k)}$. The value function is the only fix-point for the above update. However, a convergence guarantee is still needed to show we can compute the satisfaction probability using the above dynamic programming update.

When $\gamma<1$, the convergence is guaranteed by the one-step contraction shown as

As $\gamma=1$, this contraction no longer holds, and the convergence to the value function is still an open question. This motivates us to study the following problem.

Problem Formulation: For an MDP with Büchi objective $\mathcal{M}$ by Definition 1 and the surrogate reward (2), given a policy $\pi$. Starting with $U_{(0)}=\mathbb{O}$, show approximate value function $U_{(k)}$ updated by dynamic programming (7) will converge to the value function $V$ as $k\to\infty$. And give an upper bound for the error $\|U_{(k)}-V_{\pi}\|_{\infty}$.

In the following, we assume a fixed policy $\pi$, leading us to omit the $\pi$ subscript from most notation when its implication is clear from the context.

When $\gamma=1$, we find a multi-step contraction shown as

exists for the dynamic programming update, where $N\in\mathbb{N}^{+}$ and $c\in(0,1)$ is a constant. Even though rejecting states lacks discounting, their reachability to accepting states still provides contraction. With this finding, we claim the convergence guarantee as follows.

As the theorem claims, one can use the surrogate reward and dynamic programming to compute the satisfaction probability of the Büchi objective on the MDP. Thus, the following corollary holds.

Here, we give the convergence guarantee based on the discount factor $\gamma,\gamma_{B}$ and the reachability to the discounted state expressed as $\varepsilon^{n^{\prime}}$. The first bound is commonly seen for dynamic programming as each update provides one-step contraction when $\gamma<1$. The second bound relies on the multi-step contraction shown in the following section.

The sufficient condition in Lemma 1 always holds as we initialize $U_{(0)}=\mathbb{O}$. Since the approximate value function on the rejecting BSCCs stays at zero. We can simplify the dynamic programming update (7) by dropping all states inside rejecting BSCCs,

where

Here, the state space is partitioned into three sets of states $B$, $\neg B_{R}$, $\neg B_{T,A}$ representing the set of accepting states, the set of states in the rejecting BSCCs and the set of remaining rejecting states. $U_{\pi}^{B}\in\mathbb{R}^{m}$, $U_{\pi}^{\neg B_{T,A}}\in\mathbb{R}^{n^{\prime}}$ are the vectors listing the approximate value function for all $s\in{B}$, $s\in{\neg B_{T,A}}$, respectively. Matrix $T$ represents the transition between states in $X:=\{B,\neg B_{T,A}\}$. Sub-matrix $P_{B\rightarrow B}$, $P_{B\rightarrow\neg B_{T,A}}$ etc. contains the transition probability from a set of states to a set of states.

At each dynamic programming update, the approximation error is updated by a linear mapping as

where

$V_{\pi}^{B}\in\mathbb{R}^{m}$, $V_{\pi}^{\neg B_{T,A}}\in\mathbb{R}^{n^{\prime}}$ are the vectors listing the value function for states in $B$ and ${\neg B_{T,A}}$, respectively. When setting $\gamma=1$, the requirement for the one-step contraction (8), which is $\|H\|_{\infty}<1$ does not hold.

Even with $\gamma=1$, we can still show there exists a $N\in\mathbb{N}^{+}$ such that $\|H^{N}\|_{\infty}<1$. The multi-step update is given as

By showing each row sum of $H^{N}$ is strictly less than that of $T^{N}$, we guarantee $\|H^{N}\|_{\infty}<1$. In $T^{N}$, each element $\{T^{N}\}_{ij}$ is the probability of a path starting at $i$ visiting $j$ in the next $N$ steps, thus $\|T^{N}\|_{\infty}\leq 1$. In $H^{N}$, each element $\{H^{N}\}_{ij}$ is expressed as a “discounted” version of $\{T^{N}\}_{ij}$,

where

Whenever a one-step transition starting from the accepting state happens, a discount $\gamma_{B}$ shall be applied in (18), making $\{H^{N}\}_{ij}<\{T^{N}\}_{ij}$.

The row sum of $H^{N}$ shall be strictly less than the corresponding row sum of $T^{N}$ if the probability of visiting an accepting state within the future $N-1$ steps is greater than zero. Thus, the contraction $\|H^{N}\|_{\infty}<1$ is brought in by the reachability from rejecting states to accepting, which is formalized as the following Lemma.

By this reachability property, we show the multi-step contraction, which is technically described by the following lemma.

The multi-step update always provides a multi-step contraction, so we can upper bound the convergence of approximation error.

In the case of $\gamma=1$, we get the $N$-step update of the approximation error as,

By Lemma 3, after every $N$ update, the infinite norm of error must shrink by a constant $c<1$,

As $n\to\infty$, the error $\|{D}_{(nN)}\|_{\infty}\to 0$.

Meanwhile, since the sum of each row of $H\leq 1$, the error won’t grow at each one-step update. Thus, we have the convergence as,

Theorem 1 also considers the case when $\gamma<1$. We get the upper bound for the approximation error as

The upper bound on $\|D_{(k)}\|_{\infty}$ instantly holds for $\|U_{(k)}-V\|_{\infty}$ as starting the approximate value function at $\mathbb{O}$ guarantees $U^{\neg B_{R}}_{(k)}-V^{\neg B_{R}}=\mathbb{O}$, where $V^{\neg B_{R}}$ is the vector listing the value function for all states inside a rejecting BSCCs. $\blacksquare$