Route Guidance for Satisfying Temporal Logic Specifications on Aircraft Motion

A new technique for aircraft route guidance subject to linear temporal logic specifications is presented. The proposed approach is based on workspace partitioning, and it relies on the idea of so-called lifted graphs. Briefly, edges in a lifted graph are successions of adjacent edges in the topological graph associated with the workspace partition. Edges of the lifted graph are associated with certain reachability properties of the aircraft model. The main result of this paper is the precise characterization of acceptable routes (namely, sequences of cells) that are guaranteed to be traversable by admissible state trajectories of the aircraft model while satisfying the given linear temporal logic specifications. The proposed approach incorporates nonholonomic kinematic constraints, does not require complete controllability in the presence of workspace constraints, and does not require linearization of the aircraft model. Numerical methods to implement the proposed route-planning algorithm are discussed. The proposed algorithm is illustrated with numerical simulation examples that reflect the practical significance of linear temporal logic specifications in aircraft guidance.