Sampling-Based Optimal Control Synthesis for Multi-Robot Systems under Global Temporal Tasks

TL;DR

This paper introduces a scalable, sampling-based optimal control synthesis algorithm for multi-robot systems with global temporal logic tasks, capable of handling extremely large state spaces efficiently.

Contribution

A novel sampling-based algorithm that constructs incrementally trees to approximate the product automaton, reducing memory use and increasing scalability for multi-robot planning.

Findings

Handles product automata with billions of states.

Proves probabilistic completeness and asymptotic optimality.

Outperforms existing methods in large-scale scenarios.

Abstract

This paper proposes a new optimal control synthesis algorithm for multi-robot systems under global temporal logic tasks. Existing planning approaches under global temporal goals rely on graph search techniques applied to a product automaton constructed among the robots. In this paper, we propose a new sampling-based algorithm that builds incrementally trees that approximate the state-space and transitions of the synchronous product automaton. By approximating the product automaton by a tree rather than representing it explicitly, we require much fewer memory resources to store it and motion plans can be found by tracing sequences of parent nodes without the need for sophisticated graph search methods. This significantly increases the scalability of our algorithm compared to existing optimal control synthesis methods. We also show that the proposed algorithm is probabilistically complete and asymptotically optimal. Finally, we present numerical experiments showing that our approach can synthesize optimal plans from product automata with billions of states, which is not possible using standard optimal control synthesis algorithms or off-the-shelf model checkers.

Equations

$$\hat{J}(\tau )=\sum _{k=1}^{|\tau |-1}{w}_{\text{PTS}}(\tau (k),\tau (k+1)).$$

$$J(\tau )=\hat{J}({\tau }^{\text{pre}})+\hat{J}({\tau }^{\text{suf}}),$$

$$\text{Cost}(q_P)=\hat{J}({\tau }_T),$$

$${\mathcal{X}}_{\text{goal}}^{\text{pre}}=\{q_P=(q_{\text{PTS}},q_B)\in {\mathcal{Q}}_P|q_B\in {\mathcal{Q}}_B^F\}.$$

$$f_{\text{rand}}(q_P|{\mathcal{V}}_T)=\{\begin{array}{ll}\frac{1}{|{\mathcal{V}}_T|},& \text{mbox}if{q}_P\in {\mathcal{V}}_T,\\ 0,& \text{mbox}otherwise.\end{array}$$

$${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})=\{q_{\text{PTS}}\in {\mathcal{Q}}_{\text{PTS}}|q_{\text{PTS}}^{\text{rand}}{\to }_{\text{PTS}}{q}_{\text{PTS}}\}$$

$${\mathcal{R}}_{{\mathcal{V}}_T}^{\to }(q_P^{\text{new}})=\{q_P\in {\mathcal{V}}_T|q_P{\to }_P{q}_P^{\text{new}}\},$$

$$q_P^{\text{prev}}=$$

$${\text{argmin}}_{q_P\in {\mathcal{R}}_{{\mathcal{V}}_T}^{\to }(q_P^{\text{new}})}[\text{Cost}(q_P)+w_{\text{PTS}}(\Pi {|}_{\text{PTS}}{q}_P,\Pi {|}_{\text{PTS}}{q}_P^{\text{new}})],$$

$$\text{Cost}(q_P^{\text{new}})=$$

$$+\underset{\text{cost of reaching qPnew from qPprev}}{\underbrace{w_{\text{PTS}}(\Pi {|}_{\text{PTS}}{q}_P^{\text{prev}},\Pi {|}_{\text{PTS}}{q}_P^{\text{new}})}},$$

$${\mathcal{R}}_{{\mathcal{V}}_T}^{\leftarrow }(q_P^{\text{new}})=\{q_P\in {\mathcal{V}}_T|q_P^{\text{new}}{\to }_P{q}_P\},$$

$$\mathcal{S}(q_P)=$$

$$\text{a multi hop path in}{\mathcal{G}}_T\},$$

$${\mathcal{X}}_{\text{goal}}^{\text{suf}}(q_P^r)=$$

$$(q_P,L(q_{\text{PTS}}),q_P^r)\in {\to }_P\},$$

$${\mathcal{R}}_P(q_P)=\{q_P^{\prime }\in {\mathcal{Q}}_P|q_P{\to }_P{q}_P^{\prime }\},$$

$$\underset{k\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{R}}_P(q_P^{\text{rand},n})\subseteq {\mathcal{V}}_T^{n+k}\}\right)=1,$$

$$\underset{n\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{R}}_P(q_P)\subseteq {\mathcal{V}}_T^n\}\right)=1,$$

$$\underset{n\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{V}}_T^n\cap {\mathcal{X}}_{\text{goal}}\ne \varnothing \}\right)=1,$$

$${\mathcal{R}}_P^{\infty }(q_P^r)={\cup }_{m=1}^{\infty }{\mathcal{R}}_P^m(q_P^r),$$

$$\underset{n\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{R}}_P^{\infty }(q_P^r)={\mathcal{V}}_T^n\}\right)=1.$$

$$\mathbb{P}\left(\left\{\underset{n_{\text{max}}^{\text{pre}}\to \infty ,n_{\text{max}}^{\text{suf}}\to \infty }{\lim }J(\tau )=J^{\ast }\right\}\right)=1,$$

$${\text{Cost}}^{m\bar{n}}(q_P)>{\text{Cost}}^{m\bar{n}+1}(q_P)>\cdots >{\text{Cost}}^{m\bar{n}+K}(q_P),$$

$$\mathbb{P}(A^{\text{rand},n+k}(q_P))=f_{\text{rand}}(q_P|{\mathcal{V}}_T^{n+k})\ge f_{\text{rand}}(q_P|{\mathcal{Q}}_P),$$

$$\sum _{k=0}^{\infty }\mathbb{P}(A^{\text{rand},n+k}(q_P))\ge \sum _{k=0}^{\infty }{f}_{\text{rand}}(q_P|{\mathcal{Q}}_P).$$

$$\sum _{k=0}^{\infty }\mathbb{P}(A^{\text{rand},n+k}(q_P))=\infty .$$

$$\underset{k\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{R}}_P(q_P^{\text{rand},n})\subseteq {\mathcal{V}}_T^{n+k}\}\right)=1,$$

$$\underset{k\to \infty }{\lim }\mathbb{P}\left(\{{\mathcal{R}}_P(q_P)\subseteq {\mathcal{V}}_T^{n+k}\}\right)=1,\forall q_P\in {\mathcal{V}}_T^n.$$

Full text

I Introduction

Robot motion planning is a fundamental problem that has received considerable research attraction [1]. The basic motion planning problem consists of generating robot trajectories that reach a desired goal region starting from an initial configuration while avoiding obstacles. More recently, a new class of planning approaches have been developed that can handle a richer class of tasks than the classical point-to-point navigation, and can capture temporal and boolean specifications. Such tasks can be, e.g., sequencing or coverage [2], data gathering [3], intermittent communication [4], or persistent surveillance [5], and can be modeled using formal languages, such as Linear Temporal Logic (LTL) [6, 7], that are developed in concurrency theory. Given a task described by a formal language, model checking algorithms can be employed to synthesize correct-by-construction controllers that satisfy the assigned tasks.

Control synthesis for mobile robots under complex tasks, captured by Linear Temporal Logic (LTL) formulas, build upon either bottom-up approaches when independent LTL expressions are assigned to robots [8, 9, 10] or top-down approaches when a global LTL formula describing a collaborative task is assigned to a team of robots [11, 12], as in this work. Common in the above works is that they rely on model checking theory [6, 7] to find paths that satisfy LTL-specified tasks, without optimizing task performance. Optimal control synthesis under local and global LTL specifications has been addressed in [13, 14] and [15, 16, 17], respectively. In top-down approaches [15, 16, 17], optimal discrete plans are derived for every robot using the individual transition systems that capture robot mobility and a Non-deterministic B$\ddot{\text{u}}$chi Automaton (NBA) that represents the global LTL specification. Specifically, by taking the synchronous product among the transition systems and the NBA, a synchronous product automaton can be constructed. Then, representing the latter automaton as a graph and using graph-search techniques, optimal motion plans can be derived that satisfy the global LTL specification and optimize a cost function. As the number of robots or the size of the NBA increases, the state-space of the product automaton grows exponentially and, as a result, graph-search techniques become intractable. Consequently, these motion planning algorithms scale poorly with the number of robots and the complexity of the assigned task.

To mitigate these issues, we propose an optimal control synthesis algorithm for multi-robot systems under global temporal specifications that avoids the explicit construction of the product among the transition systems and the NBA. Motivated by the $\text{RRT}^{*}$ algorithm [18], we build incrementally through a B$\ddot{\text{u}}$chi-guided sampling-based algorithm directed trees that approximately represent the state-space and transitions among states of the synchronous product automaton. Specifically, first a tree is built until a path from an initial to an accepting state is constructed. This path corresponds to the prefix part of the motion plan and is executed once. Then, a new tree rooted at an accepting state is constructed in a similar way until a cycle-detection method discovers a loop around the root. This cyclic path corresponds to the suffix part of the motion plan and is executed indefinitely. The advantage of the proposed method is that approximating the product automaton by a tree rather than representing it explicitly by an arbitrary graph, as existing works do, results in significant savings in resources both in terms of memory to save the associated data structures and in terms of computational cost in applying graph search techniques. In this way, our proposed model-checking algorithm scales much better compared to existing top-down approaches. Also, we show that the proposed LTL-based planning algorithm is probabilistically complete and asymptotically optimal. We present numerical simulations that show that the proposed approach can synthesize optimal motion plans from product automata with billions of states, which is impossible using existing optimal control synthesis algorithms or the off-the-shelf symbolic model checkers PRISM [19] and NuSMV [20].

To the best of our knowledge, the most relevant works are presented in [21, 22, 23, 24]. In [21], a sampling-based algorithm is proposed which builds incrementally a Kripke structure until it is expressive enough to generate a motion plan that satisfies a task specification expressed in deterministic $\mu$-calculus. Specifically, in [21], since control synthesis from $\omega$-regular languages requires cyclic patterns, an RRG-like algorithm is employed to construct a Kripke structure. However, building arbitrary graph structures to represent transition systems, compromises scalability of temporal logic planning methods since, as the number of samples increases, so does the density of the constructed graph increasing in this way the required resources to save the associated structure and search for optimal plans using graph search methods. Therefore, the algorithm proposed in [21] can be typically used only for single-robot motion planning problems in simple environments and for LTL tasks associated with small NBA. Motivated by this limitation, in [22], a sampling-based temporal logic path planning algorithm is proposed, that also builds upon the RRG algorithm, but constructs incrementally sparse graphs representing transition systems that are then used to construct a product automaton. Then, correct-by-construction discrete plans are synthesized applying graph search methods on the product automaton. However, similar to [21], as the number of samples increases, the sparsity of the constructed graph is lost and as a result this method does not scale well to large planning problems either. Common in the works [21, 22] is that a discrete abstraction of the environment is built until it becomes expressive enough to generate a motion plan that satisfies the LTL specification. To the contrary, our proposed sampling-based approach, given a discrete abstraction of the environment [25, 26, 27, 28, 29], builds trees, instead of arbitrary graphs, to approximate the product automaton. Therefore, it is more economical in terms of memory requirements and does not require the application of expensive graph search techniques to find the optimal motion plan, but instead it tracks sequences of parent nodes starting from desired accepting states. In this way, we can handle more complex planning problems with more robots and LTL tasks that correspond to larger NBA, compared to the ones that can be solved using the approach in [22]. Moreover, we show that our proposed planning algorithm is asymptotically optimal which is not the case in [22].

In our previous work [23, 24], we have proposed sampling-based planning algorithms for multi-robot systems under global temporal logic tasks. Specifically, [23] transforms given transition systems that abstract robot mobility into trace-included transition systems with smaller state-spaces that are still rich enough to construct motion plans that satisfy the global LTL specification. However, this algorithm does not scale well with the number of robots, since it relies on the construction of a product automaton among all agents. A more tractable and memory-efficient approach is proposed in [24] that builds trees incrementally, similar to the approach proposed here, that approximate the product automaton. Here, we extend the work in [24] by improving the sampling process of the algorithm so that samples are drawn among the sets of nodes that are reachable from the current tree rather than drawn arbitrarily from the state-space of the product automaton, as in [24]. Since the state-space of the product automaton can be arbitrarily large drawing samples randomly can result in very slow growth of the tree, since these samples are not necessarily reachable from the current tree, as we show through numerical experiments. As in [24], here too we show that the proposed algorithm is probabilistically complete and asymptotically optimal. Nevertheless, the completeness and optimality proofs are entirely different due to the different sampling process. To the best of our knowledge, this is the first optimal control synthesis algorithm for global temporal task specifications that is probabilistically complete, asymptotically optimal, and scalable, as it is resource efficient both in terms of memory requirements and computational time.

The rest of the paper is organized as follows. In Section II, we provide a brief overview of LTL and in Section III we present the problem formulation. In Section IV we describe our proposed sampling-based planning algorithm and we examine its correctness and optimality in Section V. Numerical experiments are presented in Section VI.

II Preliminaries

In this section we formally describe Linear Temporal Logic (LTL) by presenting its syntax and semantics. Also, we briefly review preliminaries of automata-based LTL model checking. A detailed overview of this theory can be found in [6].

Linear temporal logic is a type of formal logic whose basic ingredients are a set of atomic propositions $\mathcal{AP}$, the boolean operators, i.e., conjunction $\wedge$, and negation $\neg$, and two temporal operators, next $\bigcirc$ and until $\mathcal{U}$. LTL formulas over a set $\mathcal{AP}$ can be constructed based on the following grammar: $\phi::=\text{true}~{}|~{}\pi~{}|~{}\phi_{1}\wedge\phi_{2}~{}|~{}\neg\phi~{}|~{}\bigcirc\phi~{}|~{}\phi_{1}~{}\mathcal{U}~{}\phi_{2}$, where $\pi\in\mathcal{AP}$. For the sake of brevity we abstain from presenting the derivations of other Boolean and temporal operators, e.g., always $\square$, eventually $\lozenge$, implication $\Rightarrow$, which can be found in [6].

An infinite word $\sigma$ over the alphabet $2^{\mathcal{AP}}$ is defined as an infinite sequence $\sigma=\pi_{0}\pi_{1}\pi_{2}\dots\in(2^{\mathcal{AP}})^{\omega}$, where $\omega$ denotes an infinite repetition and $\pi_{k}\in 2^{\mathcal{AP}}$, $\forall k\in\mathbb{N}$. The language $\texttt{Words}(\phi)=\left\{\sigma\in(2^{\mathcal{AP}})^{\omega}|\sigma\models\phi\right\}$ is defined as the set of words that satisfy the LTL formula $\phi$, where $\models\subseteq(2^{\mathcal{AP}})^{\omega}\times\phi$ is the satisfaction relation.

Any LTL formula $\phi$ can be translated into a Nondeterministic B$\ddot{\text{u}}$chi Automaton (NBA) over $(2^{\mathcal{AP}})^{\omega}$ denoted by $B$ [30], which is defined as follows:

Definition II.1

