NNgTL: Neural Network Guided Optimal Temporal Logic Task Planning for Mobile Robots

Extracted source text · arXiv 2309.14050

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%2345678901234567890123456789012345678901234567890123456789012345678901234567890
%        1         2         3         4         5         6         7         8

\documentclass[letterpaper, 10 pt, conference]{ieeeconf}  % Comment this line out if you need a4paper

%\documentclass[a4paper, 10pt, conference]{ieeeconf}      % Use this line for a4 paper

\IEEEoverridecommandlockouts                              % This command is only needed if 
                                                          % you want to use the \thanks command

\overrideIEEEmargins                                      % Needed to meet printer requirements.

%In case you encounter the following error:
%Error 1010 The PDF file may be corrupt (unable to open PDF file) OR
%Error 1000 An error occurred while parsing a contents stream. Unable to analyze the PDF file.
%This is a known problem with pdfLaTeX conversion filter. The file cannot be opened with acrobat reader
%Please use one of the alternatives below to circumvent this error by uncommenting one or the other
%\pdfobjcompresslevel=0
%\pdfminorversion=4

% See the \addtolength command later in the file to balance the column lengths
% on the last page of the document

% The following packages can be found on http:\\www.ctan.org
%\usepackage{graphics} % for pdf, bitmapped graphics files
%\usepackage{epsfig} % for postscript graphics files
%\usepackage{mathptmx} % assumes new font selection scheme installed
%\usepackage{times} % assumes new font selection scheme installed
%\usepackage{amsmath} % assumes amsmath package installed
%\usepackage{amssymb}  % assumes amsmath package installed
\usepackage{subcaption}
\usepackage{cite}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{algorithmic}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{url}
\usepackage{xcolor}
\usepackage{siunitx} \usepackage{flushend}
\usepackage{tikz}
\usetikzlibrary{positioning, arrows.meta,automata}
\usetikzlibrary{calc}
\def\XY#1{{\textcolor{red}{ {\bf XY:} #1}}}
\def\RJ#1{{\textcolor{red}{ {\bf RJ:} #1}}}
\newtheorem{problem}{Problem}

\def \x{\mathbf{x}}
\def \Q{\mathcal{Q}}
\def \W{\mathcal{W}}

\def \T{\mathcal{T}}
\def \V{\mathcal{V}}
\def \E{\mathcal{E}}
\def \Q{\mathcal{Q}}
\def \Al{\square}
\def \Ev{\Diamond}

\title{\LARGE \bf NNgTL: Neural Network Guided Optimal Temporal Logic\\ Task Planning for Mobile Robots
}


\author{Ruijia Liu, Shaoyuan Li and Xiang Yin% <-this % stops a space
\thanks{This work was supported by the National Natural Science Foundation of China (62061136004, 62173226, 61803259).)
}% <-this % stops a space
\thanks{R. Liu, S. Li and  X. Yin are with the Department of Automation, Shanghai Jiao Tong University, Shanghai 200240, China, and also with the Key Laboratory of System Control and Information Processing, the Ministry of Education of China, Shanghai 200240, China. {\tt  E-mail: \{liuruijia,syli,yinxiang\}@sjtu.edu.cn}} 
}

\begin{document}



\maketitle
\thispagestyle{empty}
\pagestyle{empty}
\setlength{\abovecaptionskip}{3pt}
\setlength{\belowcaptionskip}{0pt}
\setlength{\textfloatsep}{6pt}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{abstract}
In this work, we investigate task planning for mobile robots  under linear temporal logic (LTL) specifications. This problem is particularly challenging when robots navigate in continuous workspaces due to the high computational complexity involved. Sampling-based methods have emerged as a promising avenue for addressing this challenge   by incrementally constructing random trees, thereby sidestepping the need to explicitly explore the entire state-space. However, the 
performance of this sampling-based approach hinges crucially on the chosen sampling strategy, and a well-informed heuristic can notably enhance sample efficiency. 
In this work, we propose a novel \emph{neural-network guided} (NN-guided) sampling  strategy tailored for LTL planning. Specifically, we employ a multi-modal neural network capable of extracting features concurrently from both the workspace and the B\"{u}chi automaton. This neural network generates predictions that serve as guidance for random tree construction, directing the sampling process toward more optimal directions.
Through numerical experiments, we compare our approach with existing methods and demonstrate its superior efficiency, requiring less than 15\% of the time of the existing methods to find a feasible solution. 
\end{abstract}

\input{contents/introduction}



% !TEX root = ../root.tex

\section{Problem Formulation}

\subsection{System Model} 
We consider the scenario, where a single robot navigating in a two-dimensional continuous workspace  represented by a compact subset $\mathcal{W}\subseteq \mathbb{R}^2$. 
The workspace is assumed to be partitioned as $\mathcal{W}=\mathcal{W}_\text{free}\dot{\cup}\mathcal{O}$, 
where $\mathcal{O}$ is an open subset representing obstacle regions and $\mathcal{W}_\text{free}$ is the free region in which the robot can move.  
The free workspace is further partitioned as  $m$ labeled regions of interest and a non-labeled region
$\mathcal{W}_\text{free}=\mathcal{R}_1\dot{\cup} \cdots\dot{\cup} \mathcal{R}_m\dot{\cup} \mathcal{R}_{non}$. 
 
The mobility of the robot can be captured by  a weighted transition system 
\[
TS = (\mathcal{W}, \mathbf{x}_0, \rightarrow_T, \mathcal{A P}, L, C),
\]
where 
$\mathcal{W}$ is set of infinite positions of the robot; 
$\mathbf{x}_0$ is its initial position; 
$\rightarrow_T \subseteq \mathcal{W} \times \mathcal{W}$ is the transition relation such that: 
for any $\x,\x'\in \mathcal{W}$, we have $(\x,\x')\in \to_T $ if along the straight line between $\x$ and $\x'$ 
(i) does not intersect with $\mathcal{O}$; and  
(ii)  crosses any  boundary of labeled regions at most once \cite{luo2021abstraction};  
$\mathcal{A P}=\{\pi^{1},\dots, \pi^{m}\}$ is the set of atomic propositions
with labeling function $L: \mathcal{W} \to \mathcal{A P}$ such that $L(\x)=\pi^{i}$ iff $\x\in \mathcal{R}_i$; 
$C: \mathcal{W} \times \mathcal{W} \to \mathbb{R}^{+}$ is the weight function  calculating  the Euclidean distance, i.e., $C(\mathbf{x}_1, \mathbf{x}_2) = \left\|\mathbf{x}_1 - \mathbf{x}_2\right\|_2$. 


An infinite \emph{path} is a sequence $\tau \!=\! \tau(1) \tau(2) \cdots\! \in\! \mathcal{W}^\omega$ such that 
$\tau(1) = \x_0$ and  $(\tau(k),\tau(k+1))\in \to_T, k=1,2,\dots$.  
The \emph{trace} of infinite path $\tau$ is  $\operatorname{trace}(\tau) = L(\tau(1)) L(\tau(2)) \cdots \in (\mathcal{AP})^\omega$. 
We say a path $\tau$ is finite if it is a finite sequence of points, and we denote by $|\tau|$ its \emph{length}. 
For  a finite path $\tau$, its cost $J(\tau)$ is defined as the the cumulative distances between consecutive states, 
i.e.,  $J(\tau) = \sum_{k=1}^{|\tau|-1} C(\tau(k), \tau(k+1))$.

\subsection{Temporal Logic Tasks}
%
The formal specification of robot is captured by an linear temporal logic formula without next (LTL$_{-\bigcirc}$), which is widely used in robot task planning in continuous workspace \cite{kloetzer2008fully}. 
The syntax of LTL$_{-\bigcirc}$ is given as follows: 
\[
\phi::=\text{true} \mid  \pi\in \mathcal{A P}\mid   \neg \phi  \mid \phi_1 \wedge \phi_2  \mid   \phi_1  \mathcal{U}   \phi_2, 
\]
where $\neg$ and $\wedge$ are Boolean operators ``negation" and ``conjunction", respectively; 
$\mathcal{U}$ is the temporal operator ``until", which can further induce temporal operators ``eventually" $\Diamond$ and ``always" $\square$. 

An LTL formula $\phi$ is evaluated over an infinite word $\sigma=\sigma(1)\sigma(2)\cdots\in \mathcal{AP}^\omega$. 
We denote by $\sigma\models \phi$ that word $\sigma$ satisfies LTL formula $\phi$; the reader is referred to \cite{baier2008principles} for the formal semantics. 
We denote by $\operatorname{Words}(\phi)$   the set of all words   satisfying  formula $\phi$. 
It is well-known that, for any LTL formula $\phi$, $\operatorname{Words}(\phi)$ can be accepted by a non-deterministic B\"{u}chi automaton (NBA) \cite{baier2008principles}.  
Formally, an NBA is a tuple $B=(\mathcal{Q}_B, \mathcal{Q}_B^0,\Sigma, \rightarrow_B, \mathcal{Q}_B^F)$, 
where 
$\mathcal{Q}_B$ is the set of states, 
$\mathcal{Q}_B^0$ is the set of initial states, 
$\Sigma =\mathcal{AP}$ is the alphabet, 
$\rightarrow_B \subseteq \mathcal{Q}_B \times \Sigma \times \mathcal{Q}_B$ is the transition relation, 
and $\mathcal{Q}_B^F$ is the set of accepting states. 
For simplicity, we assume that the initial-state is unique, i.e.,  $\mathcal{Q}_B^0=\{q_B^0\}$. 

An infinite run $\rho_B$ of $B$ over an infinite word $\sigma=\pi_0 \pi_1   \cdots \in\left( {\mathcal{A P}}\right)^\omega$  is a sequence $\rho_B=q_B^0 q_B^1 q_B^2 \cdots$ such that  $q_B^0 \in \mathcal{Q}_B^0,\left(q_B^i, \pi_i, q_B^{i+1}\right) \in \rightarrow_B, \forall i=0,1,\dots$. We say infinite run $\rho_B$  is accepting if it contains accepting states infinite number of times; 
we say a word is accepting if it induces an accepting run, and we denote by $\mathcal{L}_B$ the set of all accepting words of $B$. 
Hereafter, $B$ is referred to as the NBA that accepts $\phi$, i.e., $\mathcal{L}_B = \operatorname{Words}(\phi)$. 

