# Learning-based Bounded Synthesis for Semi-MDPs with LTL Specifications

Ryohei Oura  Ryohei Oura and Toshimitsu Ushio  This work was partially
supported by JST-ERATO HASUO Project Grant Number JPMJER1603, Japan and JST
CREST Grant Number JPMJCR2012, Japan. The authors are with the Graduate School
of Engineering Science, Osaka University, Toyonaka 560-8531, Japan (e-mail:
<EMAIL_ADDRESS>ushio@sys.es.osaka-u.ac.jp).

(October 2021)

###### Abstract

This letter proposes a learning-based bounded synthesis for a semi-Markov
decision process (SMDP) with a linear temporal logic (LTL) specification. In
the product of the SMDP and the deterministic $K$-co-Büchi automaton (d$K$cBA)
converted from the LTL specification, we learn both the winning region of
satisfying the LTL specification and the dynamics therein based on
reinforcement learning and Bayesian inference. Then, we synthesize an optimal
policy satisfying the following two conditions. (1) It maximizes the
probability of reaching the wining region. (2) It minimizes a long-term risk
for the dwell time within the winning region. The minimization of the long-
term risk is done based on the estimated dynamics and a value iteration. We
show that, if the discount factor is sufficiently close to one, the
synthesized policy converges to the optimal policy as the number of the data
obtained by the exploration goes to the infinity.

###### Index Terms:

Bounded Synthesis, Linear Temporal Logic, Reinforcement Learning, Bayesian
inference, Semi-Markov Decision Process.

##  I Introduction

Linear temporal logic (LTL) is used to describe a complex control
specification [1]. In recent years, several automata-guided reinforcement
learning (RL) have been investigated to synthesize an optimal controller for
an unknown controlled stochastic system, e.g., Markov decision process (MDP),
under an LTL specification [2, 3, 4, 5]. They constructed the product MDP from
the MDP and a Rabin or Büchi automaton converted from the LTL specification.
An optimal controller was learned on the product MDP by maximizing the
expected return with a reward assignments according to the acceptance
condition. In [6, 7], truncated LTL specifications were used and rewards were
assigned according to the converted automaton. Bounded synthesis is an
alternative synthesis approach to avoid the state-complexity of Rabin automata
[8]. A bounded synthesis and reinforcement learning-based optimal controller
synthesis for MDPs has been proposed [9].

On the other hand, many systems have intrinsic stochasticity of a time
interval between state transitions, namely dwell time, as well as that of
state transition. The stochasticity of the dwell time may degrade a
quantitative performance of the controller that satisfies the LTL
specification. For example, a round trip time in patrol of a museum by a
mobile robot depends on dwell times in exhibition rooms. So, in practice, it
is important to take a risk for the dwell time, e.g., the variance of the
dwell time, into account to achieve a long-term task. A semi-Markov decision
process (SMDP) is leveraged as a model of a controlled stochastic system to
represent the stochasticity of the dwell time and that of the state transition
[10]. Several reinforcement learning methods for SMDPs have been advocated
[11, 12]. They mainly aimed at maximizing an accumulative rewards in the
continuous time. To the best of our knowledge, however, reinforcement learning
of a control policy satisfying an LTL specification under the stochastic dwell
time has not been addressed. Several model-based RL methods for LTL
specifications and cost minimization have been addressed [13, 14, 15].
However, they only considered the (almost) sure satisfaction of the LTL
specifications and applied a model-based RL to all states.

In this letter, we propose a bounded synthesis and learning-based method for
the optimal policy synthesis that minimizes a long-term risk for the dwell
time under the satisfaction of a given LTL specification with the maximal
probability. First, we represent the unknown controlled system by an SMDP and
convert the given LTL specification into a d$K$cBA. Then, for the product SMDP
from them, we synthesize an optimal policy satisfying the following two
conditions. (1) It maximizes the probability of reaching the winning region.
(2) It minimizes the risk for the dwell time within the winning region.

The rest of this letter is organized as follows. Section II reviews an SMDP,
LTL, and $\omega$-automata. Section III formulates a control problem given by
an LTL specification with a risk by the dwell time. Section IV proposes a
bounded synthesis and learning-based method for an optimal policy synthesis.

###### Notations

$\mathbb{N}$ is the set of positive integers. $\mathbb{N}_{0}$ is the set of
non-negative integers. $\mathbb{R}$ is the set of real numbers.
$\mathbb{R}_{\geq 0}$ is the set of non-negative real numbers. For a set $A$,
we denote its cardinality by $|A|$ and the set of probability distributions
over $A$ by $\mathcal{D}(A)$. For two sets $A$ and $B$, denoted by $A^{B}$ is
the set of mappings from $B$ to $A$. We denote the empty string by
$\varepsilon$.

##  II Preliminaries

###  II-A Semi-Markov decision process

A semi-Markov decision process (SMDP) is a continuous-time dynamic system [10,
11, 12] modeled by a tuple $\mathcal{SM}=(S,A,T,D,s^{I},AP,L)$, where $S$ is
the finite set of sates, $A$ is the finite set of actions, $T:S\times S\times
A\to[0,1]$ is the state transition probability, $D:S\times A\times
S\to\mathcal{D}(\mathbb{R}_{\geq 0})$ is the dwell time probability function,
$s^{I}\in S$ is the initial state, $AP$ is the finite set of atomic
propositions, and $L:S\to 2^{AP}$ is the labeling function [1]. Let
$A(s)=\\{a\in A\;|\;\exists s^{\prime}\in S\mbox{ s.t.
}T(s^{\prime}\;|\;s,a)>0\\}$. Note that $\sum_{s^{\prime}\in
S}T(s^{\prime}\;|\;s,a)=1$ for any $s\in S$ and any $a\in A(s)$. We sometimes
denote $D(\cdot\;|\;s,a,s^{\prime})$ instead of $D(s,a,s^{\prime})(\cdot)$ for
any $(s,a,s^{\prime})\in S\times A\times S$.

###### Remark 1

The semi-Markov kernel $P:S\times\mathcal{B}(\mathbb{R}_{\geq 0})\times
S\times A\to[0,1]$, where $\mathcal{B}(\mathbb{R}_{\geq 0})$ is the Borel set
over $\mathbb{R}_{\geq 0}$, is defined as
$P(s^{\prime},\tau\;|\;s,a)=T(s^{\prime}\;|\;s,a)D(\tau\;|\;s,a,s^{\prime})$
for any $(s,a,s^{\prime})\in S\times A\times S$ and any
$\tau\in\mathcal{B}(\mathbb{R}_{\geq 0})$.

