摘要：AbstractThis paper presents a new approach for control synthesis of non-deterministic transition systems under Linear Temporal Logic specifications with applications to multiple Unmanned Aerial Vehicles (UAV) motion planning problems. The consideration of such systems is motivated by the non-determinism possibly introduced while abstracting dynamical systems into finite transition systems. More precisely, we consider transition systems enhanced with a progress set describing the fact that the system cannot stay indefinitely in some subset of states. The control synthesis problem is firstly translated into a terminating planning problem. Then, a backward reachability strategy searches for a path from the initial set to the goal set. At each iteration, subsets of states contained in the progress set are added to the path, thus ensuring the reachability to the goal set in finite time. If a solution to the terminating problem is found, the obtained controller is translated back to the initial problem formulation. This approach is validated through an experiment involving two UAVs with a surveillance specification.
关键词：KeywordsGuidancenavigationcontrol of vehiclesMulti-vehicle systemsFormal control synthesisTemporal logic specificationsNon-deterministic transition system
