An Online Human-Aware Behavior Planning Method for Nondeterministic UAV System Under Probabilistic Model Checking

This paper proposes an online human-aware behavior planning method to enable Unmanned Aerial Vehicles (UAVs) to dynamically satisfy high-level linear temporal logic (LTL) task descriptions from human collaborators. The proposed method has the potential to be applied to the industrial human–UAV collaboration. The specific process is as follows. Firstly, the global high-level task of the UAV is described using the formal language of LTL, which can usually be issued by human collaborators in natural language. Secondly, the task description is transformed into a deterministic Rabin automaton, and then the state values of the automaton are given by the distance from the accepted states. Thirdly, the Markov decision process is used to construct the probabilistic behavior model of the UAV offline. Based on this model, a finite state automaton in the finite horizon is dynamically constructed online, and the Cartesian product system within the horizon is constructed, in which the expected arrival states within the horizon are set by the minimum state values. Finally, aiming at maximizing the reachability probability of the expected states, the value iterative algorithm is introduced to solve the optimal behavior plan online within the finite horizon. After it, an infinite horizon planning and execution algorithm is formed. Experiments and analysis show that the results of the online behavior planning are consistent with the task logic at the semantic level, indicating the correctness of the proposed method. Moreover, the proposed method can effectively alleviate the state explosion caused by the global probabilistic model checking and improve the efficiency of plan generation.