\subsection{LTL Task Planning Problem}
%
To fulfill an  $\mathrm{LTL}_{-\bigcirc}$ formula $\phi$, the robot needs to execute an infinite path. 
For the purpose of planning, it suffices to consider paths in the   ``prefix-suffix'' structure 
$\tau = \tau^{\mathrm{pre}}[\tau^{\mathrm{suf}}]^\omega$, 
where the prefix part $\tau^{\mathrm{pre}}$ repeats only once and the suffix part $\tau^{\mathrm{suf}}$ repeats indefinitely \cite{guo2015multi}. The cost of   prefix-suffix path $\tau$ is  defined by 
$J(\tau)=\lambda J(\tau^{\mathrm{pre}})+(1-\lambda)J(\tau^{\mathrm{suf}})$, where $\lambda \in [0,1]$ is a user-defined weight coefficient.


Then our objective is to find a plan for the robot in the prefix-suffix structure such that  
a given LTL formula is fulfilled with minimum cost.  
 
\begin{problem}\label{problem1}
Given $\mathrm{LTL}_{-\bigcirc}$ formula $\phi$, determine a prefix-suffix path $\tau$ in   transition system $TS$ 
such that (i) $\operatorname{trace}(\tau)\models \phi$; and 
(ii) for any prefix-suffix path $\tau'$ such that $\operatorname{trace}(\tau')\models \phi$, 
we have $J(\tau)\leq J(\tau')$. 
\end{problem}

  
\section{Sampling-Based Task Planning}\label{section_heuristicsample}
%
To  solve  Problem \ref{problem1}, a typical approach is to perform graph-search  on the \emph{product} of $TS$ and $B$ \cite{smith2011optimal}. 
However, when the state space $\mathcal{W}$ is continuous, building  the entire product space is infeasible even by discretizations.  
Therefore, in \cite{luo2021abstraction}, the authors proposed a (continuous space) sampling-based algorithm, called TL-RRT*, that incrementally builds trees on-the-fly without construct  the entire product space a priori. 
Our work is build upon the sampling-based approach; therefore, we review it briefly in this section. 
The readers are referred to \cite{luo2021abstraction} for more details on this method. 

\subsection{Main Sampling-Based Algorithm} 
The TL-RRT* algorithm is essentially a random search over the product space $\Q_P:=\mathcal{W}_{\text{free}}\times \Q_B$. It consists of two parts, prefix part and suffix part, and for each part, a similar random tree construction is employed in order to search the optimal path. We briefly sketch the procedures. 
 
\subsubsection{Prefix Search}
Starting from the initial state $q_0=(\x_0, q_B^0)$, one first builds a prefix tree $\T=( \mathcal{V}_{\mathcal{T}},\mathcal{E}_{\mathcal{T}},\operatorname{Cost} )$ by incrementally adding vertices, where $\mathcal{V}_{\mathcal{T}}$ and $\E_\T$ are the sets of vertices and edges in $\T$, respectively.  
The tree contains some  \emph{goal states}  defined by
    $\mathcal{Q}_{\text {goal}}:=  \mathcal{W}_{\text{free}}\times  \mathcal{Q}_B^F$.  
By projecting paths in tree onto $\mathcal{W}$,  
the path from the initial state $q_0$ to each goal state 
    $q_{\text{goal}}\in\V_\T\cap \mathcal{Q}_{\text {goal}}$ forms a prefix path $\tau^{\mathrm{pre}}$, whose cost is stored by function $\text {Cost}: \mathcal{V}_{\mathcal{T}} \rightarrow \mathbb{R}^{+}$. 

\subsubsection{Suffix Search}
The suffix part is very similar to the prefix part, 
the main difference is that one needs to construct a set of random trees rooted from  goal states $\mathcal{P}:=\T\cap \mathcal{Q}_{\text {goal}}$ in the prefix tree
such that they can return back to the goal states. 
This gives us a suffix  plan  $\tau^{\mathrm{suf}}$ from  each goal state,  and the prefix-suffix plan with minimum cost among all goal states is the final optimal plan.  
    
    
\subsubsection{Constructing Random Trees}
In the above two parts, the key is construction of random tree  $\T=( \mathcal{V}_{\mathcal{T}},\mathcal{E}_{\mathcal{T}},\operatorname{Cost} )$ on-the-fly. The main construction steps are  as follows. 
\begin{enumerate}
    \item 
    Sample a state $ \mathbf{x}^{\text {rand}}\in  \mathcal{W}_{\text {free }}$ ``randomly"; 
    \item
    Determine a  new state $ \mathbf{x}^{\text {new}} $ to be added to the tree based on some distance criteria 
    on $ \mathbf{x}^{\text {rand}} $ and $\T$;  
    \item 
    Determine set  $ \Q^{\text {near}} \subseteq \V_\T$  based on some distance criteria
    from which the tree will be extended to $\x^{\text {new}}$; 
    \item 
    For each state 
    $ q_{P}^{\text {near }}=(\mathbf{x}^{\text{near}},q_B^{\text{near}}) \in  \mathcal{Q}_{P}^{\text {near }} $, 
    we consider a potential edge from  
    $q_P$  to  $ q_{P}^{\text {new}}=\left(\mathbf{x}^{\text {new}}, q_B\right) $ 
    if 
    $ (\x^{\text{near}} , \x^{\text{new}})\in \rightarrow_T $ 
    and $(q_B^{\text {near }}, L (\x^{\text {near }}), q_B^{\text {new }}) \in \rightarrow_B $;   
    \item 
    Add $q_{P}^{\text {new}}$ to tree $\T$ from state $q_P\in \mathcal{Q}_{P}^{\text {near }}$ to minimize  $ \operatorname{Cost}(q_{P}^{\text {new }})\!=\!\operatorname{Cost}(q_{P}^{\text {near}})\!+\!C(q_{P}^{\text {near}},q_{P}^{\text {new}}) $; 
    \item 
    After adding $q_{P}^{\text {new}}$, the tree edges and costs are reconfigured so that each vertex is reached by a path with minimum cost from the root.
\end{enumerate} 
% \begin{enumerate}
%     \item 
%     Sampling a state $ \mathbf{x}^{\text {rand}} $ ``randomly" from $ \mathcal{W}_{\text {free }} $.
%     \item Find the set $ \mathcal{Q}_{P}^{\text {nearest }} $, consisting of nodes $ q_{P}^{\text {nearest }}=\left(\mathbf{x}^{\text {nearest}}, q_{B}^{\text {nearest }}\right) $ from $ \mathcal{V}_{\mathcal{T}} $ that are closest to $ \mathbf{x}^{\text {rand}} $ based on the distance $ \left\|\mathbf{x}^{\text {rand}}-\mathbf{x}^{\text {nearest }}\right\| $. $ \mathcal{Q}_{P}^{\text {nearest}} $ may contain multiple nodes with the same $ \mathbf{x}^{\text {nearest }} $ but different $ \mathcal{Q}_{P}^{\text {nearest}} $.
%     \item Construct a new state $ \mathbf{x}^{\text {new}} $ from $ \mathcal{W}_{\text {free}} $ such that $ \left\|\mathbf{x}^{\text {new}}-\mathbf{x}^{\text {rand}}\right\| \leq\left\|\mathbf{x}^{\text {nearest}}-\mathbf{x}^{\text {rand}}\right\| $ and $ \left\|\mathbf{x}^{\text {nearest }}-\mathbf{x}^{\text {new }}\right\| \leq\eta $, with $ \eta $ being a user-specified step size. If no $ \mathbf{x}^{\text {new}} $ fulfills these criteria, revert to the first step.
%     \item Form the node set $ \mathcal{Q}_{P}^{\text {near}} \subseteq \mathcal{V}_{\mathcal{T}} $ as a union of $ \mathcal{Q}_{P}^{\text {nearest}} $ and the set $ \left\{q_P= \left(\mathbf{x}, q_B\right) \mid \left\|\mathbf{x}-\mathbf{x}^{\text {new}}\right\| \leq r_n\left(\mathcal{V}_{\mathcal{T}}\right)\right\} $. The exact definition of $ r_n\left(\mathcal{V}_{\mathcal{T}}\right) $ can be referenced in \cite{luo2021abstraction}, with details being omitted here due to space constraints.
%     \item For every state $ q_B $ in the Büchi automaton, combine it with $ \mathbf{x}^{\text {new}} $ to obtain the state $ q_{P}^{\text {new}}=\left(\mathbf{x}^{\text {new}}, q_B\right) $. For each node $ q_{P}^{\text {near }}=(\mathbf{x}^{\text{near}},q_B^{\text{near}}) $ in $ \mathcal{Q}_{P}^{\text {near }} $, if $ \mathbf{x}^{\text{near}}\rightarrow_T \mathbf{x}^{\text{new}} $ and $ \left(q_B^{\text {near }}, L\left(\mathbf{x}^{\text {near }}\right), q_B^{\text {new }}\right) \in \rightarrow_B $ hold, then select $ q_{P}^{\text {near}} $ as a potential parent node for $ q_{P}^{\text {new}} $. Calculate $ \operatorname{Cost}(q_{P}^{\text {new }}) $ with $ q_{P}^{\text {near}} $ as the parent node, defined as $ \operatorname{Cost}(q_{P}^{\text {new }})=\operatorname{Cost}(q_{P}^{\text {near}})+C(q_{P}^{\text {near}},q_{P}^{\text {new}}) $. From all potential parent nodes, select the one minimizing $ \operatorname{Cost}(q_{P}^{\text {new}}) $ (denoted as $ q_{P}^{\text {min}} $) as $ q_{P}^{\text {new}} $'s parent node, and draw an edge between them, completing the addition of node $ q_{P}^{\text {new}} $.
%     \item Upon adding $ q_{P}^{\text {new}} $ to the search tree, evaluate every node $ q_{P}^{\text {near}} $ in $ \mathcal{Q}_{P}^{\text {near}} $ to see if $ \operatorname{Cost}(q_{P}^{\text {near}}) > \operatorname{Cost}(q_{P}^{\text {new}}) + C(q_{P}^{\text {new}},q_{P}^{\text {near}}) $. If true, sever the connection of $ q_{P}^{\text {near}} $ from its parent node and set its parent to $ q_{P}^{\text {new}} $.
%     \item The construction of search tree $ \mathcal{T} $ wraps up after $ n_\mathrm{max} $ iterations, where $ n_\mathrm{max} $ is user-specified. For every goal state $ q_P^{\text{goal}} $ in $ \mathcal{V}_{\mathcal{T}} \cap \mathcal{Q}_{\text {goal}} $ within the tree, the projection of the path between it and the root node $ q_P^0 $ on $ \mathcal{W} $ represents a viable prefix path.
% \end{enumerate}


\subsection{Sampling Strategies} 
In the construction of random trees, it remains to specify how state $\x^{\text{rand}}$ is sampled ``randomly".  
In \cite{luo2021abstraction}, the authors proposed two different sampling strategies for $\x^{\text{rand}}$: 
\begin{itemize}
    \item 
    \emph{Uniform Sampling: } 
    $\x^{\text{rand}}$ is selected according to a uniform distribution   on $\W_\text{free}$ 
    (in fact,  any distribution  as long as all states has non-zero probability);
    \item 
    \emph{Biased Sampling: }  
    $\x^{\text{rand}}$ is selected according to a biased distribution on $\W_\text{free}$
    such that one has more chance to move towards an accepting state in $B$. 
\end{itemize}
Since our NN-guided approach is related to the biased sampling, we briefly review this method. 
First, one needs to pre-process the NBA $B$ so that infeasible transitions are removed. 
Then based on the simplified NBA, 
one defines a distance function $\rho: \mathcal{Q}_B \times \mathcal{Q}_B \rightarrow \mathbb{N}$ to capture the length of the shortest path between each pair of states. 
Then the selection of $\x^{\text{rand}}$ is determined as follows:
\begin{enumerate}
    \item[S-1] 
    Select a \emph{feasible accepting state} $q_B^{F,\mathrm{feas}}\in\Q_B^F$ such that $\rho(q_B^0,q_B^{F,\mathrm{feas}})\neq \infty $ and $\rho(q_B^{F,\mathrm{feas}},q_B^{F,\mathrm{feas}})\neq \infty$;
    \item[S-2] 
    Define the set of vertices 
    $\mathcal{D}_\mathrm{min}\subseteq \mathcal{V}_{\mathcal{T}}$ that are closest to $q_B^{F,\mathrm{feas}}$  according the distance function $\rho$.  
    Then select a vertex 
    $q_{P}^{\mathrm {closest}}=\left(\mathbf{x}^{\mathrm {closest }}, q_{B}^{\mathrm {closest }}\right)\in \mathcal{V}_{\mathcal{T}}$ from the tree 
    according to a specific  distribution \cite{luo2021abstraction} such that states in $\mathcal{D}_\mathrm{min}$ has more chance to be selected;
    \item[S-3] 
    Select two successive states $q_{B}^{\text{succ,1}}, q_{B}^{\text{succ,2}}\in \Q_B$   such that $q_{B}^{\text{closest}} 
    \!\!\xrightarrow{L\left(\mathbf{x}^{\text {closest }}\right)}_B\! \! q_{B}^{\text{succ},1}\! \to_{B}\! q_{B}^{\text{succ},2}$, and
    $\rho(q_{B}^{\text{succ},2},q_B^{\mathrm{feas}})\!\leq\! \rho(q_{B}^{\text{succ},1},q_B^{F,\mathrm{feas}}) \!\leq\!  \rho(q_{B}^{\text{closest}},q_B^{F,\mathrm{feas}})$;
    \item[S-4] 
    Select a state $ \mathbf{x}^\mathcal{L}$ 
    such that  $ q_{B}^{\text{succ,1}}  \xrightarrow{L(\mathbf{x}^\mathcal{L})}_B q_{B}^{\text{succ, 2}} $ is feasible;  
    \item[S-5] 
    Compute the shortest path from 
    $\mathbf{x}^\mathcal{L} $ and $ \mathbf{x}^{\mathrm {closest}} $ within $ \mathcal{W}_{\text{free}} $. 
    Pick the second point in the shortest path, 
    denoted by $ \mathbf{x}^{\mathrm {target}} $
    as a heuristic direction for sampling;  
    \item[S-6] 
    Finally, 
    select $\x^{\text{rand}}$ according to a distribution  that has more chance to sample towards the direction of $\x^{\text{target}}$.
\end{enumerate}

 

\section{Neural Network Guided Sampling}
%
% As we discussed in the previous section, in sampling-based LTL planning, one of the key factor is how each new state is sampled. 
Although biased sampling provides a more efficient approach compared with the uniform sampling,  it solely relies on the distance information in B\"{u}chi automaton.  
For example, when  $q_B^{F,\mathrm{feas}}$ 
as well as 
intermediate states
$q_{B}^{\text{succ,1}}$  and $q_{B}^{\text{succ,2}}$
are selected, one only consider 
whether or not the task progress can be pushed forward in the NBA. 
However,  the information from the workspace, i.e., whether the task progress is feasible physically, is neglected.

To further improve the sample efficiency for the random tree construction,  one essentially needs to \emph{jointly} consider the information workspace and the NBA in order to have more chance to sample states that can move towards accepting states \emph{by paths that are feasible in the workspace}.  
However, obtaining such a good heuristic is very challenging since the workspace is continuous.  In this section, we present a new neural network guided (NN-guided) sampling strategy,  where a ``sample net" is used that effectively fuses the information of the workspace and the NBA.  
All implementation details as well as source codes are available at \url{https://github.com/LRJ-2000/NNgTL} 

 

% To harness the full potential of information from the workspace and the NBA, we propose leveraging neural networks. These networks are designed to extract features from both domains, aiming to predict the optimal path's probability distribution in the workspace and its associated state sequence in the NBA. By integrating these neural network predictions, we seek to refine our sampling strategy, striving for greater algorithmic efficiency.
\begin{figure*}[htbp]
    \centering
    \includegraphics[width=17cm]{contents/model2.pdf}
    \caption{Overview of the sampling network.\vspace{-10pt}}
    \label{fig:model}
\end{figure*}

\subsection{Overview of  NN-Guided Approach}
%
\subsubsection{Purposes of Network Networks}
The main architecture of our sample net is shown in Figure~\ref{fig:model}  consisting of two sub-networks:  the Path Prediction Network ({PathNet}) and the State Prediction Network ({StateNet}). 
The inputs of the  {PathNet} and the  {StateNet} are the same, which are both the workspace map as well as the NBA for the LTL task. 
However, their purposes and outputs are different. 
Specifically, 
\begin{itemize}
    \item 
    % The output of the  {StateNet} is a subset of 
    % NBA states $\hat{Q}_B\subseteq {Q}_B$. 
    % Intuitively,  {StateNet} is a classifier  
    % such that   $\hat{Q}_B$ is classified as the set of states in the NBA that are maybe involved in the optimal path. 
    % The predicted state set $\hat{Q}_B$ is used to restrict the choices of 
    % $q_B^{F,\text{feas}},q_{B}^{\text{succ,1}}, q_{B}^{\text{succ,2}}\in \Q_B$ in the biased sampling. \XY{do you need to change this part?}
    
    The output of the {StateNet} is a vector $\mathbf{p}$ with a length of $\left | \mathcal{Q}_B \right |$. In this vector, each entry $p_i$ denotes the probability that state $i$ is involved in the optimal path. The prediction vector $\mathbf{p}$ is employed to guide the choices of $q_B^{F,\text{feas}},q_{B}^{\text{succ,1}}, q_{B}^{\text{succ,2}}\in \Q_B$ in the biased sampling.
    
    \item 
    The output of the  {PathNet} is a 
    $200\times 200$ matrix $\mathcal{P}$ 
    such that the value of each entry represents the likelihood that the entry is on the optimal path. 
    Therefore, this weight matrix $\mathcal{P}$  is used 
    as a more reasonable metric for sampling $\x^{\text{rand}}$ by considering the workspace information with preforming shortest path search. 
\end{itemize}


\subsubsection{NN-Guided Sampling Strategy}
Now, let us discuss how the proposed neural networks are used to guide the sampling process.
It still follows the basic idea of biased sampling method as detailed in steps S1-S6. 
However,  we further leverage the outputs of the two sub-networks to improve and simply the sampling process. Specifically,  at each instant, suppose that the output of the  {StateNet} and the  {PathNet} are $\mathbf{p}$ and $\mathcal{P}$. 
We set  $\alpha\in (0,1)$ as a parameter that specifies the probability of using the predicted information of  {StateNet} to guide the sampling. 
Then, to determine the sample point $\x^{\text{rand}}$, our approach makes the following changes C-1 and C-2 to steps S-1 to S-6.  
 
C-1: When selecting $q_B^{F,\mathrm{feas}}$, $q_{B}^{\mathrm {closest}}$, $q_{B}^{\text{succ,1}}$ 
    as in steps S1-S3 in the biased sampling,  
    there is a $1-\alpha$ probability that we still follow exactly the same strategy in S-1 to S-3. 
    However, there is an $\alpha$ probability that  
    all these states selected according to the probability vector $\mathbf{p}$.  In other words, we have $\alpha$ probability to activate the prediction result of the  {StateNet}. 


C-2:  After obtaining state $\mathbf{x}^\mathcal{L}$ in step S-4, to sample state $\x^{\text{rand}}$,  we simplify steps S-5 and S-6 as a single step. 
    Particularly, instead of first computing the shortest path and then using the second point in the path to generate a sample distribution, here we directly use 
    the prediction result $\mathcal{P}$ by the  {PathNet} to sample $\x^{\text{rand}}$. 
    More specifically, let $(x_1,y_1)$ and $(x_2,y_2)$ be the coordinations of $\mathbf{x}^\mathcal{L}$ and $\mathbf{x}^{\mathrm {closest}}$, respectively. 
    We consider the rectangle region 
    $\textsc{Rec}=[x_1:x_2,y_1:y_2]$.  
    We define a discrete distribution over 
    all grids in $\textsc{Rec}$ according to the normalized 
    value of their weights in $\mathcal{P}$, i.e., 
    grids with larger value has more chance to be selected. 
    Then  $\x^{\text{rand}}$ is sampled randomly from the rectangle region according to this distribution.  

% This approach of combining the predictive outcomes of neural networks with heuristic sampling strategies can effectively utilize the information from both the workspace and NBA, enhancing the quality of sampling and thereby improving the search speed. Simultaneously, it can minimize the uncertainties introduced by the neural networks.

Here, we discuss the main features of the purposed NN-guided sampling strategy. 
First, our NN-guided approach subsumes all properties, such as probabilistic completeness and  asymptotic optimality,  of the TL-RRT* algorithm in \cite{luo2021abstraction} since we still follow the main structure of TL-RRT* and at each step, our algorithm has a non-zero probability to switch to the original sampling strategy. However, compared with the biased sampling strategy adopted in \cite{luo2021abstraction}, our NN-guided sampling strategy further jointly considers both the workspace information and the NBA, which provides a better heuristic for ``good" samples. 
Furthermore, since our strategy uses the predicted distribution directly without involving the shorstest path search for each step, its online execution is also much faster that the biased sampling strategy. 

% By integrating the predictions of neural networks with heuristic sampling strategies, we effectively harness information from both the workspace and NBA. This fusion not only elevates the sampling quality, leading to faster search outcomes, but also curtails uncertainties inherent to neural networks.

\subsection{Inputs Encodings}\label{encoding} 
%
Recall that, for both the  {PathNet} and the  {StateNet}, their inputs are the workspace map and the NBA for the LTL formula.  
To leverage neural networks for processing the workspace with continuous space and NBA with graph structure, appropriate encoding techniques are needed. 

\subsubsection{Encoding for Workspace}
First, we consider the continuous workspace as a $200\times 200$ pixel image or a grid map.  
Each grid in the image corresponds to a specific point in the workspace, which is labeled, obstacle or free.  
Then  the image is  transformed into a tensor of dimensions $(m+1)\times 200 \times 200$ with $m$ be the number of different labels, i.e.,  each grid in the workspace is encoded as a vector $\mathbf{a}=[a_0,a_1,...,a_m]$. 
Specifically,  the first entry $a_0$ represents the grid's status, where  $-1$ for the initial location, $0$ for free space, and $1$ for an obstacle. 
For $i=1,\dots,m$,  we  have  $a_i=1$ if it belongs to $\mathcal{R}_i$, and  $a_i=0$ otherwise.

% The encoding technique for the NBA is described below:
% \begin{enumerate}
%     \item Represent the NBA as a directed graph, where the states and transitions in the NBA correspond to the nodes and edges of the graph respectively. The initial features of a node are given as $v=[v_1,v_2,v_3]$. If the node corresponds to an initial state, then $v_1=1$, otherwise $v_1=0$; if the node corresponds to a feasible accepting state, then $v_2=1$, otherwise $v_2=0$. The value $v_3$ represents the distance between the node's corresponding state and its nearest feasible accepting state, with all distances normalized. If a node cannot reach any feasible accepting state, then $v_3=-1$. The initial features of an edge are given as $e=[e_1,e_2,...,e_T]$, representing the conditions that need to be met for the corresponding transition in the NBA. Specifically, if a transition requires the label $\ell_i$ to be true, then the corresponding $e_i=1$; If it requires $\neg \ell_i$ to be true, then $e_i=-1$; If there is no requirement for $\ell_i$, then $e_i=0$.
%     \item To better utilize GNN for edge feature processing, we transform the directed graph into a heterogeneous graph. In this approach, we insert a new node within each edge of the original graph, thereby transferring the edge's features to this new node. To achieve superior feature aggregation and propagation effects, we also add a self-loop to each node and introduce a pooling node, connecting a directed edge from all nodes to this pooling node.
% \end{enumerate}
\subsubsection{Encoding for B\"{u}chi Automata} 
First, we convert NBA to a directed graph, where nodes and edges correspond to states and transitions, respectively, and have their features. 
Specifically, the feature for a node is a vector  $\mathbf{v}=[v_1,v_2,v_3]$, 
where 
$v_1\in \{0,1\}$ represents whether or not it is an initial state, 
$v_2\in \{0,1\}$ represents whether or not it is an feasible accepting state, and 
$v_3$ is the (normalized) distance to the closest feasible accepting state. 
For each edge, the feature is a vector $\mathbf{e}=[e_1,e_2,...,e_m]\in \{-1,0,1\}^m$ specifying the atomic propositions that need to be true for the underlying transition in the NBA.  
% signifying the prerequisites for the NBA's corresponding transition. For instance, a transition demanding label $\ell_i$ to be true means $e_i=1$. If it necessitates $\neg \ell_i$ to be true, then $e_i=-1$, and if $\ell_i$ is irrelevant, $e_i=0$.  
Since later on we   use graph neural networks (GNN) to process features of the NBA,  we  further transform the directed graph into a heterogeneous graph. 
This transformation involves adding a new node within each  original edge  so that the features of the edges are inherited by the nodes added. 
Additionally, to augment feature aggregation and spread,  a self-loop is added to each node, and a pooling node is added so that each node has a directed edge leading to this pooling node.



\subsection{Implementation Details of Neural Networks}\label{subsection_network}
%
% In this subsection, we detail how the  {PathNet} and the  {StateNet} are implemented. 

 
\subsubsection{PathNet}  It has the following four building blocks. 


\textbf{Map Encoder:} The purpose is to extract features from the grid map by five convolutional blocks. Each block houses a $4\times 4$ convolutional layer with a stride of $2$ and padding of $1$, complemented by a batch-norm layer, a dropout layer with probability $0.5$, and a LeakyReLU activation with a negative slope of $0.2$. Note that the sizes of the map evolves from $m \times 200 \times 200$ to $1024 \times 6 \times 6$ when passing through these blocks.  

\textbf{NBA Encoder:} 
The purpose is to extract  global features from the NBA. Comprising five layers, the encoder utilizes Graph Attention (GAT) convolutions  to address distinct edge types in the heterogeneous graph\cite{velickovic2017graph}. The node  features are proceeded by a dropout layer and a ReLU activation after convolutions. 
Finally, global mean pooling operations  are used to accumulate feature representation of the entire graph.

\textbf{Fusion Network: }
The purpose is to amalgamate features from both the workspace Map Encoder and the NBA Encoder. 
This is done by the following two steps. First, NBA features are transformed via a linear layer to attain compatibility with map features. 
Then vector concatenation are used to fuse  these harmonized features.

\textbf{Path Predictor: }
The purpose is to output the weight matrix $\mathcal{P}\in \mathbb{R}^{200\times 200}$ as the prediction for optimal paths.  
To this end, we use five up-convolution blocks to upscale and to refine the amalgamated features.
Each block is structured with a transposed convolutional layer, a batch-norm layer, a dropout layer (with probability $0.5$), and a ReLU activation. 
Drawing from the ``U-Net" architecture \cite{ronneberger2015u}, our design integrates skip connections, merging features from both the third convolutional modules of the Map and NBA Encoders. This approach capitalizes on the synergy of both encoders, enhancing the merged feature representation. Subsequent to this fusion, features are relayed to the Path Predictor via concatenation. Leveraging these connections ensures the retention of intricate spatial details alongside the depth of hierarchical features. 
Finally,  we use an $1\times1$ convolution to reshape the features to $1\times200\times200$ dimensions, and a sigmoid activation is used to refine the output.  
% The PathNet mainly consists of four components: the Map Encoder, the NBA Encoder, the Fusion Network, and the Prediction Network. The roles and configurations of these elements are detailed below:

% \textbf{Map Encoder} is designed to extract features from the grid map. It contains five convolutional blocks. Each block consists of a $4\times 4$ convolutional layer with a stride of 2 and padding of 1, a batch-norm layer, a dropout layer with probability 0.5, and a LeakyReLU activation with a negative slope of 0.2. As the input map traverses these blocks, its spatial dimensions reduce while the depth increases, transitioning from an initial size of $T \times 200 \times 200$ to a final size of $1024 \times 6 \times 6$.

% \textbf{NBA Encoder} is responsible for extracting global features from the NBA. It is structured with five layers, each employing a Graph Attention (GAT) convolution designed to process different edge types in the heterogeneous graph. Following each layer, the features of nodes are passed through a dropout layer and a ReLU activation function, enhancing generalization and introducing non-linearity. After the convolutional layers, a global mean pooling operation is applied to aggregate global information, thereby obtaining a feature representation of the entire graph structure, which is used for subsequent prediction.

% \textbf{Fusion Network} is designed to integrate features from Map Encoder and NBA Encoder. To ensure compatibility and effective integration, the network first passes the NBA features through a linear layer, adjusting its size to match that of the map features. Subsequently, the two feature sets are fused through vector concatenation.

% \textbf{Prediction Network} is responsible for predicting the probability distribution of the optimal path based on the fused features, and its output is a $1\times200\times200$ matrix, where each element represents the probability of the optimal path passing through the corresponding grid. The network employs five up-convolution blocks, aiming to upscale and refine the fused feature maps. Each up-convolution block comprises a transposed convolutional layer, also known as a deconvolution layer, followed by a batch-norm layer, a dropout layer with probability 0.5, and concludes with a ReLU activation function. Inspired by the classic image segmentation network ``U-Net'' \cite{ronneberger2015u}, we introduced skip connections into our network to ensure better feature integration and retention of high-resolution details. Specifically, we fused the output features from the third convolutional module of our Map Encoder with those from the third convolutional module of the NBA Encoder. This fusion allows us to capture complementary information from both encoders, enriching the combined representation. After achieving this fusion, we feed the merged features into the Prediction Network through feature concatenation. By incorporating these skip connections and concatenating features, our network effectively retains fine-grained spatial details while also harnessing the depth of hierarchical features, enhancing the overall accuracy and robustness of our optimal path prediction. The final layer of the Prediction Network is a $1\times1$ convolution, which projects the features into the size of $1\times200\times200$. Finally, the output undergoes a sigmoid activation, which maps the raw output values into the range between 0 and 1. This transformation ensures that the network's output is a probability distribution that can be directly used in the following process.



% The StateNet mainly consists of two components: the Map Encoder and the Node Classifier. Compared to PathNet, the structure of StateNet is more straightforward. Initially, the Map Encoder is used to encode the map into a feature vector of length 256. Subsequently, this feature vector is concatenated with the initial features of all nodes corresponding to the NBA. Finally, the classification of nodes is accomplished by the Node Classifier, predicting whether a state is in the state sequence corresponding to the optimal path. The detailed structure of these components are as follows:

% \textbf{Map Encoder} begins by employing a $1\times 1$ convolutional layer to transform the input from 8 channels to 3 channels, making it compatible with traditional image processing models. Subsequently, the features undergo a pre-trained ``ResNet-50'' model\cite{he2016deep}, a renowned deep learning model known for its efficacy in image recognition. To tailor the output to our specific needs, we excluded the final fully connected layer of the ResNet model and introduced our own, converting the ResNet output to a feature vector of length 256.

% \textbf{Node Classifier} is specifically designed for node classification tasks. Initially, the network employs a GAT convolutional layer to expand the node features of the graph to a length of 256, matching the dimension of the map features. Following this, features of each node are concatenated with the feature vector of the map generated by the Map Encoder, thus fusing spatial and structural information at each node. The network then engages in a series of information propagation steps through five successive GAT modules. Each of these modules consists of a GAT convolutional layer, a ReLU activation function for introducing non-linearity, and a dropout layer with a probability of 0.5 for regularization. To finalize the classification task, the network employs two consecutive fully connected layers that process the integrated features for each node and output the classification results.

\subsubsection{StateNet} 
This net is essentially a classifier for the NBA states. It has a simpler structure   consisting of the following two components. 

%  The Map Encoder, The latter, leveraging the output from the Map Encoder, classifies nodes to determine if a state is part of the state sequence corresponding to the optimal path. The architectures of these components are detailed below:

\textbf{Map Encoder: } 
The main purpose is to encode the map into a $256$-length feature vector, which will be served as a precursor to the Node Predictor. 
Specifically, the map is processed by an $1\times 1$ convolution, transitioning the $8$-channel input to $3$ channels, thus aligning with conventional image processing frameworks.  The features then engage with the pre-trained ``ResNet-50'' model \cite{he2016deep}. 
The terminal fully connected layer of the ResNet is omitted, and is replaced by our bespoke fully connected layer, rendering the output as a $256$-length feature vector.

\textbf{Node Predictor}, tailored for node classification, starts with a GAT convolution layer, stretching the graph's node features to a 256-length dimension, in line with the map features. Each node's features are subsequently concatenated with the Map Encoder-generated map feature vector, amalgamating spatial and structural data at every node. A sequence of information dissemination follows via five sequential GAT modules, each housing a GAT convolution, a ReLU activation for non-linearity, and a dropout (with probability $0.5$) for regularization. The classification culminates with two sequential fully connected layers and a Softmax layer, analyzing the consolidated node features to yield the classification probability.


\subsection{Training Neural Networks}\label{subsection_training}
% Before training, we randomly generated 15400 sets of workspace and LTL expressions as the training and testing data set. To ensure the generated workspace meets the requirements from \ref{encoding}, we directly generated a $200 \times 200$ grid map as the workspace. Two types of random obstacles were set, as shown in figure \ref{fig:sub1} and figure \ref{fig:sub2}. Subsequently, we randomly selected seven $3 \times 3$ regions in the free regions to serve as different label regions. Finally, the robot's starting position was chosen at random. The complete workspace is presented in figure \ref{fig:sub3}. To utilize the expert algorithm for generating the expert path, we transformed the grid map into its corresponding continuous workspace through coordinate mapping. For each generated workspace and LTL expression, we employed the heuristic sampling-based planning algorithm discussed previously to devise a plan. We used the path obtained after 10,000 iterations of the algorithm as the expert path. Subsequently, we encoded the expert path in the workspace into a $200 \times 200$ 0-1 matrix. Grids traversed by the expert path, along with their eight surrounding grids, have a value of 1, with the remainder set to 0. Similarly, we encoded the expert path in the NBA as 0-1 labels for the nodes. Finally, we employed data augmentation techniques to expand the data to 107800 groups.

\subsubsection{Data Set Preparations}
Initially, we randomly generate $15400$ pairs of workspace and LTL formulae.  
Specifically, in each $200 \times 200$ grid map workspace, we randomly place obstacles as well as seven distinct labeled regions. The initial location of the robot is also randomized. Note that grid map are only used for the  purpose of map generation, it is still mapped to and used as  continuous workspace. 
To order to obtain an expert path for each pair of workspace and LTL task, 
we use the existing biased-sampling approach  with $10,000$ iterations. 
The obtained expert path is then encoded into a $200 \times 200$ binary matrix. 
Specifically, we mark those grids crossed by the expert path, as well as their immediate neighbors, as $1$. Then we label NBA states visited by the expert path as $1$. Finally, through data augmentations, this data set is expanded to $107800$ cases.


% . In line with the requirements from \ref{encoding}, a $200 \times 200$ grid map was directly generated to represent the workspace. This workspace incorporated two forms of random obstacles, visualized in figure \ref{fig:sub1} and figure \ref{fig:sub2}. Next, seven distinct label regions were designated by randomly selecting $3 \times 3$ sections within free areas. The robot's start position was also randomized, with the entire workspace depicted in figure \ref{fig:sub3}. 




% \begin{figure}[htbp]
%     \centering
%     \begin{subfigure}[b]{0.3\columnwidth}
%         \includegraphics[width=\linewidth]{contents/obs2.png}
%         \caption{obstacle type 1}
%         \label{fig:sub1}
%     \end{subfigure}
%     \hfill
%     \begin{subfigure}[b]{0.3\columnwidth}
%         \includegraphics[width=\linewidth]{contents/obs3.png}
%         \caption{obstacle type 2}
%         \label{fig:sub2}
%     \end{subfigure}
%     \hfill
%     \begin{subfigure}[b]{0.3\columnwidth}
%         \includegraphics[width=\linewidth]{contents/workspace.png}
%         \caption{workspace}
%         \label{fig:sub3}
%     \end{subfigure}
%     \caption{Overview of obstacle types and workspace}
%     \label{fig:main}
% \end{figure}
\subsubsection{Training Procedures}  
The training process started  with training the  {StateNet} first.
Specifically, we  first fixed  the parameters of the ResNet portion and only update the parameters of the other parts. 
When the loss became stable after 100 epochs, we unfroze the parameters of the ResNet and continued  training for another 20 epochs. 
The trainings were performed by the Adam optimizer with an initial learning rate of $0.001$ and a batch size of $128$. 
We used  cross entropy loss as the loss function. 
After training the StateNet, we trained the PathNet. 
Specifically, we  first initialized the GAT layers in the NBA Encoder using the parameters from  the GAT layers in StateNet. 
After training for 150 epochs, the loss stabilized. 
We still used the Adam optimizer with an initial learning rate of $0.0001$ and a batch size of $128$. 
We employed  the binary cross entropy loss as the loss function.
 
%  \begin{figure*}[htbp]
%     \centering
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred1_1.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred1_2.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred1_3.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred1_4.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred2_1.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred2_2.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred2_3.png}
%     \end{subfigure}%
%     \begin{subfigure}{0.125\textwidth}
%         \includegraphics[width=\linewidth]{contents/pred2_4.png}
%     \end{subfigure}
%     \caption{Prediction results of PathNet and the corresponding expert path}
%     \label{fig:test_results}
% \end{figure*}
 
%  After the training was completed, we tested the performance of PathNet and StateNet on the test set. Figure \ref{fig:test_results} shows the prediction results of PathNet (first row) in comparison with the corresponding expert path (second row). It can be observed that the predictions from PathNet effectively reflect the distribution of the expert path. We also evaluated the classification performance of StateNet. The average accuracy reached 0.9245, the average precision reached 0.8871, the average recall reached 0.9258, the average F1 score reached 0.8938, and the average AUC was 0.8804. These test results suggest that both networks perform as expected, and their predictions can be used to guide the sampling process.

% \subsubsection{Evaluations}  
% After the training was completed, we evaluated PathNet and StateNet on our test dataset. PathNet's predictions, depicted in the first row of Figure \ref{fig:test_results}, closely mirrored the expert path shown in the second row. StateNet's classification performance yielded an average accuracy of 0.9245, precision of 0.8871, recall of 0.9258, F1 score of 0.8938, and AUC of 0.8804. These results underscore the networks' efficacy, indicating their suitability for guiding the sampling strategy.

 




\section{Simulations \& Numerical Experiments}
In this section, we provide simulation results for the proposed method. 
First, a case study is provided to illustrate our approach. 
Then we perform a set of numerical experiments to evaluate the efficiency of our approach compared with existing sampling strategies. 
All algorithms were implemented using \texttt{Python} on a Windows 11 computer with an Intel Core i7-13700K 5.40GHz processor. \vspace{-3pt}
 

\subsection{Case Study}
We consider a robot moving in a workspace shown in Figure~\ref{fig:path} with initial position of the robot, obstacles, and labeled regions as depicted in the figure.  
We consider the following LTL task for the robot\vspace{-3pt}
\[
\phi=\square \Diamond l_1 \wedge \neg l_1 \mathcal{U} l_2 \wedge \Diamond l_3, \vspace{-3pt}
\]
i.e., the robot needs to (i) visit $l_2$ at least once without visiting $l_1$; (ii) visit $l_3$ at least once; (iii) visit $l_1$ infinitely often. 
The NBA of $\phi$ is shown in Figure~\ref{fig:nba}, where state $4$ is the unique feasible accepting state.  
The optimal plan searched by our algorithm is shown as the red lines in Figure~\ref{fig:path}. 
The robot first goes to $l_2$, then hoes to $l_3$, and finally stays at $l_1$. That is, only the prefix part contributes to the overall cost.

To better illustrate our NN-guided sampling strategy, we explain how the random tree $\mathcal{T}$ for the prefix path is expended initially from the root $q_P^0=(\mathbf{x}_0, q_B^{\mathrm{init}})$. 
Since the NBA only has one feasible accepting state, the choice for $q_B^{F,\mathrm{feas}}$ is unique, and we have $q_P^{\mathrm{closest}}=q_P^0$ since the tree only has a root so far. 
Then the StateNet predicts $\mathbf{p}=\left[0999,0.486,0.902,0.994,0.997\right]$.  
Since $0 \!\!\xrightarrow{L\left(\mathbf{x}_{0}\right)}_B\! \! 0$, we have  $q_{B}^{\text{succ,1}}=0$. From the feasible successor states of $q_{B}^{\text{succ,1}}$, we choose $q_{B}^{\text{succ},2}=2$ since it has a higher probability (0.902) than state $1$ (0.486).
% From  the intersection of $\hat{Q}_B$  and the successor states of $q_{B}^{\text{succ},1}$, 
% we choose $q_{B}^{\text{succ},2}=2$.
Then according to the transition condition $0\xrightarrow{l_2}_B2$ in the NBA, 
we select a point in the labeled region $l_2$ as $\mathbf{x}^{\mathcal{L}}$, which is shown as the yellow point in Figure~\ref{fig:case_study}.  
Then we construct the rectangle region between $\mathbf{x}^{\mathcal{L}}$ and $\mathbf{x}^{\mathrm{closest}}$, 
and state $\mathbf{x}^{\mathrm{rand}}$ is sampled randomly according to the distribution determined by  the PathNet prediction $\mathcal{P}$  as shown in Figrue~\ref{fig:prob}.  

Note  that, in this example, there are actually two feasible prefix paths: $l_2 \to l_3 \to l_1$ and $l_3 \to l_2 \to l_1$. 
Clearly, the former is optimal with less cost.  
This information is captured by the prediction result of the StateNet, which prefers state $2\in \Q_B$ for the optimal path. 
Furthermore,  the prediction  result of the PathNet can effectively avoid obstacles and has more chance to sample near the optimal path.  
Therefore, these prediction results by the neural networks guide our search process to converge to a desired solution more quickly.\vspace{-16pt}
\begin{figure}  
    \centering 
        \includegraphics[width=3.5cm]{contents/path3.pdf}
        \caption{Workspace of the robot, where  the gray regions denote obstacles, 
        the green regions denote labeled regions, and the red lines denote the optimal path synthesized.}
        \label{fig:path}
\end{figure}


\begin{figure} 
    \begin{subfigure}{0.4\columnwidth}
    \centering  
        \includegraphics[width=3cm]{contents/prob1.pdf}
        \caption{Output of PathNet.}
        \label{fig:prob}
    \end{subfigure} 
    \quad 
    \begin{subfigure}{0.6\columnwidth}
    \centering  
        % \includegraphics[width=3cm]{contents/NBA1.pdf}
        \resizebox{1.0\linewidth}{!}{
            \input{contents/NBA}
        }
        \caption{Output of  StateNet.}
        \label{fig:nba}
    \end{subfigure}
    \caption{Predication results of the neural networks. }
    \label{fig:case_study}
\end{figure}
 
\subsection{Comparison with Existing Methods}

\subsubsection{Experiment Settings} 
We conduct a set of experiments to illustrate the efficiency of our NN-guided sampling strategy  compared with the existing uniform and biased sampling strategies. 
Specifically, 
independent from the training set, we generate another $240$ pairs of workspace map  and LTL task. 
For each instance, we run our method with $\alpha = 0.8$ as well as the two existing method to find a feasible plan. 
Note that, since all these RRT-based approaches are probabilistic optimal, 
we focus on comparing \emph{how fast} these strategies can find \emph{the first feasible solution}, and the performance of the first feasible solution in terms of its length. 
Formally, we consider the following metrics when   the first feasible solution is found: 
the execution time $T$ taken, 
the number of iterations $n$ required, 
the number of nodes $m$ in the random tree, and 
the length of the first feasible solution $len$. 
 

\subsubsection{Statistic Results}
The numerical experiments results are shown in Table~\ref{table}. 
Specifically, based on the execution time $T$ of the uniform sampling approach, we divide the tasks into  simple tasks  with $T\leq \SI{180}{\second}$  and complex tasks with $T>\SI{180}{\second}$.
Then Tables \ref{table_simple} and   \ref{table_complex} show the average value of  each metric for each algorithm within these two task categories, respectively.  
Note that many complex tasks, 
the uniform sampling strategy fails to find a feasible path within \SI{2000}{\second}. For such  cases, we terminate the search by only recording  $T,n$ and $m$ without consider the length $len$.

\begin{table} 
    \centering
    \small % 减小字体大小
    \caption{Experiment Results}
    \begin{subtable}[t]{0.45\textwidth}
        \centering
        \caption{Statistic Results for Simple Tasks\vspace{-6pt}}
        \begin{tabular}{|c|c|c|c|c|}
            \hline
            Method  & $T(\SI{}{\second})$ & $n$ & $len$ & $m$\\
            \hline
            Uniform    & 54.2475 & 1908.13  & \textbf{0.78789} & 3167.63 \\
            \hline
            Biased    & 1.03305  & 101.000 & 0.80842 & 200.307 \\
            \hline
            NN-Guided  & \textbf{0.09518} & \textbf{22.8941} & 0.90546 & \textbf{48.1395} \\
            \hline
        \end{tabular}
        \label{table_simple}
    \end{subtable}
    
     \vspace{0.1cm} % 两个子表格之间的垂直间距,可以根据需要调整

    \begin{subtable}[t]{0.45\textwidth}
        \centering
        \caption{Statistic Results for Complex Tasks\vspace{-6pt}}
        \begin{tabular}{|c|c|c|c|c|}
            \hline
            Method  & $T(\SI{}{\second})$ & $n$ & $len$ & $m$\\
            \hline
            Uniform     & 1401.78 & 7401.27  & - & 21501.2 \\
            \hline
            Biased    & 15.5639  & 321.553 & \textbf{1.08553} & 704.082 \\
            \hline
            NN-Guided  & \textbf{2.19490} & \textbf{44.8549} & 1.12555 & \textbf{182.743} \\
            \hline
        \end{tabular}
        \label{table_complex}
    \end{subtable}\label{table}
\end{table}

The statistic results show that, for both simple and complex tasks, our NN-guided sampling strategy can  significantly enhance the  efficiency of the RRT-based algorithm.
In particular, 
the timed required to obtain a feasible solution by our NN-guided sampling strategy  
is  less than 15\% of that of the biased sampling strategy, which is already much more efficient than uniform sampling strategy. 
Furthermore, the length of the first feasible solution found by our strategy is similar to those of the other two strategies. 
We would like the remark that the metric of $len$ is not essential compared with other metrics since this is just the performance of the first feasible solution. 
The entire algorithm will converge to the optimal solution when the number of iterations increases. 


% In simple tasks, the time required to obtain an initial solution is less than 10\% of that taken by the algorithm based on heuristic sampling, and the required iteration count is approximately 20\%. In complex tasks, both the execution time and the number of iterations are less than 15\% of that taken by the algorithm based on heuristic sampling. 

% Additionally, we observed that the length of the initial feasible path found by the algorithm based on the neural network-guided sampling strategy is slightly longer than that of the other two algorithms. The primary reason for this is the notably fewer number of nodes added to the search tree compared to the other two methods, resulting in a decrease in the representation precision of the search tree. Consequently, this leads to a marginally longer path, but it remains within an acceptable range.

 


\section{Conclusion}
%
In this paper, building upon the current state-of-the-art sampling-based LTL planning algorithms, we propose a novel sampling strategy based on multi-modal neural networks to guide the sampling process.  
Our approach, on the one hand, leverages the feature extraction power of neural networks in an end-to-end fashion, 
and on the other hand, still enjoys all good properties of the sampling-based methods such as probabilistic optimality/completeness. 
Experimental results show that our proposed sampling strategy can significantly enhance the planning efficiency of the algorithm. 
In future research, we will further improve the feature fusion methods  for multi-robot planning problems.

\newpage 

\bibliographystyle{IEEEtran}
\bibliography{references}{}



\end{document}

% !TEX root = ../root.tex

\section{Introduction}
With the ongoing development and widespread deployment of mobile robots, there has been an increasing focus on path planning for high-level tasks. Among the formal languages used for specifying such complex tasks, Linear Temporal Logic (LTL) stands out as a widely adopted choice. LTL provides a structured means for the users to articulate complex  requirements, such as navigating a robot to a target region without collision with obstacles or ensuring specific locations are visited infinitely often \cite{guo2018probabilistic,cai2022learning,luo2022temporal,yu2022security}. In recent years, the field of robot path planning for LTL tasks has witnessed extensive investigation,  spurred by its broad  applications. These applications encompass a wide range of scenarios, such as environmental surveillance \cite{smith2011optimal}, search and rescue missions \cite{plaku2016motion}, and   intelligent warehousing systems \cite{yang2019formal,scher2020warehouse}.

In the context of LTL path planning,  one of the most foundational methods is the automata-theoretical approach  based on finite abstractions  \cite{smith2011optimal,guo2015multi,kloetzer2009automatic,shi2022path,ulusoy2014optimal}. 
This approach involves the creation of a discrete abstraction of the workspace, which effectively captures the robot's mobility constraints. Subsequently, the discrete abstraction is synchronized with an automaton representation of the LTL task. This synchronization enables the formulation of the planning problem as a graph-search problem within the product space.
% For instance, in \cite{ulusoy2014optimal}, the emphasis lies on addressing the issues of optimality and robustness within the planned paths. Similarly,   in \cite{guo2015multi} the authors propose a framework that allows for plan reconfiguration based on real-time information, enhancing adaptability.
However, this graph-search approach, although conceptually powerful, faces a significant computational challenge. In particular, as the system's dimensionality increases, the state-space of the finite abstraction grows exponentially, rendering the graph-search problem infeasible.

Sampling-based methods, such as rapid random trees (RRT), have emerged as a promising solution to tackle the computational challenges associated with path planning in continuous state-spaces  \cite{karaman2011sampling}. More recently,   sampling-based algorithms have been introduced to enhance the computational efficiency of solving LTL planning problems \cite{karaman2012sampling,vasile2013sampling,kantaros2018sampling,kantaros2020stylus,luo2021abstraction}.
For example,  in \cite{kantaros2018sampling}, a sampling-based algorithm, inspired by the RRT*, is proposed to find optimal paths that satisfy LTL tasks with a prefix-suffix structure. This  algorithm circumvents the necessity of explicitly exploring the entire state-space by incrementally constructing random trees over the product state-space. Building upon this advancement,  \cite{kantaros2020stylus} further introduces a biased sampling strategy that leverages automata information to significantly improve sample efficiency. Moreover, in  \cite{luo2021abstraction}, the authors extend the methods in \cite{kantaros2020stylus} to continuous workspaces without discretization. Specifically, they introduce an abstraction-free planning algorithm that directly samples within a continuous space and integrates these samples with automata states.


 


% To address this scalability concern, various sampling-based planning algorithms have emerged \cite{karaman2012sampling,vasile2013sampling,kantaros2015intermittent,kantaros2018sampling,kantaros2020stylus,luo2021abstraction}. In \cite{karaman2012sampling}, a sampling-based algorithm is introduced for deterministic $\mu$-calculus tasks. This method incrementally constructs a Kripke structure, akin to the rapidly exploring random graph (RRG), and utilizes the rapidly exploring random tree star (RRT*) to derive the optimal plan. \cite{vasile2013sampling} offers 
% a sampling-based temporal logic path planning algorithm that uses RRG for transition system construction and graph search techniques on the product automaton for optimal path determination. Kantaros and Zavlanos, in \cite{kantaros2015intermittent}, put forth an RRT*-based temporal logic planning algorithm. This approach, rather than fully constructing a product automaton, samples within the transition system, merging it with NBA states. It incrementally crafts a search tree symbolizing the product automaton and ensures path optimality from the tree's root to all nodes. This method's efficiency in tackling complex problems, such as intricate LTL expressions or multi-robot tasks, stems from bypassing the need for graph search algorithms on the product automaton. Building on this, \cite{kantaros2020stylus} introduces a heuristic sampling strategy, boosting the algorithm's convergence rates. However, both algorithms necessitate prior discrete abstraction modeling for the transition system. \cite{luo2021abstraction} presents an abstraction-free planning algorithm that directly samples transition system states in a continuous space and merges them with NBA states. While it employs heuristic sampling strategies to heighten feasible plan construction efficiency, the simultaneous planning in both the transition system and NBA makes these manually-designed strategies inefficient, often failing to harness information from both domains and adding significant computational overhead.
In sampling-based LTL planning, one of the key factor is how each new state is sampled.  While biased sampling strategies offer an enhanced approach compared to uniform sampling, they primarily rely on distance information within the B\"{u}chi automaton. This approach neglects valuable insights from the workspace, such as the physical feasibility of task progression. However, integrating continuous workspace information with the B\"{u}chi automaton  is very challenging  due to the inherently heterogeneous structures of these components. Recently, there has been a notable 
progress in leveraging the power of neural networks for expediting solutions to intricate problems. For instance, within the domain of path planning, neural networks have been employed to predict the probability distribution of optimal paths  \cite{ichter2018learning,wang2020neural,ma2021conditional,qureshi2020motion}. Moreover, neural networks have been applied, in an end-to-end fashion, for generating solutions to temporal logic tasks  \cite{liu2021recurrent,hashimoto2022stl2vec,cai2021modular,aloor2023follow}. 

In this paper, we introduce a novel neural-network guided (NN-guided) sampling strategy designed specifically for LTL planning. Our approach builds upon the basic architecture of the sampling-based algorithm   for continuous workspaces, as established in \cite{luo2021abstraction}. However, instead of relying solely on automata information, we incorporate a multi-modal neural network capable of jointly extracting features from both the workspace and the B\"{u}chi automaton. This neural network offers predictive capabilities to steer the sampling process in directions that are more likely to yield optimal solutions, ones that are not only task-progressive but also feasible within the workspace. 
To demonstrate the efficiency of our approach, 
we compare the proposed NN-guided sampling strategy with existing sampling strategies on a set of randomly generated problem instances. 
The statistical results underscore the effectiveness of our new strategy, as it requires less than 15\% of the time needed by the existing strategies to find a feasible solution.



% In this work, we propose a novel neural-network guided (NN-guided) sampling strategy tailored for LTL planning.  Specifically, we still follow the basic structure of the sampling-based algorithm for continuous workspace as developed in \cite{luo2021abstraction}. 
% However, instead of solely replying on the automata information,  we further employ a multi-modal neural network to extract features jointly from both the workspace and the B\"{u}chi automaton.  This neural network provides predictions to guide the sampling process toward more optimal directions, which is more likely to be both task-progressive and workspace-feasible. 
% To illustrate the efficiency of our approach, we compare the proposed NN-gudied sampling strategy with existing sampling strategies on a set of randomly generated problem instances. 
% The statistic result shows that, to find a feasible solution, our new strategy only requires less than 20% of time of the existing strategies.   


%   Inspired by these studies, in this paper, we propose a neural network-guided sampling strategy based on the work presented in \cite{luo2021abstraction}. We utilize multi-modal neural networks to end-to-end predict the probability distribution of optimal paths in the workspace as well as the corresponding NBA state sequences and use them to guide the sampling process of the RRT* planning algorithm.  
% Compared to the heuristic sampling strategy employed in \cite{luo2021abstraction}, our neural network-guided sampling strategy can fully harness information from both the workspace and NBA. With reduced computational overhead and improved sampling quality, it can significantly enhance the efficiency of the RRT* planning algorithm. To the best of our knowledge, we are the first to combine multi-modal networks with sampling-based planning algorithms to address temporal logic planning problems.


\begin{tikzpicture}[->,>={Latex}, thick, initial text={}, node distance=2cm, initial where=above, thick, base node/.style={circle, draw, minimum size=5mm, font=\normalsize}]		
	%		\draw[help lines] (0,0) grid [step=.5] (3,7);
	\node[state, base node, ] (0) at (0,0) {$0$}; 
	\node[below=of 0, xshift=0.05cm, yshift = 1.92cm] {\fontsize{10}{1} $0.999$};
	\node[state, base node, ](1) at (1.5,1.5) {$1$};
	\node[right=of 1, xshift=-2.2cm, yshift = 0cm] {\fontsize{10}{1} $0.486$};
	\node[state, base node, ](2) at (1.5,-1.5) {$2$};
	\node[right=of 2, xshift=-2.2cm, yshift = 0cm] {\fontsize{10}{1} $0.902$};
	\node[state, base node, ](3) at (2.7,0) {$3$};
	\node[below=of 3, xshift=0cm, yshift = 1.9cm] {\fontsize{10}{1} $0.994$};
	\node[state, accepting, base node, ](4) at (4.3,0) {$4$};
	\node[below=of 4, xshift=-0.1cm, yshift = 2cm] {\fontsize{10}{1} $0.997$};
	
	\path[]
	(0) edge node [right, xshift=-0.3cm, yshift=-0.2cm] {\fontsize{10}{1} $\neg l_1 \wedge l_3$} (1)
	(0) edge [loop above, looseness=8] node {\fontsize{10}{1} $\neg l_1$} (0)
	(1) edge [loop left, looseness=8] node {\fontsize{10}{1} $\neg l_1$} (1)
	(2) edge [loop left, looseness=8] node {\fontsize{10}{1} $1$} (2)
	(3) edge [loop above, looseness=8] node {\fontsize{10}{1} $1$} (3)
	(4) edge [loop above, looseness=8] node {\fontsize{10}{1} $l_1$} (4)
	(0) edge node [right, xshift=-0.2cm, yshift=0.12cm] {\fontsize{10}{1} $l_2$} (2)
	(0) edge node [below] {\fontsize{10}{1} $l_2\wedge l_3$} (3)
	(1) edge node [right, xshift=-0.2cm, yshift=0.2cm] {\fontsize{10}{1} $l_2$} (3)
	(2) edge node [right, xshift=-0.2cm, yshift=-0.2cm] {\fontsize{10}{1} $l_3$} (3)
	(3) edge node [above] {\fontsize{10}{1} $l_1$} (4)
	(4) edge [bend left=40] node [below] {\fontsize{10}{1} $1$} (3)
	;
	
\end{tikzpicture}
% 	(1) edge node [right, xshift=-0.2cm, yshift=0.15cm] {\fontsize{10}{1} $u \backslash\! \{o_1\}$} (4)
% 	(2) edge[bend right] node [left, xshift=0.1cm] {\fontsize{10}{1} $a\! \backslash\! \{o_1,o_2\} $} (3)
% 	(3) edge[bend right] node [below, xshift=0.3cm, yshift=-0.3cm] {\fontsize{10}{1} $b\! \backslash\! \{o_2\} $} (2)
% 	(4) edge[bend left] node [right, xshift=-0.1cm] {\fontsize{10}{1} $a\! \backslash\! \{o_1\} $} (5)
% 	(5) edge[bend left] node [above, xshift=-0.4cm, yshift=0.3cm] {\fontsize{10}{1} $b\! \backslash\! \{o_2\} $} (4);

% \[
% \phi::=\text{true} \mid  \pi\in \mathcal{A P}\mid   \neg \phi  \mid \phi_1 \wedge \phi_2  \mid   \phi_1  \mathcal{U}   \phi_2, 
% \]
% Generated by IEEEtran.bst, version: 1.14 (2015/08/26)
\begin{thebibliography}{10}
\providecommand{\url}[1]{#1}
\csname url@samestyle\endcsname
\providecommand{\newblock}{\relax}
\providecommand{\bibinfo}[2]{#2}
\providecommand{\BIBentrySTDinterwordspacing}{\spaceskip=0pt\relax}
\providecommand{\BIBentryALTinterwordstretchfactor}{4}
\providecommand{\BIBentryALTinterwordspacing}{\spaceskip=\fontdimen2\font plus
\BIBentryALTinterwordstretchfactor\fontdimen3\font minus
  \fontdimen4\font\relax}
\providecommand{\BIBforeignlanguage}[2]{{%
\expandafter\ifx\csname l@#1\endcsname\relax
\typeout{** WARNING: IEEEtran.bst: No hyphenation pattern has been}%
\typeout{** loaded for the language `#1'. Using the pattern for}%
\typeout{** the default language instead.}%
\else
\language=\csname l@#1\endcsname
\fi
#2}}
\providecommand{\BIBdecl}{\relax}
\BIBdecl

\bibitem{guo2018probabilistic}
M.~Guo and M.~M. Zavlanos, ``Probabilistic motion planning under temporal tasks
  and soft constraints,'' \emph{IEEE Transactions on Automatic Control},
  vol.~63, no.~12, pp. 4051--4066, 2018.

\bibitem{cai2022learning}
M.~Cai, H.~Peng, Z.~Li, and Z.~Kan, ``Learning-based probabilistic ltl motion
  planning with environment and motion uncertainties,'' \emph{IEEE Transactions
  on Automatic Control}, vol.~66, no.~5, pp. 2386--2392, 2022.

\bibitem{luo2022temporal}
X.~Luo and M.~M. Zavlanos, ``Temporal logic task allocation in heterogeneous
  multirobot systems,'' \emph{IEEE Transactions on Robotics}, vol.~38, no.~6,
  pp. 3602--3621, 2022.

\bibitem{yu2022security}
X.~Yu, X.~Yin, S.~Li, and Z.~Li, ``Security-preserving multi-agent coordination
  for complex temporal logic tasks,'' \emph{Control Engineering Practice}, vol.
  123, p. 105130, 2022.

\bibitem{smith2011optimal}
S.~L. Smith, J.~T{\u u}mov{\'a}, C.~Belta, and D.~Rus, ``Optimal path planning
  for surveillance with temporal-logic constraints,'' \emph{The International
  Journal of Robotics Research}, vol.~30, no.~14, pp. 1695--1708, 2011.

\bibitem{plaku2016motion}
E.~Plaku and S.~Karaman, ``Motion planning with temporal-logic specifications:
  Progress and challenges,'' \emph{AI Communications}, vol.~29, no.~1, pp.
  151--162, 2016.

\bibitem{yang2019formal}
Y.~Yang, J.~Zhao, X.~Yin, and S.~Li, ``Formal synthesis of warehouse robotic
  systems with temporal logic specifications,'' in \emph{IEEE Conference on
  Robotics, Automation and Mechatronics}, 2019, pp. 469--474.

\bibitem{scher2020warehouse}
G.~Scher and H.~Kress-Gazit, ``Warehouse automation in a day: from model to
  implementation with provable guarantees,'' in \emph{IEEE International
  Conference on Automation Science and Engineering}, 2020, pp. 280--287.

\bibitem{guo2015multi}
M.~Guo and D.~V. Dimarogonas, ``Multi-agent plan reconfiguration under local
  ltl specifications,'' \emph{The International Journal of Robotics Research},
  vol.~34, no.~2, pp. 218--235, 2015.

\bibitem{kloetzer2009automatic}
M.~Kloetzer and C.~Belta, ``Automatic deployment of distributed teams of robots
  from temporal logic motion specifications,'' \emph{IEEE Transactions on
  Robotics}, vol.~26, no.~1, pp. 48--61, 2009.

\bibitem{shi2022path}
W.~Shi, Z.~He, W.~Tang, W.~Liu, and Z.~Ma, ``Path planning of multi-robot
  systems with {B}oolean specifications based on simulated annealing,''
  \emph{IEEE Robotics and Automation Letters}, vol.~7, no.~3, pp. 6091--6098,
  2022.

\bibitem{ulusoy2014optimal}
A.~Ulusoy, S.~L. Smith, and C.~Belta, ``Optimal multi-robot path planning with
  ltl constraints: guaranteeing correctness through synchronization,'' in
  \emph{Distributed Autonomous Robotic Systems: The 11th International
  Symposium}, 2014, pp. 337--351.

\bibitem{karaman2011sampling}
S.~Karaman and E.~Frazzoli, ``Sampling-based algorithms for optimal motion
  planning,'' \emph{The International Journal of Robotics Research}, vol.~30,
  no.~7, pp. 846--894, 2011.

\bibitem{karaman2012sampling}
------, ``Sampling-based algorithms for optimal motion planning with
  deterministic $\mu$-calculus specifications,'' in \emph{American Control
  Conference}, 2012, pp. 735--742.

\bibitem{vasile2013sampling}
C.~I. Vasile and C.~Belta, ``Sampling-based temporal logic path planning,'' in
  \emph{International Conference on Intelligent Robots and Systems}, 2013, pp.
  4817--4822.

\bibitem{kantaros2018sampling}
Y.~Kantaros and M.~M. Zavlanos, ``Sampling-based optimal control synthesis for
  multirobot systems under global temporal tasks,'' \emph{IEEE Transactions on
  Automatic Control}, vol.~64, no.~5, pp. 1916--1931, 2018.

\bibitem{kantaros2020stylus}
------, ``Stylus*: A temporal logic optimal control synthesis algorithm for
  large-scale multi-robot systems,'' \emph{The International Journal of
  Robotics Research}, vol.~39, no.~7, pp. 812--836, 2020.

\bibitem{luo2021abstraction}
X.~Luo, Y.~Kantaros, and M.~M. Zavlanos, ``An abstraction-free method for
  multirobot temporal logic optimal control synthesis,'' \emph{IEEE
  Transactions on Robotics}, vol.~37, no.~5, pp. 1487--1507, 2021.

\bibitem{ichter2018learning}
B.~Ichter, J.~Harrison, and M.~Pavone, ``Learning sampling distributions for
  robot motion planning,'' in \emph{IEEE International Conference on Robotics
  and Automation}, 2018, pp. 7087--7094.

\bibitem{wang2020neural}
J.~Wang, W.~Chi, C.~Li, C.~Wang, and M.~Q.-H. Meng, ``Neural rrt*:
  Learning-based optimal path planning,'' \emph{IEEE Transactions on Automation
  Science and Engineering}, vol.~17, no.~4, pp. 1748--1758, 2020.

\bibitem{ma2021conditional}
N.~Ma, J.~Wang, J.~Liu, and M.~Q.-H. Meng, ``Conditional generative adversarial
  networks for optimal path planning,'' \emph{IEEE Transactions on Cognitive
  and Developmental Systems}, vol.~14, no.~2, pp. 662--671, 2021.

\bibitem{qureshi2020motion}
A.~H. Qureshi, Y.~Miao, A.~Simeonov, and M.~C. Yip, ``Motion planning networks:
  Bridging the gap between learning-based and classical motion planners,''
  \emph{IEEE Transactions on Robotics}, vol.~37, no.~1, pp. 48--66, 2020.

\bibitem{liu2021recurrent}
W.~Liu, N.~Mehdipour, and C.~Belta, ``Recurrent neural network controllers for
  signal temporal logic specifications subject to safety constraints,''
  \emph{IEEE Control Systems Letters}, vol.~6, pp. 91--96, 2021.

\bibitem{hashimoto2022stl2vec}
W.~Hashimoto, K.~Hashimoto, and S.~Takai, ``Stl2vec: Signal temporal logic
  embeddings for control synthesis with recurrent neural networks,'' \emph{IEEE
  Robotics and Automation Letters}, vol.~7, no.~2, pp. 5246--5253, 2022.

\bibitem{cai2021modular}
M.~Cai, M.~Hasanbeig, S.~Xiao, A.~Abate, and Z.~Kan, ``Modular deep
  reinforcement learning for continuous motion planning with temporal logic,''
  \emph{IEEE Robotics and Automation Letters}, vol.~6, no.~4, pp. 7973--7980,
  2021.

\bibitem{aloor2023follow}
J.~J. Aloor, J.~Patrikar, P.~Kapoor, J.~Oh, and S.~Scherer, ``Follow the rules:
  Online signal temporal logic tree search for guided imitation learning in
  stochastic domains,'' in \emph{IEEE International Conference on Robotics and
  Automation}, 2023, pp. 1320--1326.

\bibitem{kloetzer2008fully}
M.~Kloetzer and C.~Belta, ``A fully automated framework for control of linear
  systems from temporal logic specifications,'' \emph{IEEE Transactions on
  Automatic Control}, vol.~53, no.~1, pp. 287--297, 2008.

\bibitem{baier2008principles}
C.~Baier and J.-P. Katoen, \emph{Principles of model checking}.\hskip 1em plus
  0.5em minus 0.4em\relax MIT press, 2008.

\bibitem{velickovic2017graph}
P.~Velickovic, G.~Cucurull, A.~Casanova, A.~Romero, P.~Lio, Y.~Bengio
  \emph{et~al.}, ``Graph attention networks,'' \emph{Stat}, vol. 1050, no.~20,
  pp. 10--48\,550, 2017.

\bibitem{ronneberger2015u}
O.~Ronneberger, P.~Fischer, and T.~Brox, ``U-net: Convolutional networks for
  biomedical image segmentation,'' in \emph{Medical Image Computing and
  Computer-Assisted Intervention}, 2015.

\bibitem{he2016deep}
K.~He, X.~Zhang, S.~Ren, and J.~Sun, ``Deep residual learning for image
  recognition,'' in \emph{IEEE Conference on Computer Vision and Pattern
  Recognition}, 2016, pp. 770--778.

\end{thebibliography}