A Nondeterministic B$\ddot{\text{u}}$chi Automaton (NBA) $B$ over $2^{\mathcal{AP}}$ is defined as a tuple $B=\left({\mathcal{Q}}_{B},{\mathcal{Q}}_{B}^{0},\Sigma,\rightarrow_{B},\mathcal{Q}_{B}^{F}\right)$, where ${\mathcal{Q}}_{B}$ is the set of states, ${\mathcal{Q}}_{B}^{0}\subseteq{\mathcal{Q}}_{B}$ is a set of initial states, $\Sigma=2^{\mathcal{AP}}$ is an alphabet, $\rightarrow_{B}\subseteq{\mathcal{Q}}_{B}\times\Sigma\times{\mathcal{Q}}_{B}$ is the transition relation, and ${\mathcal{Q}}_{B}^{F}\subseteq{\mathcal{Q}}_{B}$ is a set of accepting/final states.

An infinite run $\rho_{B}$ of $B$ over an infinite word $\sigma=\pi_{0}\pi_{1}\pi_{2}\dots$, where $\pi_{k}\in\Sigma$, for all $k\in\mathbb{N}$, is a sequence $\rho_{B}=q_{B}^{0}q_{B}^{1}q_{B}^{2}\dots$ such that $q_{B}^{0}\in{\mathcal{Q}}_{B}^{0}$ and $(q_{B}^{k},\pi_{k},q_{B}^{k+1})\in\rightarrow_{B}$, $\forall k\in\mathbb{N}$. An infinite run $\rho_{B}$ is called accepting if $\texttt{Inf}(\rho_{B})\cap{\mathcal{Q}}_{B}^{F}\neq\varnothing$, where $\texttt{Inf}(\rho_{B})$ represents the set of states that appear in $\rho_{B}$ infinitely often. The words $\sigma$ that result in an accepting run of $B$ constitute the accepted language of $B$, denoted by ${\mathcal{L}}_{B}$. It is proven [6] that the accepted language of $B$ is equivalent to the words of $\phi$, i.e., ${\mathcal{L}}_{B}=\texttt{Words}(\phi)$.

III Problem Formulation

Consider $N$ mobile robots that evolve in a complex workspace $\mathcal{W}\subset\mathbb{R}^{d}$ according to the following dynamics: $\dot{\bf{x}}_{i}(t)=f_{i}({\bf{x}}_{i}(t),{\bf{u}}_{i}(t))$, where ${\bf{x}}_{i}(t)$ and ${\bf{u}}_{i}(t)$ are the position and the control input associated with robot $i$, $i\in\{1,\dots,N\}$. We assume that there are $W$ disjoint regions of interest in $\mathcal{W}$ that are worth investigation or surveillance. The $j$-th region is denoted by $\ell_{j}$ and it can be of any arbitrary shape. Given the robot dynamics, robot mobility in the workspace ${\mathcal{W}}$ can be represented by a weighted transition system (wTS) obtained through an abstraction process [25, 26, 27, 28, 29].The wTS for robot $i$ is defined as follows

Definition III.1** (wTS)**

A weighted Transition System (wTS) for robot $i$, denoted by $\text{wTS}_{i}$ is a tuple $\text{wTS}_{i}=\left(\mathcal{Q}_{i},q_{i}^{0},\rightarrow_{i},w_{i},\mathcal{AP}_{i},L_{i}\right)$ where: (a) $\mathcal{Q}_{i}=\bigcup_{j=1}^{W}\{q_{i}^{\ell_{j}}\}$ is the set of states, where a state $q_{i}^{\ell_{j}}$ indicates that robot $i$ is at location $\ell_{j}$; (b) $q_{i}^{0}\in\mathcal{Q}_{i}$ is the initial state of robot $i$; $\rightarrow_{i}\subseteq\mathcal{Q}_{i}\times\mathcal{Q}_{i}$ is the transition relation for robot $i$. Given the robot dynamics, if there is a control input ${\bf{u}}_{i}$ that can drive robot $i$ from location $\ell_{j}$ to $\ell_{e}$, then there is a transition from state $q_{i}^{\ell_{j}}$ to $q_{i}^{\ell_{e}}$ denoted by $(q_{i}^{\ell_{j}},q_{i}^{\ell_{e}})\in\rightarrow_{i}$; (c) $w_{i}:\mathcal{Q}_{i}\times\mathcal{Q}_{i}\rightarrow\mathbb{R}_{+}$111$\mathbb{R}_{+}$ and $\mathbb{N}_{+}$ stand for the positive real and natural numbers, respectively. is a cost function that assigns weights/cost to each possible transition in wTS. For example, such costs can be associated with the distance that needs to be traveled by robot $i$ in order to move from state $q_{i}^{\ell_{j}}$ to state $q_{i}^{\ell_{k}}$; (d) $\mathcal{AP}_{i}=\bigcup_{j=1}^{W}\{\pi_{i}^{\ell_{j}}\}$ is the set of atomic propositions, where $\pi_{i}^{\ell_{j}}$ is true if robot $i$ is inside region $\ell_{j}$ and false otherwise; and (e) $L_{i}:\mathcal{Q}_{i}\rightarrow 2^{\mathcal{AP}_{i}}$ is an observation/output relation giving the set of atomic propositions that are satisfied in a state, i.e., $L_{i}(q_{i}^{\ell_{j}})=\pi_{i}^{\ell_{j}}$.

Given the definition of the wTS, we can define the synchronous Product Transition System (PTS), which captures all the possible combinations of robots’ states in their respective $\text{wTS}_{i}$, as follows [6]:

Definition III.2** (PTS)**

Given $N$ transition systems $\text{wTS}_{i}=(\mathcal{Q}_{i},q_{i}^{0},\rightarrow_{i},w_{i},\mathcal{AP}_{i},L_{i})$, the product transition system $\text{PTS}=\text{wTS}_{1}\otimes\text{wTS}_{2}\otimes\dots\otimes\text{wTS}_{N}$ is a tuple $\text{PTS}=(\mathcal{Q}_{\text{PTS}},q_{\text{PTS}}^{0},\longrightarrow_{\text{PTS}},w_{\text{PTS}},\mathcal{AP},L_{\text{PTS}})$ where (a) $\mathcal{Q}_{\text{PTS}}=\mathcal{Q}_{1}\times\mathcal{Q}_{2}\times\dots\times\mathcal{Q}_{N}$ is the set of states; (b) $q_{\text{PTS}}^{0}=(q_{1}^{0},q_{2}^{0},\dots,q_{N}^{0})\in\mathcal{Q}_{\text{PTS}}$ is the initial state, (c) $\longrightarrow_{\text{PTS}}\subseteq\mathcal{Q}_{\text{PTS}}\times\mathcal{Q}_{\text{PTS}}$ is the transition relation defined by the rule222The notation of this rule is along the lines of the notation used in [6]. In particular, it means that if the proposition above the solid line is true, then so does the proposition below the solid line. $\frac{\bigwedge_{\forall i}\left(q_{i}\rightarrow_{i}q_{i}^{\prime}\right)}{q_{\text{PTS}}\rightarrow_{\text{PTS}}q_{\text{PTS}}^{\prime}}$, where with slight abuse of notation $q_{\text{PTS}}=(q_{1},\dots,q_{N})\in\mathcal{Q}_{\text{PTS}}$, $q_{i}\in\mathcal{Q}_{i}$. The state $q_{\text{PTS}}^{\prime}$ is defined accordingly. In words, this transition rule says that there exists a transition from $q_{\text{PTS}}$ to $q_{\text{PTS}}^{\prime}$ if there exists a transition from $q_{i}$ to $q_{i}^{\prime}$ for all $i\in\left\{1,\dots,N\right\}$; (d) $w_{\text{PTS}}:\mathcal{Q}_{\text{PTS}}\times\mathcal{Q}_{\text{PTS}}\rightarrow\mathbb{R}_{+}$ is a cost function that assigns weights/cost to each possible transition in PTS, defined as $w_{\text{PTS}}(q_{\text{PTS}},q_{\text{PTS}}^{\prime})=\sum_{i=1}^{N}w_{i}(\Pi|_{\text{wTS}_{i}}q_{\text{PTS}},\Pi|_{\text{wTS}_{i}}q_{\text{PTS}}^{{}^{\prime}})\geq 0$, where $q_{\text{PTS}}^{\prime},q_{\text{PTS}}\in\mathcal{Q}_{\text{PTS}}$, and $\Pi|_{\text{wTS}_{i}}q_{\text{PTS}}$ stands for the projection of state $q_{\text{PTS}}$ onto the state space of $\text{wTS}_{i}$. The state $\Pi|_{\text{wTS}_{i}}q_{\text{PTS}}\in\mathcal{Q}_{i}$ is obtained by removing all states in $q_{\text{PTS}}$ that do not belong to $\mathcal{Q}_{i}$; (e) $\mathcal{AP}=\bigcup_{i=1}^{N}\mathcal{AP}_{i}$ is the set of atomic propositions; and, (f) $L_{\text{PTS}}=\bigcup_{\forall i}L_{i}:\mathcal{Q}_{\text{PTS}}\rightarrow 2^{\mathcal{AP}}$ is an observation/output relation giving the set of atomic propositions that are satisfied at a state $q_{\text{PTS}}\in\mathcal{Q}_{\text{PTS}}$.

In what follows, we give definitions related to the PTS, that we will use throughout the rest of the paper. An infinite path $\tau$ of a PTS is an infinite sequence of states, $\tau=\tau(1)\tau(2)\tau(3)\dots$ such that $\tau(1)=q_{\text{PTS}}^{0}$, $\tau(k)\in\mathcal{Q}_{\text{PTS}}$, and $(\tau(k),\tau(k+1))\in\rightarrow_{\text{PTS}}$, $\forall k\in\mathbb{N}_{+}$, where $k$ is an index that points to the $k$-th entry of $\tau$ denoted by $\tau(k)$. A finite path of a PTS can be defined accordingly. The only difference with the infinite path is that a finite path is defined as a finite sequence of states of a PTS. Given the definition of the weights $w_{\text{PTS}}$ in Definition 2, the cost of a finite path $\tau$, denoted by $\hat{J}(\tau)$, can be defined as

[TABLE]

In (1), $|\tau|$ stands for the number of states in $\tau$. In words, the cost (1) captures the total cost incurred by all robots during the execution of the finite path $\tau$. Notice that the cost function $\hat{J}(\cdot)$ is additive, i.e., $\hat{J}(\tau_{1}|\tau_{2})=\hat{J}(\tau_{1})+\hat{J}(\tau_{2})$, where $\tau_{1}$ and $\tau_{2}$ are two finite paths of the PTS so that there is a feasible transition from the last state in $\tau_{1}$ to the first state in $\tau_{2}$, according to $\rightarrow_{\text{PTS}}$, and $|$ stands for concatenation. Also, since $\hat{J}(\cdot)$ is additive and $w_{\text{PTS}}(q_{\text{PTS}},q_{\text{PTS}}^{\prime})\geq 0$ by Definition 2, we get that $\hat{J}(\cdot)$ is monotone i.e., $\hat{J}(\tau_{1})\leq\hat{J}(\tau_{1}|\tau_{2})$.

The trace of an infinite path $\tau=\tau(1)\tau(2)\tau(3)\dots$ of a PTS, denoted by $\texttt{trace}(\tau)\in\left(2^{\mathcal{AP}}\right)^{\omega}$, where $\omega$ denotes infinite repetition, is an infinite word that is determined by the sequence of atomic propositions that are true in the states along $\tau$, i.e., $\texttt{trace}(\tau)=L(\tau(1))L(\tau(2))\dots$.

Given the PTS and the NBA $B$ that corresponds to the LTL $\phi$, we can now define the Product B$\ddot{\text{u}}$chi Automaton (PBA) $P=\text{PTS}\otimes B$ [6], as follows:

Definition III.3** (PBA)**

Given the product transition system $\text{PTS}=(\mathcal{Q}_{\text{PTS}},\allowbreak q_{\text{PTS}}^{0},\longrightarrow_{\text{PTS}},w_{\text{PTS}},\mathcal{AP},L_{\text{PTS}})$ and the NBA $B=(\mathcal{Q}_{B},\mathcal{Q}_{B}^{0},\Sigma,\rightarrow_{B},\mathcal{Q}_{B}^{F})$, we can define the Product B$\ddot{\text{u}}$chi Automaton $P=\text{PTS}\otimes B$ as a tuple $P=(\mathcal{Q}_{P},\mathcal{Q}_{P}^{0},\longrightarrow_{P},w_{P},\mathcal{Q}_{P}^{F})$ where (a) $\mathcal{Q}_{P}=\mathcal{Q}_{\text{PTS}}\times\mathcal{Q}_{B}$ is the set of states; (b) $\mathcal{Q}_{P}^{0}=q_{\text{PTS}}^{0}\times\mathcal{Q}_{B}^{0}$ is a set of initial states; (c) $\longrightarrow_{P}\subseteq\mathcal{Q}_{P}\times 2^{\mathcal{AP}}\times\mathcal{Q}_{P}$ is the transition relation defined by the rule: $\frac{\left(q_{\text{PTS}}\rightarrow_{\text{PTS}}q_{\text{PTS}}^{\prime}\right)\wedge\left(q_{B}\xrightarrow{L_{\text{PTS}}\left(q_{\text{PTS}}\right)}q_{B}^{\prime}\right)}{q_{P}=\left(q_{\text{PTS}},q_{B}\right)\longrightarrow_{P}q_{P}^{\prime}=\left(q_{\text{PTS}}^{\prime},q_{B}^{\prime}\right)}$. Transition from state $q_{P}\in\mathcal{Q}_{P}$ to $q_{P}^{\prime}\in\mathcal{Q}_{P}$, is denoted by $(q_{P},q_{P}^{\prime})\in\longrightarrow_{P}$, or $q_{P}\longrightarrow_{P}q_{P}^{\prime}$; (d) $w_{P}(q_{\text{P}},q_{\text{P}}^{\prime})=w_{\text{PTS}}(q_{\text{PTS}},q_{\text{PTS}}^{\prime})\geq 0$, where $q_{\text{P}}=(q_{\text{PTS}},q_{B})$ and $q_{\text{P}}^{\prime}=(q_{\text{PTS}}^{\prime},q_{B}^{\prime})$; and (e) $\mathcal{Q}_{P}^{F}=\mathcal{Q}_{\text{PTS}}\times\mathcal{Q}_{B}^{F}$ is a set of accepting/final states.

In what follows, we assume that the robots have to accomplish a complex collaborative task captured by a global LTL statement $\phi$ defined over the set of atomic propositions $\mathcal{AP}=\bigcup_{i=1}^{N}\mathcal{AP}_{i}$. Given such an LTL formula $\phi$, we define the language $\texttt{Words}(\phi)=\left\{\sigma\in(2^{\mathcal{AP}})^{\omega}|\sigma\models\phi\right\}$, where $\models\subseteq(2^{\mathcal{AP}})^{\omega}\times\phi_{i}$ is the satisfaction relation, as the set of infinite words $\sigma\in(2^{\mathcal{AP}})^{\omega}$ that satisfy the LTL formula $\phi$. Given such a global LTL formula $\phi$ and the PBA an infinite path $\tau$ of a PTS satisfies $\phi$ if and only if $\texttt{trace}(\tau)\in\texttt{Words}(\phi)$, which is equivalently denoted by $\tau\models\phi$.

