Decomposition of Multi-Agent Planning under Distributed Motion and
Task LTL Specifications

arXiv:1610.08379v1 [cs.SY] 26 Oct 2016

Jana Tumova and Dimos V. Dimarogonas
Abstract— The aim of this work is to introduce an efficient procedure for discrete multi-agent planning under local
complex temporal logic behavior specifications. While the first
part of an agent’s behavior specification constraints the agent’s
trace and is independent, the second part of the specification
expresses the agent’s tasks in terms of the services to be
provided along the trace and may impose requests for the
other agents’ collaborations. To fight the extreme computational
complexity of centralized multi-agent planning, we propose a
two-phase automata-based solution, where we systematically
decouple the planning procedure for the two types of specifications. At first, we only consider the former specifications
in a fully decentralized way and we compactly represent each
agents’ admissible traces by abstracting away the states that
are insignificant for the satisfaction of their latter specifications. Second, the synchronized planning procedure uses only
the compact representations. The satisfaction of the overall
specification is guaranteed by construction for each agent. An
illustrative example demonstrating the practical benefits of the
solution is included.

I. INTRODUCTION
Automated synthesis of correct-by-design controllers complying with complex behavior specifications has recently
found a wide support in formal verification methods and
temporal logics. A number of the suggested solutions build
on a hierarchical approach [2], [9], [11], [17], where the
dynamics of the system is abstracted into a finite, discrete
transition system, a discrete plan that meets the specification
is synthesized and next translated into a controller for the
original system. This work focuses on a multi-agent version
of the above problem, and particularly on the second step of
the hierarchical approach. We consider a heterogeneous team
of agents (e.g., robots), that are assigned a behavior specification each, comprising of the requirements on the sequence of
states they go through (e.g., the robots’ trajectories) and the
services they provide (e.g., loading an object). The agents’
tasks are though not completely independent; in order to
achieve their task a collaboration of the other agents might
be required (e.g., helping to load a heavy object). Our aim
in this paper is to efficiently synthesize a strategy for each
agent, such that all requirements are met. As a specification
language, we use Linear Temporal Logic (LTL), for its
resemblance to natural language [7], and expressive power.
This work was supported by EU STREP RECONFIG, European Unions
Horizon 2020 Research and Innovation Programme under the Grant Agreement No.644128 (AEROWORKS), Swedish Research Council (VR), and
H2020 European Reasearch Council (ERC) Starting Grant BUCOPHSYS.
The authors are with the ACCESS Linnaeus Center, School of Electrical Engineering, KTH Royal Institute of Technology, Stockholm, Sweden and with
the KTH Centre for Autonomous Systems. Email: tumova@kth.se,
dimos@kth.se.

The goal is viewed from the bottom-up perspective, where
we introduce the notion of local specification satisfaction
based on the individual agents’ own viewpoints.
Multi-agent planning from temporal logic specification has
been explored in several recent works. Planning for a team
of robots from a global LTL specification was addressed,
e.g., in [10], [12]. The authors in [8] considered LTL for
vehicle routing and in [16] for search and rescue missions.
A decentralized control of a robotic team from local LTL
specification with communication constraints is proposed
in [4], [6]. In contrast to our work, the agents therein do not
impose any constraints on the other agents’ behavior. In [3],
[15], a top-down approach to LTL planning is investigated;
the team is given a global specification and an effort is
made to decompose the formula into independent local
specifications that can be treated separately. In [5], bottomup planning from LTL specifications is considered, and a
partially decentralized solution is proposed that decomposes
the group into clusters of dependent agents. To cope with
the state space explosion, in [13], [14] we have proposed a
receding horizon approach to multi-agent planning.
In this paper, we take into account an extension of the
previous problem, where besides the high-level tasks in
terms of services to be provided, the agents’ behaviors are
limited by additional temporal logic constraints, allowing
to express safety, surveillance, sequencing, or reachability
properties of their traces, which we call motion specifications
for simplicity. We propose to decouple the planning for the
former and the latter parts of the specification. The main idea
is to build local synchronized product automata for each of
the agents’ motion separately and reduce their size before
creating the global product. The contribution of this paper
can thus be summarized as the introduction of an efficient,
bottom-up control strategy synthesis for multi-agent systems
from local LTL motion and task specifications. The designed
strategy allows the agents to execute their finite plans to a
large extent independently, in an asynchronous manner.
The rest of the paper is structured as follows. In Sec. II, we
fix necessary notation. Sec. III formalizes the problem statement. In Sec. IV, the details of the solutions are provided.
An illustrative example is given in Sec. V.
II. NOTATION AND PRELIMINARIES
Given a set S, let 2S , and Sω denote the set of all subsets
of S, and the set of all infinite sequences of elements of S,
respectively. The i-th element of the sequence w is w(i), and
a subsequence of an infinite sequence w = w(1)w(2) . . . is
a finite or infinite sequence w(ι1 )w(ι2 ) . . ., such that 1 ≤