In the SMDP $\mathcal{SM}$, an infinite (time-abstract) path starting from a
state $s_{0}\in S$ is defined as a sequence $\rho\ =\ s_{0}a_{0}s_{1}\ldots\
\in S(AS)^{\omega}$ such that $T(s_{i+1}|s_{i},a_{i})>0$ for any
$i\in\mathbb{N}_{0}$. A finite path is a finite sequence in $S(AS)^{\ast}$. In
addition, we sometimes represent $\rho$ as $\rho^{I}$ to emphasize that $\rho$
starts from $s_{0}=s^{I}$. For a path $\rho\ =\ s_{0}a_{0}s_{1}\ldots$, we
define the corresponding labeled path $L(\rho)\ =\
L(s_{0})L(s_{1})\ldots\in(2^{AP})^{\omega}$. $InfPath^{SM}\ (\text{resp.,
}FinPath^{SM})$ is defined as the set of infinite (resp., finite) paths
starting from $s_{0}=s^{I}$ in the SMDP $\mathcal{SM}$. For each finite path
$\rho$, $last(\rho)$ denotes its last state.

Let $InfPath^{\mathcal{SM}}_{\pi}$ (resp., $FinPath^{\mathcal{SM}}_{\pi}$) be
the set of infinite (resp., finite) paths starting from $s_{0}=s^{I}$ in the
SMDP $\mathcal{SM}$ under a policy $\pi$. The time-abstract behavior of the
SMDP $\mathcal{M}$ under a policy $\pi$ is defined on a probability space
$(InfPath^{\mathcal{SM}}_{\pi},\mathcal{F}_{InfPath^{\mathcal{SM}}_{\pi}},Pr^{\mathcal{SM}}_{\pi})$
[1].

###  II-B Linear Temporal Logic and $\omega$-automata

A linear temporal logic (LTL) formula is used to describe a complex control
specification. See [1] for the detail of LTL.

For an LTL formula $\varphi$ and an infinite path $\rho=s_{0}a_{0}s_{1}\ldots$
of the SMDP $\mathcal{SM}$, we denote the satisfaction relation as
$\mathcal{SM},\rho\models\varphi$ and sometimes we omit $\mathcal{SM}$.

An $\omega$-automaton is a tuple $A=(X,\Sigma,\delta,x^{I},Acc)$, where $X$ is
the finite set of states, $\Sigma$ is the input alphabet, $\delta\subseteq
X\times\Sigma\times X$ is the set of transitions, $x^{I}\in X$ is the initial
state, and $Acc\subseteq X$ is the accepting set.

We say that $A$ is deterministic if $|\;\\{x^{\prime}\in
X\;|\;(x,\sigma,x^{\prime})\in\delta\\}\;|\leq 1$ for any $x\in X$ and any
$\sigma\in\Sigma$. $A$ is complete if $\\{x^{\prime}\in
X\;|\;(x,\sigma,x^{\prime})\in\delta\\}\neq\emptyset$ for any $x\in X$ and any
$\sigma\in\Sigma$.

An infinite sequence $w\in\Sigma^{\omega}$ is called a word. An infinite
sequence $r=x_{0}\sigma_{0}x_{1}\ldots\in X(\Sigma X)^{\omega}$ is called a
run on $A$ generated by a word $w=\sigma_{0}\sigma_{1}\ldots\Sigma^{\omega}$
if $(x_{i},\sigma_{i},x_{i+1})\in\delta\ $ for any $i\in\mathbb{N}_{0}$. For
an $\omega$-automaton $A$ and a word $w$, we denote by $Runs(w;A)$ the set of
runs on $A$ generated by $w$. Moreover, for a state $x$ and a run $r$, we
denote by $Visits(x;r)$ the number of times $r$ visits $x$. An
$\omega$-automaton $A$ is called a universal co-Büchi automaton (cBA) (resp.
$K$-co-Büchi automaton ($K$cBA) ) if (1) (resp. (2) ) holds.

$\displaystyle\forall r\in Runs(w;A),\forall x\in Acc.Visits(x;r)<\infty.$ (1)

$\displaystyle\forall r\in Runs(w;A).\sum_{x\in Acc}Visits(x;r)\leq K.$ (2)

We denote the sets of words accepted by a cBA and a $K$cBA by
${\mathcal{L}}_{c}(A)$ and ${\mathcal{L}}_{c,K}(A)$, respectively. Moreover,
the co-Büchi automaton (cBA) and the $K$-co-Büchi automaton ($K$cBA) are
denoted by $B$ and $(B,K)$, respectively, to make clear which acceptance
condition is adopted.

We construct a determinization of $K$cBA (d$K$cBA)
$det(B,K)=(\mathcal{F},\Sigma,\Delta,F^{I},Acc_{d})$ from the $K$cBA
$(B,K)=(X,\Sigma,\delta,x^{I},Acc)$ by a subset construction scheme combined
with the counter for visits to $Acc$. See [8] for the detailed construction
method. For any $K\in\mathbb{N}_{0}$, $det(B,K)$ is deterministic and
complete, and satisfies

$\displaystyle\mathcal{L}_{c,K}(B)=\mathcal{L}_{c,0}(det(B,K)).$ (3)

It is known that, for any LTL formula $\varphi$, there exists a cBA
$B_{\varphi}$ that accepts all words satisfying $\varphi$ [8], where the
alphabet is given by $\Sigma=2^{AP}$.

Let $A=(X,\Sigma,\delta,x^{I},Acc)$ be an $\omega$-automaton. For the subset
of states $X_{sub}\subseteq X$, we call $X_{sub}$ a sink set if there is no
outgoing transition from $X_{sub}$ to $X\setminus X_{sub}$, namely,
$\\{(x,\sigma,x^{\prime})\in\delta\;|\;x\in
X_{sub},\sigma\in\Sigma,x^{\prime}\in X\setminus X_{sub}\\}=\emptyset$.

Note that the set of accepting sates $Acc_{d}$ can be constructed as a sink
set for any d$K$cBA $det(B,K)$. This is because, for any run $r\in X(\Sigma
X)^{\omega}$, once $r$ enters $Acc_{d}$, it never satisfies the acceptance
condition of $det(B,K)$. Without loss of generality, $Acc_{d}$ can be
constructed as a singleton.

For any policy $\pi$ and any state $s\in S$, the probability of paths starting
from $s$ satisfies an LTL formula $\varphi$ on the SMDP $\mathcal{SM}$ under
$\pi$ is defined as follows.

$\displaystyle
Pr^{\mathcal{SM}}_{\pi}(s\models\varphi):=Pr^{\mathcal{SM}}_{\pi}(\\{\rho\\!\in\\!InfPath^{\mathcal{SM}}_{\pi}(s)\;|\;\rho\\!\models\varphi\\}).$

Similarly, we define the probability of paths starting from the initial state
$s$ and the initial action $a$ satisfies $\varphi$ as
$Pr^{\mathcal{SM}}_{\pi}(s,a\models\varphi)$. We call
$Pr^{\mathcal{SM}}_{\pi}(s^{I}\models\varphi)$ the satisfaction probability of
$\varphi$ on $\mathcal{SM}$ under $\pi$.

###  II-C Bayesian inference

To estimate the state transition and the dwell time probability, we use the
following Bayesian inference procedure [16].