Given an LTL formula $\phi$, if there is a path satisfying $\phi$, then there exists a path $\tau\models\phi$ that can be written in a finite representation, called prefix-suffix structure, i.e., $\tau=\tau^{\text{pre}}[\tau^{\text{suf}}]^{\omega}$, where the prefix part $\tau^{\text{pre}}$ is executed only once followed by the indefinite execution of the suffix part $\tau^{\text{suf}}$ [31, 14]. The prefix part $\tau^{\text{pre}}$ is the projection of a finite path of the PBA, i.e., a finite sequence of states of the PBA, denoted by $p^{\text{pre}}$, onto ${\mathcal{Q}}_{\text{PTS}}$, which has the following structure $p^{\text{pre}}=(q_{\text{PTS}}^{0},q_{B}^{0})(q_{\text{PTS}}^{1},q_{B}^{1})\dots(q_{\text{PTS}}^{K},q_{B}^{K})$ with $(q_{\text{PTS}}^{K},q_{B}^{K})\in{\mathcal{Q}}_{B}^{F}$. The suffix part $\tau^{\text{suf}}$ is the projection of a finite path of the PBA, denoted by $p^{\text{suf}}$, onto ${\mathcal{Q}}_{\text{PTS}}$, which has the following structure $p^{\text{suf}}=(q_{\text{PTS}}^{K},q_{B}^{K})(q_{\text{PTS}}^{K+1},q_{B}^{K+1})\dots(q_{\text{PTS}}^{K+S},q_{B}^{K+S})(q_{\text{PTS}}^{K+S+1},q_{B}^{K+S+1})$, where $(q_{\text{PTS}}^{K+S+1},q_{B}^{K+S+1})=(q_{\text{PTS}}^{K},q_{B}^{K})$. Then our goal is to compute a plan $\tau=\tau^{\text{pre}}[\tau^{\text{suf}}]^{\omega}=\Pi|_{\text{PTS}}p^{\text{pre}}[\Pi|_{\text{PTS}}p^{\text{suf}}]^{\omega}$, where $\Pi|_{\text{PTS}}$ stands for the projection on the state-space ${\mathcal{Q}}_{\text{PTS}}$, so that the following objective function is minimized

[TABLE]

which captures the total cost incurred by all robots during the execution of the prefix and a single execution of the suffix part. In (2), $\hat{J}(\tau^{\text{pre}})$ and $\hat{J}(\tau^{\text{suf}})$ stands for the cost of the prefix and suffix part, where the cost function $\hat{J}(\cdot)$ is defined in (1), i.e., $\hat{J}(\tau^{\text{pre}})=\sum_{k=1}^{K-1}w_{\text{PTS}}(\Pi|_{\text{PTS}}p^{\text{pre}}(k),\Pi|_{\text{PTS}}p^{\text{pre}}(k+1)),~{}\hat{J}(\tau^{\text{suf}})=\sum_{k=K}^{K+S}w_{\text{PTS}}(\Pi|_{\text{PTS}}p^{\text{suf}}(k)\Pi|_{\text{PTS}}p^{\text{suf}}(k+1))$. Specifically, in this paper we address the following problem.

Problem 1

Given a global LTL specification $\phi$, and transition systems $\text{wTS}_{i}$, for all robots $i$, determine a discrete team plan $\tau$ that satisfies $\phi$, i.e., $\tau\models\phi$, and minimizes the cost function (2).

III-A A Solution to Problem 1

Problem 1 is typically solved by applying graph-search methods to the PBA, see e.g., [31, 14]. Specifically, to generate a motion plan $\tau$ that satisfies $\phi$, the PBA is viewed as a weighted directed graph $\mathcal{G}_{P}=\{\mathcal{V}_{P},\mathcal{E}_{P},w_{P}\}$, where the set of nodes $\mathcal{V}_{P}$ is indexed by the set of states $\mathcal{Q}_{P}$, the set of edges $\mathcal{E}_{P}$ is determined by the transition relation $\longrightarrow_{P}$, and the weights assigned to each edge are determined by the function $w_{P}$. Then we find the shortest paths from the initial states to all reachable final/accepting states $q_{P}\in\mathcal{Q}_{P}^{F}$ and projecting these paths onto the PTS results in the prefix parts $\tau^{\text{pre},a}$, where $a\in\{1,\dots,|\mathcal{Q}_{P}^{F}|\}$. The respective suffix parts $\tau^{\text{suf},a}$ are constructed similarly by computing the shortest cycle around the $a$-th accepting state. All the resulting motion plans $\tau^{a}=\tau^{\text{pre},a}[\tau^{\text{suf},a}]^{\omega}$ satisfy the LTL specification $\phi$. Among all these plans, we can easily compute the optimal plan that minimizes the cost function defined in (2) by computing the cost $J(\tau^{a})$ for all plans and selecting the one with the smallest cost; see e.g. [14, 16, 17].

IV Sampling-based Optimal Control Synthesis

Since the size of the PBA can grow arbitrarily large with the number of robots and the complexity of the task, constructing this PBA and applying graph-search techniques to find optimal plans, as discussed in Section III-A, is resource demanding and computationally expensive. In this section, we propose a sampling-based planning algorithm that is scalable and constructs a discrete motion plan $\tau$ in prefix-suffix structure, i.e., $\tau=\tau^{\text{pre}}[\tau^{\text{suf}}]^{\omega}$, that satisfies a given global LTL specification $\phi$. The procedure is based on the incremental construction of a directed tree that approximately represents the state-space $\mathcal{Q}_{P}$ and the transition relation $\rightarrow_{P}$ of the PBA defined in Definition III.3. The construction of the prefix and the suffix part is described in Algorithm 1. In Algorithm 1, first the LTL formula is translated to a NBA $B=\{{\mathcal{Q}}_{B},{\mathcal{Q}}_{B}^{0},\rightarrow_{B},{\mathcal{Q}}_{B}^{F}\}$ [line 1, Alg. 1]. Then, in lines 1-1, the prefix parts $\tau^{\text{pre},a}$ are constructed, followed by the construction of their respective suffix parts $\tau^{\text{suf},a}$ in lines 1-1. Finally, using the constructed prefix and suffix parts, the optimal plan $\tau=\tau^{\text{pre},a^{*}}[\tau^{\text{suf},a^{*}}]^{\omega}\models\phi$ is synthesized in lines 1-1.

In what follows, we denote by $\mathcal{G}_{T}=\{\mathcal{V}_{T},\mathcal{E}_{T},\texttt{Cost}\}$ the tree that approximately represents the PBA $P$. Also, we denote by $q_{P}^{r}$ the root of ${\mathcal{G}}_{T}$. The set of nodes $\mathcal{V}_{T}$ contains the states of $\mathcal{Q}_{P}$ that have already been sampled and added to the tree structure. The set of edges $\mathcal{E}_{T}$ captures transitions between nodes in $\mathcal{V}_{T}$, i.e., $(q_{P},q_{P}^{\prime})\in\mathcal{E}_{T}$, if there is a transition from state $q_{P}\in\mathcal{V}_{T}$ to state $q_{P}^{\prime}\in\mathcal{V}_{T}$. The function $\texttt{Cost}:{\mathcal{V}}_{T}:\rightarrow\mathbb{R}_{+}$ assigns the cost of reaching node $q_{P}\in\mathcal{V}_{T}$ from the root $q_{P}^{r}$ of the tree. In other words,

[TABLE]

where $q_{P}\in{\mathcal{V}}_{T}$ and $\tau_{T}$ is the path in the tree ${\mathcal{G}}_{T}$ that connects the root to $q_{P}$.

IV-A Construction of Prefix Parts

In this Section, we describe how to construct the tree $\mathcal{G}_{T}=\{\mathcal{V}_{T},\mathcal{E}_{T},\texttt{Cost}\}$ that will be used for the synthesis of the prefix part [lines 1-1, Alg. 1]. Since the prefix part connects an initial state $q_{P}^{0}=(q_{\text{PTS}}^{0},q_{B}^{0})\in{\mathcal{Q}}_{P}^{0}$ to an accepting state $q_{P}=(q_{\text{PTS}},~{}q_{B})\in{\mathcal{Q}}_{P}^{F}$, with $q_{B}\in\mathcal{Q}_{B}^{F}$, we can define the goal region for the tree ${\mathcal{G}}_{T}$, as [line 1, Alg. 1]

[TABLE]

The root $q_{P}^{r}$ of the tree is an initial state $q_{P}^{0}=(q_{\text{PTS}}^{0},q_{B}^{0})$ of the PBA and the following process is repeated for each initial state $q_{B}^{0}\in{\mathcal{Q}}_{B}^{0}$ [line 1-1, Alg. 1]. The construction of the tree is described in Algorithm 2 [line 1, Alg. 1]. In line 1 of Algorithm 1, ${\mathcal{Q}}_{B}^{0}(b_{0})$ stands for the $b_{0}$-th initial state assuming an arbitrary enumeration of the elements of the set ${\mathcal{Q}}_{B}^{0}$. The set $\mathcal{V}_{T}$ initially contains only the root $q_{P}^{r}$, i.e., an initial state of the PBA [line 2 , Alg. 2] and, therefore, the set of edges is initialized as $\mathcal{E}_{T}=\emptyset$ [line 2, Alg. 2]. By convention, we assume that the cost of $q_{P}^{r}$ is zero [line 2, Alg. 2].

IV-A1 Sampling a state $q_{P}^{\text{new}}\in\mathcal{Q}_{P}$

The first step in the construction of the graph $\mathcal{G}_{T}$ is to sample a state from the state-space of the PBA. This is achieved by a sampling function Sample; see Algorithm 3. Specifically, we first create a state $q_{\text{PTS}}^{\text{rand}}=\Pi|_{\text{PTS}}q_{P}^{\text{rand}}$, where $q_{P}^{\text{rand}}$ is sampled from a given discrete distribution $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}):{\mathcal{V}}_{T}\rightarrow[0,1]$ [lines 3-3, Alg. 3]. The probability density function $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T})$ defines the probability of selecting the state $q_{P}\in{\mathcal{V}}_{T}$ as the state $q_{P}^{\text{rand}}$ at iteration $n$ of Algorithm 2 given the set ${\mathcal{V}}_{T}$. We make the following assumption for $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T})$.

Assumption IV.1** (Probability density function $f_{\text{rand}}$)**

(i) The probability density function $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}):{\mathcal{V}}_{T}\rightarrow[0,1]$ is bounded away from zero on ${\mathcal{V}}_{T}$. (ii) The probability density function $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}):{\mathcal{V}}_{T}\rightarrow[0,1]$ remains the same for all iterations $n$ and for a given state $q_{P}\in{\mathcal{V}}_{T}$ is monotonically decreasing with respect to the size of $|{\mathcal{V}}_{T}|$. This also implies that for a given $q_{P}\in{\mathcal{V}}_{T}$, the probability $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T})$ remains the same for all iterations $n$ if the set ${\mathcal{V}}_{T}$ does not change. (iii) Independent samples $q_{P}^{\text{rand}}$ can be drawn from $f_{\text{rand}}$.

By definition of $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T})$ we have that $q_{P}^{\text{rand}}$ always belongs to ${\mathcal{V}}_{T}$. Also, by assumption IV.1(i), we have that any node $q_{P}\in{\mathcal{V}}_{T}$ has a non-zero probability to be selected as the node $q_{P}^{\text{rand}}$. Also, notice that assumption IV.1(ii) is reasonable, as it requires that the probability of selecting a given state $q_{P}\in{\mathcal{V}}_{T}$ decreases as the cardinality of ${\mathcal{V}}_{T}$ increases. An example of a distribution that satisfies Assumption IV.1 is the discrete uniform distribution

[TABLE]

Notice that other sampling methods for $q_{P}^{\text{rand}}$ can be employed that do not require the more strict conditions of Assumption IV.1(ii); see Remark A.1 in Appendix A.

Given a state $q_{\text{PTS}}^{\text{rand}}$, we define its reachable set in the PTS

[TABLE]

i.e., ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})\subseteq{\mathcal{Q}}_{\text{PTS}}$ collects all the states $q_{\text{PTS}}\in{\mathcal{Q}}_{\text{PTS}}$ that can be reached from $q_{\text{PTS}}^{\text{rand}}$ in one hop. Then, we sample a state $q_{\text{PTS}}^{\text{new}}$ from a discrete distribution $f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand}}):{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})\rightarrow[0,1]$ [line 3, Alg. 3] that satisfies the following assumption.

Assumption IV.2** (Probability density function $f_{\text{new}}$)**

(i) The probability density function $f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand}}):{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})\rightarrow[0,1]$ is bounded away from zero on ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$. (ii) For a given $q_{\text{PTS}}^{\text{rand}}$, the distribution $f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand}})$ remains the same for all iterations $n$. (iii) Given a state $q_{\text{PTS}}^{\text{rand}}$, independent samples $q_{\text{PTS}}^{\text{new}}$ can be drawn from the probability density function $f_{\text{new}}$.

By definition of $f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand}})$, we have that $q_{\text{PTS}}^{\text{rand}}$ always belongs to ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$. Also, observe that by Assumption IV.2(i), we have that any node $q_{P}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$ has a non-zero probability to be $q_{\text{PTS}}^{\text{new}}$. Moreover, notice that the state $q_{P}^{\text{rand}}$ can change at every iteration $n$ and, therefore, clearly, so does the reachable set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$. Nevertheless, observe that the set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$ remains the same for all iterations $n$ for a given $q_{\text{PTS}}^{\text{rand}}$. Finally, note that other sampling methods for $q_{\text{PTS}}^{\text{new}}$ can be employed that do not require the more strict conditions of Assumption IV.2(ii); see Remark A.2 in Appendix A.

Remark IV.3** (Reachable set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$)**

In practice in order to obtain the state $q_{\text{PTS}}^{\text{new}}$ we do not need to construct the reachable set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$, which is a computationally expensive step. In fact, we only need the reachable sets ${\mathcal{R}}_{\text{TS}_{i}}(q_{i}^{\text{rand}})$, for all robots $i$, that collect all states that are reachable from the state $q_{i}^{\text{rand}}=\Pi|_{\text{TS}_{i}}q_{\text{PTS}}^{\text{rand}}\in{\mathcal{Q}}_{i}$ in one hop, defined as ${\mathcal{R}}_{\text{TS}_{i}}(q_{i}^{\text{rand}})=\{q_{i}\in{\mathcal{Q}}_{i}|q_{i}^{\text{rand}}\rightarrow_{i}q_{i}\}$. Then, we can define the probability density functions $f_{\text{new},i}(q_{i}|q_{i}^{\text{rand}}):{\mathcal{R}}_{\text{TS}_{i}}(q_{i}^{\text{rand}})\rightarrow[0,1]$ that are bounded away from zero on ${\mathcal{R}}_{\text{TS}_{i}}(q_{i}^{\text{rand}})$ and use them to draw a sample $q_{i}^{\text{new}}$ that is reachable from $q_{i}^{\text{rand}}$, for all $i\in\left\{1,\dots,N\right\}$. Stacking these samples in a vector we can define $q_{\text{PTS}}^{\text{new}}=[q_{1}^{\text{new}},q_{2}^{\text{new}},\dots,q_{N}^{\text{new}}]$ and the probability density function $f_{\text{new}}$ becomes $f_{\text{new}}=f_{\text{new},1}\cdot f_{\text{new},2}\cdot\dots\cdot f_{\text{new},N}$ that has to satisfy Assumption IV.2. Clearly, the resulting state $q_{\text{PTS}}^{\text{new}}$ belongs to the reachable set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand}})$. Throughout the paper, for simplicity, our analysis is based on $f_{\text{new}}$ and not on the probability density functions $f_{\text{new},i}$.