ιj ≤ ιj+1 , for all 1 ≤ j. Boolean operator XOR (exclusive
or) is denoted by ⊕, positive integers and non-negative real
numbers are denoted by N and R+
0 , respectively.
A labeled transition system (TS) is a tuple
T = (S, sinit , A, T, Π, L), where S is a finite set of
states; sinit ∈ S is the initial state; A is a finite set of
actions; T ⊆ S × A → S is a partial deterministic transition
function; Π is a set of atomic propositions; and L : S → 2Π
is a labeling function. A trace of T is an infinite alternating
sequence of states and actions τ = s1 α1 s2 α2 . . ., such that
s1 = sinit , and for all i ≥ 1, T (si , α) = si+1 .
An LTL formula ϕ over the set of atomic propositions Σ is
defined inductively: (i) π ∈ Σ is a formula, and (ii) if ϕ1 and
ϕ2 are formulas, then ϕ1 ∨ϕ2 , ¬ϕ1 , X ϕ1 , ϕ1 U ϕ2 , F ϕ1 , and
G ϕ1 are each a formula, where ¬ and ∨ are standard Boolean
connectives, and X (next), U (until), F (eventually), and G
(always) are temporal operators. The semantics of LTL are
defined over infinite words over 2Π (see, e.g., [1]). A trace
τ = s1 α1 s2 α2 . . . of T satisfies an LTL formula ϕ over Π
(τ |= ϕ) iff L(s1 )L(s2 ) . . . satisfies ϕ (L(s1 )L(s2 ) . . . |= ϕ).
A Büchi automaton (BA) is a tuple A = (Q, qinit , Σ, δ, F ),
where Q is a finite set of states; qinit ∈ Q is the initial state;
Σ is an input alphabet; δ ⊆ Q × Σ × Q is a non-deterministic
transition relation; F ⊆ Q is an accepting condition. A run
of the BA B from a state q1 ∈ Q over a word w = σ1 σ2 . . . ∈
Σω is a sequence ρ = q1 q2 . . ., such that (qi , σi , qi+1 ) ∈ δ,
for all i ≥ 1 and it is accepting if it intersects F infinitely
many times. A word w is accepted by B if there exists an
accepting run over w from the state qinit . Any LTL formula
ϕ over Π can be algorithmically translated into an equivalent
BA B with Σ = 2Π . Any BA can be also viewed as a graph
and the terminology from graph theory applies.
III. PROBLEM FORMULATION
Two general viewpoints can be taken in multi-agent planning: either the system acts as a team with a common goal,
or the agents have their individual, local specifications. Here,
we adopt the second viewpoint and we do not look at the
global team behavior. In contrast, we propose local specification satisfaction to determine whether an agent’s task
is fulfilled from its own perspective. Each agent’s temporal
specification comprises of a motion and a task formula.
Loosely speaking, the motion formula can be viewed as the
agent’s safety, reachability, surveillance or sequencing, while
the task one represents its effectiveness, i.e, the motion formula limits the sequence of states the agent’s goes through,
while the task formula corresponds to an accomplishment of
a high-level task composed of simple services that the agent
has the ability to provide. Unlike the motion one, the task
formula may involve collaboration requirements.
Our goal is to synthesize a control strategy for each agent
that involves (i) the actions to be executed and (ii) the
requests for synchronization imposed on other agents. Together, the strategies have to ensure the local satisfaction of
each of the motion and task specifications regardless of the
time duration of the planned action executions.

A. System Model
Let us consider N agents (e.g., robots in a partitioned
environment). Each agent i ∈ N , where N = {1, . . . , N }
has two different types of capabilities: the ability to execute
an action primitive, and to synchronize with the others.
1) Action Execution Capabilities: The agent i’s actionexecution capabilities are modeled as a finite TS
Ti = (Si , sinit,i , Ai , Ti , Πi , Li ). The states of the TS correspond to states of the agents (e.g., the location of the robots in
the regions of the environment). The atomic propositions represent inherent properties of the system states (e.g., the robot
is in a safe region). The actions represent abstractions of
the agent’s low-level controllers, and the transitions between
the states correspond to the agent’s capabilities to execute
the actions (e.g., the ability of the robots to move between
two regions of the environment). The traces are, roughly
speaking, the abstractions of the agents’ long-term behaviors
(e.g., the robots’ trajectories). Each of the agents’ action
executions takes a certain amount of time. Given a trace
τ = s1 α1 s2 α2 . . . of Ti , we denote by ∆αj ∈ R+
0 the time
αj
duration of the transition sj −→ sj+1 . Note that a transition
duration is arbitrary and unknown prior its execution, and
that the execution of the same action α may induce different
transition durations in its different instances on the trace.
2) Synchronization Capabilities: Next to the actionexecution capabilities, the agents have the ability to synchronize, i.e., to wait for each other and to proceed with
the further execution simultaneously. The synchronization is
modeled through the synchronization requests. While being
in a state s, an agent i can send a request synci (I) to a
subset of agents {i} ⊆ I ⊆ N notifying that it is ready to
synchronize. Then, before proceeding with the execution of
any action α ∈ Ai , it has to wait till synci0 (I) has been
sent by each agent i0 ∈ I, i.e., till the moment when each
agent i0 ∈ I is ready to synchronize, too. For simplicity,
we assume the perfect propagation of the synchronization
requests. The synchronization is immediate once each of
the agents i0 ∈ I has sent its request synci0 (I) and all
agents in I start executing the next action collaboratively,
at the same time. The set of all synchronization requests
of an agent i is Sync i = {sync i (I) | {i} ⊆ I ⊆ N }.
Note that the synchronization request synci ({i}) indicates
that no synchronization with the others is needed, and the
next action of agent i is executed immediately, independently
on the other agents. We assume that each agent sends a
synchronization request instantly once it completes an action
execution and that it starts executing an action instantly once
it synchronizes with the other agents. Instead of allowing for
idling, we include an existence of a special action stay i ∈ Ai
stay i
and a so-called self-loop s −−−→
s for all s ∈ Si , and all
Ti , where i ∈ N . Given a trace τi = si,1 αi,1 si,2 αi,2 . . .
of Ti , we denote by ∆si,j ∈ R+
0 the time duration of the
synchronization that has been requested in the state si,j . Note
that ∆si,j = 0 for sync i ({i}) in si,j .
3) Services: Each of the agents’ specification is given via
two components: the first one are temporal requirements on

