IEEE Robotics & Automation Magazine - September 2011 - 77

bisimulations [17], the motion planning and control problem can be reduced to a model-checking or formal synthesis
problem for a finite transition system for which several techniques are readily available.
Some recent works suggest that such single-robot techniques can be extended to multirobot systems through the
use of parallel composition [7], [18] or reactive games [19].
However, such bottom-up approaches are expensive and
can lead to a state-space explosion even for relatively simple problems. As a result, one of the main challenges in the
area of motion planning and control of distributed teams
based on formal verification is to create provably correct,
top-down approaches in which a global, rich specification
can be decomposed into local (individual) specifications,
which can then be used to automatically synthesize robot
control and communication strategies. In such a framework, the construction of the parallel composition of the
individual motions is not necessary, and therefore, the
state-space explosion problem is avoided.
In this article, we first describe a bottom-up approach
that was developed in [18]. We show that control and communication strategies can be automatically generated
through a simple adaptation of existing LTL model-checking
algorithms. While rich specifications given as arbitrary LTL
formulas over regions of interest can be accommodated, the
method is very expensive, both in terms of the amount of
offline computation and the necessary communication during deployment. We then present a distributed top-down
approach, which was inspired from the area of distributed
formal synthesis [20] and was developed in [21]. The specification language is restricted to regular expressions (REs)
over a set of requests occurring at different places in the
environment. Our approach, which is based on decomposing a global specification (a task for the entire team) into
local specifications (tasks for individual robots), is able to
guarantee correctness without parallel composition of the
individual motions. Both methods are quite general and can
be used in conjunction with cell-based decomposition
motion planning techniques described earlier. We illustrate
the computational frameworks with simulations and experiments in Khepera-based platforms, one of which is the
RULE shown in Figure 1 (also see our Web site http://
hyness.bu.edu/RULE.html).
Specification Languages
In our view, a formal specification language for robot motion
should be natural (close to human language), expressive
(allow for the specification of a large class of tasks), and computationally feasible (the algorithms for analysis and controller synthesis from its specifications should have manageable
complexity). Drawing inspiration from formal analysis, candidates for such specification languages include REs, lcalculus, and formulas of temporal logics such as LTL, CTL,
and CTL* (see [9] and [22] for detailed descriptions).
In this article, we first focus on the specifications given
as LTL formulas. Some groups also recommended the use

of CTL as a specification language for multirobot systems
[7]. While CTL model checking is cheaper than LTL model
checking, there are three main problems associated with its
use in robotics. First, it has been proven in [23] that the
translation from natural language to CTL formulas is
prone to errors. Second, some useful robotic missions, such
as surveillance, cannot be expressed in CTL. Finally, since
the language satisfying an LTL formula can be generated
uchi automaton [9], which can be constructed using
by a B€
off-the-shelf tools, LTL is more suited to formal synthesis
than CTL. l-Calculus is strictly more expressive than LTL
and has been used to express robotic tasks [3]. However,
because of its unnatural semantics, l-calculus formulae are
difficult for a human to specify and understand.
An LTL formula is specified with respect to a set of
propositions P, which in the context of task specifications
correspond to regions of interest in the environment or
properties assigned to these regions. Informally, an LTL
formula is built up from the set P: standard Boolean operators : (negation), _ (disjunction), ^ (conjunction), )
(implication), and , (equivalence) and temporal operators  (next), U (until), } (eventually), and ( (always).
An LTL formula is evaluated over infinite sequences of
symbols (such a sequence is called a word), where each
symbol is a subset of P.
By interconnecting Boolean and temporal operators, we
can specify a wide variety of robot tasks, such as a sequence
of goals: "First visit region p1 , and then p2 " (}(p1 ^ }p2 ));
coverage: "Visit region p3 and region p4 , regardless of
order" }p3 ^ }p4 ); and surveillance: "Visit region p1 and
then p2 , infinitely many times" ((}ðp1 ^ }p2 Þ). We can
also chain together multiple formulas, e.g., "achieve task /
while always avoiding region p4 ((:p4 ^ /). Some of
these formulas may require a team effort as they cannot be
achieved by a single robot, e.g., "visit regions p1 and p2 at
the same time" (}ðp1 ^ p2 Þ).
Motivated by the recent results in the nascent area of
formal synthesis [20], we also consider robotic task specifications given as REs over properties satisfied at the regions
of some partitioned environment. An RE is evaluated over
finite sequences (instead of infinite sequences in the LTL
case) of symbols from a set P (the set of properties). Informally, an RE over P is built from the set P and three
standard operators: alternation (denoted by þ), concatenation (denoted by Á, but is usually omitted), and Kleene star
(denoted by Ã ). Expression p1 þ p2 means that either
property p1 or p2 can be satisfied; p1 p2 means that p2 is satisfied after p1 ; and pÃ1 means that p1 can be satisfied a finite
(or zero) number of times. For example, consider a task in
an urban environment: First, gather two pieces of data in
arbitrary order, one can be gathered at locations labeled as
p1 and the other at locations labeled as p2 and then fuse and
transmit the data at one of the transmission stations labeled
as p3 . This task specification can be written as an RE:
(p1 p2 þ p2 p1 )p3 . For each RE, there exists a finite state
automaton (FSA) (see e.g., [22]) that accepts all and only
SEPTEMBER 2011

*

IEEE ROBOTICS & AUTOMATION MAGAZINE

*

77
http://hyness.bu.edu
Table of Contents for the Digital Edition of IEEE Robotics & Automation Magazine - September 2011