In order to build incrementally a graph whose set of nodes approximates the state-space $\mathcal{Q}_{P}$ we need to append to $q_{\text{PTS}}^{\text{new}}$ a state from the state-space $\mathcal{Q}_{B}$ of the NBA $B$. Let $q_{B}^{\text{new}}=\mathcal{Q}_{B}(b)$ [line 2, Alg. 2] be the candidate B$\ddot{\text{u}}$chi state that will be attached to $q_{\text{PTS}}^{\text{new}}$, where $\mathcal{Q}_{B}(b)$ stands for the $b$-th state in the set ${\mathcal{Q}}_{B}$ assuming an arbitrary enumeration of the elements of the set ${\mathcal{Q}}_{B}$. The following procedure is repeated for all $q_{B}^{\text{new}}={\mathcal{Q}}_{B}(b)$ with $b\in\{1,\dots,|\mathcal{Q}_{B}|\}$. First, we construct the state $q_{P}^{\text{new}}=(q^{\text{new}}_{\text{PTS}},q_{B}^{\text{new}})\in\mathcal{Q}_{P}$ [line 2, Alg. 2] and then we check if this state can be added to the tree $\mathcal{G}_{T}$ [lines 2-2, Alg. 2]. If the state $q_{P}^{\text{new}}$ does not already belong to the tree from a previous iteration of Algorithm 2, i.e, if $q_{P}^{\text{new}}\notin\mathcal{V}_{T}$ [line 1, Alg. 2], we check which node in $\mathcal{V}_{T}$ (if there is any) can be the parent of $q_{P}^{\text{new}}$ in the tree $\mathcal{G}_{T}$. This is achieved by the function Extend described in Algorithm 4 [line 2, Alg. 2] and in Section IV-A2. If $q_{P}^{\text{new}}\in{\mathcal{V}}_{T}$, then the rewiring step follows described in Algorithm 5 [lines 2-2, Alg. 2] and in Section IV-A3 that aims to reduce the cost of nodes $q_{P}\in{\mathcal{V}}_{T}$.

IV-A2 Adding a new edge to $\mathcal{E}_{T}$

Assume that $q_{P}^{\text{new}}\notin{\mathcal{V}}_{T}$ [lines 2, Alg. 2]. Then the function Extend described in Algorithm 4 [line 2, Alg. 2] is used to check if the tree can be extended towards $q_{P}^{\text{new}}$. The first step in Algorithm 4 is to construct the set $\mathcal{R}^{\rightarrow}_{{\mathcal{V}}_{T}}(q_{P}^{\text{new}})\subseteq\mathcal{V}_{T}$ defined as

[TABLE]

that collects all states $q_{P}\in\mathcal{V}_{T}$ that satisfy the transition rule $(q_{P},q_{P}^{\text{new}})\in\rightarrow_{P}$, i.e., all states that can directly reach $q_{P}^{\text{new}}$ [line 4, Alg. 4]. If the resulting set $\mathcal{R}^{\rightarrow}_{{\mathcal{V}}_{T}}(q_{P}^{\text{new}})$ is empty then the sample $q_{P}^{\text{new}}$ is not added to the tree. On the other hand, if $\mathcal{R}^{\rightarrow}_{{\mathcal{V}}_{T}}(q_{P}^{\text{new}})\neq\emptyset$, then the state $q_{P}^{\text{new}}$ is added to the tree [lines 4-4, Alg. 4]. The parent of $q_{P}^{\text{new}}$ is selected as

[TABLE]

where $\texttt{Cost}(q_{P})+w_{\text{PTS}}(\Pi|_{\text{PTS}}q_{P},\Pi|_{\text{PTS}}q_{P}^{\texttt{new}})$ captures the cost of the node $q_{P}^{\text{new}}$ if it gets connected to the root through the node $q_{P}$. In other words, the parent $q_{P}^{\text{prev}}$ of node $q_{P}^{\text{new}}$ is selected among all states in $\mathcal{R}^{\rightarrow}_{{\mathcal{V}}_{T}}(q_{P}^{\text{new}})$ so that the cost of $q_{P}^{\text{new}}$ is minimized [line 4, Alg. 4]. The set of nodes and edges is updated as $\mathcal{V}_{T}=\mathcal{V}_{T}\cup\{q_{P}^{\text{new}}\}$ and $\mathcal{E}_{T}=\mathcal{E}_{T}\cup\{(q_{P}^{\text{prev}},q_{P}^{\text{new}})\}$ [lines 4 and 4, Alg. 4]. Given the parent $q_{P}^{\text{prev}}$ of the node $q_{P}^{\text{new}}$, the cost of $q_{P}^{\text{new}}$ is [line 4, Alg. 4]:

[TABLE]

due to (1) and (3). Algorithm 4 is illustrated in Figure 1, as well.

IV-A3 Rewiring

Once a new state $q_{P}^{\text{new}}=(q^{\text{new}}_{\text{PTS}},q_{B}^{\text{new}})$ has been added to the tree or if the new sample $q_{P}^{\text{new}}$ already belongs to the tree [line 2, Alg. 2], the rewiring step follows [line 2, Alg. 2]. Specifically, we rewire the nodes in $q_{P}\in\mathcal{V}_{T}$ that can get connected to the root $q_{P}^{r}$ through the node $q_{P}^{\text{new}}$ if this rewiring can decrease their cost $\texttt{Cost}(q_{P})$. The rewiring process is described in Algorithm 5 and is illustrated in Figure 2.

In Algorithm 5 we first construct the reachable set $\mathcal{R}_{{\mathcal{V}}_{T}}^{\leftarrow}(q_{P}^{\text{new}})\subseteq\mathcal{V}_{T}$ defined as

[TABLE]

that collects all states of $q_{P}\in\mathcal{V}_{T}$ that satisfy the transition rule $(q_{P}^{\text{new}},q_{P})\in\rightarrow_{P}$, i.e., all states that can be directly reached by $q_{P}^{\text{new}}$ [line 5, Alg. 5]. Then, for all states $q_{P}\in\mathcal{R}_{{\mathcal{V}}_{T}}^{\leftarrow}(q_{P}^{\text{new}})$ we check if their current cost $\texttt{Cost}(q_{P})$ is greater than their cost if they were connected to the root through $q_{P}^{\text{new}}$ [line 5, Alg. 5]. If this is the case for a node $q_{P}\in\mathcal{R}_{{\mathcal{V}}_{T}}^{\leftarrow}(q_{P}^{\text{new}})$, then the new parent of $q_{P}$ becomes $q_{P}^{\text{new}}$, i.e, a directed edge is drawn from $q_{P}^{\text{new}}$ to $q_{P}$, and the edge that was connecting $q_{P}$ to its previous parent is deleted [lines 5-5, Alg. 5]. The cost of node $q_{P}$ is updated as $\texttt{Cost}(q_{P})=\texttt{Cost}(q_{P}^{\text{new}})+w_{\text{PTS}}(\Pi|_{\text{PTS}}q_{P}^{\texttt{new}},\Pi|_{\text{PTS}}q_{P})$ to take into account the new path through which it gets connected to the root [line 5, Alg. 5]. Once a state $q_{P}$ gets rewired, the cost of all its successor nodes in ${\mathcal{G}}_{T}$, collected in the set

[TABLE]

is updated to account for the change in the cost of $q_{P}$ [line 5, Alg. 5].

IV-A4 Construction of Paths

The construction of the tree ${\mathcal{G}}_{T}$ ends after $n_{\text{max}}^{\text{pre}}$ iterations, where $n_{\text{max}}^{\text{pre}}$ is user specified [line 2, Alg. 2]. Then, we construct the set ${\mathcal{P}}={\mathcal{V}}_{T}\cap{\mathcal{X}}_{\text{goal}}^{\text{pre}}$ [line 2, Alg. 2] that collects all the states $q_{P}\in{\mathcal{V}}_{T}$ that belong to the goal region ${\mathcal{X}}_{\text{goal}}^{\text{pre}}$. Given the tree ${\mathcal{G}}_{T}$ and the set ${\mathcal{P}}$ [line 1, Alg. 1] that collects all states $q_{P}\in{\mathcal{X}}_{\text{goal}}^{\text{pre}}\cap{\mathcal{V}}_{T}$, we can compute the prefix plans [lines 1-1, Alg. 1]. In particular, the path that connects the $a$-th state in the set $\mathcal{P}$, denoted by ${\mathcal{P}}(a)$, to the root $q_{P}^{r}$ constitutes the $\alpha$-th prefix plan and is denoted by $\tau^{\text{pre},a}$ [line 1, Algorithm 1]. Its computation is described in Algorithm 6. Specifically, the prefix part $\tau^{\text{pre},a}$ is constructed by tracing the sequence of parents of nodes starting from the node that represents the accepting state $\mathcal{P}(a)$ and ending at the root of the tree [lines 6-6, Alg. 6]. The parent of each node is computed by the function $\texttt{parent}:\mathcal{V}_{T}\rightarrow\mathcal{V}_{T}$ that maps a node $q_{P}\in\mathcal{V}_{T}$ to a unique vertex $q_{P}^{\prime}\in\mathcal{V}_{T}$ if $(q_{P}^{\prime},q_{P})\in\mathcal{E}_{T}$, i.e., $\texttt{parent}(q_{P})=q_{P}^{\prime}$ if $(q_{P}^{\prime},q_{P})\in\mathcal{E}_{T}$. By convention, we assume that $\texttt{parent}(q_{P}^{r})=q_{P}^{r}$. In line 6, $\Pi|_{\text{PTS}}p_{T}$ stands for the projection of the path $p_{T}$ onto the state-space of the PTS. In line 6 of Algorithm 6, $|$ stands for the concatenation of paths. Thus, for the resulting prefix plan $\tau^{\text{pre},a}$, it holds that $\tau^{\text{pre},a}(1)=\Pi|_{\text{PTS}}q_{P}^{r}$ and $\tau^{\text{pre},a}(|\tau^{\text{pre},a}|)=\Pi|_{\text{PTS}}\mathcal{P}(a)$.

IV-B Construction of Suffix Parts

Once the prefix plans $\tau^{\text{pre},a}$ for all $a\in\{1,\dots,|{\mathcal{P}}|\}$ are constructed, the corresponding suffix plans $\tau^{\text{suf},a}$ are constructed [lines 1-1, Alg. 1]. Specifically, every suffix part $\tau^{\text{suf},a}$ is a sequence of states in ${\mathcal{Q}}_{P}$ that starts from the state $\mathcal{P}(a)$ and ends at the same state $\mathcal{P}(a)$, i.e., a cycle around state $\mathcal{P}(a)$ where any two consecutive states in $\tau_{i}^{\text{suf},a}$ respect the transition rule $\rightarrow_{P}$. To construct the suffix plan $\tau_{i}^{\text{suf},a}$ we build a tree $\mathcal{G}_{T}=\{\mathcal{V}_{T},\mathcal{E}_{T},\texttt{Cost}\}$ that approximates the PBA $P$, in a similar way as in Section IV-A, and implement a cycle-detection mechanism to identify cycles around the state $P(a)$. The only differences are that: (i) the root of the tree is now $q_{P}^{r}={\mathcal{P}}(a)$, i.e., it is an accepting/final state [line 1, Alg. 1] detected during the construction of the prefix plans, (ii) the goal region corresponding to the root $q_{P}^{r}={\mathcal{P}}(a)$, is defined as

[TABLE]

and, (iii) we first check if $q_{P}^{r}\in{\mathcal{X}}_{\text{goal}}^{\text{suf}}$, i.e., if $(\Pi|_{B}q_{P}^{r},L(\Pi|_{\text{PTS}}q_{P}^{r}),\Pi|_{B}q_{P}^{r})$ and if the cost of such a self loop has zero cost, i.e., if $w_{P}(q_{P}^{r},q_{P}^{r})=0$ [line 1, Alg. 1]. If so, the construction of the tree is trivial, as it consists of only the root, and a loop around it with zero cost [line 1, Alg. 1].333Clearly, any other suffix part will have non-zero cost and, therefore, it will not be optimal and it will be discarded by Algorithm 1 [lines 1-1, Alg. 1]. For this reason, the construction of the tree ${\mathcal{G}}_{T}$ is terminated if a self-loop around $q_{P}^{r}$ is detected. If $q_{P}^{r}\notin{\mathcal{X}}_{\text{goal}}^{\text{suf}}$, then the tree ${\mathcal{G}}_{T}$ is constructed by Algorithm 2 [line 1, Alg. 1]. Once a tree rooted at $q_{P}^{r}={\mathcal{P}}(a)$ is constructed, a set ${\mathcal{S}}_{a}\subseteq{\mathcal{V}}_{T}$ is formed that collects all states $q_{P}\in{\mathcal{V}}_{T}\cap{\mathcal{X}}_{\text{goal}}^{\text{suf}}(q_{P}^{r})$ [lines 1, 1, Alg. 1]. Then for each state $q_{P}\in{\mathcal{S}}_{a}$, we compute the cost $\hat{J}(\tilde{\tau}^{\text{suf},e})$ of each possible suffix plan $\tilde{\tau}^{\text{suf},e}$, for all $e\in\{1,\dots,|{\mathcal{S}}_{a}|\}$, associated with the root $q_{P}^{r}$. By construction of the cost functions Cost and $\hat{J}(\cdot)$, it holds that $\hat{J}(\tilde{\tau}^{\text{suf},e})=\texttt{Cost}({\mathcal{S}}_{a}(e))+w_{\text{PTS}}(\Pi|_{\text{PTS}}{\mathcal{S}}_{a}(e),\Pi|_{\text{PTS}}q_{P}^{r})$, where ${\mathcal{S}}_{a}(e)$ stands for the $e$-th state in the set ${\mathcal{S}}_{a}$. Among all detected suffix plans $\tilde{\tau}^{\text{suf},e}$ associated with the accepting state $\mathcal{P}(a)$, we select the suffix plan with the minimum cost, which constitutes the suffix plan $\tau^{\text{suf},a}$ [lines 1-1, Alg. 1]. This process is repeated for all $a\in\{1,\dots,|{\mathcal{P}}|\}$ [line 1, Alg. 1]. In this way, for each prefix plan $\tau^{\text{pre},a}$ we construct its corresponding suffix plan $\tau^{\text{suf},a}$, if it exists.

IV-C Construction of Optimal Discrete Plans

By construction, any motion plan $\tau^{a}=\tau^{\text{pre},a}[\tau^{\text{suf},a}]^{\omega}$, with $\mathcal{S}_{a}\neq\emptyset$, and $a\in\{1,\dots,|\mathcal{P}|\}$ satisfies the global LTL specification $\phi$. The cost $J(\tau^{a})$ of each plan $\tau^{a}$ is defined in (2). Given an initial state $q_{B}^{0}\in{\mathcal{Q}}_{B}^{0}$, among all the motion plans $\tau^{a}\models\phi$, we select the one with the smallest cost $J(\tau^{a})$ [line 1, Alg. 1]. The plan with the smallest cost given an initial state $q_{B}^{0}$ is denoted by $\tau_{q_{B}^{0}}$. Then, among all plans $\tau_{q_{B}^{0}}$, we select again the one with smallest cost $J(\tau_{q_{B}^{0}})$, i.e., $\tau=\tau^{a_{*}}$, where $a_{*}=\text{argmin}_{a_{q_{B}^{0}}}{J(\tau_{q_{B}^{0}})}$ [lines 1-1, Alg. 1].