the atomic propositions that need to hold along its trace, and
the second one is a task given in terms of events of interest
associated with their actions, which we call services (e.g.,
an object pick-up). The set of services that can be provided
by an agent i ∈ N is Σi . Services are provided within the
agents’ transitions; each action α ∈ Ai is associated, or in
other words labeled, either with (i) a service set σ ∈ 2Σi
provided by i upon the execution of α, or (ii) a special
silent service set Ei = {εi }, where εi 6∈ Σi indicating
that the action α does not provide any event of interest.
Hence, two additional components of the agent i’s model are
the set of all available services Σi and the action-labeling
function Li : Ai → 2Πi ∪ 2Ei . Note that we specifically
distinguish between a silent service set Ei and an empty
service set {}. The above mentioned self-loops of form
stay i
s −−−→
s that we use to model the agents’ ability of
staying in their respective current states are labeled with the
silent service set Li (stay i ) = Ei . Without loss of generality,
we assume that Σi ∩ Σi0 = ∅, for all i, i0 ∈ N , such
that i 6= i0 , which is necessary for the final step of our
solution. Finally, we model an agent i ∈ N as the tuple
Mi = (Ti = (Si , sinit,i , Ai , Ti , Πi , Li ), Sync i , Σi , Li ).
4) Behaviors: Behavior of an agent i is defined by its
states, actions, synchronizations with the others, and the time
instants of the action executions and the synchronizations.
Definition 1 (Behavior and strategy). A behavior of an agent
i is a tuple β = (τ, γ, T), where
•
•
•

τ = s1 α1 s2 α2 . . . is a trace of Ti ;
γ = r1 r2 . . . is a synchronization sequence, where rj ∈
Sync i is the synchronization request sent at sj ; and
T = ts1 tα1 ts2 tα2 . . . is a non-decreasing behavior
time sequence, where tsj is the time instant when the
synchronization request rj was sent, and tαj is the time
instant when the action αj started being executed. The
following properties hold: ts1 = 0, and for all j ≥ 1,
tsj+1 − tαj = ∆αj , and tαj − tsj = ∆sj .

B. Motion and Task Specifications
The individual agents’ tasks are collaborative; on the one
hand, they involve requirements on the agents’ states, i.e.,
the atomic propositions associated with them and on the
other hand, they concern the respective agent’s services as
well as the services of the other agents. Formally, each
of the agents is given (i) an LTL\X formula φi over Πi ,
which we call a motion specification
and (ii) a collaborative
S
LTL formula ψi over Σ = i0 ∈N Σi0 , which we call a
task specification. Consider for a moment a single agent
Mi = (Ti , Sync i , Σi , Li ), and its behavior β = (τ, γ, T),
where τ = s1 α1 s2 α2 . . ., and T = ts1 tα1 ts2 tα2 . . ..
Definition 3 (Words and time sequences). We denote by
vτ = $1 $2 . . . = Li (α1 )Li (α2 ) . . . ∈ (2Σi ∪ 2Ei )ω the service set sequence associated with τ . The word wτ produced
by τ is the subsequence of the non-silent elements of vτ ;
wτ = $ι1 $ι2 . . . ∈ (2Σi )ω , such that $1 , . . . , $ι1 −1 = Ei ,
and for all j ≥ 1, $ιj 6= Ei and $ιj +1 , . . . , $ιj+1 −1 = Ei .
With a slight abuse of notation, we use T(vτ ) = t1 t2 . . . =
tα1 tα2 . . . to denote the service time sequence, i.e. the subsequence of T when the services are provided. Furthermore,
T(wτ ) = tι1 tι2 . . . denotes the word time sequence, i.e. the
subsequence of T(vτ ) that corresponds to the time instances
when the non-silent services are provided.
As in this work we are interested in infinite behaviors, we
consider as valid traces only those producing infinite words.
Definition 4 (Service set at a time). Let τ be a trace of Ti
with vτ = $1 $2 . . ., and T(vτ ) = t1 t2 . . .. Given t ∈ R+
0,
the service set vτ (t) ∈ 2Πi ∪2Ei provided at time t is vτ (t) =
$j if t = tj for some j ≥ 1; and vτ (t) = Ei otherwise.

A strategy (τ, γ) for an agent i is a trace τ and a synchronization sequence γ.

Note that the above definition is designed in a way
accommodating the general asynchronicity of the agents.
Each formula ψi is interpreted locally, from the agent i’s
point of view, based on the word wτi it produces and on
the services of the other agents i0 ∈ N provided at the
time instances T(wτi ). In other words, the agent i takes into
consideration the other agents’ services only at times, when
i provides a non-silent service set (even an empty one) itself.

The notion of behavior does not reflect the above described
inter-agent synchronization rules. To that end, we define
behaviors induced by strategies admissible by a team of
agents. We denote the behavior of an agent i ∈ N by
βi = (τi , γi , Ti ), and we use τi = si,1 αi,1 si,2 αi,2 . . .,
γi = ri,1 ri,2 . . ., and Ti = tsi,1 tαi,1 tsi,2 tαi,2 . . . to denote
its trace, synchronization and time sequence.

