IEEE Robotics & Automation Magazine - September 2011 - 70

automaton. Note that the road
behavior layer was synthesized once
and could be reused as long as the
o1,2
traffic laws did not change. The drivC2,1
C1,2
ing control, which included the
motion abstraction as encoded in the
o1,3
C3,1 C3,2 C3,3
RNDF and the checkpoints encoded
in the MDF, was generated for differC1,3
C2,2
C2,1 C2,2 C2,3
ent files.
o2,3
Figures 5 and 6 depict simulations
of the synthesized system. Since the
C3,2
C2,3
C1,1 C1,2 C1,3
focus was on the high-level behavior
(i.e., robust feedback controllers were
assumed), the dynamics of the vehi(a)
(b)
cle were abstracted by motion on a
line representing the road. Figure 5
Figure 3. Automaton and execution of the behavior of an autonomous vehicle from
Example 2. (a) Snippet of the synthesized automaton. The red transitions correspond to
depicts the behavior of a robot on
the specific run. (b) Example execution, in which an obstacle is detected in cell C1,3 (o1;3
one of the national qualifying event
becomes true).
(NQE) maps, area A, where the robot
challenge. The route network definition file (RNDF) con- had to go through two checkpoints (denoted by black
tains the description of the course, road segments, lanes, circles) as many times as possible. In this simulation, the
waypoints, and locations of stop signs and checkpoints. The robot detects an obstacle and after waiting for a predefined
second file, given to the team five minutes before the start of time decides that the road is blocked and moves on to an
the mission, is the mission data file (MDF), containing the alternate route. Figure 6 depicts the behavior of the robot in
sequence of checkpoints to be traversed together with speed area C of the NQE. There the robot exhibits appropriate
limits for the different road segments. In addition to this, behavior at a four-way stop, first allowing the green car to
the robot was expected to follow the California traffic laws go through and then moving through the intersection.
regarding right of way, etc. In [18], we have shown how the
We note that the controllers used in the simulation were
DUC mission can be encoded in structured English that was automatically generated from the same set of LTL specificathen transformed to LTL formulas and synthesized into tions and the appropriate RNDF and MDF files. The behava correct-by-construction controller. To deal with the ior is different in part due to the information the robot
state explosion problem, we decomposed the problem receives at run time such as obstacles and cars at intersecinto four sets of disjoint specifications and then generated tions. Furthermore, any desired change in the high-level
four automata that, when composed, generated the correct behavior is simple to implement (change some of the senbehavior. Figure 4 shows the structure of the composed tences) and the correctness guarantees are preserved.
C1,1

Sensor-Processing Modules

InterOcc
Intersections

Stop
Obstacles

Road Behavior
Hazard, Blocked

RNDF
MDF
Driving Control
Velocity, Steering,
Signal Lights
Figure 4. Structure of discrete automaton for the DUC example.

IEEE ROBOTICS & AUTOMATION MAGAZINE

SEPTEMBER 2011

Estop

Tool
We have built LTL MissiOn Planner
(LTLMoP) [36], an open-source
python-based toolbox for the design,
synthesis, and implementation of
high-level robot control from structured English specifications. Some of
the toolbox features are as follows:
l modular design to accommodate
different research advancements
(such as in the control, language
interface, automata synthesis, etc.)
l a graphical user interface for drawing the regions of interest of a
workspace (RegionEditor),
l a structured English grammar
for writing specifications that
supports non-projective locative
prepositions such as "between"
and "within x" [37]

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