Remark IV.4** (Execution of plan $\tau$)**

The motion plan $\tau$ generated by Algorithm 1 satisfies the global LTL formula, if all robots pick their next states either synchronously or asynchronously as in [16]. For asynchronous execution of the plan $\tau$, we only need to add ‘traveling states’ to the transition systems that capture cases where robots $i$ are traveling from states $q_{i}^{\ell_{j}}\in{\mathcal{Q}}_{i}$ to $q_{i}^{\ell_{e}}\in{\mathcal{Q}}_{i}$ that satisfy $(q_{i}^{\ell_{j}},q_{i}^{\ell_{e}})\in\rightarrow_{i}$. More details about the traveling states can be found in [16]. Note that adding traveling states to the trees increases the computational cost of synthesizing plans that can be executed asynchronously and satisfy the assigned LTL formula.

IV-D Complexity Analysis

The memory resources needed to store the PBA as a graph structure ${\mathcal{G}}_{P}=\left\{{\mathcal{V}}_{P},{\mathcal{E}}_{P},w_{P}\right\}$, defined in Section III-A, using its adjacency list is $O(|{\mathcal{V}}_{P}|+|{\mathcal{E}}_{P}|)$ [32]. On the other hand, the memory needed to store a tree, constructed by Algorithm 2, that approximates the PBA is $O(|{\mathcal{V}}_{T}|)$, since $|{\mathcal{E}}_{T}|=|{\mathcal{V}}_{T}|-1$. Due to the incremental construction of the tree we get that $|{\mathcal{V}}_{T}|\leq|{\mathcal{V}}_{P}|<|{\mathcal{V}}_{P}|+|{\mathcal{E}}_{P}|$ which shows that our proposed algorithm requires fewer memory resources compared to existing optimal control synthesis algorithms that rely on the construction of the PBA [16, 17].

Next, observe that the time complexity of sampling the state $q_{\text{PTS}}^{\text{new}}$ in Algorithm 3 is $O(\sum_{i}|{\mathcal{Q}}_{i}|)$; see also Remark IV.3. Moreover, the time complexity of extending the graph towards $q_{P}^{\text{new}}$ is $O(|{\mathcal{V}}_{T}|(N+1))$; see Algorithm 4. The reason is that Algorithm 4 can be equivalently written as a for-loop over the set ${\mathcal{V}}_{T}$ where we first examine if $q_{P}\in{\mathcal{V}}_{T}$ can reach $q_{P}^{\text{new}}$, based on the transition rule $\rightarrow_{P}$, and then we compute the cost of such a transition while keeping track of the node $q_{P}\in{\mathcal{V}}_{T}$ that incurs the minimum cost. These calculations have cost $O(N+1)$ and the time complexity of the for-loop over ${\mathcal{V}}_{T}$ is $O(|{\mathcal{V}}_{T}|)$. With this implementation of Algorithm 4, we do not need to construct the set ${\mathcal{R}}_{{\mathcal{V}}_{T}}^{\rightarrow}(q_{P}^{\text{new}})$.444Definition of ${\mathcal{R}}_{{\mathcal{V}}_{T}}^{\rightarrow}(q_{P}^{\text{new}})$ is only used in Section V to simplify the proof of completeness and optimality of the proposed algorithm. For the same reason, the time complexity of the rewiring step is $O(|{\mathcal{V}}_{T}|(N+1))$; see Algorithm 5. Finally the time complexity of Algorithm 6 that finds a path in the tree ${\mathcal{G}}_{T}$ is $O(|{\mathcal{V}}_{T}|)$. On the other hand, using the Dijkstra algorithm to find the shortest path from an initial to a final state or a cycle around a final state of a PBA is $O(|\mathcal{E}_{P}|+|\mathcal{V}_{P}|\log(|\mathcal{V}_{p}|))$; clearly, it holds that $|\mathcal{E}_{P}|+|\mathcal{V}_{P}|\log(|\mathcal{V}_{P}|)>|\mathcal{V}_{T}|$. If the PBA is represented as an implicit graph using its transition rule $\rightarrow_{P}$, then we can apply the uniform cost search algorithm [33, 34] to find the optimal prefix and suffix paths with time and space complexity $O(b^{1+C^{*}/\epsilon})$, where $b$ is the branching factor of ${\mathcal{G}}_{P}$, $C^{*}$ is the optimal cost of either the prefix or suffix path, and $\epsilon>0$ is the minimum increase in the cost of the path as we move from one node of ${\mathcal{G}}_{P}$ to another. Note that this approach is also memory efficient since it does not require the explicit construction of the PBA but it can become computationally intractable (i) for dense graphs, i.e., as $b$ increases or (ii) for long paths, i.e., as $C^{*}/\epsilon$ increases. In comparison, the computational cost per iteration of our algorithm depends linearly only on $|{\mathcal{V}}_{T}|$ and the size of the network and not on the structure of ${\mathcal{G}}_{P}$.

V Correctness and Optimality

In this section, we first characterize the rate at which the constructed trees grow and then we provide the main results pertaining to the probabilistic completeness and optimality of the proposed Algorithm 1. In what follows, we denote by $\mathcal{G}_{T}^{n}=\{\mathcal{V}_{T}^{n},\mathcal{E}_{T}^{n},\texttt{Cost}\}$ the tree that has been built by Algorithm 2 at the $n$-th iteration for the construction of either a prefix or suffix part. Also, we denote the nodes $q_{P}^{\text{rand}}$ and $q_{P}^{\text{new}}$ at iteration $n$ by $q_{P}^{\text{rand},n}$ and $q_{P}^{\text{new},n}$, respectively. Moreover, in the following results, we denote the reachable set of $q_{P}\in{\mathcal{Q}}_{P}$ in the state-space of the PBA by:

[TABLE]

that collects all states $q_{P}^{\prime}\in{\mathcal{Q}}_{P}$ that can be reached from $q_{P}\in{\mathcal{Q}}_{P}$ in one hop.

Proposition V.1** (Growth Rate of ${\mathcal{G}}_{T}^{n}$)**

Assume that the reachable set of $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})$ in the PBA is non-empty, i.e., that ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\{q_{P}^{\prime}\in{\mathcal{Q}}_{P}~{}|~{}q_{P}^{\text{rand},n}\rightarrow q_{P}^{\prime}\}\neq\emptyset$. Then, there is at least one $b\in\{1,\dots,|{\mathcal{Q}}_{B}|\}$ so that either the state $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new}},{\mathcal{Q}}_{B}(b))$ will be added to ${\mathcal{V}}_{T}^{n}$ at iteration $n$ if $q_{P}^{\text{new},n}\notin{\mathcal{V}}_{T}^{n}$, or rewiring to $q_{P}^{\text{new},n}$ will occur if $q_{P}^{\text{new},n}\in{\mathcal{V}}_{T}^{n}$ and ${\mathcal{R}}_{{\mathcal{V}}_{T}^{n}}^{\leftarrow}(q_{P}^{\text{new},n})\neq\emptyset$. If ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$, then the tree may remain unaltered at iteration $n$.

Proof:

To show this result, recall that a state $q_{P}^{\prime}=(q_{\text{PTS}}^{\prime},q_{B}^{\prime})$ belongs to ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ if $q_{P}^{\text{rand},n}\rightarrow_{P}q_{P}^{\prime}$, i.e., if (i) $q_{\text{PTS}}^{\text{rand},n}\rightarrow_{\text{PTS}}q_{\text{PTS}}^{\prime}$ and (ii) $q_{B}^{\text{rand},n}\stackrel{{\scriptstyle L(q_{\text{PTS}}^{\text{rand},n})}}{{\longrightarrow_{B}}}q_{B}^{\prime}$. In what follows, we first examine the case ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$ and then the case ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})\neq\emptyset$.

Assume that ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$. This means that for the state $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})$, there are either no states $q_{\text{PTS}}^{\prime}$ that satisfy condition (i), or no states $q_{B}^{\prime}$ that satisfy condition (ii), or possibly both. If there are no states $q_{\text{PTS}}^{\prime}$ that satisfy condition (i), then $q_{\text{PTS}}^{\text{rand},n}$ is a terminal state of the PTS, i.e., ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})=\emptyset$, where ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ is defined in (6). As a result, this implies that we cannot create any state $q_{\text{PTS}}^{\text{new},n}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ and, therefore, it is trivial to see that no states will be added to ${\mathcal{V}}_{T}^{n}$ at iteration $n$ and the tree will not change at iteration $n$. On the other hand, if there are no states $q_{B}^{\prime}$ that satisfy condition (ii), i.e., if there is no $b$ such that $q_{B}^{\text{rand},n}\stackrel{{\scriptstyle L(q_{\text{PTS}}^{\text{rand},n})}}{{\longrightarrow_{B}}}{\mathcal{Q}}_{B}(b)$, then $q_{\text{PTS}}^{\text{rand},n}$ is a state at which the LTL formula $\phi$ is violated, by construction of the NBA. However, this does not necessarily mean that the tree will remain the same at iteration $n$. The reason is that if ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})\neq\emptyset$, then there exist states $q_{\text{PTS}}^{\text{new},n}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ and, consequently, states $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(b))$ can be constructed. Such states can possibly be added to the tree if there exists a state $q_{P}\in{\mathcal{V}}_{T}^{n}$ such that $q_{P}\in{\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n}}(q_{P}^{\text{new},n})$; see line 4 in Algorithm 4. Also, if $q_{P}^{\text{new},n}\in{\mathcal{V}}_{T}^{n}$ and if ${\mathcal{R}}_{{\mathcal{V}}_{T}^{n}}^{\leftarrow}(q_{P}^{\text{new},n})\neq\emptyset$ then rewiring to these states may occur; see line 5 in Algorithm 5. Clearly if $q_{\text{PTS}}^{\text{rand},n}$ is both a terminal state of PTS and a state at which $\phi$ is violated, then the tree will remain unchanged at iteration $n$.555Observe that if ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$, then the state $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}$ will remain forever a leaf node in the tree ${\mathcal{G}}_{T}^{n}$.

Next, assume that ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})\neq\emptyset$. Following the same logic as in the previous case, this means that $q_{\text{PTS}}^{\text{rand},n}$ is not a terminal state of the PTS, i.e., ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})\neq\emptyset$, and $q_{\text{PTS}}^{\text{rand},n}$ is not a state at which the LTL formula $\phi$ is violated. Since ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})\neq\emptyset$ and since $q_{\text{PTS}}^{\text{new},n}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ by construction, we get that $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(b))$ satisfies condition (i) for all $b$. Next, since $q_{\text{PTS}}^{\text{rand},n}$ is not a state at which the LTL formula $\phi$ is violated, this means that there is at least one value for $b$, denoted hereafter by $\bar{b}$, such that $q_{B}^{\text{rand},n}\stackrel{{\scriptstyle L(q_{\text{PTS}}^{\text{rand},n})}}{{\longrightarrow_{B}}}{\mathcal{Q}}_{B}(\bar{b})$, by construction of the NBA. Thus, we get that $(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(\bar{b}))\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$. This result along with the fact that $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}$, by definition of $f_{\text{rand}}$, entail that $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(\bar{b}))$ satisfies $q_{P}^{\text{rand},n}\in{\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n}}(q_{P}^{\text{new},n})$, i.e., ${\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n}}(q_{P}^{\text{new},n})\neq\emptyset$. This equivalently means that if $q_{P}^{\text{new},n}\notin{\mathcal{V}}_{T}^{n}$ then the state $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(\bar{b}))$ will be added to ${\mathcal{V}}_{T}^{n}$ at iteration $n$; see line 4 in Algorithm 4. Otherwise, if $q_{P}^{\text{new},n}\in{\mathcal{V}}_{T}^{n}$ and ${\mathcal{R}}_{{\mathcal{V}}_{T}^{n}}^{\leftarrow}(q_{P}^{\text{new},n})\neq\emptyset$ rewiring to $q_{P}^{\text{new},n}$ will follow (see line 5 in Algorithm 5), completing the proof. ∎

Remark V.2** (Emptiness of ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$)**

Observe that ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$ for a state $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})$, if $q_{\text{PTS}}^{\text{rand},n}$ is either a terminal state of the PTS, i.e., ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})=\emptyset$, where ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ is defined in (6), or a state at which the LTL formula $\phi$ is violated, or both. For example, if the PTS has no terminal states and the LTL formula does not include the negation operator $\neg$, i.e., there are no states in ${\mathcal{Q}}_{\text{PTS}}$ that can violate $\phi$, then ${\mathcal{R}}_{P}(q_{P})\neq\emptyset$, $\forall q_{P}\in{\mathcal{Q}}_{P}$.

To show that Algorithm 1 is probabilistically complete and asymptotically optimal we need first to show the following results that rely on the second Borel-Cantelli lemma [35] presented below. The proofs of the following lemmas are provided in Appendix A.

Lemma V.3** (Borel-Cantelli [35])**

Consider a sequence of independent events $A=\{A^{n}\}_{n=1}^{\infty}$. If $\sum_{n=1}^{\infty}\mathbb{P}(A^{n})=\infty$ then $\mathbb{P}(\limsup_{n\to\infty}A^{n})=1$, i.e., the probability that infinitely many events $A^{n}$ occur is 1.

Lemma V.4** (Sampling $q_{P}^{\text{rand},n}$)**

Consider any state $q_{P}\in{\mathcal{V}}_{T}^{n}$ and any fixed iteration index $n$. Then, there exists an infinite number of subsequent iterations $n+k$, where $k\in\mathcal{K}$ and $\mathcal{K}\subseteq\mathbb{N}$ is a subsequence of $\mathbb{N}$, at which the state $q_{P}\in{\mathcal{V}}_{T}^{n}$ is selected by Algorithm 3 to be the node $q_{P}^{\text{rand},n+k}$.

Using Lemma V.4 we can show the following result for the node $q_{\text{PTS}}^{\text{new},n}$.

Lemma V.5** (Sampling $q_{\text{PTS}}^{\text{new},n}$)**

Consider any state $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})\in{\mathcal{V}}_{T}^{n}$ selected by Algorithm 3 and any fixed iteration index $n$. Then, for any state $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$, where ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ is defined in (6), there exists an infinite number of subsequent iterations $n+k$, where $k\in\mathcal{K}^{\prime}$ and $\mathcal{K}^{\prime}\subseteq\mathcal{K}$ is a subsequence of the sequence of $\mathcal{K}$ defined in Lemma V.4, at which the state $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ is selected by Algorithm 3 to be the node $q_{\text{PTS}}^{\text{new},n+k}$.

By Lemma V.5, we have the following corollary for the state $q_{P}^{\text{new},n}$.

Corollary V.6** (Sampling $q_{P}^{\text{new},n}$)**

Consider any state $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})\in{\mathcal{V}}_{T}^{n}$ selected by Algorithm 3 and any fixed iteration index $n$. Then, for any state $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$, where ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ is defined in (12), there exists an infinite number of iterations $n+k$, where $k\in\mathcal{K}^{\prime}$ and $\mathcal{K}^{\prime}$ is the subsequence defined in Lemma V.5, at which the state $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$, is selected by Algorithm 3 to be the node $q_{P}^{\text{new},n+k}$.