Let $\Theta$ be the metric space of parameters and $O$ be the set of
observations. For $\mathcal{O}\subseteq O$ and $\bm{\theta}\in\Theta$, we
first introduce a parametric model $p(\mathcal{O}|\bm{\theta})$ and choose a
prior $p(\bm{\theta})$. Next, we observe data
$\mathcal{O}_{n}=\\{\bm{o}_{0},\bm{o}_{1},\ldots,\bm{o}_{n}\\}$ from the
system. We then calculate the posterior

$\displaystyle p(\bm{\theta}|\mathcal{O}_{n})\propto
p(\mathcal{O}_{n}|\bm{\theta})p(\bm{\theta}).$ (4)

Doob’s theorem guarantees that the posterior probability concentrates in the
neighborhood of the true parameter under mild conditions as $n\to\infty$ [17],
namely the estimated parameter converges to the true parameter in probability.

###### Assumption 1

Assume the following conditions.

  1. 1.

$\bm{\theta}\mapsto p(\cdot\;|\;\bm{\theta})$ is measurable.

  2. 2.

$\bm{\theta}\neq\bm{\theta}^{\prime}$ implies $p(\cdot\;|\;\bm{\theta})\neq
p(\cdot\;|\;\bm{\theta}^{\prime})$.

######  Theorem 1 ([17])

Under Assumption 1, there exists $\Theta_{1}\subseteq\Theta$ with
$p(\Theta_{1})=1$ and, for any $\bm{\theta}_{1}\in\Theta_{1}$, if
$\mathcal{O}_{n}=\\{\bm{o}_{1},\ldots,\bm{o}_{n}\\}\sim
p(\cdot\;|\;\bm{\theta}_{1})\mbox{ i.i.d.}$ then, for any neighborhood $B$ of
$\bm{\theta}_{1}$, we have $\lim_{n\to\infty}p(\bm{\theta}\in
B\;|\;\mathcal{O}_{n})=1\mbox{ a.s. }[p(\cdot\;|\;\bm{\theta}_{1})].$

##  III Problem Statement

We consider the SMDP $\mathcal{SM}$ with unknown $T$ and $D$ and the LTL
specification $\varphi$. We aim to synthesize a control policy that minimizes
the long-term risk for the dwell time of $\mathcal{SM}$ under the achievement
of $\varphi$ with the maximal probability.

To determine the satisfaction of $\varphi$ for $\mathcal{SM}$, we introduce
the product SMDP $\mathcal{SM}^{\otimes}$ of the SMDP
$\mathcal{SM}$$=$$(S,A,T,D,s^{I},AP,L)$ and the d$K$cBA
$det(B_{\varphi},K)$$=$$(\mathcal{F},\Sigma,\Delta,F^{I},Acc_{d})$.
$\mathcal{SM}^{\otimes}$ is given by the tuple
$(S^{\otimes},A^{\otimes},T^{\otimes},D^{\otimes},s^{\otimes
I},Acc^{\otimes})$, where $S^{\otimes}=S\times F$ is the finite set of states;
$s^{\otimes I}=(s^{I},\hat{F}^{I})$ is the initial states, where
$(F^{I},L(s^{I}),\hat{F}^{I})\in\Delta$; $A^{\otimes}$$=$$A$ and
$\mathcal{A}^{\otimes}(s^{\otimes})$$=$$\mathcal{A}(s)$ for each
$s^{\otimes}$$=$$(s,F)\in S^{\otimes}$; $T^{\otimes}:S^{\otimes}\times
S^{\otimes}\times A^{\otimes}\to[0,1]$ is the transition probability defined
as, for any $s^{\otimes}=(s,F),s^{\otimes\prime}=(s^{\prime},F^{\prime})\in
S^{\otimes}$ and any $a\in A(s)$,

$\displaystyle T^{\otimes}(s^{\otimes\prime}|s^{\otimes},a)=$
$\displaystyle\left\\{\begin{aligned} &T(s^{\prime}|s,a)&&\text{if}\
(F,L(s),F^{\prime})\in\Delta,\\\ &0&&\text{otherwise},\end{aligned}\right.$
(5)

$D^{\otimes}:S^{\otimes}\times A\times
S^{\otimes}\to\mathcal{\mathbb{R}}_{\geq 0})$ is the dwell time probability
defined as, for any
$(s^{\otimes}=(s,F),a,s^{\otimes\prime}=(s^{\prime},F^{\prime}))\in
S^{\otimes}\times A\times S^{\otimes}$,
$D^{\otimes}(s^{\otimes},a,s^{\otimes\prime})=D(s,a,s^{\prime})$, where
$s^{\otimes}=(s,F)$ and $s^{\otimes\prime}=(s^{\prime},F^{\prime})$, and
$Acc^{\otimes}=S\times Acc_{d}$. Note that $Acc^{\otimes}$ is non-empty since
$Acc_{d}$ is non-empty. In the following, the product SMDP
$\mathcal{SM}^{\otimes}$ of a given SMDP and a d$K$cBA converted from an LTL
formula $\varphi$ will be called a product SMDP associated with $\varphi$. For
any product SMDP $\mathcal{SM}^{\otimes}$, its acceptance condition is a
safety condition since it is satisfied when any path generated on
$\mathcal{SM}^{\otimes}$ under a policy always stays in $S^{\otimes}\setminus
Acc^{\otimes}$.

For a subset $S_{sub}^{\otimes}$ of $S^{\otimes}$, we introduce an atomic
proposition “This state belongs to $S_{sub}^{\otimes}$”, which denotes
$S_{sub}^{\otimes}$ by abuse of notation. Namely, we say that a state $s\in
S^{\otimes}$ satisfies $S^{\otimes}_{sub}$ if $s\in S^{\otimes}_{sub}$. Then,
the acceptance condition of $\mathcal{SM}^{\otimes}$ is represented by

$\displaystyle\varphi_{B}=\Box\neg Acc^{\otimes}.$ (6)

A policy on the product SMDP $\mathcal{SM}^{\otimes}$ is defined as a mapping
$\pi:S^{\otimes}\times A\rightarrow[0,1]$. A policy $\pi$ is positional if,
for any $s\in S^{\otimes}$ and any $a\in\mathcal{A}^{\otimes}(s)$, there
exists one action $a^{\prime}\in\mathcal{A}^{\otimes}(s)$ such that
$\pi(s,a)=1$ if $a=a^{\prime}$, and $\pi(s,a)=0$ for any
$a\in\mathcal{A}^{\otimes}(s)$ with $a\neq a^{\prime}$. We sometimes denote a
positional policy $\pi$ as a mapping from $S^{\otimes}$ to $A$, that is,
$\pi(s)=a$ for any $(s,a)\in S^{\otimes}\times A$ if $\pi(s,a)=1$.

In the following, we sometimes omit the superscript $\otimes$. We define the
set of winning pairs $W_{p}\subseteq S^{\otimes}\times A$ and the winning
region $W\subseteq S^{\otimes}$ as follows.

