Reinforcement Learning of Control Policy for Linear Temporal Logic Specifications Using Limit-Deterministic Generalized Büchi Automata

Recall that $\Sigma=\bar{\Sigma}$. We prove set inclusions in both directions.

• $\subset$:

  Consider any $w=\sigma_{0}\sigma_{1}\ldots\in\mathcal{L}(B)$. Then, there exists a run $r=x_{0}\sigma_{0}x_{1}$ $\sigma_{1}x_{2}\ldots\in X(\Sigma X)^{\omega}$ of $B$ such that $x_{0}=x_{init}$ and $inf(r)\cap F_{j}\neq\emptyset$ for each $F_{j}\in\mathcal{F}$. For the run $r$, we construct a sequence $\bar{r}=\bar{x}_{0}\bar{\sigma}_{0}\bar{x}_{1}\bar{\sigma}_{1}\bar{x}_{2}\ldots\in\bar{X}(\bar{\Sigma}\bar{X})^{\omega}$ satisfying $\bar{x}_{i}=(x_{i},{v}_{i})$ and $\bar{\sigma}_{i}=\sigma_{i}$ for any $i\in\mathbb{N}$, where ${v}_{0}=\mathbf{0}$ and

  $\displaystyle{v}_{i+1}\!=\!reset\Big{(}\!Max\big{(}{v}_{i},visitf((x_{i},\bar{\sigma}_{i},x_{i+1}))\big{)}\!\Big{)},\forall i\in\mathbb{N}.$

  Clearly from the construction, we have $(\bar{x}_{i},\bar{\sigma}_{i},\bar{x}_{i+1})\in\bar{\delta}$ for any $i\in\mathbb{N}$. Thus, $\bar{r}$ is a run of $\bar{B}$ starting from $\bar{x}_{0}=(x_{init},\mathbf{0})=\bar{x}_{init}$.

  We now show that $inf(\bar{r})\cap\bar{F}_{j}\neq\emptyset$ for each $\bar{F}_{j}\in\bar{\mathcal{F}}$. Since $inf(r)\cap F_{j}\neq\emptyset$ for each $F_{j}\in\mathcal{F}$, we have

  $\displaystyle inf\!(\bar{r})\!\cap\!\{\!(\bar{x},\!\bar{\sigma},\!\bar{x}^{\prime})\!\in\!\bar{\delta};visitf\!(\!([\![\bar{x}]\!]_{X},\!\bar{\sigma},\![\![\bar{x}^{\prime}]\!]_{X}\!)\!)_{j}\!\!=\!1\}\!\neq\!\emptyset$

  for any $j\in\{1,\ldots,n\}$, where $[\![(x,v)]\!]_{X}=x$ for each $(x,v)\in\bar{X}$. By the construction of $\bar{r}$, therefore, there are infinitely many indices $l\in\mathbb{N}$ with $v_{l}=\mathbf{0}$. Let $l_{1},l_{2}\in\mathbb{N}$ be arbitrary nonnegative integers such that $l_{1}<l_{2}$, $v_{l_{1}}=v_{l_{2}}=\mathbf{0}$, and $v_{l^{\prime}}\neq\mathbf{0}$ for any $l^{\prime}\in\{l_{1}+1,\ldots,l_{2}-1\}$. Then,

  	$\displaystyle\forall j\in\{1,\ldots,n\},\$	$\displaystyle\exists k\in\{l_{1},l_{1}+1,\ldots,l_{2}-1\},$
  		$\displaystyle(x_{k},\sigma_{k},x_{k+1})\in F_{j}\land(v_{k})_{j}=0,$

  where $(v_{k})_{j}$ is the $j$-th element of $v_{k}$. Hence, we have $inf(\bar{r})\cap\bar{F}_{j}\neq\emptyset$ for each $\bar{F}_{j}\in\bar{\mathcal{F}}$, which implies $w\in\mathcal{L}(\bar{B})$.

