

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 humanlike 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 highlevel discrete planning with lowlevel continuous planning through the use of specificationautomaton approaches to formal synthesis and samplingbased motionplanning techniques. As a result, we can support any type of robot model with arbitrarily complex dynamics, including hybrid systems and highlevel specifications with compound temporal goals.
The search for a valid motion is done by augmenting a multilayered synergistic framework called SyCLoP. SyCLoP was proposed to solve classical "A to B" motionplanning problems and yields orders of magnitude speedup over traditional samplingbased motionplanning 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) Highlevel 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 lowlevel search layer to construct highlevel plans. In contrast to existing approaches, this layer differs in the fact that it incorporates the exploration information from
the lowlevel search layer as well.
(b) Lowlevel search layer: The lowlevel 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 highlevel 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 highlevel and the lowlevel search layers. This layer is a critical component of the overall framework.

Probabilistic Robots
In realworld 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.

Abstraction
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 logicbased control strategies that utilize those probabilities. The goal is to autonomously deploy a robot that executes a rich, humanlike 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 indoorlike environment, whose topology can be easily reconfigured by moving the foam walls. Top Right Picture: Robot closeups. 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.

