Traditional motion planning problems have only considered simple specifications, like “go from A to B while avoiding obstacles”, and there are a number of algorithms that have been developed to solve such an instance depending on the problem domain. A real mission, however, may require complex tasks including attainment B or C from A, visiting targets sequentially (e.g., “go to A, and then B, and then C”), and conditional and temporal statements (e.g. “Do not go to C unless A or B is visited and always avoid D”). To accommodate such complex goals, the use of temporal logics such as Linear Temporal Logics (LTL) have been suggested as specification languages in the recent works.
An increasing number of algorithms have been proposed to find motion plans and control strategies from complex specifications. The majority of these algorithms, however, make limiting assumptions like simple (linear) dynamics or the existence of a finite set of discrete motion primitives (control actions) for the robot. In our work, we avoid making such assumptions and consider high dimensional systems with general (complex and possibly nonlinear) dynamics. In our current framework, we are able to automatically generate a motion plan and the necessary control actions for a robot to satisfy an LTL formula defined over regions of the environment. Satisfaction is achieved by combining high-level discrete planning with low-level continuous planning through the use of specification-automaton approaches to formal synthesis and sampling-based motion-planning techniques. As a result, we can support any type of robot model with arbitrarily complex dynamics, including hybrid systems and high-level specifications with compound temporal goals such as:
“Eventually, visit region A, and then visit region B or region C,”
“Eventually, pick up a load from region A, and then do not pick up another load until it is dropped off in either region B or region C.”
To allow for complex specifications, we have drawn inspirations from the automaton approaches to formal synthesis. In these approaches, a specification is given as a temporal logic formula. An automaton is then constructed from the formula and utilized to find a system trajectory that satisfies the specification. In our work, we focus on motion specifications that can be expressed as syntactically co-safe LTL formulas. This class of LTL formulas can be satisfied by finite trajectories of the system which makes it desirable for robotic applications. To generate a continuous robot trajectory that satisfies a co-safe specification, we use sampling-based motion-planning techniques in a multi-layered synergistic framework that is explained below.
The search for a valid motion is done by augmenting a multi-layered synergistic framework called SyCLoP. SyCLoP was proposed to solve classical “A to B” motion-planning problems and yields orders of magnitude speedup over traditional sampling-based motion-planning techniques. The augmented framework that includes the logic specification and the SyCLoP framework is shown below and consists of three main layers:
This framework follows from a long chronology of multi-layered synergistic motion planning techniques. As mentioned above, the base of the framework is SyCLoP which is a discrete-search guided motion-planning technique accommodating only simple specifications. It was then extended to perform safety analysis for hybrid systems. To allow for complex tasks, SyCLoP was extended to planning from LTL specifications. In a recent work, we have successfully applied this framework to problems for robots with hybrid dynamics.
This work has been supported by NSF CNS 0615328, and NSF CCF 1018798.