IEEE Robotics & Automation Magazine - September 2011 - 68

Note that the sensor propositions represent the behavior of the environment and the robot has no control over
their value.
We represent the set of environment (sensor) propositions as X ¼ fs1 , . . . sm g. The location and action propositions represent the robot behavior and are set by the robot
controller. We represent the set of robot propositions as
Y ¼ fr1 , . . . rn , a1 , . . . , ak g.
Once the problem is abstracted using a set of atomic
propositions, the robot task can be written as a conjunction
of LTL formulas of a given structure [3], [21]. These formulas capture: 1) initial conditions of the environment and the
robot, 2) the motion capabilities of the robot by encoding the
possible transitions between regions of the workspace, 3) any
assumptions about the behavior of the sensor propositions,
i.e., about the behavior of the environment, and 4) the
restrictions, conditions, and goals for the robot's behavior.
Example 2: Consider the autonomous driving problem
described in Example 1. We consider different levels of abstraction. For example, in a coarse abstraction [Figure 2(a)],
a location proposition R1 can be used to indicate whether the
robot is currently traveling on road R1 . A sensor proposition
RoadBlocked can represent the binary output (blocked/
not blocked) of a combined vision and lidar system that reasons about the state of the road. A sensor proposition redLight can represent the perception system alerting the
robot that there is a red traffic light at the intersection. An
action proposition stop can cause the robot to employ the
breaks and stop its motion. Examples for LTL formulas
representing the desired behavior are as follows:
l ((R2 ) ( R2 _ I1 _ I3 )) expresses that from R2
the robot can either stay in R2 or move to I1 or I3 .
l (( redLight ) stop) expresses that the robot
should stop at a red light.

-
+

I2
R6

-
+

+
-

+ R2

(a)
C3,1

C3,2

C3,L

C2,1

C2,2

C2,L

C1,1

C1,2

C1,L

(b)
Figure 2. Different levels of abstraction for the motion of an
autonomous vehicle: (a) a coarse partition of a network of roads
and intersections and (b) a fine-grain partition of a two-lane
road into cells.

IEEE ROBOTICS & AUTOMATION MAGAZINE

SEPTEMBER 2011

(}R4 expresses that the robot should eventually
reach R4 .
In a finer abstraction, suppose R1 has two lanes. It
can be partitioned as shown in Figure 2(b) where
cells C1, 1 , . . . , C1, L are completely in the right lane,
C2, 1 , . . . , C2, L cover the center of the road, and C3, 1 , . . . ,
C3, L are completely in the left lane. Here, for each
i 2 f1, 2, 3g, j 2 f1, . . . , Lg, Ci, j is a location proposition,
whereas oi, j , which represents the existence of an obstacle
in cell (i, j), is a sensor proposition. Examples of LTL
formulas are as follows:
l ^i,j ((oi,j ) :Ci,j ) is the obstacle avoidance requirement.
l ^j ((:(o1, j _ o1, jÀ1 _ o1, jþ1 ) ) (:C2, j ^ :C3, j )), where
o1, 0 , o1, Lþ1 False is the staying in lane requirement.
Since the robot does not control the environment propositions, the synthesis algorithm needs to take into account
all the possible values of redLight (in the coarse abstraction case), oi, j (in the finer abstraction case), and the resulting behavior of the system needs to satisfy the specification
(LTL formulas as listed above) for all these values.
l

From Discrete Solution to Continuous Execution
The synthesized automaton A that satisfies the LTL formulas
(synthesized based on [3]) is implemented as a hybrid controller for the robot as described in Algorithm 1. Given A, an
LTL formula uinitial describing the initial condition of the
propositions in the current execution and an initial pose for
the robot p0 , the initial state q0 2 Q is determined and the
robot actions are enabled/disabled. Then, at each iteration,
the value of the environmental propositions X determine
what the next state NxtState and the next region
NxtReg 2 c(NxtState) should be. The controller then
invokes a continuous controller that drives the robot towards
the next region. If the robot enters the next region, the current
automaton state changes and the appropriate actions are
enabled/disabled. If the robot is neither in the current region
nor in the next region, which could only happen if the environment violated its assumptions, the execution is stopped
with an error. Note that unlike traditional discrete automaton
execution in which transitions between states are instantaneous, here the transitions usually correspond to the robot moving between regions and therefore take time.
Simulations/bisimulations [4] provide a proof that the
continuous execution preserves the correctness of the
discrete plan. Informally, for the discrete solution to be
implementable, we require a set of continuous controllers
that are able to correctly implement any discrete transition
in the controller automaton. For example, if there is a transition from a state in which C1, 1 is true (the robot is in cell
C1, 1 ) to a state in which C1, 2 is true, there must be a controller able to drive the robot from any point within cell C1, 1
across the boundary to cell C1, 2 without going through any
other cell along the way. Clearly, the abstraction of the robot
dynamics has to be created such that the set of controllers
exists, and furthermore, the robustness of such controllers
will determine the granularity of the abstraction. We refer to

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