# Temporal Logic Planning and Receding Horizon Control for Signal Source Localization
## 1 Introduction  
In the last decade, signal source localization has received much attention from researchers [1; 2; 3; 4; 5; 6; 7; 8] since this problem is easily found in nature and society, such as searching for odor sources, rescuing victims, and detecting electromagnetic sources, to name a few. In order to deal with this problem, some control strategies have been proposed [6; 8; 9]. For example, in [8], [PERSON] et al. used a probability map to label the positions of signal sources and designed a controller to enable the robot to move toward the signal source. In [6], [PERSON] et al. used particle filters to estimate the position of a signal source and designed movement for the behavior of the leader to search for signal clues. It should be pointed out that these control strategies consist of a decision level and a control level. At the decision level, source positions are estimated by the probability method or the particle filter [10], such as the grid probability method [8] and the particle filter [9]. At the control level, in terms of the estimated source position, the corresponding controller controls the robot to move toward the possible source positions. However, there exist two drawbacks to the control approaches described above. One drawback is that some specifications for signal source localization are not considered. For example, a wide search area is usually divided into Region 1, Region 2, Region 3, Region 4, and so on. In each region, the positions of obstacles and signal sources are different. Correspondingly, a task specification can be described as \"The mobile robot is required to orderly visit each region and search for signal sources while avoiding obstacles\". These task specifications can be expressed by linear temporal logic (LTL) [11; 12; 13; 14; 15]. On the other hand, the LTL specifications are viewed as the limitations for the movement trajectories of the robots. Hence, from the viewpoint of path planning [16; 17; 18], one requires the finding of a path that satisfies the LTL specifications. The other drawback is that the dynamic events are not efficiently managed, and path constraints cannot be well integrated into the above approaches. Receding horizon control (RHC) [19; 20] can enable efficient management of dynamic events and integration of the trajectories constraints. Based on the RHC approach, one can obtain a control sequence by solving a finite horizon optimization problem and then apply the first control input in this sequence in the current moment. In the next moment, anew control sequence is recalculated by the next sampling information. However, how to give a control strategy that combines the receding horizon control with the LTL specifications for signal source localization is not understood. The main challenge is how to build the cost functions in terms of the LTL specifications. Therefore, by facing the above challenges, our aims are to design an RHC approach with temporal logic specifications. The main contributions of this paper are summarized in the following. 1. We design a temporal logic planning approach where the task of signal source localization is transformed into a path planning task based on the product automaton. One main characteristic is that the product automaton can be built in an offline fashion, while the other characteristic is that the product automaton can be real-time trimmed based on the estimated position of the signal source according to particle filters. 2. On the basis of the product automaton, an RHC approach with temporal logic planning is proposed such that the robot can locate signal sources while avoiding obstacles. Moreover, the generated movement trajectories meet the given LTL formula. 3. We validate the proposed RHC approach with temporal logic planning through the simulation results and experimental results. The results reveal that our approach controls the robot to orderly find the signal sources. The rest of the paper is organized as follows. In Section 2, we introduce the kinematics of the robot and the signal strength model.