Temporal Logic Based Motion Planning with Infeasible LTL Specification

In this paper, we consider the problem of robot motion planning with the given LTL specification. Informally, the general algorithm to such problem operates in two phases: (i) the high level synthesis phase constructs an available discrete planning; (ii) the low level synthesis phase designs the control inputs of the robot associated with the transitions along the discrete planning. However, when phase (i) fails, that is, the LTL specification is infeasible in the current environment, it is desired that the system can provide a solution to such cases. In this paper, we utilize the relaxed product automaton to obtain a feasible specification that violates the original specification to a minimum extent and construct an implementable motion planning. The specification automaton is revised by adding the minimum number of transition relations that cannot be satisfied. The overall scheme is demonstrated by a case study.