Using Corollary V.6, we can show the following result for the reachable set $\mathcal{R}_{P}(q_{P}^{\text{rand},n})$.

Lemma V.7** (Reachable set $\mathcal{R}_{P}(q_{P}^{\text{rand},n})$)**

Consider any state $q_{P}^{\text{rand},n}=(q_{\text{PTS}}^{\text{rand},n},q_{B}^{\text{rand},n})\in{\mathcal{V}}_{T}^{n}$ selected by Algorithm 3 and any fixed iteration index $n$. Then, Algorithm 2 will add to ${\mathcal{V}}_{T}^{n+k}$ all states that belong to the reachable set ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$, where ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ is defined in (12), as $k\to\infty$, with probability 1, i.e.,

[TABLE]

Using Lemma V.4, we can show that Lemma V.7 holds for all nodes $q_{P}\in{\mathcal{V}}_{T}^{n}$. This result is stated in the following corollary.

Corollary V.8** (Reachable set $\mathcal{R}_{P}(q_{P})$)**

Given any state $q_{P}=(q_{\text{PTS}},q_{B})\in{\mathcal{V}}_{T}^{n}$, Algorithm 2 will add to ${\mathcal{V}}_{T}^{n}$ all states that belong to the reachable set ${\mathcal{R}}_{P}(q_{P})$, as $n\to\infty$, with probability 1, i.e.,

[TABLE]

Using Corollary V.8, in the next theorem, we show that Algorithm 1 is probabilistically complete.

Theorem V.9** (Probabilistic Completeness)**

If there exists a solution to Problem 1, then Algorithm 1 is probabilistically complete, i.e., it will find with probability 1 a motion plan $\tau$ that satisfies the LTL specification $\phi$, as $n_{\text{max}}^{\text{pre}}\to\infty$ and $n_{\text{max}}^{\text{suf}}\to\infty$.

Proof:

to show this result, we need to show that Algorithm 2 satisfies

[TABLE]

for both goal regions ${\mathcal{X}}_{\text{goal}}$ defined in (4) and in (IV-B).

To show (15), it suffices to show that the set of nodes ${\mathcal{V}}_{T}^{n}$ will eventually contain all states in the state-space ${\mathcal{Q}}_{P}$ that are reachable from the root $q_{P}^{r}$ through a multi-hop path that respects the transition rule $\rightarrow_{P}$.666Recall that the root for the construction of the prefix parts is $q_{P}^{r}=(q_{\text{PTS}}^{0},q_{B}^{0})$, where $q_{B}^{0}$ is each possible state in ${\mathcal{Q}}_{B}^{0}$, and for the construction of the suffix parts the root $q_{P}^{r}$ is each possible final state detected during the construction of the prefix parts. We collect these states in the set ${\mathcal{R}}^{\infty}_{P}(q_{P}^{r})$, defined as

[TABLE]

where the reachable set ${\mathcal{R}}_{P}^{m}(q_{P}^{r})$ collects all states $q_{P}\in{\mathcal{Q}}_{P}$ that are reachable from the root $q_{P}^{r}$ in $m$-hops.777The superscript $\infty$ in (16) means that the reachable set collects all states that are reachable from $q_{P}^{r}$ in the state-space ${\mathcal{Q}}_{P}$ in any number of hops.

In mathematical terms, we need to show that

[TABLE]

Since we assume that there exists a solution to Problem 1, if (17) holds, then ${\mathcal{R}}_{P}^{\infty}(q_{P}^{r})\cap\mathcal{X}_{\text{goal}}\neq\emptyset$, which equivalently means that (15) holds, as well.

To show that (17) holds it suffices to show that the event $\{\mathcal{R}_{P}(q_{P})\subseteq\mathcal{V}_{T}^{n},~{}\forall q_{P}\in{\mathcal{V}}_{T}^{n}\}$, is equivalent to the event $\{{\mathcal{R}}^{\infty}_{P}(q_{P}^{r})=\mathcal{V}_{T}^{n}\}$. Then the result follows due to (14) in Corollary V.8. To show this, observe that if $q\in\mathcal{R}_{P}(q_{P})$, with $q_{P}\in{\mathcal{V}}_{T}^{n}$ then, clearly $q$ is reachable from the root $q_{P}^{r}$ through a multi-hop path, since by construction of the tree there is a multi-hop path that connects $q_{P}$ to the root $q_{P}^{r}$, i.e., $q\in{\mathcal{R}}^{\infty}_{P}(q_{P}^{r})$. Next, if $q\in{\mathcal{R}}^{\infty}_{P}(q_{P}^{r})={\mathcal{V}}_{T}^{n}$ then there exists a node $q_{P}\in{\mathcal{R}}^{\infty}_{P}(q_{P}^{r})={\mathcal{V}}_{T}^{n}$, so that $q$ is reachable from $q_{P}$ due to (16), i.e., $q\in{\mathcal{R}}_{P}(q_{P})$, completing the proof. ∎

To show that Algorithm 1 is asymptotically optimal, we need the following corollary that is proved in Appendix A.

Corollary V.10** (Sampling $q_{P}^{\text{new},n}$)**

Consider any state $q_{P}\in{\mathcal{V}}_{T}^{n}$ and any fixed iteration $n$. Then, there exists and infinite number of subsequent iterations $n+k$, where $k\in\mathcal{K}^{\prime}$ is the subsequence defined in Lemma V.5, at which the state $q_{P}\in{\mathcal{V}}_{T}^{n}$ is selected by Algorithm 3 to be the node $q_{P}^{\text{new},n+k}$.

Theorem V.11** (Asymptotic Optimality)**

Assume that there exists an optimal solution to Problem 1. Then, Algorithm 1 is asymptotically optimal, i.e., the optimal motion plan for a given LTL formula $\phi$ will be found with probability 1, as $n_{\text{max}}^{\text{pre}}\to\infty$ and $n_{\text{max}}^{\text{suf}}\to\infty$. In other words, the discrete motion plan $\tau$ that is generated by this algorithm for a given global LTL specification $\phi$ satisfies

[TABLE]

where $J$ is the cost function (2), $J^{*}$ is the optimal cost, and $n_{\text{max}}^{\text{pre}}$ and $n_{\text{max}}^{\text{suf}}$ are the maximum number of iterations of Algorithm 2 for the prefix and suffix part synthesis, respectively.

Proof:

To show that Algorithm 2 is asymptotically optimal, we will show that as $n_{\text{max}}^{\text{pre}}\to\infty$ and $n_{\text{max}}^{\text{suf}}\to\infty$, all states $q_{P}\in{\mathcal{V}}_{T}^{n}$ are connected to the root $q_{P}^{r}$ through the path in the PBA that has the minimum cost. A necessary and sufficient condition for this is to show that as $n_{\text{max}}^{\text{pre}}\to\infty$ and $n_{\text{max}}^{\text{suf}}\to\infty$, the set of edges ${\mathcal{E}}_{T}^{n}$ of the tree ${\mathcal{G}}_{T}^{n}$ constructed by Algorithm 2 contains the transitions between states in the plans $\tau^{\text{pre},*}$ and $\tau^{\text{suf},*}$, where $\tau^{*}=\tau^{\text{pre},*}[\tau^{\text{suf},*}]^{\omega}$ is the optimal motion plan. Specifically, to prove that, we first show that every node $q_{P}\in{\mathcal{V}}_{T}^{n}$ will get rewired only a finite number of times as $n\to\infty$, which means that the cost of each node will converge to a finite number, as $n\to\infty$ (necessary condition that guarantees convergence). Then we show that this means that the cost of every node $q_{P}$ has converged to its optimal cost, which equivalently means that the set of edges ${\mathcal{E}}_{T}^{n}$ of the tree ${\mathcal{G}}_{T}^{n}$ constructed by Algorithm 2 contains the transitions between states in the optimal prefix $\tau^{\text{pre},*}$ and suffix $\tau^{\text{suf},*}$ part (sufficient condition).

To show that every node $q_{P}\in{\mathcal{V}}_{T}^{n}$ will get rewired only a finite number of times as $n\to\infty$ we use contradiction. Assume that as $n\to\infty$, there exists a node $q_{P}$ for which rewiring will take place infinitely often. Equivalently, this means that the path that connects $q_{P}$ to the root $q_{P}^{r}$ of the tree will change infinitely often. This can happen if: (i) The sets ${\mathcal{V}}_{T}^{n}$ and ${\mathcal{E}}_{T}^{n}$ are infinite as $n\to\infty$. This is not possible by construction of the PBA, since $|{\mathcal{V}}_{T}^{n}|\leq|{\mathcal{Q}}_{P}|<\infty$ for all $n\in\mathbb{N}_{+}$; (ii) The sets ${\mathcal{V}}_{T}^{n}$ and ${\mathcal{E}}_{T}^{n}$ are finite but the cost of each node $q_{P}\in{\mathcal{V}}_{T}^{n}$ is not bounded below. This is not possible, by definition of the PBA, since the cost of all states $q_{P}\in{\mathcal{Q}}_{P}$ is bounded below by [math]; and (iii) The sets ${\mathcal{V}}_{T}^{n}$ and ${\mathcal{E}}_{T}^{n}$ are finite but the path that connects $q_{P}$ to $q_{P}^{r}$ in the tree ${\mathcal{G}}_{T}^{n}$, denoted by $\pi^{n}(q_{P})$, reoccurs periodically. This means that there exist constants $\bar{n}$, $K>0$ so that $\pi^{m\bar{n}}(q_{P})=\pi^{m\bar{n}+K}(q_{P})$ for all $n>m\bar{n}$ and $m\in\mathbb{N}_{+}$

In what follows, we show by contradiction that case (iii) is not possible either. With slight abuse of notation, we denote by $\texttt{Cost}^{n}(q_{P})$ the cost of $q_{P}$ at iteration $n$. Since, by assumption, $q_{P}$ gets rewired indefinitely, we have that

[TABLE]

for any $\bar{n},K>0$ and for all $m\in\mathbb{N}_{+}$. Clearly, this contradicts the fact that $\pi^{m\bar{n}}(q_{P})=\pi^{m\bar{n}+K}(q_{P})$ which implies that $\texttt{Cost}^{m\bar{n}}(q_{P})=\texttt{Cost}^{m\bar{n}+K}(q_{P})$. Therefore, as $n\to\infty$, every node $q_{P}\in{\mathcal{V}}_{T}^{n}$ will get rewired only a finite number of times.

Next, we show by contradiction that when rewiring has ended for all nodes in ${\mathcal{V}}_{T}^{n}$, every node in the constructed tree has achieved its optimal cost. Specifically, assume that rewiring has ended for all nodes and that there exists at least one node $q_{P}\in{\mathcal{V}}_{T}^{n}$ that has not reached its optimal cost. This means that there exists at least one pair of nodes $q_{P}\in{\mathcal{V}}_{T}^{n}$ and $q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}$ such that (i) $q_{P}\rightarrow_{P}q_{P}^{\prime}$ and (ii) if $q_{P}$ gets rewired to $q_{P}^{\prime}$ the cost of $q_{P}$ will decrease. However, by Corollary V.10, $q_{P}^{\prime}$ will be selected by Algorithm 3 to be $q_{P}^{\text{new},n+k}$ infinitely often, meaning that $q_{P}^{\prime}$ will eventually get rewired to $q_{P}$ by Algorithm 2. This contradicts the fact that rewiring has ended for all nodes in ${\mathcal{V}}_{T}^{n}$. Therefore, when all nodes have been rewired finitely many times and the rewiring process has terminated, every node $q_{P}$ has achieved its optimal cost.

Finally note that by Theorem V.9, as $n\to\infty$ we have that ${\mathcal{V}}_{T}^{n}={\mathcal{R}}^{\infty}_{P}(q_{P}^{r})$ with probability 1. Since ${\mathcal{R}}_{P}^{\infty}$ is fixed (because ${\mathcal{Q}}_{P}$ is finite), so is ${\mathcal{V}}_{T}^{n}$ as $n\to\infty$. Moreover, since Problem 1 has a solution, ${\mathcal{V}}_{T}^{n}$ also includes the final state $q_{P}^{F}$ that appears in $\tau^{\text{pre},*}$ as $n\to\infty$. Therefore, by the above argument, as $n\to\infty$, every state in ${\mathcal{V}}_{T}^{n}$, including the final state $q_{P}^{F}$, will reach its optimal cost with probability 1. This means that the cost of the path that corresponds to the prefix part constructed by Algorithm 2 that connects the final state $q_{P}^{F}$ to the root $q_{P}^{r}$ will be $\hat{J}(\tau^{\text{pre},*})$. Following the same logic, the cost of the respective suffix part, i.e., the cycle around the final state $q_{P}^{F}$ will be $\hat{J}(\tau^{\text{suf},*})$ completing the proof. ∎

VI Numerical Experiments

In this section, we present two case studies, implemented using MATLAB R2016a on a computer with Intel Xeon CPU at 2.93 GHz and 4 GB RAM, that illustrate our proposed algorithm and compare it to existing methods. The first case study pertains to a motion planning problem with a PBA that has $3,099,363,912$ states. Recall that the state-space of the PBA defined in Definition III.3 has $\Pi_{i=1}^{N}|\mathcal{Q}_{i}||\mathcal{Q}_{B}|$ states. This problem cannot be solved by standard optimal control synthesis algorithms, discussed in Section I, that rely on the explicit construction of the PBA defined in Section III, due to memory requirements. Representing the PBA as an implicit graph and using the uniform-cost search (UCS) algorithm [33, 34] to find the optimal plan also failed to detect a final state within 24 hours. In fact, our implementation for both approaches of the algorithm presented in Section III-A cannot provide a plan for PBA with more than few millions of states and transitions either due to memory requirement or excessively high runtime. This problem cannot be solved by the off-the-shelf model checker PRISM either, due to excessive memory requirements. Our implementation of [23] failed also to provide a motion plan for the considered case study due to the large state-space of the resulting PBA. On the other hand, NuSMV can generate a feasible, but not the optimal, plan that satisfies the considered LTL-based task. A direct comparison with [22] cannot be made, since in [22] samples of the robot positions are drawn from the continuous space, which is not the case here. Note, however, that as the size of the regions that observe the atomic propositions in [22] becomes smaller, more samples are needed to construct expressive enough transition systems that are needed to generate a motion plan. In this case, the state space of the PBA may become too large to store, let alone apply graph search methods. This issue becomes more pronounced, as the size of the NBA increases. Also, scalability in [22] relies on the construction of a sparse graph rather than a tree as in our proposed method. However, sparsity of the graph is lost as the number of samples increases. Moreover, we also compare the proposed control synthesis algorithm to our previous work [24] and we show a significant improvement in terms of scalability, due to the fast exploration of the state-space of the PBA as predicted by Proposition V.1. In the second case study, we consider a motion planning problem with a PBA that has 6,144 states. This state-space is small enough to manipulate and construct an optimal plan using the standard method described in Section III-A. In this simulation study, we examine the performance of the proposed algorithm in terms of runtime and optimality. In what follows, we consider discrete uniform distributions for both $f_{\text{rand}}$ and $f_{\text{new}}$ for all iterations $n$ and also we assume that the weights $w_{i}$ defined in Definition 1 represent distance between locations.