$\displaystyle W=\\{s\in S^{\otimes}\;|\;\exists\pi\mbox{ s.t.
}Pr^{\mathcal{SM}^{\otimes}}_{\pi}(s\models\varphi_{B})=1\\}.$ $\displaystyle
W_{p}=\\{(s,a)\in S^{\otimes}\times A\;|\;\exists\pi\mbox{ s.t.
}Pr^{\mathcal{SM}^{\otimes}}_{\pi}(s,a\models\varphi_{B})=1\\}.$

We define a risk factor for the dwell time $\mathsf{Risk}:S\times A\times
S\to\mathbb{R}_{\geq 0}$ as follows. For any $(s,a,s^{\prime})\in S\times
A\times S$,

$\displaystyle\mathsf{Risk}(s,a,s^{\prime})=f(D(s,a,s^{\prime})),$ (7)

where $f:\mathcal{D}(\mathbb{R}_{\geq 0})\to\mathbb{R}$. As examples of $f$,
we have $f_{\alpha}(d)=\inf\\{t\;|\;d(\tau>t)<\alpha\\}$ with $\alpha\in[0,1]$
and $f_{\lambda}(d)=\mu+\lambda\sigma$ with $\lambda\in[0,1]$, where $\mu$ and
$\sigma$ are the mean and the standard deviation of $d$, respectively.

For a policy $\pi$ on the SMDP $\mathcal{SM}$ and a risk factor for the dwell
time $\mathsf{Risk}$, we define the value function
$V^{\mathsf{Risk}}_{\pi}:W\to\mathbb{R}$ for the risk factor as follows. For
any $s\in W$,

$\displaystyle
V^{\mathsf{Risk}}_{\pi}(s)=\mathbb{E}_{\pi}[\sum_{n=0}^{\infty}\gamma^{n}_{\mathsf{r}}\mathsf{Risk}(s_{n},a_{n},s_{n+1})\;|\;s_{0}=s],$

where $\mathbb{E}_{\pi}$ denotes the expected value given that the action
selection follows the policy $\pi$ from the state $s$ and
$\gamma_{\mathsf{r}}\in[0,1)$ is a discount factor. We define the action-value
function $Q^{\mathsf{Risk}}_{\pi}:W_{p}\to\mathbb{R}$ as follows. For any
$(s,a)\in W_{p}$,

$\displaystyle
Q^{\mathsf{Risk}}_{\pi}(s,a)=\mathbb{E}_{\pi}[\sum_{n=0}^{\infty}\gamma^{n}_{\mathsf{r}}\mathsf{Risk}(s_{n},a_{n},s_{n+1})\;|\;s_{0}=s,a_{0}=a]$

Then, we aim at the synthesis of a positional policy
$\pi^{\ast}:S^{\otimes}\to A$ on the product SMDP $\mathcal{SM}^{\otimes}$
that satisfies the following conditions:

  1. 1.

$\pi^{\ast}\in\Pi^{\ast}_{\varphi_{B}}(s^{\otimes I})$.

  2. 2.

$\pi^{\ast}\in\operatorname*{arg\,min}_{\pi\in\Pi^{\ast}_{\varphi_{B}}(s^{\otimes})}V^{\mathsf{Risk}}_{\pi}(s),\forall
s^{\otimes}=(s,F)\in W$,

where $\Pi^{\ast}_{\varphi_{B}}(s^{\otimes})=\operatorname*{arg\,max}_{\pi\in
A^{S^{\otimes}}}Pr^{\mathcal{SM}^{\otimes}}_{\pi}(s^{\otimes}\models\varphi_{B})$
for any $s^{\otimes}\in S^{\otimes}$. We say that the above policy
$\pi^{\ast}$ is optimal with respect to $\varphi_{B}$ and $\mathsf{Risk}$ or
simply optimal. We denote the set of optimal policies as
$\Pi^{\ast}_{\varphi_{B}\succ\mathsf{Risk}}$.

###### Running example

We consider the surveillance problem of a mobile robot in a grid world
depicted in Fig. 1 as a running example. The set of states is
$S=\\{1,\ldots,5\\}^{2}$. The set of actions is $A=\\{UL,UR,DL,DR\\}$. The
black disk represents the robot and its initial state is the right corner
$(5,5)$. The robot moves up and left with probabilities 0.5 under the actions
$UL$. Under $UR$, it moves up and right with probabilities of 0.5,
respectively. Likewise, $DL$ and $DR$ trigger each transition to down, left,
and right with probabilities of 0.5. Under an action, if the robot faces a
wall, it makes the transition to a movable direction w.p.1. If the robot has
no movable direction under an action, it stays in the same state. The blue and
green areas represent the recharge point and the access point, which are
labeled with $a$ and $b$. The red area represents the dangerous area, which is
labeled with $c$. The dwell time probability is given by the exponential
distribution
$D(d\tau\;|\;s,a,s^{\prime})=\lambda_{sas^{\prime}}e^{-\lambda_{sas^{\prime}}\tau}d\tau$
for each transition $(s,a,s^{\prime})$. The parameter $\lambda_{sas^{\prime}}$
is given by $10\max\\{s_{x}-3,s_{y}-3\\}$, where $s=(s_{x},s_{y})$, which
implies that the closer the robot is to the wall, the larger the tail of the
dwell time distribution is. The specification is given as “Visit the blue and
green areas infinitely often while avoiding the red area”. The specification
formally represented as

$\displaystyle\varphi_{ex}=\Box\diamondsuit a\land\Box\diamondsuit
b\land\neg\Box c.$ (8)

The d$K$cBA with $K=20$ converted from $\varphi_{ex}$ is shown in Fig. 1.
Intuitively, the robot is required to visit the blue and the green areas
within $K=20$ time steps infinitely often. The robot aims to satisfy
$\varphi_{B}$ obtained from $\varphi_{ex}$ with the maximal probability and
simultaneously minimize the accumulative risk of the dwell time. When we set
$\mathsf{Risk}(s,a,s^{\prime})=\lambda_{sas^{\prime}}$, the robot has to move
as near the state $(3,3)$ as possible.

Figure 1: (a) The grid world that the robot (black disk) moves. The blue and
the green areas are the access point and the recharge point, respectively. The
areas are labeled with $a$ and $b$, respectively. The red area is the
dangerous area, which is labeled with $c$. (b) The d$K$cBA with $K=20$
converted from $\varphi_{ex}$. Each state is numbered with
$q_{i},i=0,\ldots,442$. For simplicity, we omit the states transitioned by the
label $c$, other some states, and some edges. Each dotted line represents the
consecutive transition by the label.

##  IV Bounded Synthesis and Learning of Policy

We synthesize an optimal policy by the following 3 phases.

  1. 1.

We estimate $W$ and $W_{p}$ of $\mathcal{SM}^{\otimes}$. Simultaneously, we
learn the dynamics $T$ and $D$ of $\mathcal{SM}$ within $W_{p}$ based on the
Bayesian inference. After that, we learn the policy
$\pi_{tr}:S^{\otimes}\setminus W\to A$ that achieves the maximum satisfaction
probability of $\varphi_{B}$. Note that learning the behavior in and outside
$W$ separately is based on the safety acceptance condition of d$K$cBA.

  2. 2.