• $\supset$:

  Consider any $\bar{w}\in\bar{\sigma}_{0}\bar{\sigma}_{1}\ldots\in\mathcal{L}(\bar{B})$. Then, there exists a run $\bar{r}=\bar{x}_{0}\bar{\sigma}_{0}\bar{x}_{1}\bar{\sigma}_{1}$ $\bar{x}_{2}\ldots\in\bar{X}(\bar{\Sigma}\bar{X})^{\omega}$ of $\bar{B}$ such that $\bar{x}_{0}=\bar{x}_{init}$ and $inf(\bar{r})\cap\bar{F}_{j}\neq\emptyset$ for each $\bar{F}_{j}\in\bar{\mathcal{F}}$, i.e.,

  	$\displaystyle\forall j\in$	$\displaystyle\{1,\ldots,n\},\ \forall k\in\mathbb{N},\ \exists l\geq k,$
  		$\displaystyle([\![\bar{x}_{l}]\!]_{X},\bar{\sigma}_{l},[\![\bar{x}_{l+1}]\!]_{X})\in F_{j}\land(\bar{v}_{l})_{j}=0.$		(1)

  For the run $\bar{r}$, we construct a sequence $r=x_{0}\sigma_{0}x_{1}\sigma_{1}x_{2}\ldots\in X(\Sigma X)^{\omega}$ such that $x_{i}=[\![\bar{x}_{i}]\!]_{X}$ and $\sigma_{i}=\bar{\sigma}_{i}$ for any $i\in\mathbb{N}$. It is clear that $r$ is a run of $B$ starting from $x_{0}=x_{init}$. It holds by Eq. ($\supset$: ‣ III) that $inf(r)\cap F_{j}\neq\emptyset$ for each $F_{j}\in\mathcal{F}$, which implies $\bar{w}\in\mathcal{L}(B)$.

∎

Suppose that $MC^{\otimes}_{\pi}$ satisfies neither conditions 1 nor 2. Then, there exist a policy $\pi$, $i\in\{1,\ldots,h\}$, and $j_{1}$, $j_{2}$ $\in\{1,\ldots,n\}$ such that $\delta^{\otimes i}_{\pi}\cap\bar{F}^{\otimes}_{j_{1}}=\emptyset$ and $\delta^{\otimes i}_{\pi}\cap\bar{F}^{\otimes}_{j_{2}}\neq\emptyset$. In other words, there exists a nonempty and proper subset $J\in 2^{\{1,\ldots,n\}}\setminus\{\{1,\ldots,n\},\emptyset\}$ such that $\delta^{\otimes i}_{\pi}\cap\bar{F}^{\otimes}_{j}\neq\emptyset$ for any $j\in J$. For any transition $(s,a,s^{\prime})\in\delta^{\otimes i}_{\pi}\cap\bar{F}^{\otimes}_{j}$, the following equation holds by the properties of the recurrent states in $MC^{\otimes}_{\pi}$[13].

where $p^{k}((s,a,s^{\prime}),(s,a,s^{\prime}))$ is the probability that the transition $(s,a,s^{\prime})$ reoccurs after it occurs in $k$ time steps. Eq. (3) means that each transition in $R^{\otimes i}_{\pi}$ occurs infinitely often. However, the memory vector $v$ is never reset in $R^{\otimes i}_{\pi}$ by the assumption. This directly contradicts Eq. (3). ∎