VI-A Case Study I

In the first simulation study, we consider a team of $N=9$ robots residing in a workspace with $W=9$ regions of interest. The transition system describing the motion of each robot has $|\mathcal{Q}_{i}|=9$ states and 39 transitions, including self-loops around each state, as shown in Figure 4(a). The collaborative task that is assigned to the robots describes an intermittent connectivity problem, that was defined in our previous work [4]. Specifically, the robots move along the edges of a mobility graph and communicate only when they meet at the vertices of this graph. The communication network is intermittently connected if communication occurs at the vertices of the mobility graph infinitely often. This intermittent connectivity requirement can be captured by a global LTL formula, which for the case study at hand takes the form $\phi=[\Box\Diamond(\pi_{1}^{\ell_{5}}\wedge\pi_{2}^{\ell_{5}})]\wedge[\Box\Diamond(\pi_{2}^{\ell_{1}}\wedge\pi_{3}^{\ell_{1}}\wedge\pi_{4}^{\ell_{1}})]\wedge[\Box\Diamond(\pi_{4}^{\ell_{7}}\wedge\pi_{5}^{\ell_{7}}\wedge\pi_{6}^{\ell_{7}})]\wedge[\Box\Diamond(\pi_{6}^{\ell_{8}}\wedge\pi_{7}^{\ell_{8}})]\wedge[\Box\Diamond(\pi_{7}^{\ell_{4}}\wedge\pi_{8}^{\ell_{4}})]\wedge[\Box\Diamond(\pi_{8}^{\ell_{3}}\wedge\pi_{9}^{\ell_{3}})]\wedge[\neg(\pi_{1}^{\ell_{5}}\wedge\pi_{2}^{\ell_{5}})\mathcal{U}\pi_{1}^{\ell_{7}}]$. In words, (a) robots 1 and 2 need to meet at location $\ell_{5}$ infinitely often, (b) robots 2, 3 and 4 need to meet at location $\ell_{1}$, infinitely often, (c) robots 4, 5, and 6 need to meet at location $\ell_{7}$, infinitely often, (d) robots 6 and 7 need to meet at location $\ell_{8}$ infinitely often, (e) robots 7 and 8 need to meet at location $\ell_{4}$, infinitely often, (f) robots 8 and 9 need to meet at location $\ell_{3}$, infinitely often, and (g) robots 1 and 2 should never meet at location $\ell_{5}$ until robot $1$ visits location $\ell_{7}$ to collect some available information. This LTL formula corresponds to a NBA with $|\mathcal{Q}_{B}|=8$ states, $|{\mathcal{Q}}_{B}^{0}|=1$, $|{\mathcal{Q}}_{B}^{F}|=1$, and $36$ transitions.888The translation of the LTL formula to a NBA was made by the tool developed in [36].

In Algorithm 1, we select $n_{\text{max}}^{\text{pre}}=n_{\text{max}}^{\text{suf}}=6500$. The first final state was detected in $13$ minutes. After 6500 iterations that took approximately 30 minutes, $|{\mathcal{P}}|=11$ final states were detected and a tree $\mathcal{G}_{T}$ with $|\mathcal{V}_{T}|=23893$ nodes was constructed. Figure 5(a) depicts the number of rejected states per iteration $n$ of Algorithm 2, i.e., samples $q_{P}^{\text{new},n}\notin{\mathcal{V}}_{T}^{n}$ that cannot be added to ${\mathcal{V}}_{T}^{n}$ at each iteration $n$, during the construction of the prefix part. Observe in Figure 5(a), that at every iteration $n$, there is at least one sample $q_{P}^{\text{new}}$ that either is added to the tree if $q_{P}^{\text{new},n}\notin{\mathcal{V}}_{T}^{n}$ or enables the rewiring operation if $q_{P}^{\text{new},n}\in{\mathcal{V}}_{T}^{n}$. Given the detected final states, the construction of the suffix part follows, where the average time to compute each suffix part $\tau_{\text{pre},a}$, $a=\{1,\dots,11\}$ was 17 minutes. Given the prefix and suffix parts, the resulting optimal motion plan that satisfies the considered LTL task was synthesized in less than 1 second and its cost is $J(\tau)=\hat{J}(\tau^{\text{pre}})+\hat{J}(\tau^{\text{suf}})=387.2293+387.2293=774.4586$ meters. Notice also that storage of each of the constructed trees required approximately only 3MBs while the computation of paths over the trees associated with either the prefix or the suffix part required 0.02 seconds on average rendering our approach resource and computationally efficient.

VI-A1 Comparison with [24]

Next, we compare the proposed sampling approach with our previous work [24] in terms of their ability to minimize cost and grow the tree as a function of runtime. Before presenting the comparative results, recall first that [24] consists of two parts. In the first part, samples are drawn randomly from ${\mathcal{Q}}_{P}$. If these samples do not already belong to the tree but they are reachable from the tree, then the tree is extended towards them and the rewiring step follows, as in our proposed algorithm. If they are not reachable from the tree, then they are rejected, as in our proposed algorithm too. On the other hand, if these samples already belong to the tree, then they are rejected in [24] while in our proposed algorithm, rewiring to these samples follows. A more detailed description of this first part can be found in Algorithm 1 and 7 in [24]. The second part of [24], that does not exist in our sampling-based algorithm, pertains to the optimization of the tree structure. Specifically, once the first part of [24] has been executed for a user-specified number of iterations, then a rewiring-based algorithm follows that minimizes the cost of each node; see Algorithm 5 in [24]. This algorithm is terminated once the set of edges of the tree stops changing and it is necessary to obtain asymptotic optimality of the method in [24].

To compare Algorithm 1 and [24], we executed Algorithm 1 and the first part of [24] three times for a duration of about 15 hours per experiment. Notice that Algorithm 1 detected 338 final states in 15.42 hours in average while [24] found 108 final states in 15.65 hours in average. In every experiment, every time a new final state was detected, we computed the cost of the best prefix part, i.e., the minimum cost among all detected final states, and the size of the constructed tree. The evolution of the average cost with time is illustrated in Figure 6 for both algorithms. Observe in Figure 6 that the proposed algorithm can find the first final state in 30 minutes in average, while [24] can do so in 3.5 hours, approximately. Also, observe in Figure 6 that the prefix part generated by [24] has always a higher cost than the one synthesized by Algorithm 1. The reason is that the first part of [24] only partially optimizes the tree, as rewiring occurs only for samples that do not already exist in the tree but they are reachable from it. As discussed before, optimization of the tree structure is accomplished by the second part of [24] which, however, requires additional computational time. Figure 6 also shows how the cost of the best prefix part changes with time during the execution of the second part of [24]. Observe that when [24] has optimized the tree that was built until the detection of the first final state (the last triangle in the top green dashed line in Figure 6), our proposed method has already detected 338 final states and has also constructed a much better prefix part (the last red rhombus in Figure 6), in terms of the cost function $\hat{J}(\tau^{\text{pre}})$ defined in (1).

Figure 7, shows how the average size of the tree changes with time during the execution of our proposed algorithm and the first part of [24]. Observe that [24] explores the state-space of the PBA faster than our proposed method, since at every iteration $n$ the first part of [24] executes fewer operations due to the way the rewiring step is triggered, as discussed before. The time required to execute the second part of [24] that optimizes the tree structure is also depicted in Figure 7, that shows that [24] is much slower than our proposed method in synthesizing optimal plans.

Finally, in Figure 7, we present the average size of the constructed trees per iteration $n$ during the execution of the proposed algorithm and the first part of [24]. Observe that at any given iteration $n$ the proposed method has built a much larger tree than [24]. The reason is that in [24] samples are taken arbitrarily from the state space ${\mathcal{Q}}_{\text{PTS}}$ and, therefore, they are not necessarily reachable from the constructed tree and, as a result, they are rejected. On the other hand, here, samples are drawn from reachable sets accelerating the construction of the tree with respect to iterations $n$, as shown in Proposition V.1.

VI-A2 Comparison with off-the-shelf model checkers

Notice that the off-the-shelf model checker PRISM could not verify the considered LTL specification due to memory requirements. Specifically, PRISM could verify only a smaller part of the considered LTL formula that involved 6 robots, which was $\bar{\phi}=[\Box\Diamond(\pi_{1}^{\ell_{5}}\wedge\pi_{2}^{\ell_{5}})]\wedge[\Box\Diamond(\pi_{2}^{\ell_{1}}\wedge\pi_{3}^{\ell_{1}}\wedge\pi_{4}^{\ell_{1}})]\wedge[\Box\Diamond(\pi_{4}^{\ell_{7}}\wedge\pi_{5}^{\ell_{7}}\wedge\pi_{6}^{\ell_{7}})]$. In this case, the size of the state-space of the PBA was $|\mathcal{Q}_{P}|=9,765,625$. PRISM finished the model-checking process in 1.5 minutes while our method found a plan within 17 minutes. We also applied NuSMV to this problem that was able to generate a feasible plan within few seconds with cost equal to $J(\tau)=J(\tau^{\text{pre}})+J(\tau^{\text{suf}})=336.1216+336.1216=672.2431$ meters while our method found a plan with cost $J(\tau)=J(\tau^{\text{pre}})+J(\tau^{\text{suf}})=298.5286+269.6571=568.1857$ meters. Notice that NuSMV can only generate a feasible plan and not the optimal plan, as our proposed algorithm does. The optimal control synthesis method described in Section III-A failed to design a plan that satisfies the considered LTL formula and so did the algorithm presented in [23] due to excessive memory requirements.

VI-B Case Study II

In the second simulation study, we consider a team of $N=2$ robots. The transition system describing the motion of each robot is shown in Figure 4(b), and has $|\mathcal{Q}_{i}|=16$ states and $70$ transitions, including self-loops around each state. The assigned task is expressed in the following temporal logic formula: $\phi=\square\Diamond(\pi_{1}^{\ell_{6}}\wedge\Diamond(\pi_{2}^{\ell_{14}}))\wedge\square(\neg\pi_{1}^{\ell_{9}})\wedge\square(\pi_{2}^{\ell_{14}}\rightarrow\bigcirc(\neg\pi_{2}^{\ell_{14}}{\mathcal{U}}\pi_{1}^{\ell_{4}}))\wedge(\Diamond\pi_{2}^{\ell_{12}})\wedge(\square\Diamond\pi_{2}^{\ell_{10}})$ where the respective NBA has $|\mathcal{Q}_{B}|=24$ states with $|{\mathcal{Q}}_{B}^{0}|=1$, $|{\mathcal{Q}}_{B}^{F}|=4$, and $163$ transitions. In words, this LTL-based task requires (a) robot 1 to visit location $\ell_{6}$, (b) once (a) is true robot 2 to visit location $\ell_{14}$, (c) conditions (a) and (b) to occur infinitely often, (d) robot 1 to always avoid location $\ell_{9}$, (e) once robot 2 visits location $\ell_{14}$, it should avoid this area until robot 1 visits location $\ell_{4}$, (f) robot 2 to visit location $\ell_{12}$ eventually, and (g) robot 2 to visit location $\ell_{10}$ infinitely often. In this simulation study, the state space of the PBA consists of $\Pi_{i=1}^{N}|\mathcal{Q}_{i}||\mathcal{Q}_{B}|=6,144$ states, which is small enough so that the method discussed in Section III-A can be used to find the optimal plan. The cost of the optimal plan is $J^{*}=14.6569$ meters.

Algorithm 1 was run for various values of the parameters $n_{\text{max}}^{\text{pre}}$ and $n_{\text{max}}^{\text{suf}}$. Observe in Figure 8 that as we increase $n_{\text{max}}^{\text{pre}}$ and $n_{\text{max}}^{\text{suf}}$, the cost of the resulting plans decreases and eventually the optimal plan is found, as expected due to Theorem V.11. The number of detected final states and runtime for each case are also depicted in the same figure. PRISM verified that there exists a motion plan that satisfies the considered LTL formula in few seconds and NuSMV in less than 1 second. However, neither of them can synthesize the optimal motion plan that satisfies the considered LTL task. For instance, the cost of the plan generated by NuSMV is $30.8995$ meters while our algorithm can find the optimal plan with cost $J^{*}=14.6569$, as shown in Figure 8. Figure 5(b) depicts the number of rejected states with respect to the iterations $n$ of Algorithm 2. Notice that, as in the previous simulation study, at every iteration $n$ there is at least one state that is added to the tree.

VII Conclusion

In this paper we proposed a sampling-based control synthesis algorithm for multi-robot systems under global linear temporal logic (LTL) formulas. Existing planning approaches under global temporal goals rely on graph search techniques applied to a synchronous product automaton constructed among the robots. In this paper, we proposed a new sampling-based algorithm to build incrementally trees that approximated the state-space and transitions of the synchronous product automaton increasing in this way significantly scalability of our method compared to existing model-checking approaches. Moreover, we showed that the proposed algorithm is probabilistically complete and asymptotically optimal. Finally, we presented numerical experiments that show that it can be used to synthesize optimal plans from product automata with billions of states, which was not possible using standard optimal control synthesis algorithms or off-the-shelf model checkers.

Appendix A Proofs of Lemmas

A-A Proof of Lemma V.4

The proof of this results relies on Lemma V.3. Let $A^{\text{rand},n+k}(q_{P})=\{q_{P}^{\text{rand},n+k}=q_{P}\}$, with $k\in\mathbb{N}$, denote the event that at iteration $n+k$ of Algorithm 2 the state $q_{P}\in{\mathcal{V}}_{T}^{n}$ is selected by the function Sample to be the node $q_{P}^{\text{rand},n+k}$ [line 3, Alg. 3]. Also, let $\mathbb{P}(A^{\text{rand},n+k}(q_{P}))$ denote the probability of this event, i.e., $\mathbb{P}(A^{\text{rand},n+k}(q_{P}))=f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}^{n+k})$.

Next, define the infinite sequence of events $A^{\text{rand}}=\{A^{\text{rand},n+k}(q_{P})\}_{k=0}^{\infty}$, for a given node $q_{P}\in{\mathcal{V}}_{T}^{n}$. In what follows, we show that the series $\sum_{k=0}^{\infty}\mathbb{P}(A^{\text{rand},n+k}(q_{P}))$ diverges and then we complete the proof by applying Lemma V.3. Recall first that the size of ${\mathcal{V}}_{T}^{n+k}$ cannot grow arbitrarily large, since it holds that $|{\mathcal{V}}_{T}^{n+k}|\leq|{\mathcal{Q}}_{P}|<\infty$, for all $k\in\mathbb{N}$. Also, by Assumption IV.1(ii), we have that for a given $q_{P}\in{\mathcal{V}}_{T}^{n}$, the probability $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}^{n+k})$ decreases monotonically with respect to $|{\mathcal{V}}_{T}^{n+k}|$. From these two observations we deduce that

[TABLE]

for all $k\in\mathbb{N}$, where $f_{\text{rand}}(q_{P}|{\mathcal{Q}}_{P})$ is the probability assigned to selecting the state $q_{P}\in{\mathcal{V}}_{T}^{n}$ as $q_{P}^{\text{rand},n+k}$ when ${\mathcal{V}}_{T}^{n+k}={\mathcal{Q}}_{P}$. Note that $f_{\text{rand}}(q_{P}|{\mathcal{Q}}_{P})$ is a strictly positive term due to Assumption IV.1(i). Also, $f_{\text{rand}}(q_{P}|{\mathcal{Q}}_{P})$ is constant, by Assumption IV.1(ii), since ${\mathcal{Q}}_{P}$ is a fixed set.