Definition 5 (Local LTL satisfaction). Let B = β1 , . . . , βN
be a collection of behaviors, where βi = (τi , γi , Ti ) for all
i ∈ N and let T(wτi ) = ti,ι1 ti,ι2 . . . be the word time
sequence of agent i. The local word S
produced by B is
wBi = ωi,ι1 ωi,ι2 . . . , where ωi,ιj =
i0 ∈N vτi0 (ti,ιj ) ∩
Σ, for all j ≥ 1. B locally satisfies the formula ψi for the
agent i, B |=i ψi , iff wBi |= ψi .

Definition 2 (Induced behaviors). The set of behaviors induced by a collection of strategies (τ1 , γ1 ), . . . , (τN , γN ) of
agents in N are the subset of the collections of their behaviors B ⊆ {B ∈ {β1 , . . . , βN | βi is a behavior of agent i}}
satisfying the following condition for all i ∈ N , and j ≥ 1:
Suppose that ri,j = synci (I). Then for all i0 ∈ I there exists
a matching index j 0 ≥ 1, such that ri0 ,j 0 = synci0 (I), and
tαi,j = tαi0 ,j0 . Furthermore, there exists at least one i0 ∈ I,
such that tsi0 ,j0 = tαi0 ,j0 , i.e., such that ∆si0 ,j0 = 0, for the
matching index j 0 .

Note that even if ψi = ψj , it is possible that B |=i ψi for
the agent i, while B 6|=j ψj for the agent j, since it might
be the case that wBi 6= wBj .
C. Problem Statement
Problem 1. Consider a set of agents N = {1, . . . , N },
and suppose that each agent i ∈ N is modeled as a tuple
Mi = (Ti = (Si , sinit,i , Ai , Ti , Πi , Li ), Sync i , Σi , Li ), and
assigned a task inSthe form of an LTL\X formula φi over Πi
and ψi over Σ = i0 ∈N Σi0 . For each i ∈ N find a strategy,

i.e., (i) a trace τi = si,1 αi,1 si,2 αi,2 . . . of Ti and (ii) a
synchronization sequence γi over Sync i with the property
that the set of induced behaviors B from Def. 2 is nonempty,
and for all B ∈ B and all i ∈ N , it holds that the trace τi
satisfies φi and the word wBi produced by B locally satisfies
ψi for the agent i in terms of Def. 5.
As each LTL formula can be translated into a BA, from
now on, we pose the problem with the motion specification of
φ
, δiφ , 2Π , Fiφ ),
each agent i given as a BA Biφ = (Qφi , qinit,i
ψ
ψ ψ
and the task one as a BA Bi = (Qi , qinit,i , δiψ , 2Σ , Fiψ ).
Given that τi = si,1 αi,1 si,2 αi,2 . . ., the motion specification
satisfaction is formulated as L(si,1 )L(si,2 ) . . . ∈ Lang(Biφ )
and the local satisfaction of the task specification as wBi ∈
Lang(Biψ ).
IV. PROBLEM SOLUTION
Even though the agents’ motion specifications are mutually independent, each of them is dependent on the agent’s
respective task specification, which is dependent on the task
specifications of the other agents. As a result, the procedures
of synthesizing the desired N strategies cannot be decentralized in an obvious way. However, one can quite easily
obtain a centralized solution when viewing the problem as a
synthesis of a single team strategy.
First of all, we realize that if there exists a solution to
Problem 1, then there exists a solution in which all the agents
synchronize after every single step. Informally, the reason is
that each agent i is able to execute action stay i , i.e., that
Li (stay i ) = Ei , and that the motion specification φi is a
formula of LTL\X , i.e., that the execution of stay i does not
influence its satisfaction. The standard automata-based procedure for solving the LTL control strategy synthesis problem
for deterministic systems can be then easily applied in multiagent settings in a centralized way. 1) A synchronized TS
TN with the set of states SN = S1 × . . . × SN is built that
represents all stepwise-synchronized traces
V of the agents in
N . 2) A BA BSN is built for the formula i∈N (φi ∧ ψi ) over
the alphabet 2 i∈N Πi ∪Σ . 3) A product automaton PN of TN
and BN is constructed that captures only the agents’ traces
that are admissible by TN and result into behaviors that
satisfy φ1 , . . . , φN , and locally satisfy ψ1 , . . . , ψN , for the
agents 1, . . . , N , respectively. The product PN is analyzed
using standard graph algorithms in order to find its accepting
run that projects onto the desired traces of Ti , for all i ∈
N . 4) The synthesized strategy for an agent i ∈ N is a
trace τi = si,1 αi,1 si,2 αi,2 . . . of Ti , and a synchronization
sequence γi = ri,1 ri,2 . . . where ri,j = sync i {N }, for
all j ≥ 1. We notice that the amount of synchronization
required by agent i ∈ N can be reduced by replacing
ri,j = sync i (N ) with sync i ({i}), if for each agent i0 ∈ N it
holds that Li0 (αi0 ,j ) = Ei0 , since in such a case, wBi remains
unchanged. Furthermore, the stay i actions can be removed
from τi without any harm, since they influence neither the
satisfaction of φi , nor the word wB0i for any i0 ∈ N .

