IEEE Robotics & Automation Magazine - September 2011 - 82

than the runs of the individual agents, since at each state of
its transition system a robot must choose which request (if
any) should be serviced. To accommodate this, we use a
so-called motion and service (MS) plan to control individual robots. An MS plan is similar to a run on a transition
system, except that the request to be serviced at a state is
inserted immediately after the corresponding state. For
example, an MS plan vi (0)vi (1)r1 vi (2)vi (3)r2 vi (3)r3 means
that request r1 is serviced after state vi (1) is reached, and
r2 is serviced after vi (3) is reached, followed by request r3 ,
and no request is serviced after states vi (0) and vi (2) are
reached. If the MS plans of several robots contain a shared
request, then they synchronize (communicate) when this
request is to be serviced (all robots owning a shared request
wait until all others reach a region where the request
occurs, and then service the request together). Otherwise,
no synchronization or communication is necessary to
deploy the team with this control strategy.
Given a set of MS plans for the robot team, there may
exist many possible sequences of requests serviced by the
team due to parallel executions of individual agents. For
example, one agent may service request r1 and the other
agent may service request r2 , both independently. Since
there is no synchronization, the sequence of requests
serviced by the team can be either r1 r2 or r2 r1 . Furthermore, distributed deployment may cause deadlock for
some robots servicing a shared request. For example, if r
is a shared request, it does not appear in the MS plan of
one of the agents who owns r (this may happen if the MS
plan is designed incorrectly) but appears in the MS plans
of some other agents, then these agents will be stuck and
wait indefinitely. When such a deadlock scenario occurs,
the behavior of the team does not satisfy the specification.
Therefore, a major challenge of this framework is to
ensure that all possible sequences of requests serviced
by the team satisfy the task specification, and no deadlock
is reached.
Checking If a Task Specification Is Distributable
Given a sequence of requests (a word w) and the distribution fR1 , . . . , Rn g, which characterizes the ownership of
requests by the robots, we can precisely determine the
sequence of requests required to be serviced by robot i by
projecting w onto Ri . Projecting a word w onto a subset
Ri R means removing all symbols in w that do not
belong to Ri . Such a projection operation will be denoted
as wdRi . For example, assume that there are two robots and
three requests r1 , r2 , and r3 with the distribution:
R1 ¼ fr1 ; r3 g and R2 ¼ fr2 ; r3 g (i.e., r1 and r2 are independent requests and r3 is shared). If w ¼ r3 r1 r2 r3 , then
wdR1 ¼ r3 r1 r3 , and wdR2 ¼ r3 r2 r3 .
Note that different words can produce exactly the same
set of projections. In the previous example, the word
r3 r2 r1 r3 would produce the same projections as w. If a
number of words produce the same projections, then they
are called trace equivalents. If each robot i is required to
82

IEEE ROBOTICS & AUTOMATION MAGAZINE

SEPTEMBER 2011

service a word wi , to guarantee the correctness of the team
behavior, we have to ensure that all the words that can generate the projections fw1 , . . . , wn g satisfy the specification.
For a task specification given as an RE / over R, we
showed that this condition is satisfied if the set of all words
satisfying / is trace closed [21]. In this case, we can find a
top-down distributed solution to the deployment problem
if any of its satisfying words (sequences of requests) can be
implemented by a team of robots.
Using the previous example with the same distribution,
the specification r3 r1 r2 r3 þ r3 r2 r1 r3 is trace closed (since
all of its satisfying words, r3 r1 r2 r3 and r3 r2 r1 r3 , are trace
equivalent). On the other hand, specification r3 r1 r2 r3 by
itself is not trace closed since the word r3 r2 r1 r3 violates the
formula but generates the same trace. This is intuitive, since
r1 and r2 are independent and can be executed in any
order. This specification cannot be distributed, since an execution in the wrong order (e.g., robot two services r2 before
robot one services r1 ) violates the formula.
Given an RE / over R and a distribution fR1 , . . . , Rn g,
checking for trace closedness can be done quickly, as the
operation is linear in the number of states of the FSA
accepting the words satisfying /. An algorithm to check
for trace closedness can be found in [26].
Finding Individual MS Plans
Not all distributable task specifications can be executed by
the team due to the robots' individual motion constraints
modeled by the transitions of Ti . To deal with this, we first
obtain an implementable local FSA for each robot i, which
captures all the words that can be projections of words satisfying / and can be implemented by robot i. The construction of this FSA requires the individual transition
systems Ti , but since it only captures the satisfying words
and not the environment, the size of this FSA is small. We
then obtain an implementable FSA for the team, which
contains all possible satisfying words of / that can be
implemented by the team. It is obtained by taking the
synchronous product among the individual implementable
FSAs. This product is similar to the parallel composition
but for automata instead of transition systems.
The implementable team FSA, however, may contain
words that violate /. By taking the synchronous product
between the implementable team FSA and the FSA accepting the language of /, we get the exact set of words that
satisfy / and can be executed by the team. We then choose a
satisfying word w from this product by a simple graph
search. To decompose w into local specifications, we construct the projections wdRi , which are then used to generate
an MS plan for each robot. For each robot i, this MS plan
can be generated by finding a run on Ti that services the
local specification wdRi and sequentially inserting each
request in wdRi after its corresponding state. From the construction of an implementable FSA, such an MS plan is
guaranteed to exist and be executable. Because the initial
task / is distributable (i.e., trace closed), all possible

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