Suppose that $\pi^{\ast}$ is an optimal policy but does not satisfy the LTL formula $\varphi$. Then, for any recurrent class $R^{\otimes i}_{{\pi}^{\ast}}$ in the Markov chain $MC^{\otimes}_{{\pi}^{\ast}}$ and any accepting set $\bar{F}^{\otimes}_{j}$ of the product MDP $M^{\otimes}$, $\delta^{\otimes i}_{\pi^{\ast}}\cap\bar{F}^{\otimes}_{j}=\emptyset$ holds by Lemma 1. Thus, the agent under the policy $\pi^{\ast}$ can obtain rewards only in the set of transient states. We consider the best scenario in the assumption. Let $p^{k}(s,s^{\prime})$ be the probability of going to a state $s^{\prime}$ in $k$ time steps after leaving the state $s$, and let $Post(T^{\otimes}_{\pi})$ be the set of states in recurrent classes that can be transitioned from states in $T^{\otimes}_{\pi}$ by one action. For the initial state $s_{init}$ in the set of transient states, it holds that

where the action $a$ is selected by $\pi^{\ast}$. By the property of the transient states, for any state $s^{\otimes}$ in $T^{\otimes}_{\pi^{\ast}}$, there exists a bounded positive value $m$ such that $\sum_{k=0}^{\infty}\gamma^{k}p^{k}(s_{init},s)\leq\sum_{k=0}^{\infty}p^{k}(s_{init},s)<m$ [13]. Therefore, there exists a bounded positive value $\bar{m}$ such that $V^{\pi^{\ast}}(s_{init})<\bar{m}$. Let $\bar{\pi}$ be a positional policy satisfying $\varphi$. We consider the following two cases.

1. 1.

   Assume that the initial state $s_{init}$ is in a recurrent class $R^{\otimes i}_{\bar{\pi}}$ for some $i\in\{1,\ldots,h\}$. For any accepting set $\bar{F}^{\otimes}_{j}$, $\delta^{\otimes i}_{\bar{\pi}}\cap\bar{F}^{\otimes}_{j}\neq\emptyset$ holds by the definition of $\bar{\pi}$. The expected discounted reward for $s_{init}$ is given by

   		$\displaystyle V^{\bar{\pi}}(s_{init})$
   	$\displaystyle=$	$\displaystyle\sum_{k=0}^{\infty}\sum_{s\in R^{\otimes i}_{\bar{\pi}}}\!\gamma^{k}p^{k}(s_{init},s)\!\!\sum_{s^{\prime}\in R^{\otimes i}_{\bar{\pi}}}P^{\otimes}_{\bar{\pi}}(s^{\prime}|s)\mathcal{R}(s,a,s^{\prime}),$

   where the action $a$ is selected by $\bar{\pi}$. Since $s_{init}$ is in $R^{\otimes i}_{\bar{\pi}}$, there exists a positive number $\bar{k}=\min\{k\ ;\ k\geq n,p^{k}(s_{init},s_{init})>0\}$ [13]. We consider the worst scenario in this case. It holds that

   	$\displaystyle V^{\bar{\pi}}(s_{init})\geq$	$\displaystyle\sum_{k=n}^{\infty}p^{k}(s_{init},s_{init})\sum_{i=1}^{n}\gamma^{k-i}r_{p}$
   	$\displaystyle\geq$	$\displaystyle\sum_{k=1}^{\infty}p^{k\bar{k}}(s_{init},s_{init})\sum_{i=0}^{n-1}\gamma^{k\bar{k}-i}r_{p}$
   	$\displaystyle>$	$\displaystyle r_{p}\sum_{k=1}^{\infty}\gamma^{k\bar{k}}p^{k\bar{k}}(s_{init},s_{init}),$

   whereas all states in $R(MC^{\otimes}_{\bar{\pi}})$ are positive recurrent because $|S^{\otimes}|<\infty$ [14]. Obviously, $p^{k\bar{k}}(s_{init},s_{init})\geq(p^{\bar{k}}(s_{init},s_{init}))^{k}>0$ holds for any $k\in(0,\infty)$ by the Chapman-Kolmogorov equation [13]. Furthermore, we have $\lim_{k\rightarrow\infty}p^{k\bar{k}}(s_{init},s_{init})>0$ by the property of irreducibility and positive recurrence [15]. Hence, there exists $\bar{p}$ such that $0<\bar{p}<p^{k\bar{k}}(s_{init},s_{init})$ for any $k\in(0,\infty]$ and we have

   $\displaystyle V^{\bar{\pi}}(s_{init})>$

   $\displaystyle r_{p}\bar{p}\frac{\gamma^{\bar{k}}}{1-\gamma^{\bar{k}}}.$

   Therefore, for any $r_{p}<\infty$ and any $\bar{m}\in(V^{\pi^{\ast}}(s_{init}),\infty)$, there exists $\gamma^{\ast}<1$ such that $\gamma>\gamma^{\ast}$ implies $V^{\bar{\pi}}(s_{init})>r_{p}\bar{p}\frac{\gamma^{\bar{k}}}{1-\gamma^{\bar{k}}}>\bar{m}.$

