Temporal Logic Control and Motion Planning for Complex Dynamical, Hybrid, and Stochastic Systems

Robot motion tasks are usually specified simply as “Go from A to B and avoid obstacles”. By using tools from formal methods, concurrency, and control theory, we extend motion specification languages to arbitrary temporal and logic statements given in human-like language, and develop tools for provably correct automatic deployment of robots from such specifications.  Our approach includes two steps: (1) abstraction of the motion of the probabilistic robot (continuous stochastic system) in a partitioned environment (state space) into Markov models and (2) control of such models using formal (temporal logic) approaches.

Temporal Logic

In the classical robotic motion planning problem, a specification is given simply as “go from A to B while avoiding obstacles”. However, a real mission might be significantly more complicated than this.  For instance, it could involve a sequential visit of multiple regions (“reach A, and then B, and then C”), convergence to a region (“reach A and stay there for all the future times”), perform surveillance among different regions (visit A and B infinitely often), or even more complicated statements (“Go to A. Don’t go to B unless C or D was visited”). Such expressivity can be achieved through the use of temporal logics such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).  In the recent years, there have been major developments in utilizing these languages in the field of model checking and formal analysis.  We use algorithms inspired from this field to find motion plans and control strategies from such specifications.

Deterministic Robots

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, possibly nonlinear and hybrid) 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.

SyCLoP_diagramThe 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 to the right and consists of three main layers:

(a) High-level search layer: This is the layer that uses the automaton obtained by the considered logic formula, a discrete abstraction for the robot model, and the exploration information from the low-level search layer to construct high-level plans. In contrast to existing approaches, this layer differs in the fact that it incorporates the exploration information from the low-level search layer as well.

(b) Low-level search layer: The low-level search layer is the layer that accounts for the physics of the problem. This layer takes into account the robot dynamics and the geometric constraints while exploring the physical space for feasible trajectories. The layer uses suggested high-level plans to explore the state space for solution trajectories.

(c) Synergy layer: The synergy layer is an intermediate layer that facilitates the synergistic interaction between the high-level and the low-level search layers. This layer is a critical component of the overall framework.


roomba5Probabilistic Robots

In real-world applications, we must always deal with some level of uncertainty. This may arise from a variety of sources, including noise in the sensors and actuators of the robot. The goal of our work is to achieve a given task in the face of this uncertainty by finding the control strategy that maximizes the probability of satisfying the specification.


The starting point for this work is to abstract the evolution of the system (robot) in the (partitioned) state pace (environment) as a Markov model.  To achieve this, we make the assumption that despite input noise (noisy sensors in the case of robot), current region in the state space can be determined precisely.  This assumption is not overly restrictive for indoor navigation applications where, for instance, a large number of RFID tags can be placed in the environment. Thus, the robot motion plan becomes a Markov Decision Process (MDP).



Probabilistic Computation Logic (PCTL)

We are focusing on specifications given in a temporal logic. Given a specification, we would like to automatically determine the control strategy that maximizes the probability of achieving this specification. To date, we have achieved this by using statements in PCTL, a probabilistic version of the Computation Tree Logic.

Robotic InDoor Environment (RIDE)

To experimentally validate our approach, we utilize primarily the Robotic InDoor Environment (RIDE). RIDE is an experimental platform designed to generate control action transition probabilities and test temporal logic-based control strategies that utilize those probabilities. The goal is to autonomously deploy a robot that executes a rich, human-like logic specification within a given environment using a control strategy that maximizes the probability of satisfying the specification.

This system utilizes pieces of extruded polystyrene as building blocks, allowing environments of different geometries to be easily constructed. The mobile platform is an iRobot Create fitted with a laser range finder, an RFID reader, and a netbook. It can move autonomously through corridors and intersections that can be easily reconfigured.

The robotic setup allows for actuation noise (i.e., the control actions enable transitions with known probabilities) and/or uncertain knowledge of current region - two major limitations of existing temporal logic approaches that focus on guaranteed (deterministic) transition systems and knowledge of precise location - in order to generate a control strategy for a Markov Decision Process (MDP).

RIDE is also equipped with a simulator that can be used to help generate the MDP model and to test the produced control strategies.

Pictures on the Left: An iRobot Create mobile platform equipped with a laptop, a laser range finder, and RFID reader moves autonomously through the corridors and intersections of an indoor-like environment, whose topology can be easily reconfigured by moving the foam walls.  Top Right Picture: Robot close-ups.  Bottom Right Picture: Snapshots from the RIDE simulator. The robot is represented as a white disk. The arrow inside the white disk shows the robot’s heading.

Robot Deployment

Using our method, we have successfully deployed robots from different specifications in RIDE simulator and experimental platform. For videos click here.