A. Our solution
A major drawback of the centralized solution is the state
space explosion, which makes it practically unusable. We aim
to decentralize the solution as much as possible. Namely,
we aim to separate the synthesis of service plans yielding
the local satisfaction of the task specifications from the
syntheses of traces that guarantee the motion specifications.
Our approach is to pre-compute possible traces and represent
them efficiently, abstracting away the features that are not
significant for the synthesis of action plans. This abstraction
serves as a guidance for the action and synchronization
planning, which, by construction, allows for finding a trace
complying with both the synthesized action and synchronization plans and and the motion specification.
1) Preprocessing the motion specifications: Consider for
now an agent i ∈ N modeled as Mi = (Ti , Sync i , Σi , Li ),
where Ti = (Si , sinit,i , Ai , Ti , Πi , Li ) and its motion specification BA Biφ . We slightly modify the classical construction
of a product automaton of Ti and Biφ to obtain a BA that
represents the traces of Ti accepted by Biφ and furthermore
explicitly captures the services provided along the trace.
Definition 6 (Motion product). The motion product of
a TS Ti = (Si , sinit,i , Ai , Ti , Πi , Li ), and a BA Biφ =
φ
(Qφi , qinit,i
, δiφ , 2Πi , Fiφ ) is a BA Pi = (Qi , qinit,i , δi , 2Σi ∪
φ
{Ei }, Fi ), where Qi = Si × Qφi ; qinit,i = (sinit,i , qinit,i
);
0 0
0
((s, q), Li (α), (s , q ) ∈ δi if and only if (s, α, s ) ∈ Ti , and
(q, Li (s), q 0 ) ∈ δiφ ; and Fi = {(s, q) | q ∈ Fiφ }.
Intuitively, we propose to keep only the significant states
that have an outgoing transition labeled with Li (α) 6= Ei
and replace exact sequences of transitions in Pi with single
transitions representing reachability. While doing so, we have
to take into account whether the removed state is accepting
or not to correctly preserve the accepting condition of Pi .
Definition 7 (Insignificant states in Pi ). A state p of the
motion product Pi is significant if it is (i) the initial state
p = qinit,i , or (ii) if there exists a transition (p, σ, p0 ) ∈ δi ,
such that σ 6= Ei ; and insignificant otherwise.
A reduced motion product P̈i is built from Pi according
to Alg. 1. First, we remove all insignificant non-accepting
states and their incoming and outgoing transitions (lines 3, 4).
We replace each state with a set of transitions leading
directly from the state’s predecessors to its successors, i.e.,
we concatenate the incoming and the outgoing transitions
(line 5). The labels of the new transitions differ: if both labels
of the concatenated incoming and outgoing transition are Ei ,
then the new label will be Ei to indicate that the transition
represents a sequence of actions that are not interesting with
respect to the local satisfaction of task specifications. On the
other hand, if the label σ of the incoming transition belongs
to 2Σi , we use the action σ as the label for the new transition.
Each path between two significant states in Pi maps onto a
path between the same states in P̈i and the sequences of
non-silent services read on the labels of the transitions of
the two paths are equal; and vice versa. Second, we handle
the insignificant accepting states (line 7) similarly to the non-

accepting ones, however, we do not remove the states whose
predecessors include a significant state in order to preserve
the accepting condition. There is a correspondence between
the infinite runs of Pi and the infinite runs of P̈i : for each
run of Pi there exists a a run of P̈i , such that the states of the
latter one are a subsequence of the states of the former one,
the sequences of non-silent services read on the labels of the
transitions of the two runs are equal, and that the latter one
is accepting if and only if the former one is accepting; and
vice versa. This correspondence will allow us to reconstruct
a desired run of Pi from a run of P̈i , as we will show in
Sec. IV-A.4. From P̈i , we further remove all states from
which none of the states in F̈i is reachable, and we can
keep only one copy of duplicate states that have analogous
incomming and outgoing edges (omitted from Alg. 1).
Algorithm 1 Reduction of the motion product
Input: motion product Pi = (Qi , qinit,i , δi , 2Σi ∪ 2Ei , Fi )
Output: reduced BA P̈i = (Q̈i , q̈init,i , δ̈i , 2Σi ∪ 2Ei , F̈i )
1: initialize P̈i := Pi
2: for all insignificant states p ∈ Qi \ Fi do
3:
Q̈i := Q̈i \ {p}
4:
δ̈i := δ̈i \ {(p0 , σ, p), (p, σ, p0 )|p0 ∈ Q̈i , σ ∈ 2Σi ∪ 2Ei }
5:
δ̈i := δ̈i ∪ {(p0 , σ, p00 ) | p0 , p00 ∈ Q̈i , σ ∈ 2Σi ∪ 2Ei ,
(p0 , σ, p), (p, Ei , p00 ) ∈ δ̈i }
6: end for
7: for all insignificant states p ∈ Fi , such that all predecessors
of p in P̈i are insignificant do
8:
if (p, Ei , p) ∈ δ̈i then
9:
δ̈i := δ̈i ∪ {(p0 , Ei , p0 ) | (p0 , Ei , p) ∈ δ̈i }
10:
end if
11:
Q̈i := Q̈i \ {p}
12:
δ̈i := δ̈i \ {(p0 , σ, p), (p, σ, p0 )|p0 ∈ Q̈i , σ ∈ 2Σi ∪ 2Ei }
13:
δ̈i := δ̈i ∪ {(p0 , Ei , p00 ) | p0 , p00 ∈ Q̈i , (p0 , Ei , p), (p, Ei , p00 )
∈ δ̈i }
14: end for

2) Preprocessing the task specifications: Next, we build
a local task and motion product automaton for each agent i
separately, to capture the admissible traces of i that comply
both with its motion and task specification. At this stage, the
other agents’ collaboration capabilities are not yet included.
Definition 8 (Task and motion product). The task and
motion product of a reduced motion product automaton
P̈i = (Q̈i , q̈init,i , δ̈i , 2Σi ∪ 2Ei , F̈i ), and the task specifiψ
ψ Σ
ψ
cation BA Biψ = (Qψ
i , qinit,i , δi , 2 , Fi ) is a BA P̄i =
Σ
Ei
(Q̄i , q̄init,i , δ̄i , 2 ∪2 , F̄i ), where Q̄i = Q̈i ×Qψ
i ×{1, 2, 3};
ψ
q̄init,i = (qinit,i , qinit,i
, 1); F̄i = {(q1 , q2 , 2) | q2 ∈ Fiψ };
and ((q1 , q2 , j), σ, (q10 , q20 , j 0 ) ∈ δ̄i iff
◦ σ = Ei , (q1 , Ei , q10 ) ∈ δ̈i , and q2 = q20 ; or
◦ σ ∈ 2Σ , (q1 , σ ∩ 2Σi , q10 ) ∈ δ̈i , and (q2 , σ, q20 ) ∈ δiψ ,
and j 0 = 2, if j = 1 and q10 ∈ F̈i , j 0 = 3 if j = 2 and
q20 ∈ F̈iψ , j 0 = 1 if j = 3, and j = j 0 otherwise.
The above construction leverages ideas from building a
BA that accepts a language intersection of multiple given
BAs. The accepting runs of P̄i map onto accepting runs
of P̈i , and hence to the traces of Ti satisfying the motion
specification φi , and onto accepting runs of Biψ ; and vice
versa. Clearly, some of the transitions of P̄i require a

collaboration of some other agents, while some of them do
not. In order to further reduce the size of P̄i , we introduce
a mapping Dep i : δ̄i → 2N to indicate for each transition
t = (p, σ, p0 ) ∈ δ̄i the set of agents Dep i (t) ⊆ N whose
collaboration is required. We formalize Dep i through the
notion of assisting services. Moreover, for each agent i, we
find a subset of its services that affect the local satisfaction
of a task specification of another agent through the notion
of globally assisting services.
Definition 9 (Assisting services). Suppose that i 6= i0 . A
service ρ ∈ Σi0 is not assisting on a transition (p, σ, p0 ) ∈ δ̄i
of P̄i if and only if it holds that (p, σ ∪ {ρ}, p0 ) ∈ δ̄i ⇐⇒
(p, σ \ {ρ}, p0 ) ∈ δ̄i ; it is assisting on (p, σ, p0 ) otherwise.
Dep i (t) = {i} ∪ {i0 | i0 6= i and ∃ρ ∈ Σi0 assisting on t}.
Definition 10 (Globally assisting services). A service ρ ∈
Σi0 of agent i0 ∈ N is globally assisting if there exists i ∈ N ,
i 6= i0 , and a transition t ∈ δ̄i , such that ρ is assisting on t.
Now, similar ideas as in Alg. 1 can be used to reduce
the size of each action and motion product P̄i , with the
following, altered definition of significant states:
Definition 11 (Insignificant states in P̄i ). A state p of the
task and motion product P̄i is significant if it is either (i) the
initial state p = q̄init,i , or (ii) if there exists a transition
(p, σ, p0 ) ∈ δ̄i , such that there exists a globally assisting
service ρ ∈ σ ∩ Σi , or (iii) if there exists a transition
(p, σ, p0 ) ∈ δ̄i , such that Dep i (p, σ, p0 ) 6= {i}; the state p
is insignificant otherwise.
Informally, the condition (ii) states that at a significant
state, the agent i has the ability to assist other agents,
whereas the condition (iii) states that at a significant state,
the assistance of the other agents influences the agent i’s
own task specification local satisfaction. With a slight abuse
of notation, we replace all labels of all outgoing transitions
of insignificant states of P̄i with Ei . This time Ei represents
a service set that is completely independent. We can now directly apply Alg. 1 to remove the insignificant states from P̄i ,
with the exception that 2Σi is at all places replaced with 2Σ .
bi = (Q
b i , qbinit,i , δbi , 2Σ ∪2Ei , Fbi ).
The resulting automaton is P
Similarly as before, there is a correspondence beween the
bi : for each run
infinite runs of P̄i and the infinite runs of P
b
of P̄i there exists a a run of Pi , such that the states of the
latter one are a subsequence of the states of the former one,
the sequences of services read on the labels of the transitions
leading from the significant states of the two runs are equal,
and that the latter one is accepting if and only if the former
bi
one is accepting; and vice versa. The number of states of P
is at most twice the number of significant states in P̄i .
3) Global product: From the reduced task and motion
b1 , . . . , P
bN , we build a single one, that
product automata P
finally represents the inter-agent collaborations. The construction is a twist to the well-known construction of BA
intersection. We associate the transitions of the BA with the
subsets of agents that are required to make this transition
collaboratively, i.e., with the subsets of agents that need to
synchronize prior this transition.