Next, since (19) holds for all $k\in\mathbb{N}$, we have that

[TABLE]

Since for any state $q_{P}\in{\mathcal{Q}}_{P}$, we have that $f_{\text{rand}}(q_{P}|{\mathcal{Q}}_{P})$ is a strictly positive constant term, the infinite $\sum_{k=0}^{\infty}f_{\text{rand}}(q_{P}|{\mathcal{Q}}_{P})$ diverges. Then, we conclude that

[TABLE]

Combining (21) and the fact that the events $A^{\text{rand},n+k}(q_{P})$ are independent by Assumption IV.1(iii), we get that $\mathbb{P}(\limsup_{k\to\infty}A^{\text{rand},n+k}(q_{P}))=1,$ due to Lemma V.3. In other words, the events $A^{\text{rand},n+k}(q_{P})$ occur infinitely often, for all $q_{P}\in{\mathcal{V}}_{T}^{n}$. This equivalently means that for every node $q_{P}\in{\mathcal{V}}_{T}^{n}$, for all $n\in\mathbb{N}_{+}$, there exists an infinite subsequence $\mathcal{K}\subseteq\mathbb{N}$ so that for all $k\in\mathcal{K}$ it holds $q_{P}^{\text{rand},n+k}=q_{P}$, completing the proof.999Note that the subsequence ${\mathcal{K}}$ is different across the nodes $q_{P}\in{\mathcal{V}}_{T}^{n}$.

Remark A.1** (Lemma V.4)**

The result shown in Lemma V.4 holds even if Assumption IV.1(ii) does not hold, i.e., if the density function $f_{\text{rand}}(q_{P}|{\mathcal{V}}_{T}^{n})$ changes every iteration $n$ for a fixed set ${\mathcal{V}}_{T}^{n}$ and a fixed node $q_{P}\in{\mathcal{V}}_{T}^{n}$, and even if it does not decrease monotonically with the cardinality of ${\mathcal{V}}_{T}^{n}$, as long as this varying density function $f_{\text{rand}}^{n}(q_{P}|{\mathcal{V}}_{T}^{n})$ is bounded below by a sequence $g^{n}(q_{P}|{\mathcal{V}}_{T}^{n})$, such that $\sum_{n=1}^{\infty}g^{n}(q_{P}|{\mathcal{V}}_{T}^{n})=\infty$, for all $q_{P}\in{\mathcal{V}}_{T}^{n}$. This will ensure that $\sum_{k=0}^{\infty}\mathbb{P}(A^{\text{rand},n+k}(q_{P}))=\sum_{k=0}^{\infty}f_{\text{rand}}^{n+k}(q_{P}|{\mathcal{V}}_{T}^{n+k})\geq\sum_{k=0}^{\infty}g^{n+k}(q_{P}|{\mathcal{V}}_{T}^{n+k})=\infty$, which replaces (20) and still yields (21).

A-B Proof of Lemma V.5

This proof relies on Lemma V.3 and resembles the proof of Lemma V.4. Let $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}$ and define the infinite sequence of events $A^{\text{new}}=\{A^{\text{new},n+k}(q_{\text{PTS}})\}_{k=0}^{\infty}$, for any given state $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$, where $A^{\text{new},n+k}(q_{\text{PTS}})=\{q_{\text{PTS}}^{\text{new},n+k}=q_{\text{PTS}}\}$, for $k\in\mathbb{N}$, denotes the event that at iteration $n+k$ of Algorithm 2 the state $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ is selected by the function Sample to be the node $q_{\text{PTS}}^{\text{new},n+k}$ [line 3, Alg. 3], given a state $q_{P}^{\text{rand},n+k}=(q_{\text{PTS}}^{\text{rand},n+k},q_{B}^{\text{rand},n+k})\in{\mathcal{V}}_{T}^{n+k}$.101010Recall that the reachable set ${\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ defined in (6) remains the same for all iterations $n$, for a given state $q_{\text{PTS}}^{\text{rand},n}$. Moreover, let $\mathbb{P}(A^{\text{new},n+k}(q_{\text{PTS}}))$ denote the probability of this event, i.e., $\mathbb{P}(A^{\text{new},n+k}(q_{\text{PTS}}))=f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand},n+k})$.

Now, consider those iterations $n+k$ with $k\in\mathcal{K}$ such that $q_{P}^{\text{rand},n+k}=q_{P}^{\text{rand},n}$ by Lemma V.4. We will show that the series $\sum_{k\in{\mathcal{K}}}\mathbb{P}(A^{\text{new},n+k}(q_{\text{PTS}}))$ diverges and then we will use Lemma V.3 to show that $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n+k})$ will be selected infinitely often to be node $q_{\text{PTS}}^{\text{new},n+k}$.

Since $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n+k})$ we have that $\mathbb{P}(A^{\text{new},n+k}(q_{\text{PTS}}))=f_{\text{new}}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand},n+k})$ is a strictly positive constant for all $k\in{\mathcal{K}}$, by Assumption IV.2(i) and IV.2(ii). Therefore, we have that $\sum_{k\in{\mathcal{K}}}\mathbb{P}(A^{\text{new},n+k}(q_{\text{PTS}}))$ diverges, since it is an infinite sum of a strictly positive constant term. Using this result along with the fact that the events $A^{\text{new},n+k}(q_{\text{PTS}})$ are independent, by Assumption IV.2(iii), we get that $\mathbb{P}(\limsup_{k\to\infty}A^{\text{new},n+k}(q_{\text{PTS}}))=1,$ due to Lemma V.3. In words, this means that the events $A^{\text{new},n+k}(q_{\text{PTS}})$ for $k\in\mathcal{K}$ occur infinitely often. Thus, for every node $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$ for all $n\in\mathbb{N}_{+}$, there exists an infinite subsequence $\mathcal{K}^{\prime}\subseteq\mathcal{K}$ so that for all $k\in\mathcal{K}^{\prime}$ it holds $q_{\text{PTS}}^{\text{new},n+k}=q_{\text{PTS}}$, completing the proof.

Remark A.2** (Lemma V.5)**

Lemma V.5 holds even if Assumption IV.2(ii) does not hold, i.e., if for any given node $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}$, the density function $f_{\text{new}}$ changes with iterations $n+k$, where $k\in{\mathcal{K}}$, for which $q_{P}^{\text{rand},n}=q_{P}^{\text{rand},n+k}$, as long as it is bounded below by a sequence $h^{n+k}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand},n})$, for all $k\in{\mathcal{K}}$, such that $\sum_{k\in{\mathcal{K}}}h^{n+k}(q_{\text{PTS}}|q_{\text{PTS}}^{\text{rand},n})=\infty$, for all $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$.

A-C Proof of Corollary V.6

Recall that a state $q_{P}=(q_{\text{PTS}},q_{B})$ belongs to ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ if $q_{P}^{\text{rand},n}\rightarrow_{P}q_{P}$, i.e., if (i) $q_{\text{PTS}}^{\text{rand},n}\rightarrow_{\text{PTS}}q_{\text{PTS}}$ and (ii) $q_{B}^{\text{rand},n}\stackrel{{\scriptstyle L(q_{\text{PTS}}^{\text{rand},n})}}{{\longrightarrow_{B}}}q_{B}$. Then, to prove this result, it suffices to show that all states $q_{P}$ that satisfy both conditions (i) and (ii) are sampled infinitely often, which is a direct result from Lemma V.5.

Specifically, observe first that, due to Lemma V.5, for all states $q_{\text{PTS}}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$, i.e., for all states that satisfy condition (i), there exists an infinite number of iterations $n+k$, at which they will selected to be the nodes $q_{\text{PTS}}^{\text{new},n+k}$ with probability 1, for all $n\in\mathbb{N}$. Second, given a state $q_{\text{PTS}}^{\text{new},n}\in{\mathcal{R}}_{\text{PTS}}(q_{\text{PTS}}^{\text{rand},n})$, the states $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(b))$, for all $b\in\{1,\dots,|{\mathcal{Q}}_{B}|\}$ are created, by construction of Algorithm 2. Therefore, given a state $q_{\text{PTS}}^{\text{new},n}$, if there exists $b\in\{1,\dots,|{\mathcal{Q}}_{B}|\}$ such that $q_{B}^{\text{rand},n}\stackrel{{\scriptstyle L(q_{\text{PTS}}^{\text{rand},n})}}{{\rightarrow_{B}}}{\mathcal{Q}}_{B}(b)$, then the state $q_{P}^{\text{new},n}=(q_{\text{PTS}}^{\text{new},n},{\mathcal{Q}}_{B}(b))\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ that satisfies (ii) will be sampled/constructed infinitely often.111111Recall that the reachable set ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ defined in (6) remains the same for all iterations $n$, for a given state $q_{P}^{\text{rand},n}$. Thus, for all states $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ there exists an infinite number of iterations $n+k$, with $k\in{\mathcal{K}}^{\prime}\subseteq{\mathcal{K}}$, at which they will be selected by Algorithm 3 to be the node $q_{P}^{\text{new},n+k}$ completing the proof.

A-D Proof of Lemma V.7

First note that (13) trivially holds for all states $q_{P}^{\text{rand},n}$ that satisfy ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})=\emptyset$. Hence, in what follows we consider only states $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}$ that satisfy ${\mathcal{R}}_{P}(q_{P}^{\text{rand},n})\neq\emptyset$. The proof of this result relies on Corollary V.6. Specifically, recall that, due to Corollary V.6, for all states $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$, there exists an infinite number of iterations $n+k$, $k\in{\mathcal{K}}^{\prime}\subseteq{\mathcal{K}}$, such that $q_{P}^{\text{new},n+k}=q_{P}$. This means that with probability 1, there exists an iteration $n+k$ of Algorithm 2 at which the state $q_{P}^{\text{new},n+k}=q_{P}$, will be sampled.

Since this iteration $n+k$ satisfies $q_{P}^{\text{new},n+k}\in\mathcal{R}_{P}(q_{P}^{\text{rand},n})$, we get that $q_{P}^{\text{rand},n}\in{\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n+k}}(q_{P}^{\text{new},n+k})\subseteq{\mathcal{V}}_{T}^{n+k}$. This follows from the definition of ${\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n+k}}(q_{P}^{\text{new},n+k})$ in (7) and the fact that since $q_{P}^{\text{rand},n}$ belongs to ${\mathcal{V}}_{T}^{n}$ it also belongs to ${\mathcal{V}}_{T}^{n+k}$. Therefore, ${\mathcal{R}}^{\rightarrow}_{{\mathcal{V}}_{T}^{n+k}}(q_{P}^{\text{new},n+k})\neq\emptyset$, which means that the state $q_{P}^{\text{new},n+k}=q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ will be added to the tree at iteration $n+k$ by construction of Algorithm 4; see line 4 in Algorithm 4. We conclude, that for all states $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ there exists a subsequent iteration $n+k$ at which they will be added to the tree with probability 1.121212If the states $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ already belong to the tree then the rewiring step follows. In mathematical terms, this result can be written as $\lim_{k\rightarrow\infty}\mathbb{P}\left(\{\mathcal{R}_{P}(q_{P}^{\text{rand},n})\subseteq\mathcal{V}_{T}^{n+k}\}\right)=1$ completing the proof.

A-E Proof of Corollary V.8

This result is due to Lemmas V.4 and V.7. Specifically, by Lemma V.7, we have that

[TABLE]

for a given state $q_{P}^{\text{rand},n}\in{\mathcal{V}}_{T}^{n}\subseteq{\mathcal{V}}_{T}^{n+k}$ and any iteration $n\in\mathbb{N}_{+}$. Also, by Lemma V.4, we have that every state $q_{P}\in{\mathcal{V}}_{T}^{n}$ will be selected infinitely often to be the node $q_{P}^{\text{rand},n+k}$, as $k\to\infty$. Therefore, we get that (22) holds for all states $q_{P}\in{\mathcal{V}}_{T}^{n}$, i.e.,

[TABLE]

Since (23) holds for any iteration $n\in\mathbb{N}_{+}$, we can rewrite (23) as $\lim_{n\rightarrow\infty}\mathbb{P}\left(\{\mathcal{R}_{P}(q_{P})\subseteq\mathcal{V}_{T}^{n}\}\right)=1,~{}\forall q_{P}\in{\mathcal{V}}_{T}^{n}$ completing the proof.

A-F Proof of Corollary V.10

The proof relies on Corollary V.6 and Lemma V.4. From Lemma V.4, we have that for every state $q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}$ there exists an infinite number of iterations $n+k$, with $k\in{\mathcal{K}}$, at which the state $q_{P}^{\prime}$ is selected by Algorithm 3 to be the node $q_{P}^{\text{rand},n+k}$. Also, for any iteration $n$ and for any state $q_{P}^{\text{rand},n}$, we know from Corollary V.6 that for every state $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\text{rand},n})$ there exists an infinite number of subsequent iterations $n+k$, with $k\in{\mathcal{K}}^{\prime}\subseteq{\mathcal{K}}$, at which the state $q_{P}$ is selected by Algorithm 3 to be the node $q_{P}^{\text{new},n+k}$, given a node $q_{P}^{\text{rand},n}$. Combining these two results, we get that for every state $q_{P}\in{\mathcal{R}}_{P}(q_{P}^{\prime})$, and for all $q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}$, there exists an infinite number of subsequent iterations $n+k$, with $k\in{\mathcal{K}}^{\prime}$, at which the state $q_{P}$ is selected to be the node $q_{P}^{\text{new},n+k}$. Equivalently, this means that for every state $q_{P}\in\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$ there exists an infinite number of iterations $n+k$, with $k\in{\mathcal{K}}^{\prime}$, at which the state $q_{P}$, is selected to be the node $q_{P}^{\text{new},n+k}$. Then, it suffices to show that the set ${\mathcal{V}}_{T}^{n}$ is a subset of the set $\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$. This would mean that for any state $q_{P}\in{\mathcal{V}}_{T}^{n}$, there exists and infinite number of iterations $n+k$, with $k\in{\mathcal{K}}^{\prime}$, at which the state $q_{P}\in{\mathcal{V}}_{T}^{n}$, is selected by Algorithm 3 to be the node $q_{P}^{\text{new},n+k}$.

To show that ${\mathcal{V}}_{T}^{n}\subseteq\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$, we will show that if $q\in{\mathcal{V}}_{T}^{n}$ then $q\in\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$. Consider a node $q\in{\mathcal{V}}_{T}^{n}$. Then, by construction of the tree, we have that there exists another node $q^{\prime}\in{\mathcal{V}}_{T}^{n}$, such that $\texttt{parent}(q)=q^{\prime}\in{\mathcal{V}}_{T}^{n}$, which means $q\in{\mathcal{R}}_{P}(q^{\prime})$. Observe that ${\mathcal{R}}_{P}(q^{\prime})\subseteq\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$, since $q^{\prime}\in{\mathcal{V}}_{T}^{n}$ by assumption. Therefore, we have that $q\in{\mathcal{R}}_{P}(q^{\prime})\subseteq\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$, i.e., $q\in\cup_{q_{P}^{\prime}\in{\mathcal{V}}_{T}^{n}}{\mathcal{R}}_{P}(q_{P}^{\prime})$ completing the proof.