Based on the value iteration, we synthesize a policy $\pi_{win}:W\to A$ that
minimizes $V^{\mathsf{Risk}}$ utilizing the estimated $T$ and $D$.

  3. 3.

We synthesize an optimal policy by combining $\pi_{tr}$ and $\pi_{win}$.

We first describe phase 1). We define a reward function
$\mathcal{R}:S^{\otimes}\to\mathbb{R}$ and a discount factor function
$\Gamma:S^{\otimes}\to\\{\gamma,\gamma_{acc}\\}$ inspired by [3], where
$\gamma,\gamma_{acc}\in(0,1)$, as follows.

$\displaystyle\mathcal{R}(s)=\left\\{\begin{aligned}
&(1-\gamma_{acc})r_{n}&&\text{if}\ s\in Acc^{\otimes},\\\
&0&&\text{otherwise},\end{aligned}\right.$ (9)

where $r_{n}$ is a negative value.

$\displaystyle\Gamma(s)=\left\\{\begin{aligned} &\gamma_{acc}&&\text{if}\ s\in
Acc^{\otimes}\\!,\\\ &\gamma&&\text{otherwise}.\end{aligned}\right.$ (10)

Then, we introduce the state-action value function $Q_{\pi}:S^{\otimes}\times
A\to\mathbb{R}$ as follows. For any $s\in S$ and any $a\in A(s)$,

$\displaystyle
Q_{\pi,\gamma}(s,a)=\mathbb{E}_{\pi}[\sum_{t=0}^{\infty}\mathcal{R}(s_{t+1})\prod_{k=0}^{t-1}\Gamma(s_{k+1})|s_{0}=s,a_{0}=a],$

where $\mathbb{E}_{\pi}$ is the expected value under the policy $\pi$. We call
the following function $Q^{\ast}:S^{\otimes}\times A\to\mathbb{R}$ an optimal
state-action value function. For any $s\in S^{\otimes}$ and any $a\in A(s)$,

$\displaystyle Q^{\ast}_{\gamma}(s,a)=\max_{\pi\in
A^{S^{\otimes}}}Q_{\pi,\gamma}(s,a).$ (11)

Algorithm 1 Learning of Winning region and Dynamics

0: LTL formula $\varphi$, SMDP $\mathcal{SM}$, and $\ell$.

0: Estimates of $W_{p}$, $h_{T}$, and $h_{D}$.

1: Convert $\varphi$ to d$K$cBA $\det(B_{\varphi},K)$.

2: Construct the product SMDP $\mathcal{SM}^{\otimes}$ of $\mathcal{SM}$ and
$det(B_{\varphi},K)$.

3: Initialize $Q:S^{\otimes}\times E^{\otimes}\to\mathbb{R}$ with -1 for any
$(s,a)\in Acc^{\otimes}\times A$ and 0 otherwise.

4: Initialize $W^{0}=\\{s\in S^{\otimes}\;|\;\exists a\in A(s)\mbox{ s.t.
}Q^{0}(s,a)=0\\}$.

5: Initialize $W_{p}^{0}=\\{(s,a)\in S^{\otimes}\times A\;|\;Q^{0}(s,a)=0\\}$.

6: Initialize $\partial W^{0}=\\{s\in W^{0}|\exists(s,a)\in W^{0}_{p},\exists
s^{\prime}\\!\not\in W^{0},\mbox{ s.t. }T(s^{\prime}|s,a)\\!>\\!0\\}$.

7: Sample $s\in W^{0}$ and set $k=0$.

8: while $W^{k}_{p}$ does not converge. do

9: while True do

10: Take action $a$ under $\pi^{k}_{ex}(s,\cdot)$. Observe
$o=(s,a,s^{\prime},\tau)$ and $r=\mathcal{R}(s,a,s^{\prime})$. Append $o$ to
$\mathcal{O}$.

11: if $s^{\prime}\not\in W^{k}$ then

12: Go to Line 16.

13: end if

14: $s\leftarrow s^{\prime}$.

15: end while

16: Remove all $(s,a,s^{\prime},\tau)$ from $\mathcal{O}$ with respect to
$(s,a)$.

17: Update $Q^{k}$, $W^{k}$, $\partial W^{k}$, and $W^{k}_{p}$ using the
update rules given by Function 2.

18: Sample $s\in\partial W^{k}$.

19: $k\leftarrow k+1$.

20: if $k/\ell\in\mathbb{N}$ then

21: Calculate the posterior of $h_{P}$ and $h_{D}$ with observed data
$\mathcal{O}$ within $W^{k}_{p}$.

22: end if

23: end while

We show the overall procedure to learn $W$, $W_{p}$, $T$, and $D$ of the SMDP
in Algorithm 1. In Line 3, we initialize the state-action value $Q^{0}$. In
Lines 4 and 5, we initialize $W^{0}$ and $W^{0}_{p}$ using $Q^{0}$ as the
estimates of $W$ and $W_{p}$, respectively. In Line 6, we initialize $\partial
W^{0}$ using $W^{0}$ and $W^{o}_{p}$, which is used in exploration. Next, in
each episode $k$, we keep exploring in $W^{k}$ until leaving $W^{k}$. We
explain the details of the exploration policy $\pi^{k}_{ex}$ later. During the
learning, we observe dwell times $\tau\in\mathbb{R}_{\geq 0}$ as well as state
transitions. In Line 16, we keep observed data only within $W_{p}^{k}$. We
denote the set of observed data as
$\mathcal{O}=\\{(s_{i},a_{i},s_{i+1},\tau_{i})\\}_{i\in I}$, where $I$ is an
index set of the data. In Line 17, using Function 2, $Q^{k}$ is updated and
$W^{k}$, $W^{k}_{p}$, and $\partial W^{k}$ are updated by $Q^{k+1}$. Then, we
sample a state from $\partial W^{k}$ and continue the learning. We model $T$
as a parametric distribution $g_{T}(\cdot\;|\;{\theta^{T}}_{sa})$ for each
$(s,a)\in S\times A$. For each $(s,a,s^{\prime})\in S\times A\times S$, we
model $D(\cdot\;|\;s,a,s^{\prime})$ as a parametric distribution
$g_{D}(\cdot\;|\;\bm{\theta}^{D}_{sas^{\prime}})$. We denote the sets of
parameters of $g_{T}$ and $g_{D}$ as $\Theta^{T}$ and $\Theta^{D}$,
respectively. In Line 20, we calculate their posteriors
$h_{T}(\bm{\theta}^{T}_{sa}\;|\;\bm{\zeta}^{T}_{sa})$ and
$h_{D}(\bm{\theta}^{D}_{sas^{\prime}}\;|\;\bm{\zeta}^{D}_{sas^{\prime}})$
based on (4) every $\ell$ step, where $\ell\in\mathbb{N}$ is a given positive
integer, with observed data.

Function 2 Update Rules

0: Transition $(s,a,s^{\prime})$, reward $r$, and $Q^{k}$.

0: $Q^{k+1}$, $W^{k+1}$, $\partial W^{k+1}$, $W^{k+1}_{p}$, and
$\pi^{k}_{ex}$.

1:
$Q^{k+1}(s,a)\leftarrow(1-\alpha)Q^{k}(s,a)+\alpha\\{r+\max_{a^{\prime}}Q^{k}(s^{\prime},a^{\prime})\\}$.

2: $W^{k+1}\leftarrow\\{s\in S^{\otimes}\;|\;\exists a\in A(s)\mbox{ s.t.
}Q^{k+1}(s,a)=0\\}$.

3: $W^{k+1}_{p}\leftarrow\\{(s,a)\in S^{\otimes}\times
A\;|\;Q^{k+1}(s,a)=0\\}$.

4: $\partial W^{k+1}\\!=\\!\\{s\in W^{k+1}|\exists(s,a)\in W^{k+1}_{p},\exists
s^{\prime}\\!\not\in W^{k+1},\mbox{ s.t. }T(s^{\prime}|s,a)\\!>\\!0\\}.$

###### Assumption 2

The following conditions hold at phase 1.

  1. 1.

The learning rate $\alpha$ is a constant.

  2. 2.

For each $s\in W^{\infty}$, $s$ is observed infinitely often w.p.1.

It is known that $W^{k}$ (resp., $W^{k}_{p}$) is monotonically decreasing
under Assumption 2, i.e., $W^{k}\subseteq W^{k^{\prime}}$ (resp.,
$W^{k}_{p}\subseteq W^{k^{\prime}}_{p}$) for any $k^{\prime}\leq k$.
Furthermore, $W^{\infty}:=\lim_{k\to\infty}W^{k}=W$ (resp.,
$W^{\infty}_{p}:=\lim_{k\to\infty}W^{k}_{p}=W_{p}$) holds w.p.1 [9].

#### Details of Exploration

To facilitate the simultaneous collection of the transition and dwell time
data efficiently, we use an entropy-based policy
$\pi^{k}_{ent}:W^{k}_{p}\to[0,1]$ that satisfies the following conditions. For
any $k$ and any $(s^{\otimes}=(s,F),a),(s^{\otimes},a^{\prime})\in W^{k}_{p}$,

$\displaystyle\text{H}[h_{T}(\cdot\;|\;\bm{\zeta}^{T}_{sa})]+\frac{1}{n_{sa}}\sum_{s^{\prime}}\text{H}[h_{D}(\cdot\;|\;\bm{\zeta}^{D}_{sas^{\prime}})]$
$\displaystyle\leq\text{H}[h_{T}(\cdot|\bm{\zeta}^{T}_{sa^{\prime}})]+\frac{1}{n_{sa^{\prime}}}\sum_{s^{\prime}}\text{H}[h_{D}(\cdot\;|\;\bm{\zeta}^{D}_{sa^{\prime}s^{\prime}})]$
$\displaystyle\Rightarrow\pi^{k}_{ent}(s^{\otimes},a)\leq\pi^{k}_{ent}(s^{\otimes},a^{\prime}),$

where $\text{H}[h(\cdot)]=-\int_{x}h(x)\ln{h(x)}dx$ is the entropy of $h$ and
$n_{sa}=|\\{s^{\prime}\in S\;|\;T(s^{\prime}\;|\;s,a)>0\\}|$. Intuitively,
$\pi^{k}_{ent}$ enhances to issue an action that triggers more informative
transitions. An estimate of $T$, denoted by $\tilde{T}$, is given as follows.
For any $((s,F),a)\in W^{k}_{p}$ and any $s^{\prime}\in S$,

$\displaystyle\tilde{T}(s^{\prime}\;|\;s,a)=\int
g_{T}(s^{\prime}\;|\;\bm{\theta}_{sa}^{P})h_{T}(\bm{\theta}_{sa}^{T}\;|\;\bm{\zeta}_{sa}^{T})d\bm{\theta}_{sa}^{T}.$
(12)

We define an estimate of the transition probability of the product SMDP
$\tilde{T}^{\otimes}:S^{\otimes}\times S^{\otimes}\times A\to[0,1]$ for
$\tilde{T}$ in accordance with (5). To facilitate the efficient learning of
$W_{p}$, we introduce $\pi^{k}_{W^{\perp}}:W^{k}_{p}\to[0,1]$ that satisfies
the following condition. For any $k$ and any
$(s^{\otimes},a),(s^{\otimes},a^{\prime})\in W^{k}_{p}$,

$\displaystyle\sum_{s^{\otimes\prime}\not\in
W^{k}}\tilde{T}^{\otimes}(s^{\otimes\prime}\;|\;s^{\otimes},a)\leq\sum_{s^{\otimes\prime}\not\in
W^{k}}\tilde{T}^{\otimes}(s^{\otimes\prime}\;|\;s^{\otimes},a^{\prime})$
$\displaystyle\Rightarrow\pi^{k}_{W^{\perp}}(s^{\otimes},a)\leq\pi^{k}_{W^{\perp}}(s^{\otimes},a^{\prime}).$

Moreover, for each episode $k$, we restrict the region where an initial state
is sampled to $\partial W^{k}$ given by

$\partial W^{k}\\!=\\!\\{s\in W^{k}|\exists(s,a)\in W^{k}_{p},\exists
s^{\prime}\not\in W^{k}\mbox{ s.t. }T(s^{\prime}|s,a)\\!>\\!0\\}.$

Intuitively, $\pi^{k}_{W^{\perp}}$ and the state-sampling from $\partial
W^{k}$ enhance to take an out-going transition from $W^{k}$ for each $k$. We
define an exploration policy $\pi^{k}_{ex}:W^{k}_{p}\to[0,1]$ as follows. For
any $k$ and any $(s,a)\in W^{k}_{p}$,

$\displaystyle\pi^{k}_{ex}(s,a)=\left\\{\begin{aligned}
&\pi^{k}_{W^{\perp}}(s,a)&&\text{if}\ s\in\partial W^{k},\\\
&\pi^{k}_{ent}(s,a)&&\text{otherwise},\end{aligned}\right.$ (13)

$\pi^{k}_{ex}$ is expected to facilitate the efficient learning of $W_{p}$ and
the unbiased learning of $T$ and $D$.

Note that, for any transition $(s,a,s^{\prime})$ stored in $\mathcal{O}$ after
the learning, using $\pi^{k}_{ex}$, we have $(s,a)\in W_{p}$ and
$s^{\prime}\in W$ w.p.1 under Assumption 2 [9].

After the learning of $W_{p}$, $T$, and $D$, we compute
$\pi^{\gamma}_{tr}:S^{\otimes}\setminus W\to A$ defined as follows. For any
$s\in S^{\otimes}\setminus W$,

$\displaystyle\pi^{\gamma}_{tr}(s)\in\operatorname*{arg\,max}_{a\in
A(s)}Q^{\ast}_{\gamma}(s,a).$ (14)

###### Theorem 2

Given a product SMDP $\mathcal{SM}^{\otimes}$ associated with an LTL formula
$\varphi$, there exists a discount factor $\gamma^{\prime}\in(0,1)$ such that,
for any $\gamma>\gamma^{\prime}$ and any $s\in S^{\otimes}$, the following
equation holds.

$\displaystyle
Pr^{\mathcal{SM}^{\otimes}}_{\pi^{\gamma}_{tr}}(s\models\varphi_{B})=\max_{\pi\in
A^{S^{\otimes}}}Pr^{\mathcal{SM}^{\otimes}}_{\pi}(s\models\varphi_{B}).$ (15)

A proof of Theorem 2 is similar to the proof of Theorem 3 in [9] and omitted.
From Theorem 2, for any $\gamma$ sufficiently close to one,
$\pi^{\gamma}_{tr}$ maximizes the satisfaction probability of $\varphi_{B}$.

The learning scheme of $\pi^{\gamma}_{tr}$ is based on the update rule of
Q-learning
$Q(s,a)\leftarrow(1-\alpha_{i})Q(s,a)+\alpha_{i}\\{r+\max_{a^{\prime}}Q(s^{\prime},a^{\prime})\\}$,
where $(s,a,s^{\prime})$ and $r$ are the observed transition and the
corresponding reward, respectively, and $i$ is the iteration number. However,
in the learning scheme, each learning episode is terminated when entering the
estimated winning region $W^{\infty}$. We denote the learned
$\pi^{\gamma}_{tr}$ as $\tilde{\pi}^{\gamma}_{tr}$. We assume the following
condition.

###### Assumption 3

$\sum_{i=1}^{\infty}\alpha_{i}=\infty$ and
$\sum_{i=1}^{\infty}\alpha_{i}^{2}<\infty$ hold.

Figure 2: (a) The average of $Ind^{k}$ per episode. (b) The black arrows are
illustrative actions taken by the learned robot at the states. The red arrows
represents an obtained sample path.

To assess the convergence of $W_{p}^{k}$ for the running example, we introduce
the index $Ind^{k}=|W_{p}|/|W_{p}^{k}|$ as the coincidence ratio between
$W_{p}$ and $W_{p}^{k}$ for each $k\in\mathbb{N}_{0}$. We show the average of
$Ind^{k}$ by repeating the learning 50 times, where the parameters are
$\gamma=0.9999$, $\gamma_{acc}=0.9$, and $r_{n}=-1$. It converges around 9000
episode. We show the action selection by $\tilde{\pi}_{tr}^{\gamma}$ at states
of the SMDP corresponding to non-winning states as black arrows in Fig. 2. We
iterate the Q-learning 5000 episodes to learn $\tilde{\pi}_{tr}^{\gamma}$. The
actions imply that the robot moves to (3,4), which corresponds to a winning
state, with the maximum probability.

Next, we describe phase 2). An estimate of $D$, denoted by $\tilde{D}$, is
given as follows. For any $((s,F),a)\in W^{\infty}_{p}$ and any $s^{\prime}\in
S$,

$\displaystyle\tilde{D}(\tau|s,a,s^{\prime})\\!=\\!\int
g_{D}(\tau|\bm{\theta}_{sas^{\prime}}^{D})h_{D}(\bm{\theta}_{sas^{\prime}}^{D}|\bm{\zeta}_{sas^{\prime}}^{D})d\bm{\theta}_{sas^{\prime}}^{D}.$
(16)

We introduce $A_{\varphi}:W^{\infty}\to A$ as follows.

$\displaystyle A_{\varphi}(s^{\otimes})=\\{a\in A\;|\;(s^{\otimes},a)\in
W^{\infty}_{p}\\}.$ (17)

Denoted by $\widetilde{\mathsf{Risk}}(s,a,s^{\prime})$ is the risk of the
transition $(s,a,s^{\prime})$ for $\tilde{D}$, i.e., by (7), we have
$\widetilde{\mathsf{Risk}}(s,a,s^{\prime})=f(\tilde{D}(s,a,s^{\prime}))$ for
any $(s,a,s^{\prime})\in S\times A\times S$. With $\tilde{T}$,
$\widetilde{\mathsf{Risk}}$, and $A_{\varphi}$, we define
$\tilde{Q}^{\mathsf{Risk}}:W^{\infty}_{p}\to\mathbb{R}$ as follows and compute
it by the value iteration.

$\displaystyle\tilde{Q}^{\mathsf{Risk}}(s^{\otimes},a)$
$\displaystyle=\sum_{s^{\otimes\prime}\in
S^{\otimes}}\\!\\!\\!\\!\\!\tilde{T}(s^{\prime}|s,a)(\widetilde{\mathsf{Risk}}(s,a,s^{\prime})\\!+\\!\gamma_{\mathsf{r}}\min_{a^{\prime}\in
A_{\varphi}(s^{\otimes})}\\!\\!\tilde{Q}^{\mathsf{Risk}}(s^{\otimes\prime},a^{\prime})),$

where $s^{\otimes}=(s,F)$. Then, we obtain $\tilde{\pi}_{win}:W^{\infty}\to A$
as follows.

$\displaystyle\tilde{\pi}_{win}(s)\in\operatorname*{arg\,max}_{a\in
A_{\varphi}(s^{\otimes})}\tilde{Q}^{\mathsf{Risk}}(s^{\otimes},a).$ (18)

Finally, in phase 3), we obtain a policy $\pi^{\infty}_{\gamma}:S^{\otimes}\to
A$ by combining $\pi^{\gamma}_{tr}$ and $\pi_{win}$. For any $s\in
S^{\otimes}$, we define $\pi^{\infty}_{\gamma}$ as follows.

$\displaystyle\tilde{\pi}^{\ast}_{\gamma}(s)=\left\\{\begin{aligned}
&\tilde{\pi}_{win}(s)&&\text{ if }s\in W^{\infty},\\\
&\tilde{\pi}^{\gamma}_{tr}(s)&&\text{ otherwise.}\end{aligned}\right.$ (19)

###### Assumption 4

Assume the following conditions

  1. 1.

For any $(s^{\otimes}\\!=\\!(s,F),a)\\!\in\\!W_{p}$ and any
$(s^{\prime},F^{\prime})\in\\{s^{\otimes^{\prime}}\in
W^{\infty}\;|\;T(s^{\otimes^{\prime}}|s^{\otimes},a)>0\\}$, there exist
$\bm{\theta}^{T}_{sa}$ and $\bm{\theta}^{D}_{sas^{\prime}}$ such that
$T(\cdot\;|\;s,a)=g_{T}(\cdot\;|\;\bm{\theta}^{T}_{sa})$ and
$D(\cdot\;|\;s,a,s^{\prime})=g_{D}(\cdot\;|\;\bm{\theta}^{D}_{sas^{\prime}})$.

  2. 2.

$g_{T}$ and $g_{D}$ satisfy Assumption 1.

###### Theorem 3

Let $\mathcal{SM}^{\otimes}$ be the product SMDP associated with an LTL
formula $\varphi$. Under Assumptions 2, 3, and 4, there exist
$\gamma^{\prime}\in(0,1)$ and an optimal policy
$\pi^{\ast}\in\Pi^{\ast}_{\varphi_{B}\succ\mathsf{Risk}}$ such that, for any
$\gamma>\gamma^{\prime}$, $\tilde{\pi}^{\ast}_{\gamma}=\pi^{\ast}$ in
probability as $|\mathcal{O}|\to\infty$.

###### Proof:

Recall that $W^{\infty}_{p}=W_{p}$ and $W^{\infty}=W$ hold w.p.1 under
Assumption 2. Thus, for any $(s,a)\in W_{p}$ and
$s^{\prime}\in\\{s^{\prime}\in W\;|\;T(s^{\prime}|s,a)>0\\}$, we have
$T(\cdot\;|\;s,a)=\tilde{T}(\cdot\;|\;s,a)$ and
$D(\cdot\;|\;s,a,s^{\prime})=\tilde{D}(\cdot\;|\;s,a,s^{\prime})$ in
probability as $|\mathcal{O}|\to\infty$ by Theorem 1 under Assumptions 2 and
4. This implies $Q^{\mathsf{Risk}}=\tilde{Q}^{\mathsf{Risk}}$. Hence, for each
$s\in W$, $\tilde{\pi}_{win}(s)$ maximizes $Q^{\mathsf{Risk}}(s,\cdot)$ on
$A_{\varphi}(s)$ in probability. By Theorem 2 and the convergence property of
Q-learning [18], under Assumption 3, there exists $\gamma^{\prime}$ such that,
for any $\gamma>\gamma^{\prime}$, $\tilde{\pi}^{\gamma}_{tr}$ maximizes the
satisfaction probability of $\varphi_{B}$ w.p.1. Therefore, there exists an
optimal policy $\pi^{\ast}\in\Pi^{\ast}_{\varphi_{B}\succ\mathsf{Risk}}$ such
that we have $\tilde{\pi}^{\ast}_{\gamma}=\pi^{\ast}$ in probability. ∎

By Theorem 3, we can synthesize an optimal policy under the discount factor
sufficiently close to 1 and the sufficient iteration in Algorithm 1.

In the running example, we model $T$ and $D$ as a categorical distribution and
an exponential distribution, respectively. Prior for each distribution is
chosen as a Dirichlet distribution and a Gamma distribution. We give the risk
for transitions as
$\mathsf{Risk}(s,a,s^{\prime})=\mu_{sas^{\prime}}+\sigma_{sas^{\prime}}$,
where $\mu_{sas^{\prime}}$ and $\sigma_{sas^{\prime}}$ are the mean and the
standard deviation of the estimated dwell time. We set the parameters as
$\gamma_{\mathsf{r}}=0.9$ and $\ell=1$. We show a sample path by the learned
$\tilde{\pi}_{\gamma}^{\ast}$ as the red arrows in Fig. 2. We observe that the
robot tends to move near (3,3) under the satisfaction of $\varphi_{ex}$ after
learning, which implies that the robot minimizes the long-term risk while
satisfying $\varphi_{ex}$.

##  V Conclusion

In this letter, for a semi-Markov decision process, we proposed a learning-
based bounded synthesis of the optimal policy that minimizes a long-term risk
for the dwell time under the satisfaction of a given LTL specification. We
show that the synthesized policy is equal to an optimal one in probability
under some assumptions and conditions. Future works are to extend the proposed
method to the continuous state space and to develop the learning method to
estimate the winning region and the policy to minimize an accumulative risk
concurrently. It is also future work to apply the proposed method to a real
system.

## References

  * [1] C. Baier and J.-P. Katoen, Principles of Model Checking.  MIT Press, 2008.
  * [2] D. Sadigh, E. S. Kim, S. Coogan, S. S. Sastry, and S. A. Seshia, “A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications,” in Proc. 53rd IEEE Conf. Decis. Control, pp. 1091–1096, 2014.
  * [3] A. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic, “Control synthesis from linear temporal logic specifications using model-free reinforcement learning,” in Proc. IEEE Int. Conf. Robot. Automation, pp. 10349–10355, 2020.
  * [4] E. M. Hahn, M. Perez, S. Schewe, F. Somenzi, A. Trivedi, and D. Wojtczak, “Omega-regular objectives in model-free reinforcement learning,” in Int. Conf. Tool. Algo. Constr. Analys. Systems, pp. 395–412, 2019.
  * [5] R. Oura, A. Sakakibara, and T. Ushio, “Reinforcement learning of control policy for linear temporal logic specifications using limit-deterministic generalized Büchi automata,” IEEE Contr. Syst. Lett., vol. 4, no. 3, pp. 761–766, 2020.
  * [6] X. Li, C.-I. Vasile, and C. Belta, “Reinforcement learning with temporal logic rewards,” in IEEE/RSJ Int. Conf. Intel. Robot. Syst., pp. 3834–3839, IEEE, 2017.
  * [7] X. Li, Z. Serlin, G. Yang, and C. Belta, “A formal methods approach to interpretable reinforcement learning for robotic planning,” Science Robotics, vol. 4, no. 37, 2019.
  * [8] E. Filiot, N. Jin, and J.-F. Raskin, “Antichains and compositional algorithms for LTL synthesis,” Form. Meth. Syst. Design, vol. 39, no. 3, pp. 261–296, 2011.
  * [9] R. Oura, T. Ushio, and A. Sakakibara, “Bounded synthesis and reinforcement learning of supervisors for stochastic discrete event systems with LTL specifications,” arXiv:2105.03081, 2021.
  * [10] S. M. Ross, Applied probability models with optimization applications.  Courier Corporation, 2013.
  * [11] S. J. Bradtke and M. O. Duff, “Reinforcement learning methods for continuous-time Markov decision,” in proc. 7th Adv. Neur. Info. Proces. Syst., vol. 7, pp. 393–400, 1994.
  * [12] S. Schmoll and M. Schubert, “Semi-Markov reinforcement learning for stochastic resource collection,” in Proc. 29th Int. Conf. Int. Joint Conf. Artif. Intel., pp. 3349–3355, 2021.
  * [13] B. Wu, B. Hu, and H. Lin, “A learning based optimal human robot collaboration with linear temporal logic constraints,” arXiv:1706.00007, 2017.
  * [14] M. Wen and U. Topcu, “Probably approximately correct learning in stochastic games with temporal logic specifications.,” in Proc. Int. Joint Conf. Artif. Intel., pp. 3630–3636, 2016.
  * [15] J. Fu and U. Topcu, “Probably approximately correct mdp learning and control with temporal logic constraints,” arXiv:1404.7073, 2014.
  * [16] C. M. Bishop, Pattern Recognition and Machine Learning.  Springer: New York, 2006.
  * [17] J. W. Miller, “A detailed treatment of Doob’s theorem,” arXiv:1801.03122, 2018.
  * [18] D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming.  Athena Scientific, 1996.