부산대학교 도서관

In order to preserve an unmanned autonomous vehicle's (UAV) safety in a dynamic obstacles environment, several technologies must be utilized including mobile obstacle prediction, path planning, and real-time obstacle avoidance. In this paper, we develop a path planning and monitoring approach where metric temporal logic (MTL) and predictive MTL (P-MTL) are used to specify the desired behavior of the UAV and specify its environment. We rely on a theory of robustness based on MTL as applied to offline verification and online control of hybrid systems to augment our previous path planning algorithm. During the path execution, a Kalman Filter is utilized to predict the motion model for the observed mobile obstacles. Then, the monitoring algorithm uses the prediction model to logically and probabilistically reason about the P-MTL formulas of the current trajectory. By predicting the obstacle's path, the MTL robustness of the trajectory can be monitored and deduced without observing the obstacle movement at each time step, which reduces the re-planning attempts and decreases the risk.