A leader-follower communication protocol for motion planning in partially known environments under temporal logic specifications

This paper considers the problem of communication protocols between leaders and its followers for motion planning in an initially partially known environment. In this setting, the leader observes the environment information to satisfy its own local objective and and the follower completes its own local objective by estimating the states of the leader and communicating with the leader to update its knowledge about the environment when it is necessary, where the local objectives can be expressed in temporal logic. A verifier construction is built first to contain all possible communication protocols between the leaders and the followers. Then, a two-step synthesis procedure is proposed to capture all feasible communication protocol that satisfy the local objectives for the leader and follower, respectively. In the first step, a sub-verifier is synthesized to satisfy the objective of the follower. In the second step, based on the obtained sub-verifier, an iterative algorithm is proposed to extract communication protocols such that the objectives of the leader and follower are satisfied, respectively. A running example is provided to illustrate the proposed procedures.