# Temporal Logic Planning and Receding Horizon Control for Signal Source Localization
## 4 Receding Horizon Control with Temporal Logic Planning
### Receding Horizon Control with Temporal Logic Planning  
According to the above temporal logic planning, we give the basic steps of the proposed control approach. (1) At \(k=0\), we initialize the node sets \(\Delta_{A}\), \(\Delta_{B}\), \(\Delta_{C}\), and \(\Delta_{D}\) where \(\Delta_{A1},\Delta_{A2},\ldots,\in\Delta_{A}\), \(\Delta_{B1},\Delta_{B2},\ldots,\in\Delta_{B}\), \  
**Case 2**: \(\mathcal{L}(\mathbf{p}_{k},\mathbf{p}_{n})>0\), and exist a \(z(z\in\{1,...,N\})\) such that \(\mathcal{L}(\mathbf{p}_{z|k-1}^{*},\mathbf{p}_{n})=0,\mathbf{p}_{n}\in\Delta_{A1}\). \[\mathbf{u}_{k}^{*} = \arg\min_{\mathbf{u}(k)}\ \sum_{l=1}^{N}\sum_{j=1}^{M}\left(\alpha|\|p_{k}(l)- \hat{p}_{k}^{j}(l)\|-d|+\beta|v_{k}(l)-\hat{v}_{k}^{j}(l)\|\right)\] (13) s.t. \[(1),\mathcal{L}(\mathbf{p}_{z-1|k},\mathbf{p}_{n})=0\] \[p_{k}(l)\in\mathcal{X},v_{k}(l)\in\mathcal{V},u_{k}(l-1)\in \mathcal{U}\]  
(3) Repeat step (2) until all elements in \(\Delta_{A}\) have arrived. Then we use \(\Delta_{B}\), \(\Delta_{C}\), \(\Delta_{D}\), and \(\Delta\) to replace \(\Delta_{A}\). (4) Repeat steps (2) and (3). In the following, the proposed control approach is summarized in Algorithm 1, and Theorem 1 describes the corresponding characteristics. **Theorem 1**. : _Consider the kinematics of robot (1). Algorithm 1 is practicable for any initial position in the application regions under an LTL formula \(\phi\) such that there exists a movement trajectory along which the robot can avoid obstacles and find the signal sources._  
Proof. : At \(k=0\), an initial trajectory can be easily generated. By induction, a sequence \(\mathbf{x}^{*}=x^{*}(1|k-1),\ldots,x^{*}(N|k-1)\) at time \(k-1\) can be attained. Hence, the corresponding sequence in \(T\) is \(\mathbf{q}^{*}=q_{1|k-1}^{*},\ldots,q_{N|k-1}^{*}\). According to Definitions 2 and 3, one can obtain \(\mathbf{p}^{*}=\mathbf{p}_{1|k-1}^{*},\ldots,\mathbf{p}_{N|k-1}^{*}\) in the automaton \(P\). At time \(k\), based on \(\widehat{x}(l|k)=x^{*}(l+1|k-1)\), \(l\in\{1,\ldots,N-1\}\), a sequence \(\widehat{\mathbf{x}}=\widehat{x}(1|k),\ldots,\widehat{x}(N-1|k)\) can be directly constructed. When conditions satisfy Case 1, we have \(\widehat{x}(N|k)\) such that \(\mathcal{L}(\mathbf{p}_{N|k},\mathbf{p}_{n})\leq\mathcal{L}(\mathbf{p}_{N|k-1},\mathbf{p}_{n})\). When the conditions meet Case 2, we have a sequence \(\widehat{\mathbf{x}}=\widehat{x}(1|k),\ldots,\widehat{x}(N|k)\) where \(\widehat{x}(1|k)=x^{*}(2|k-1),\ldots,\widehat{x}(z-1|k)=x^{*}(z|k-1)\) and \(\widehat{x}(N|k)=x^{*}(z|k-1)\). Therefore, we can conclude that there exist solutions for the proposed control at \(k=0,1,\ldots\). At time \(k\), assume that the current conditions satisfy Case 1. We have \(\mathcal{L}(\mathbf{p}_{N|k-\xi}^{*},\mathbf{p}_{n})\geq\mathcal{L}(\mathbf{p}_{N|k}^{*}, \mathbf{p}_{n})\geq\ldots\) where \(k\geq\xi\geq 0\). Since the number of nodes in \(P\) is finite, there is a time step \(z\) such that \(\mathcal{L}(\mathbf{p}_{N|k+z}^{*},\mathbf{p}_{n})=0\). Then, the current conditions meet Case 2. We have \(\mathcal{L}(\mathbf{p}_{k+z}^{*},\mathbf{p}_{n})=0\). In terms of \(\Delta_{A}\), \(\Delta_{B}\), \(\Delta_{C}\), \(\Delta_{D}\), and \(\Delta\), along with the steps to repeat, the robot can locate all the signal sources, and the trajectory satisfies the given LTL formula. Moreover, according to (12) and (13), the robot keeps a safe distance to avoid obstacles. ```
/*Initialization*/  Initialize the particle filter and the parameters of received signal strength model (2) such as \(c\), \(\alpha\), \(d_{a}\), \(\varphi\), and \(\lambda\);  Initialize the robot' parameters and give the LTL formula \(\phi\);  Build a state transition system and obtain an acceptable set of nodes \(\Delta\) based on the results of the division;  Initialize \(\Delta_{A1}\), \(\Delta_{A2}\ldots\) in \(\Delta_{A}\), \(\Delta_{B1}\), \(\Delta_{B2}\ldots\) in \(\Delta_{B}\), \(\Delta_{C1}\), \(\Delta_{C2}\ldots\) in \(\Delta_{C}\), and \(\Delta_{D1}\), \(\Delta_{D2}\ldots\) in \(\Delta_{D}\).