Difference: KG-05Annotation ( vs. 1)

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