2. 2.

   Assume that the initial state $s_{init}$ is in the set of transient states $T_{\bar{\pi}}^{\otimes}$. $P^{M^{\otimes}}_{\bar{\pi}}(s_{init}\models\varphi)>0$ holds by the definition of $\bar{\pi}$. For a recurrent class $R^{\otimes i}_{\bar{\pi}}$ such that $\delta^{\otimes i}_{\bar{\pi}}\cap\bar{F}^{\otimes}_{j}\neq\emptyset$ for each accepting set $\bar{F}^{\otimes}_{j}$, there exist a number $\bar{l}>0$, a state $\hat{s}$ in $Post(T^{\otimes}_{\bar{\pi}})\cap R^{\otimes i}_{\bar{\pi}}$, and a subset of transient states $\{s_{1},\ldots,s_{\bar{l}-1}\}\subset T^{\otimes}_{\bar{\pi}}$ such that $p(s_{init},s_{1})>0$, $p(s_{i},s_{i+1})>0$ for $i\in\{1,\ldots,$ $\bar{l}-2\}$, and $p(s_{\bar{l}-1},\hat{s})>0$ by the property of transient states. Hence, it holds that $p^{\bar{l}}(s_{init},\hat{s})>0$ for the state $\hat{s}$. Thus, by ignoring rewards in $T^{\otimes}_{\bar{\pi}}$, we have

   	$\displaystyle V^{\bar{\pi}}(s_{init})\geq\$	$\displaystyle\gamma^{\bar{l}}p^{\bar{l}}(s_{init},\hat{s})\sum_{k=0}^{\infty}\sum_{s^{\prime}\in R^{\otimes i}_{\bar{\pi}}}\gamma^{k}p^{k}(\hat{s},s^{\prime})$
   		$\displaystyle\sum_{s^{\prime\prime}\in R^{\otimes i}_{\bar{\pi}}}P^{\otimes}_{\bar{\pi}}(s^{\prime\prime}|s^{\prime})\mathcal{R}(s^{\prime},a,s^{\prime\prime})$
   	$\displaystyle>\$	$\displaystyle\gamma^{\bar{l}}p^{\bar{l}}(s_{init},\hat{s})r_{p}\bar{p}\frac{\gamma^{\bar{k}^{\prime}}}{1-\gamma^{\bar{k}^{\prime}}},$

   where $\bar{k}^{\prime}\geq n$ is a constant and $0<\bar{p}<p^{k\bar{k}^{\prime}}(\hat{s},\hat{s})$ for any $k\in(0,\infty]$. Therefore, for any $r_{p}<\infty$ and any $\bar{m}\in(V^{\pi^{\ast}}(s_{init}),\infty)$, there exists $\gamma^{\ast}<1$ such that $\gamma>\gamma^{\ast}$ implies $V^{\bar{\pi}}(s_{init})>\gamma^{\bar{l}}p^{\bar{l}}(s_{init},\hat{s})\frac{r_{p}\bar{p}\gamma^{\bar{k}^{\prime}}}{1-\gamma^{\bar{k}^{\prime}}}>\bar{m}$.