Definition 12 (Global product). The global product of the
b1 , . . . P
bN , where
reduced task and motion product automata P
Σ
Ei b
b
b
b
Pi = (Qi , qbinit,i , δi , 2 ∪ 2 , Fi ), for all i ∈ N , is a BA
P = (Q, qinit , δ, 2Σ ∪2E={Ei |i∈N } , F ) with a mapping Dep :
b 1 ×. . .× Q
b N ×{1, . . . , N +1}; qinit =
δ → 2N , where Q = Q
(b
qinit,1 , . . . , qbinit,N , 1); F̄i = {(q1 , . . . , qN , N ) | qN ∈ FbN };
0
and t = ((q1 , . . . , qN , j), σ, (q10 , . . . , qN
, j 0 )) ∈ δ iff either
◦ ∃i ∈ N , such that σ = Ei , (qi , Ei , qi0 ) ∈ δbi , qi0 = qi00 ,
for all i0 6= i, and j 0 = j + 1 if j = i and qi0 ∈ Fbi ,
j 0 = 1 if j = N + 1, and j 0 = j otherwise. Then we set
Dep(t) = {i}; or
◦ σ ∈ 2Σ , and ∃ I ⊆ N , such that for all i ∈ I it
holds that (qi , σ, qi0 ) ∈ δbS
i while for all i 6∈ I it holds
that qi = qi0 . Moreover, i∈I Dep i (qi , σ, qi0 ) ⊆ I, and
j 0 = j + 1 if j ∈ I and qj0 ∈ Fbj , j 0 = 1 if j = N + 1,
and j 0 = j otherwise. Then we set Dep(t) = I.
Each accepting run of the global product P maps directly
on the accepting runs of the reduced task and motion product
automata and vice versa, for each collection of accepting runs
of the reduced task and motion product automata, there exists
an accepting run of the global product P. Note that by this
construction, deadlocks are avoided.
4) Synthesis of the strategies: The final step of our
solution is the generation of the strategy in P and its mapping
onto a trace τi of Ti and a synchronization sequence γi over
Sync i , for all i ∈ N . Using standard graph algorithms (see,
e.g., [1]), we find an accepting run q1 q2 . . . over a word
σ1 σ2 . . . in P, where qj = (b
q1,j , . . . , qbN,j , k), for all j ≥ 1.
For each agent i ∈ N :
(i) Consider the sequence qbi,1 qbi,2 . . ., that is obtained
by the projection of the accepting run q1 q2 . . . onto
bi . Let ι1 ι2 . . . be the subsequence
the states of P
of all indexes, such that i ∈ Dep(qιj , σιj , qιj +1 ).
bi over
Then qbi,ι1 qbi,ι2 . . . is an accepting run of P
the word σι1 σι2 . . . and γ
bi = rbi,1 rbi,2 . . . =
Dep(qι1 σι1 qι1 +1 )Dep(qι2 σι2 qι2 +1 ) . . . is a synchronization sequence.
(ii) From the construction of Pbi , we know that there exists an accepting run q̄i,1 q̄i,2 . . . in P̄i over a word
σ̄i,1 σ̄i,2 . . ., such that qbi,ι1 qbi,ι2 . . . is a subsequence
q̄i,`1 q̄i,`2 . . . of q̄i,1 q̄i,2 . . . and σι1 σι2 . . . is the corresponding subsequence σ̄i,`1 σ̄i,`2 . . . of σ̄i,1 σ̄i,2 . . ..
The synchronization sequence γ̄i = r̄i,1 r̄i,2 . . . is constructed by setting r̄i,`j = rbi,ιj , for all j ≥ 1, and
r̄i,j = sync({i}) otherwise.
(iii) The mapping from the task and motion product
P̄i onto P̈i is processed as follows: Suppose that
ψ
q̄i,j = (q̈i,j , qi,j
, k), for all j ≥ 1. The accepting
run q̄i,`1 q̄i,`2 . . . then maps onto the accepting run
q̈i,`1 q̈i,`2 . . . over σ̈i,1 σ̈i,2 . . ., where σ̈i,j = Ei if σ̄i,j =
Ei , and σ̈i,j = σ̄i,j ∩ 2Σi otherwise. Naturally, γ̈i = γ̄i .
(iv) The accepting run qi,1 qi,1 . . . of the motion product Pi
over a word σi,1 σi,1 . . . and a synchronization sequence
γi is obtained from the reduced motion product P̈i by
an analogous construction as in the case of mapping
bi onto the
from the reduced task and motion product P

task and motion product P̄i .
(v) Finally, an accepting run qi,1 qi,2 . . . of Pi maps onto a
trace τi of Ti . The desired synchronization sequence is
γi .
B. Discussion
Strategy execution and event-based recomputation: In the
above described solution, the strategy for each agent is
constructed in an offline manner, and executed independently. However, the solution can be modified to an eventtriggered one, where synchronization is triggered by need
and strategies are periodically recomputed in order to adapt
to different execution speed of different agents and to handle
various optimization criteria. The details of this solution is
one of our future topics of interest. Mutually dependency:
We supposed that all of the considered agents are mutually
dependent through their task specifications, either directly
or transitively. If this is not the case, the team of agents
can be partitioned into dependency classes as suggested
in [5]. Complexity: In the worst case, our solution meets
the complexity of the centralized solution. However, this is
often not the case. Since the size of the global product is
highly dependent on the number of globally assisting services
available in the agents’ workspace, our solution is particularly suitable for systems with complex motion capabilities,
sparsely distributed services of interest, and occasional needs
for collaboration. Its benefits are demonstrated in Sec. V.
V. ILLUSTRATIVE EXAMPLE
An illustrative example with 3 robots is given in Fig. 1.
Their workspace is partitioned into 100 cells, and a robot’s
state is defined by the cell it is present at. Agent 1 (green)
is a ground vehicle and has to avoid the obstacles (in
gray), while agents 2 (orange) and 3 (purple) are UAVs
and their workspace is obstacle-free except for walls (thick).
The cells are each labeled with an atomic proposition from
{R1, R2, R3, R4} indicating the room to which the cell
belongs. Services are available in cell marked with stripes.
Agent 1 can load (green horizontal stripe) and unload (green
vertical). Agent 2 can help (orange horizontal) or inform
(orange vertical). Agent 3 can assist (purple horizontal). The
motion formulas are: For agent 1 to avoid room R1, φ1 =
G¬R1, for agent 2 to avoid R2, φ2 = G¬R2, and for agent 3
to survey R1 and R2, φ3 = GF R1∧GF R2. The task formulas
are: For agent 1 to periodically load collaboratively with
agents 2 and 3 and then to unload, collaboratively with agent
2 or 3: ψ1 = load ∧ help ∧ assist ∧ G (load ⇒ X (unload ∧
(help ∨ assist))) ∧ G (unload ⇒ X (load ∧ help ∧ assist)),
for agent 2 to periodically service inform, ψ2 = GF inform,
for agent 3 ψ3 = assist ∨¬assist, i.e., agent 3 is not assigned
a specific task. An example of as collection of the desired
trajectories and synchronizations is given in Fig. 1.
In classical centralized planning, only the synchronous
product of the TSs of the three agents would have ≈ 100
000 states. In our case, the BAs for the given formulas
had 2,2,3,2,2,1 states, respectively, and hence their language
intersection BAs reaches 2 ∗ 2 ∗ 3 ∗ 2 ∗ 2 ∗ 1 ∗ 7 ≈ 330 states.

2a

R1 R2

2b

R3 R4

1
3

Fig. 1: Examples of desired trajectories of 3 robots in a shared workspace.
The synchronization events at the moments of providing nonsilent services
are depicted with stars. First, all agents synchronize in the bottom left corner
and provide load, help, assist; then agent 2 provides inform and then agents
1 and 3 provide unload, assist, or vice versa; finally, all agents synchronize
in the bottom left corner, and start periodically executing the above.

The overall product automaton has then up to ∼ 30 millions
states. In contrast, in our solution, the individual task and
b1 , P
b2 , P
b3 after all reductions have 27,17,
motion products P
and 8 states, respectively. Hence the largest structure dealt
with during the overall procedure, i.e., the product automaton
P has only 27 ∗ 17 ∗ 8 ∗ 4 ∼ 15000 states.
R EFERENCES
[1] C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press,
2008.
[2] A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi. Motion
planning with complex goals. Robotics Automation Magazine, IEEE,
18(3):55 –64, 2011.
[3] Y. Chen, X. C. Ding, A. Stefanescu, and C. Belta. Formal approach
to the deployment of distributed robotic teams. IEEE Transactions on
Robotics, 28(1):158–171, 2012.
[4] I. Filippidis, D.V. Dimarogonas, and K.J. Kyriakopoulos. Decentralized multi-agent control from local ltl specifications. In Proceedings
of the IEEE Conference on Decision and Control, pages 6235–6240,
2012.
[5] M. Guo and D. V. Dimarogonas. Multi-agent plan reconfiguration
under local LTL specifications. International Journal of Robotics
Research, pages 218–235, 2015.
[6] M. Guo, J. Tumova, and D. V. Dimarogonas. Cooperative decentralized multi-agent control under local LTL tasks and connectivity
constraints. In Proceedings of the IEEE Conference on Decision and
Control, pages 75–80, 2014.
[7] G. Jing, C. Finucane, V. Raman, and H. Kress-Gazit. Correct highlevel robot control from structured english. In Proceedings of the
IEEE International Conference on Robotics and Automation, pages
3543–3544, 2012.
[8] S. Karaman and E. Frazzoli. Vehicle routing with temporal logic specifications: Applications to multi-UAV mission planning. International
Journal of Robust and Nonlinear Control, 21:1372–1395, 2011.
[9] M. Kloetzer and C. Belta. A fully automated framework for control of
linear systems from temporal logic specifications. IEEE Transactions
on Automatic Control, 53(1):287–297, 2008.
[10] M. Kloetzer, X. C. Ding, and C. Belta. Multi-robot deployment from
LTL specifications with reduced communication. In Proceedings of
the IEEE Conference on Decision and Control and European Control
Conference, pages 4867–4872, 2011.
[11] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal logicbased reactive mission and motion planning. IEEE Transactions on
Robotics, 25(6):1370–1381, 2009.
[12] S. G. Loizou and K. J. Kyriakopoulos. Automated planning of motion
tasks for multi-robot systems. In Proceedings of the IEEE Conference
on Decision and Control, volume 44, 2005.
[13] J. Tumova and D. Dimarogonas. A receding horizon approach to
multi-agent planning from local LTL specifications. In Proceedings of
the American Control Conference, pages 1775–1780, 2014.

[14] J. Tumova and D. Dimarogonas. Multi-agent planning under local LTL
specifications and event-based synchronization. 2015. Submitted.
[15] A. Ulusoy, S. L. Smith, X. C. Ding, C. Belta, and D. Rus. Optimality
and robustness in multi-robot path planning with temporal logic
constraints. International Journal of Robotics Research, 32(8):889–
911, 2013.
[16] C. Wiltsche, F. A. Ramponi, and J. Lygeros. Synthesis of an
asynchronous communication protocol for search and rescue robots. In
Proceedings of the European Control Conference, pages 1256–1261,
2013.
[17] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding Horizon
Control for Temporal Logic Specifications. In Hybrid systems:
Computation and Control (HSCC), pages 101–110, 2010.

