This is the first of the Kress-Gazit papers, while she was still at UPenn. It introduces the key steps in her approach to a temporal logic method for motion planning. Her goal is to unify high-level, AI style, logical symbolic reasoning with low-level, continuous motion controllers.

She uses a linear temporal logic. The syntax has the usual Until, Always, Eventually operators.

The semantic model for the LTL is trajectories of a planer, point robot moving in a polyherdral environment with no sensing. Her motion model is as follows

x'(t)=u(t) where x(t) in RxR and u(t) in U a subset of RxR

Her world model takes the continuous plane RxR and maps it to a set of discrete locations P={p1,p2,...}

The problem she solves is to autogenerate u(t) to satisfy an LTL criterion such as

Eventually p1 and (eventually p2 (and eventually p3)) that is, got to p1 then p2 then p3 or

(Eventually p1 and Eventually p2 and Eventually p3) that is, cover p1 and p2 and p3 in some order

There are 3 steps:

1. Discrete abstraction of the robot motion: she triangulates the polygonal environment to generate a set of regions. She make a transition system based on the regions and their adjacency.

2. Temporal logic planning using model checking: She uses the NuSMV tool to find a sequence of regions that satisfies the LTL.

3. Continuous implementation of the discrete plan: She places an affine vector field in each region that forces the robot to the next region in the sequence. She uses [10] below to do this; she said [9] would work too but its more computationally intensive.

[9] D.C. Conner, A. Rizzi, and H. Choset, .Composition of local potential functions for global robot control and navigation., 2003 IEEE/RSJ International Conference on Intelligent Robots and Systems

[10] C. Belta and L.C.G.J.M. Habets, .Constructing decidable hybrid systems with velocity bounds. IEEE Conference on Decision and Control, Bahamas, Dec 2004.

DamianLyons - 2011-06-17