IEEE Robotics & Automation Magazine - September 2011 - 71

connection to player/stage [38] for simulating and controlling physical robots.
Figure 7 depicts several screenshots of LTLMoP and a
photo of a robot being controlled by it. Videos showing
LTLMoP in action can be seen at http://www.youtube.
com/user/ASLCornell.

Fine Abstraction: Receding Horizon Framework
To illustrate the state explosion problem, we revisit the autonomous driving problem of Example 2. Consider the case
where the road is partitioned as in Figure 2(b). Suppose the
car starts in cell C1, 1 and the destination is the union of C1, L ,
C2, L , and C3, L . In this problem, there are 3L23L possible states
of the system. The computational complexity of the algorithm presented in [3] is O(jVj3 ), where jVj is the size of the
state space, which, in this case, is exponential in L. This type
of computational complexity limits the application of LTL
synthesis to relatively small abstractions. Furthermore, when
the complicated dynamics of an autonomous ground vehicle
needs to be incorporated, the road may need to get further
discretized [24], resulting in an even larger state space.
In many applications, however, it is not necessary for the
robot to plan for the whole execution, taking into account
all the possible behaviors of the environment, since a state
that is very far from the current state of the robot typically
does not affect the near future plan. In the context of the
autonomous driving problem of Example 2, under certain
conditions, it may be sufficient for the robot to plan out an
execution for only a short segment ahead and implement it
in a receding horizon fashion, i.e., recompute the plan as the
robot moves, starting from the currently observed state
(rather than from all the possible initial conditions).
In [19], sufficient conditions that ensure that this receding horizon implementation preserves the desired systemlevel properties are presented. This framework reduces the
computational complexity of the synthesis problem by
essentially breaking the original problem into a set of
smaller problems of shorter horizon. The size of these
smaller problems depends on the horizon length. For
example, consider the autonomous driving problem of
Example 2 where the robot starts in cell C1, 1 and the destination is the union of C1, L , C2, L , and C3, L . Suppose the
horizon length is l (i.e., the robot plans for l cells ahead).
Then, the state space for each short-horizon problem contains at most 3l23l states (whereas the size of the original
problem is 3L23L ). Hence, the horizon length should be
made as small as possible, subject to the realizability of the
resulting short-horizon specifications. A horizon that is
too short typically renders the specifications unrealizable.
For the previously mentioned autonomous driving problem, it was shown in [19] that all the short-horizon specifications are realizable with l ¼ 2. Hence, the size of the
state space for each short-horizon problem is at most 384,
regardless of the length L of the road while for L ¼ 100,
the size of the state space of the original problem is on the
order of 1092 , and it increases exponentially with L. (Note

(a)

(b)

(c)

(d)

Figure 5. Encountering a temporarily blocked road: (a) Stopping
due to obstacle (robot stopped is indicated by red triangle),
(b) timer timed out. Obstacle is determined to be a blocked road,
(c) robot takes a different route, and (d) block cleared.

that the specification considered in [19] also includes
intersection rules, which are not included in the straight
road scenario considered here. Hence, the size of the state
space reported in [19] is slightly larger than the size of the
state space of the problem considered here. However, the
same horizon length applies for both scenarios.)
The correctness of this receding horizon framework
relies on a partial order relation among the discrete states.
The notion of a receding horizon invariant, a proposition

(a)

(b)

(c)

(d)

Figure 6. Four-way stop behavior: (a) Initial locations of cars.
The robot is depicted using a blue square, (b) both the robot
and the green car stop (robot stopped is indicated by red
triangle), (c) the green car moves, and (d) the robot moves.

SEPTEMBER 2011

IEEE ROBOTICS & AUTOMATION MAGAZINE

http://www.youtube

Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011