Multi-Agent Planning under Local LTL Specifications and
Event-Based Synchronization ?
Jana Tumova a , Dimos V. Dimarogonas a

arXiv:1610.08380v1 [] 26 Oct 2016

a

School of Electrical Engineering, KTH Royal Institute of Technology, SE-100 44 Stockholm

Abstract
We study the problem of plan synthesis for multi-agent systems, to achieve complex, high-level, long-term goals that are
assigned to each agent individually. As the agents might not be capable of satisfying their respective goals by themselves,
requests for other agents’ collaborations are a part of the task descriptions. We consider that each agent is modeled as
a discrete state-transition system and its task specification takes a form of a linear temporal logic formula. A traditional
automata-based approach to multi-agent plan synthesis from such specifications builds on centralized team planning and full
team synchronization after each agents’ discrete step, and thus suffers from extreme computational demands. We aim at
reducing the computational complexity by decomposing the plan synthesis problem into finite horizon planning problems that
are solved iteratively, upon the run of the agents. We introduce an event-based synchronization that allows our approach to
efficiently adapt to different time durations of different agents’ discrete steps. We discuss the correctness of the solution and find
assumptions, under which the proposed iterative algorithm leads to provable eventual satisfaction of the desired specifications.
Key words: Temporal logic, finite state machines, formal verification, path planning, synchronization, decentralized control,
robot control.

1

Introduction

In recent years, a considerable amount of attention has
been devoted to synthesis of robot controllers for complex, high-level missions, such as “periodically survey
regions A, B, C, in this order, while avoiding region D”,
specified as temporal logic formulas. Many of the suggested solutions to variants of this problem rely on a hierarchical procedure [3, 11, 13, 21]: First, the dynamics
of the robotic system is abstracted into a finite transition system using e.g., sampling or cell decomposition
methods. Second, leveraging ideas from formal verification, a discrete plan that meets the mission is synthesized. Third, the plan is translated into a controller for
the original system. In this work, we focus on a multiagent version of the above problem. We consider a heterogeneous team of robots, that are assigned a temporal
logic mission each. As the robots may not be able to accomplish their missions without the help of the others,
the specifications may contain requirements on the other
team members’ behavior. For instance, consider a ware? This paper was not presented at any IFAC meeting. Corresponding author is J. Tumova.
Email addresses: tumova@kth.se (Jana Tumova),
dimos@kth.se (Dimos V. Dimarogonas).

Preprint submitted to Automatica

house solution with two mobile robots. A part of the first
robot’s mission is to load an object in region A, but it is
not able to load it by itself. Therefore, the mission also
includes a task for the second robot, to help loading. The
goal of this paper is to efficiently synthesize a plan for
each agent, such that each agent’s mission is met. We follow the hierarchical approach to robot controller synthesis as outlined above and we narrow our attention to the
second step of the approach, i.e., to generating discrete
plans. The application of the algorithm that we propose
is, however, not restricted to discrete systems: For the
first step of the hierarchical approach, numerous methods for discrete modeling of robotic systems can be used
(see, e.g., [11, 13, 14, 21] and the references therein); for
the third step, low-level controllers exist that can drive a
robot from any position within a region to a goal region
(see, e.g., [2]). The agents can, but do not have to, mutually synchronize after the execution of their respective
discrete steps. The desired plans thus comprise not only
of the agents’ discrete steps to be taken, but also their
synchronizations. Besides the satisfaction of all agents’
missions, our goal is to avoid unnecessary synchronization in order to improve the team performance.
As a mission specification language, we use Linear
Temporal Logic (LTL), for its resemblance to natural
language [9], and expressive power. Here, we built LTL

27 October 2016

agents towards a progress within a finite planning horizon; similar ideas were used in [6, 17] for a single-agent
LTL planning to achieve a locally optimal behavior.

formulas over services, i.e., events of interest associated with execution of certain actions rather than over
atomic propositions, i.e., inherent properties of the system states. Instead of evaluation of the specification as
a conjunction of LTL formulas over the whole team behaviors, we propose the notion of satisfaction of an LTL
formula from local perspective. This way, the problem
of finding a collective team behavior is decomposed into
several subproblems, enabling us to avoid the straightforward, but expensive fully centralized planning. The
contribution of this paper can be summarized as the
introduction of an efficient, iterative, finite horizon
planning technique in the context of bottom-up plan
synthesis for multi-agent systems from local LTL specifications. To our best knowledge, such an approach has
not been taken to address the multi-agent LTL planning
before. Our algorithm is adaptive in the sense that even
if the real behavior of the team is not as planned due to
unpredictable time durations of the agents’ steps, the
event-based synchronization and replanning still guarantees the satisfaction of all the tasks. This feature can
be especially beneficial in heterogeneous multi-robot
motion and task planning problems, where individual
robots traverse their common environment at different
speeds. This paper builds on our earlier work in [18].
In addition, it relaxes the assumption that the agents
synchronize after every discrete step of theirs and introduces the event-based synchronization and replanning.

The rest of the paper is structured as follows. In Sec. 2,
we fix the preliminaries. Sec. 3 introduces the problem
and summarizes our approach. In Sec. 4, the details of
the solution are provided. In Sec. 5, we provide analysis
and discussion of the solution. We present simulation
results in Sec. 6, and we conclude in Sec. 7.
2

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. A finite or infinite sequence of elements
of S is called a finite or infinite word over S, respectively.
The i-th element of a word w is denoted by w(i). A subsequence of an infinite word w = w(1)w(2) . . . is a finite
or infinite sequence of its elements w(i1 )w(i2 ) . . ., where
∀1 ≤ j. 1 ≤ ij ≤ ij+1 . A factor of w is a continuous, finite
or infinite, subsequence w(i)w(i + 1) . . ., where 1 ≤ i. A
prefix of w is a finite factor starting at w(1), and a suffix of w is an infinite factor. N and R+
0 denote positive
integers and non-negative real numbers, respectively.
A transition system (TS) is a tuple T = (S, sinit , A, T ),
where S is a finite set of states; sinit ∈ S is the initial
state; A is a finite set of actions; and T ⊆ S × A → S is a
partial deterministic transition function. For simplicity,
α
we denote a transition T (s, α) = s0 by s −
→ s0 . 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,
αi
si −→
si+1 . A trace fragment τ̂ is a finite factor of a
trace τ that begins and ends with a state.

Multi-agent planning from temporal logic specification
has been explored in several recent works. Planning from
computational tree logic was considered in [16], whereas
in [12, 15], the authors focus on planning behavior of
a team of robots from a single, global LTL specification. A fragment of LTL has been considered as a specification language for vehicle routing problems in [10],
and a general reactivity LTL fragment has been used
in [20]. Decentralized control of a robotic team from local LTL specification with communication constraints
is proposed in [7]. However, the specifications there are
truly local and the agents do not impose any requirements on the other agents’ behavior. Thus, the focus
of the paper is significantly different to ours. As opposed to our approach, in [4, 19], a top-down approach
to LTL planning is considered; 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 for each robot. In [8], bottom-up
planning from LTL specifications is considered, and a
partially decentralized solution is proposed that takes
into account only clusters of dependent agents instead
of the whole group. A huge challenge of the previous approach is its extreme computational complexity, which
we tackle in this work by applying receding horizon approach to multi-agent planning. Receding horizon approach was leveraged also in [21] to cope with uncertain
elements in an environment in single-robot motion planning. To guarantee the satisfaction of the formula, we use
an attraction-type function that guides the individual

A linear temporal logic (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, U, F, and G are temporal operators. The semantics
of LTL are defined over infinite words over 2Π . π ∈ Π is
satisfied on w = $1 $2 . . . if π ∈ $1 . X φ holds true if φ is
satisfied on the word that begins in the next position $2 ,
φ1 U φ2 states that φ1 has to be true until φ2 becomes
true, and F φ and G φ are true if φ holds on w eventually,
and always, respectively. We denote the satisfaction of φ
on a word w as w |= φ. The set of all words accepted by
an LTL formula φ is L(φ). For full details see, e.g., [1].
An automaton 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; and F is an accepting condition. It
is deadlock-free if ∀q ∈ Q, σ ∈ Σ. δ(q, σ) 6= ∅. We define the set of states δ̂ k (q) reachable from q ∈ Q in exactly k steps inductively as δ̂ 0 (q) = {q}, and δ̂ k (q) =

2

αj

| ∃ σ ∈ Σ. (q 0 , σ, q 00 ) ∈ δ}, ∀k ≥ 1. A
Büchi automaton (BA) is an automaton with the accepting condition F ⊆ Q. A run of the BA B from q1 ∈ Q
over w = σ1 σ2 . . . ∈ Σω is a sequence ρ = q1 q2 . . ., such
that ∀i ≥ 1. (qi , σi , qi+1 ) ∈ δ. A run ρ 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 . The set of all words accepted by B is
L(B). Any automaton (Q, qinit , Σ, δ, F ) can be viewed as
a graph (V, E) with the vertexes V = Q and the edges E
given by δ in the expected way. The standard notation
then applies: A path is a finite alternating sequence of
states and transition labels qi σi qi+1 . . . qk−1 σk−1 qk , such
that ∀i ≤ j < k. (qj , σj , qj+1 ) ∈ δ. dist(q, q 0 ) denotes
the length of the shortest path between q and q 0 , i.e.,
the minimal number of states in a path q . . . q 0 . If no
such path exists, then dist(q, q 0 ) = ∞. If q = q 0 , then
dist(q, q 0 ) = 0. The shortest path can be computed using
Dijkstra algorithm (see, e.g., [5]).
S

3

q 0 ∈δ̂ k−1 (q) {q

00

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 a trace.
The durations are not explicitly modeled in the TS Ti
due to the fact that they are unknown, but, as we will
discuss later on, their history plays an important role
in defining the semantics of the agent’s behaviors, their
interactions and satisfaction of their tasks.
Synchronization Capabilities. The agents have also
the ability to synchronize, i.e., to wait for each other and
to proceed with the further execution simultaneously.
Through the simultaneous execution of certain transitions, the agents have the ability to collaborate (e.g., an
agent loading heavy goods may need a second agent simultaneously helping to load it). The synchronization
is modeled through the synchronization requests, but
the particular implementation of the synchronization
scheme is beyond the scope of this paper. While being in
a state s, an agent i can send a request synci to the set
of agents N notifying them that it is ready to synchronize. Then, before proceeding with the execution of any
action α ∈ Ai , it has to wait till synci0 has been sent by
each agent i0 ∈ N , i.e., till the moment when each agent
i0 ∈ N is ready to synchronize, too. The synchronization
is immediate once each of the agents i0 ∈ N has sent its
request synci0 and all agents in N start executing the
next action at the same time. Alternatively, an agent i
indicates that it does not need to synchronize through requesting nosync i . The set of all synchronization requests
of an agent i is thus Sync i = {sync i , nosync i }. For simplicity, 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. In other words,
no time is spent idling in our system model. This does
not prevent us to capture the agents’ abilities of staying
in their respective states. Instead of idling, we include a
α
so-called self-loop s −
→ s for some α ∈ Ai , all s ∈ Si ,
and all Ti , 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 requested in the state si,j . Note that if
the request nosync i has been sent in si,j , then ∆si,j = 0.

Problem Formulation and Approach

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 own, independent
tasks. Although we permit each agent’s task to involve
requirements on the others, we adopt the second viewpoint; to decide whether the agents’ tasks are met, we
do not look at the global team behavior. In contrast, we
propose the concept of local specification satisfaction to
determine whether an agent’s task is fulfilled from its
own perspective. Our goal is to synthesize a plan for each
agent that comprises of (i) the actions to be executed and
(ii) the synchronization requests imposed on the other
agents. Together, the strategies have to ensure the local
satisfaction of each of the task specifications regardless
of the time duration of the planned action executions.
We consider N agents (e.g., robots in a partitioned environment). Each agent i ∈ N , where N = {1, . . . , N }
has action execution and synchronization capabilities.
Action Execution Capabilities. The agent i’s
action execution capabilities are modeled as a TS
Ti = (Si , sinit,i , Ai , Ti ), whose states correspond to
states of the agents (e.g., the locations of the robots in
the regions of their environment). The actions Ai represent abstractions of the agent’s low-level controllers, and
the transitions Ti correspond to the agent’s capabilities
to execute the actions (e.g., the ability of the robots
to move between two regions). The traces are, roughly
speaking, the abstractions of the agents’ long-term behaviors (e.g., the robots’ trajectories). For the simplicity
of the presentation, we assume that each state s ∈ Si is
reachable from all states s0 ∈ Si via a sequence of transitions. 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 duration of the

Remark 1 In order to accomodate synchronization with
a subset of agents, we can parametrize the synchronization requests Sync i = {sync i (M ) | {i} ⊆ M ⊆ N }. The
use of such a definition is discussed later in Remark 3.
Services. Each of the agents’ tasks is given in terms of
temporal requirements on events of interest, which we
call services. The set of all services that can be provided
by an agent i ∈ N is Πi . Services are provided within the
agents’ transitions; each action α ∈ Ai is labeled either
with (i) a service set $ ∈ 2Πi provided upon the execution of α, or (ii) a special silent service set Ei = {εi },
εi 6∈ Πi indicating that α is not associated with any

3

The notion of behavior, however, does not reflect the
above described synchronization scheme. To that end,
we define compatible behaviors. In what follows, the
behavior of i ∈ N is denoted by βi = (τi , γi , Ti ),
where τ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 . . ..
Definition 2 (Compatible behaviors) A set of behaviors of the agents in N is compatible, if the following
holds for all i ∈ N , and j ≥ 1: Suppose that ri,j = synci .
Then for all i0 ∈ N , there exists a matching index
j 0 ≥ 1, such that ri0 ,j 0 = synci0 , and tαi,j = tαi0 ,j0 . Furthermore, there exists i0 ∈ N , such that tsi0 ,j0 = tαi0 ,j0 ,
i.e., such that ∆si0 ,j0 = 0, for the matching index j 0 .

Fig. 1. An example of an environment partitioned into cells with
rooms R1 , . . . , R5 . Loading/unloading points are in green (light).
Simple tasks t1 , . . . , t5 can be executed in purple (dark) regions.

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 self-loops
α
of type s −
→ s introduced above to model staying are
naturally labeled with Ei . Without loss of generality, we
assume that Πi ∩ Πi0 = ∅, for all i, i0 ∈ N , i 6= i0 . As
it will become clear later, the choice of non-silent and
silent services in place of the traditional atomic propositions is motivated by the nature of multi-agent planning,
where the agents are concerned about each other only
at selected times, e.g., when collaboration is required.

Suppose that the trace τi , the synchronization sequence
γi , and the transition time durations ∆αi,1 , ∆αi,2 , . . . are
all fixed for all i ∈ N . Then there exists at most one collection of synchronization time durations ∆si,1 ∆si,2 . . .,
i ∈ N that yields a set of compatible behaviors {βi =
(τi , γi , Ti ) | i ∈ N }. In other words, if the agents follow
the synchronization scheme, the existence and the values
of their synchronization time durations and hence also
their behavior time sequences are uniquely determined
by τi , γi , and ∆αi,1 , ∆αi,2 , . . . given for all i ∈ N .

Finally, we model an agent i ∈ N as the tuple Mi =
(Ti , Sync i , Πi , Li ).

Specifications. The individual agents’ tasks may concern the respective agent’s services as well as the services of the others. Formally, each S
of the agents is given
an LTL formula φi over Πi = i0 ∈Di Πi0 , for some
{i} ⊆ Di ⊆ N . Loosely speaking, the satisfaction of an
agent’s formula depends on, and only on the behavior of
the subset of agents Di , including the agent itself.

Example 1 An illustrative example of three mobile
robots in a common partitioned workspace is depicted
in Fig. 1. The agents can transit between the adjacent
cells that are not separated by a wall or stay where they
are. The former transitions are labeled with Ei , while
non-silent services are associated with some of the latter
ones. Namely, agent 1 can load (lH , lA , lB ), carry, and
unload (uH , uA , uB ) a heavy object H or a light object
A, B, in the green cells. Agent 2 can help to load object
H (hH ), and execute simple tasks in the purple regions
(t1 − t5 ). Agent 3 is capable of taking a snapshot of the
rooms (s1 − s5 ) when being present in there.

Example 1 (continued) The robots are assigned the
following collaborative tasks. Agent 1 needs the help of
agent 2 with loading the heavy object. Then, it should
carry the heavy object to an unloading point and unload it. Then, it should periodically loadVand unload both
light objects (φ1 = F(lH ∧ hH ∧ X uH ∧ i∈{A,B} GF (li ∧
Xui ))). Agent 2 should periodically execute the simple
tasks t1 , . . . , t5 , in this order. Furthermore, it requests
agent 3 to witness the execution t5 , by taking a snapshot of the room R4 at the moment of the execution
(φ2 = GF (t1 ∧X (t2 ∧X (t3 ∧X (t4 ∧X t5 V
∧s4 )))))). Agent 3
should patrol rooms R2 , R4 , R5 (φ3 = i∈{2,4,5} GF si ).

Behaviors. The behavior of an agent i is defined by the
actions it executes, its synchronizations with the other
agents, and the time instants when the action executions
and the synchronizations take place.
Definition 1 (Behavior) A behavior of an agent i is a
tuple βi = (τi , γi , Ti ), where τi = si,1 αi,1 si,2 αi,2 . . . is a
trace of Ti ; γi = ri,1 ri,2 . . . is a synchronization sequence,
where ri,j ∈ Sync i is the synchronization request sent
at the state si,j ; and Ti = tsi,1 tαi,1 tsi,2 tαi,2 . . . is a nondecreasing behavior time sequence, where tsi,j is the time
instant when the synchronization request ri,j was sent,
and tαi,j is the time instant when the action αi,j started
being executed. The following hold: tsi,1 = 0, and for all
j ≥ 1, tsi,j+1 − tαi,j = ∆αi,j , and tαi,j − tsi,j = ∆si,j .

Let us now introduce the notation needed for formalizing the specification satisfaction. Consider for a moment a single agent Mi = (Ti , Sync i , Πi , Li ), and its
behavior βi , where, for simplicity of notation in the following paragraphs, we use βi = (τ, γ, T), where τ =
s1 α1 s2 α2 . . ., and T = ts1 tα1 ts2 tα2 . . .. We denote by
vτ = $1 $2 . . . = Li (α1 )Li (α2 ) . . . ∈ (2Πi ∪ 2Ei )ω the
unique service set sequence associated with τ . The word

4

where ω2 = {b}, ω3 = {b}, ω5 = {a, b}, and ω6 = {}.
Although B2 is valid, it does not satisfy formula φ2 .

wτ produced by τ is the subsequence of the non-silent elements of this sequence; 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(τ ) = t1 t2 . . . = tα1 tα2 . . . to denote the
trace time sequence, i.e., the subsequence of T when the
(both silent and non-silent) services are provided. Furthermore, T(wτ ) = tι1 tι2 . . . denotes the word time sequence, i.e., the subsequence of T(τ ) that corresponds
to the times when the non-silent services are provided.
The word wτ and the word time sequence T(wτ ) might
be finite as well as infinite. Since in this work we are
interested in infinite, recurrent behaviors, we will consider as valid traces only those that produce infinite
words. Consider a trace τ of Ti with the service set sequence vτ = $1 $2 . . ., and the trace time sequence
T(τ ) = t1 t2 . . .. The service set vτ (t) ∈ 2Πi ∪2Ei provided
at time t ∈ R+
0 is vτ (t) = $j if t = tj for some j ≥ 1,
and Ei otherwise. The satisfaction of each LTL 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 agents i0 ∈ Di provided at the time instances T(wτi )
when i provides a non-silent service set itself.

...

τ1
vτ1

{a}

E1

E1

E1

{a}

{}

E1

E1

T(τ1 )
wτ1

0
{a}

1

2

3

4
{a}

5
{}

6

7

T(wτ1 )
τ2

0

4

5

vτ2

E2

{b}

{b}

E2

{b}

{}

E2

E2

T(τ2 )
wτ2

0

1
{b}

2
{b}

3

4
{b}

5
{}

6

7

1

2

4

5

T(wτ2 )

...

Fig. 2. The trace, the service set the trace time sequences,
the word and the word time sequence of the agents 1, and 2.

Problem 1 Consider a set of agents N = {1, . . . , N },
and suppose that each agent i ∈ N is modeled as a
tuple Mi = (Ti , Sync i , Πi , Li ), and assignedSa task in
the form of an LTL formula φi over Πi = i0 ∈Di Πi0 ,
for some {i} ⊆ Di ⊆ N . For each i ∈ N find a
trace τi = si,1 αi,1 si,2 αi,2 . . . of Ti , and a synchronization sequence γi over Sync i , with the property that regardless of the values of the transition time durations
∆αi,1 , ∆αi,2 . . . ∈ R+
0 , i ∈ N , the set of the agents’ behaviors {βi = (τi , γi , Ti ) | i ∈ N } is compatible, and
Bi = {βi0 | i0 ∈ Di } locally satisfies φi , for all i ∈ N .

Definition 3 (Local LTL satisfaction) Let τ be a
trace of Ti with the word time sequence T(wτ ) = tι1 tι2 . . ..
The word produced by a set of compatible behaviors
0
Bi = {β
S i0 | i ∈ Di } is wBi = ωι1 ωι2 . . . , where
ωιj =
i0 ∈Di vτi0 (tιj ) ∩ Πi , for all j ≥ 1. The set of
behaviors Bi is valid if wBi is infinite. The set of compatible behaviors Bi locally satisfies φi for the agent i,
Bi |= φi , iff Bi is valid and wBi |= φi .

As each of the LTL formulas φi , i ∈ {1, . . . , N } over Πi
can be algorithmically translated into a deadlock-free
language equivalent BA [1], from now on, we pose the
problem with the task specification of each agent i given
as a BA Bi = (Qi , qinit,i , δi , Σi = 2Πi , Fi ) and the local
task satisfaction condition formulated as wBi ∈ L(Bi ).

Note that even if B = Bi = Bj , it may be the case
that wBi 6= wBj and Bi |= φ, but Bj 6|= φ. Let us provide some intuitive insight into the local LTL satisfaction through the following example.
Example 2 Consider two agents represented by models
M1 = (T1 , Sync 1 , Π1 , L1 ), and M2 = (T2 , Sync 2 , Π2 , L2 ),
with Π1 = {a}, Π2 = {b}, and their LTL specifications φ1 = a ∧ X (a ∧ b), φ2 = b ∧ X (b ∧ a), respectively. Note that both 1 ∈ D2 and 2 ∈ D1 , and
hence Π1 = Π2 = {a, b}. Let βi = (τi , γi , Ti ) be the
respective behavior of the agent i ∈ {1, 2} with the
trace τi as illustrated in Fig. 2, γi = ri,1 ri,2 . . ., where
ri,j = nosync i , and Ti = tsi,1 tαi,1 tsi,2 tαi,2 . . ., where
tsi,j = tαi,j = j, for all j ≥ 1. Fig. 2 depicts the service set sequence, the trace time sequence, the word
and the word time sequence for both agents. Specifically, T(wτ1 ) = t1 t5 t6 . . . = 0 4 5 . . . and hence, the
word produced by B1 is wB1 = ω1 ω5 ω6 . . ., where
ω1 = (vτ1 (0) ∪ vτ2 (0)) ∩ Π1 = ({a} ∪ E2 ) ∩ Π1 = {a},
ω5 = (vτ1 (4) ∪ vτ2 (4)) ∩ Π1 = {a, b} ∩ Π1 = {a, b}, and
ω6 = (vτ1 (5) ∪ vτ2 (5)) ∩ Π1 = {} ∩ Π1 = {}. Since wB1
is valid and satisfies φ1 , we conclude that B1 locally satisfies φ1 . In contrast, T(wτ2 ) = t2 t3 t5 t6 . . . = 1 2 4 5 . . .,
and the word produced by B2 is wB2 = ω2 ω3 ω5 ω6 . . .,

Remark 2 Collisions can be resolved either (i) through
an LTL formula that forbids two agents to occupy the
same cell of the environment or to exchange positions if
they are in two neighboring cells, or (ii) through low-level
controllers that implement the agents’ transitions. This
topic is however, beyond the scope of this paper.
A solution to Prob. 1 can be obtained by imposing full
synchronization and modifying the standard control
plan synthesis procedure for TS from LTL specification
(see, e.g., [11]): (1) The set of agents is first partitioned
into dependency classes similarly as in [8] by the iterative application of the rule that if i0 ∈ Di , then i0
belongs to the same dependency class I` as i; (2) For
each dependency class I` = {1` , . . . , n` } and each agent
i ∈ I` , we set γi = ri,1 ri,2 . . ., where ri,j = sync i . This
step yields compatible behaviors of all agents in N

5

4.1

independently of their traces and transition time durations. (3) For each I` = {1` , . . . , n` }, a TS T` with
S` = S1` × . . . × Sn` is constructed that represents the
stepwise-synchronized traces of the agents within the
class. (4) A product P` of T` and B1` , . . . , Bn` is built
that captures only the agents’ traces that are admissible by T` and result into behaviors that locally satisfy
φ1` , . . . , φn` , respectively. The product P` is analyzed
using graph algorithms to find its accepting run that
projects onto the desired traces of Ti , for all i ∈ I` . The
outlined procedure is correct and complete. Although a
certain level of decentralization is achieved via dependency partition, the algorithm suffers from a exponential growth of the product automaton state space with
the increasing number of dependent agents, making the
approach infeasible in practice. Furthermore, the solution requires that the agents synchronize after every
single action execution, which potentially slows down
the overall system performance.

We set γi = ri,1 ri,2 . . ., where ri,j = sync i , i.e., the preliminary synchronization sequence ensures full synchronization of all the agents after every single action execution. The behaviors of agents in N are thus compatible
regardless of their traces and transition time durations.
Namely, we have directly from Def. 1 and Def. 2:
Lemma 1 Let γi = ri,1 ri,2 . . ., where ri,j = sync i , for
all i ∈ N . For traces τi = si,1 αi,1 . . ., τi0 = si0 ,1 αi0 ,1 . . . of
Ti , Ti0 , i, i0 ∈ N , it holds that ti,αj = ti0 ,αj , for all j ≥ 1.
4.2

Finite Horizon Planning

Besides the set of agents N = {1, . . . , N } modeled
as Mi = (Ti , Sync i , Πi , Li ) and the specification BAs
Bi = (Qi , qinit,i , δi , Σi = 2Πi , F ), for all i ∈ N , the
inputs to the finite horizon planning algorithm are: the
current states of T1 , . . . , TN , denoted s1 , . . . , sN , initially
equal to sinit,1 , . . . , sinit,N , respectively; the current
states of B1 , . . . , BN , denoted q1 , . . . , qN , initially equal
to qinit,1 , . . . , qinit,N , respectively; a linear ordering ≺
over N , initially arbitrary; fixed horizons h, H ∈ N,
which, loosely speaking, set the depth of planning in
each BA and TS, respectively.

In this work, we aim to reduce the computational demands of the above solution and to prevent the unnecessarily frequent synchronization. We propose to decompose the infinite horizon planning problem into an infinite sequence of finite horizon planning problems that
are solved iteratively, upon the execution of the system.
We build the dependency classes dynamically at each
iteration. These classes are then often smaller than the
offline ones, which has a dramatic impact on the efficiency of the planning procedure. We show that the stepwise synchronization scheme can replaced with an eventtriggered one. Finally, we prove, that under certain assumptions, the repetitive execution and recomputation
of the plans leads to the satisfaction of all specifications.
4

Preliminary Synchronization Sequence

Dependency Partitioning. We start with partitioning Φ = {B1 , . . . , BN } into the smallest possible subsets Φ1 , . . . , ΦM , such that none of the transitions of any
Bi ∈ Φ` that appears within the horizon h from the current state qi of Bi imposes restrictions on any agent i0 ,
where Bi0 6∈ Φ` . This partition corresponds to the necessary and sufficient dependency up to the horizon h.

Problem Solution

Definition 4 (Participating services) We call a set
of services Πi0 , i0 ∈ Di participating in q ∈ Qi if i0 = i,
or there exist q 0 ∈ Qi , σ ∈ Σi , and ς ⊆ Πi0 such that
(q, σ, q 0 ) ∈ δi , and (q, (σ \ Πi0 ) ∪ ς, q 0 ) 6∈ δi .

This section provides the details of the proposed iterative solution to Prob. 1. In Sec. 4.1, we set the preliminary synchronization sequences to be followed. In
Sec. 4.2 we present a finite horizon plan synthesis algorithm that consists of four steps: (1) partitioning the
agents into classes based on their dependency; and then
for each of the classes separately: (2) building an intersection specification automaton up to a predefined horizon; (3) building a product capturing system behaviors
admissible by the all agents within the class and by the
intersection specification automaton up to a predefined
horizon and evaluating the states of the product to reflect their respective profit towards the satisfaction of the
specifications; and (4) finding and projecting a path in
the product that leads to the most profitable state onto
finite trace fragments of the individual agents. Sec. 4.3
discusses the iterative execution and recomputation.

Given q ∈ Qi , the alphabet Σhi of Bi up to the horizon
h
h is Σhi (q) = 2Πi (q) , where
Πhi (q) =

[

{Πi0 | Πi0 is participating in q 0 },

q 0 ∈δ̂ij (q),0≤j≤h

where δ̂ij (q) denotes the set of states reachable from q in
j steps (see Sec. 2).
Example 3 An example of a BA is illustrated in Fig. 3.
Consider that this is a specification automaton B1 , such
that D1 = {1, 2, 3}, Π1 = {a}, Π2 = {b}, and Π3 = {c},
i.e., that Π1 = {a, b, c}, and Σi = 2{a,b,c} . Π1 is by
condition (i) of Def. 4 participating in all states. Π2 is
participating in q1 , since the service b is required on the
transition from q1 to q2 . Formally, there exists q 0 = q2 ,

Without loss of generality, let us assume that all agents
in N form a single offline dependency class from Sec. 3.

6

σ = {a, b}, and ς = ∅, such that (q1 , {a, b}, q2 ) ∈ δ1 ,
but (q1 , ({a, b} \ {b}) ∪ ∅, q2 ) 6∈ δ1 . On the other hand,
Π3 is not participating in q1 as the service c is neither
required nor forbidden on the transition from q1 to q2 . Π3
is participating in q2 since c is forbidden on the transition
from q2 to q3 and moreover required on the transition
from q2 to q4 . Neither Π2 nor Π3 are participating in q4 .
Hence, the alphabet up to the horizon h = 1 and h = 2 is
Π11 (q1 ) = {a, b} and Π21 (q1 ) = {a, b, c}, respectively.
q1

{a, b}

q2

{a}

q3

{}

q4

{b}, {c}, {b, c}

Without loss of generality, let the automata in Φ` be
ordered according to ≺, i.e. i` ≺ j` , for all 1 ≤ i < j ≤ n.
Definition 6 (Intersection automaton) The
intersection automaton of B1` , . . . , Bn` up to the horizon h is Ah = (QA , qinit,A , ΣA , δA , FA ), where
QA ⊂ Q1` × . . . × Qn` × N is a finite set of states, generated
 S as described below;Π qinit,AE = (q1` , . . . ,0qn` , 1); ΣA =
i`
∪ 2 i` ) ; Let QA = {qinit,A }.
i` ∈I` σi` | σi` ∈ (2
For all 1 ≤ j ≤ h, we define (q10 ` , . . . , qn0 ` , k 0 ) ∈ QjA

j
and (q1` , . . . , qn` , k), σ, (q10 ` , . . . , qn0 ` , k 0 )
∈ δA
iff
j−1
(i) (q1` , . . . , qn` , k) ∈ QA , (ii) for all i` ∈ I` ,
either(qi` , σ ∩ Πi` , qi0` ) ∈ δi` , or qi` = qi0` , and εi` ∈ σ,
and (iii) k 0 = k + 1 if qκ` ∈ Fκ` , where κ = k mod n` and
S
k 0 = k otherwise. Finally, QA = 0≤j≤h QjA and δA =
S
j
1≤j≤h δA ; FA = {(q1` , . . . , qn` , k) ∈ QA \ {qinit,A } |
qκ` ∈ Fκ` , where κ = k mod n` }.

{a, b, c}
{a, c}

Fig. 3. BA B1 with Σ1 = 2{a,b,c} . The states are illustrated
as circles, the transitions as arrows labeled with the symbols
from Σ1 . The arrow labeled with {b}, {c}, {b, c} represents 3
different transitions, under {b}, {c}, and {b, c}, respectively.

Definition 5 (Dependency partition) Given that
q1 , . . . , qN are the respective current states of BAs
B1 , . . . , BN , the dependency partition of Φ is induced
by the equivalence ∼h defined on Φ: (i) Bi ∼h Bi ,
and (ii) if there exists Bj , such that Bi ∼h Bj , and
Πi0 ⊆ Πhj (qj ) or Πj ⊆ Πhi0 (qi0 ), then also Bi ∼h Bi0 .
The dependency partition of Φ is then {Φ1 , . . . , ΦM },
where (Bi ∼h Bi0 ) ⇐⇒ (Bi ∈ Φ` ⇐⇒ Bi0 ∈ Φ` ).
The dependency partition of the set of all agents N is
I = {I1 , . . . , IM }, where a dependency class I` , is such
that i ∈ I` ⇐⇒ Bi ∈ Φ` , for all ` ∈ {1, . . . , M }.

The intersection automaton is not interpreted over infinite words and hence, it is not a BA. However, it
is an automaton and as such, it can be viewed as a
graph (see Sec. 2). A path in Ah from the initial state
(q1` , . . . , qn` , 1) to a state (q1` , . . . , qn` , k) corresponds
to a path from qi` to qi` in each Bi` and vice versa. Formally, these two lemmas follow from the construction:
Lemma 2 Consider a path q1 σ1 q2 σ2 . . . σm−1 qm in Ah ,
where qj denotes the tuple (q1` ,j , . . . , qn` ,j , kj ) ∈ QA , for
all 1 ≤ j ≤ m. Let $i` ,j = σj ∩ (Πi` ∪ Ei` ) denote the
range restriction of σj to the services of agent i` , for all
1 ≤ j ≤ m − 1 and let $i` ,ι1 . . . $i` ,ιµ be the subsequence
of non-silent elements of $i` ,1 . . . $i` ,m−1 . Finally, let
ωi` ,j = σιj ∩ Πi` , for all 1 ≤ j ≤ µ. Then there exists
a corresponding run ρ̄i` = q̄i` ,1 . . . q̄i` ,µ+1 . . . of Bi` over
each word w̄i` = ωi` ,1 . . . ωi` ,µ . . ., with the property that
(1) qi` ,1 = q̄i` ,1 = qi` , (2) qi` ,ιj +1 = q̄i` ,j+1 , for all
1 ≤ j ≤ µ, (3) qi` ,j+1 = qi` ,j , for all 1 ≤ j ≤ m − 1,
such that j 6= ιj 0 , for any 1 ≤ j 0 ≤ µ.

The dependency partition is the function of the current
states q1 , . . . , qN . Hence it is dynamically recomputed
in each iteration of our solution. Although the local satisfaction of φi for i ∈ I` depends on the traces of all
the agents j ∈ Di , it is not influenced by the agents
j ∈ Di \ I` within the horizon h. Thus, when we now
concentrate on planning within the horizon h, we can
safely treat each dependency class I` = {1` , . . . , n` } separately. In the worst case, the dynamic dependency partition equals to the offline one from Sec. 3. This is however, often not the case and even splitting a single offline dependency class into two online ones triggers an
exponential improvement in terms of computational demands of further steps. For an example, see Sec. 6.

Lemma 3 Consider a run ρi` = qi` ,1 qi` ,2 . . . of Bi` over
a word wi` = ωi` ,1 ωi` ,2 . . . ∈ (2Πi` )ω , where qi` ,1 = qi` .
Let σ1 σ2 . . . be a word over ΣA with the property that
there exists its subsequence σι1 σι2 . . ., such that σιι ∩
Πi` = ωi` ,j , for all j ≥ 1, while σj ∩ (Πi` ∪ Ei` ) = Ei` ,
for all j ≥ 1, j 6= ιj 0 , for any j 0 ≥ 1. Then there exists
a path q̄1 σ1 q̄2 σ2 . . . σh−1 q̄h in Ah , where q̄j denotes the
tuple (q̄1` ,j , . . . , q̄n` ,j , kj ) ∈ QA , such that: (1) q̄i` ,1 =
qi` ,1 = qi` , (2) q̄i` ,ιj +1 = qi` ,j+1 , for all 1 ≤ ιj ≤ h, and
(3) q̄i` ,j+1 = q̄i` ,j , for all 1 ≤ j, ιj 0 < h, where j 6= ιj 0 .

Intersection Automaton. For each dependency class
I` , we construct a finite automaton that represents the
language intersection of the BAs in Φ` = {B1` , . . . , Bn` }
up to the pre-defined horizon h. In this step, we rely on
the fact that the preliminary synchronization sequence
set in Sec. 4.1 guarantees step-by-step synchronization.
We label the states of the intersection automaton with
values that indicate the progress towards the satisfaction
of the desired tasks. Later on, these values are used to
set temporary goals in the finite horizon plan synthesis.

Through k, we remember the progress towards the satisfaction of the individual specifications ordered according to ≺; for k ≤ n` , an accepting state is guaranteed
to be present on a the projected finite path of each Bi` ,
1 ≤ i ≤ k. For k > n` , an accepting state is surely

7

 
present on each projected run of each Bi` , at least nk`  
times for all 1 ≤ i ≤ κ, and at least nk` -times for
all κ < i ≤ n` , where κ = k mod n` . To be able to
identify “profitable” actions/transitions of the agents
w.r.t. Φ` , and thus also w.r.t. Φ, we assume that at least
a state which represents a step towards the satisfaction
of the highest-order specification B1` is present in Ah .
In Sec. 4.2 this fact will allow us to set short-term goals
in TSs T1` , . . . , Tn` . We discuss its relaxation in Sec. 5.

A path in P H can be projected onto a finite trace prefix
of each Ti` , a finite run prefix of Ah and further through
Lemma 2 onto a finite run prefix of each BA Bi` , too.
Definition 9 (Projection) Consider a path % =
q1 σ1 q2 . . . qm−1 σm−1 qm in P H , where q1 = qinit,P . % can
be projected onto a finite trace prefix τ̂i` (%) of each Ti` ,
i` ∈ I` in the expected way: for all 1 ≤ j ≤ m, the j-th
state and action of τ̂i` (%) is si` ,j and αi` ,j if the j-th state
and transition label of % is qj = (s1` ,j , . . . , sn` ,j , qA,j ),
and σj = (α1` ,j , . . . , αn` ,j , σA,j ), respectively. Furthermore, for all 1 ≤ j ≤ m, the j-th state of the projected run prefix ρ̂A (%) of Ah is qA,j if the j-th state
of % is qj = (s1` , . . . , sn` , qA,j ); and assuming that
qA,j = (q1` ,j , . . . , qn` ,j , k), the state of the corresponding
state sequence ρ̂i` (%) in Bi` is qi` ,j .

Assumption 1 Assume that FA is not empty.
Definition 7 (Automaton progressive function)
The progressive function VA : QA → N0 × Z−
0 is
for a state q = (q1` , . . . , qn` , k) defined as: VA (q) =
k, − minqf ∈FA dist(q, qf ) .

Although ρ̂i` (%) is a projection of qA,j , i.e., a sequence
of states of Bi` , it might not be a run of Bi` as such.
However, thanks to Lemma 2, ρ̂i` (%) maps to a unique
corresponding run ρ̄i` (%) of qBi` . Note that in what follows, we distinguish between ρ̂i` (%) and ρ̄i` (%).

The increasing value of VA indicates a progress towards
the satisfaction of the individual local specifications in
Φ` , ordered according to ≺. No progress can be achieved
from a state q, such that VA (q) = (k, −∞) within the
horizon h, and hence, we remove such states from Ah .
From Assump. 1, VA (qinit,A ) = (1, d), where d 6= −∞.

Definition 10 (Progressive function and state)
The progressive function VP : QP → N0 × Z−
0
is inherited from the intersection automaton Ah
(Def. 7), i.e., for all
 q = (s1` , . . . , sn` , qA ) ∈ QP ,
VP (s1` , . . . , sn` , qA ) = VA (qA ). A state q ∈ QP is a
progressive state if VP (q) > VP (qinit,P ). A maximally
progressive state is a progressive state q, with the property that for all q 0 ∈ QP , it holds VP (q) ≥ VP (q 0 ).

Product System. The intersection automaton and its
progressive function allow us to assess which service sets
should be provided in order to maximize the progress towards the satisfaction of the specifications. The remaining step is to plan the transitions of the individual agents
to reach states in which these services are available. We
do so through the definition of a product system P H .
Besides the behaviors permitted by the task specifications, the product system captures the allowed behaviors (finite trace fragments) of the agents from I` up to
the horizon H. Similarly as the states of Ah , the states
of P H are evaluated to indicate their progress towards
the specifications satisfaction.

Finite Horizon Plan Synthesis. To find a suitable
finite horizon plan, we impose the following assumption
and discuss its relaxation in Sec. 5. It states that within
H, at least one service set can be provided that makes
at least one step towards the local satisfaction of the
highest-priority formula φ1` .

Definition 8 (Product system) The product system up to the horizon H of the agent TSs Ti` , i` ∈ I` ,
and the intersection automaton Ah from Def. 6 is
an automaton P H = (QP , qinit,P , ΣP , δP ), where
QP ⊂ S1` × . . . × Sn` × QA is a finite set of states, generated as described below; qinit,P = (s1` , . . . , sn` , qinit,A );
ΣP = A1` × . . . × An` × ΣA ; Let Q0P = {qinit,P }.
For all 1 ≤ j ≤ H, q = (s1` , . . . , sn` , qA ), σ =
0
(α1` , . . . , αn` , σA ), q 0 = (s01` , . . . , s0n` , qA
), we define
j
j
0
0
that q ∈ QP and (q, σ, q ) ∈ δP iff (i) q ∈ Qj−1
P ,
(ii)for all i` ∈ I` , it holds that T (si` , αi` ) = s0i` , and
0
σA ∩ (Πi` ∪ Ei` ) = Li` (αi` ), and (iii)(qA , σA , qA
) ∈ δA .
S
S
j
j
Finally, QP = 0≤j≤H QP and δP = 1≤j≤H δP
.

Assumption 2 Assume that there is a progressive state
qp reachable in P H via a finite path q1 σ1 . . . σm−1 qm ,
where q1 = qinit,P , qm = qp , and L(α1` ,j ) 6= E1` ,j , for
some σj = (α1` ,j , . . . , αn` ,j , σA,j ), 1 ≤ j ≤ m − 1.
We compute a suitable finite horizon plan as the
shortest path % = q1 σ1 q2 . . . qm σm qm in P H from
q1 = qinit,P to a maximally progressive state qm = qmax .
Such a path can be found in linear time with respect
to the size of P H (see Sec. 2). The projection of %
onto the individual TSs gives finite trace fragments
τ̂i` (%) = si` αi` ,1 si` ,2 . . . si` ,m−1 αi` ,m−1 si` ,m , to be followed by each agent i` ∈ I` . Alg. 1 summarizes the
proposed finite horizon planning for the set of all agents
N . Since this algorithm will be run iteratively, starting
from its second execution on, it also takes as an input
the fragments τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N and the progressive

The set of accepting states FP is not significant for the
further computations, hence we omit it from P H . Analogously as Ah , P H can be viewed as a graph (see Sec. 2).

8

the ordering ≺ so that i becomes of the lowest priority
(the highest order), while maintaining the mutual ordering of all the other agents. This change reflects that a
step towards the local satisfaction of Bi has been made
and in the next iteration, progressing towards another
agent’s specification will be prioritized. Finally, all the
agents start another iteration of the algorithm simultaneously as prescribed by the synchronization sequence.
For the simplicity of the presentation, we assumed that
the computation of short horizon plan does not take any
time. In practice, we would cope with different computation times via synchronization both before and after
running the procedure short horizon plan.

function value of the maximally progressive state from
the previous iteration. In comparison to the solution
from Sec. 3, we treat separately each dynamic dependency class (lines 2–13). These classes are often smaller
than the offline dependency classes, thereby increasing
the level of decentralization of the planning procedure.
Algorithm 1 Procedure short horizon plan
Input: a set of agents N = {1, . . . , N }, their models
M1 , . . . , MN ; BAs B1 , . . . , BN ; current states s1 , . . . , sn ,
q1 , . . . , qn ; an ordering ≺ over N ; and planning horizons
h, H ∈ N, previous fragments τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N , previous maximal progressive function value VP,max
Output: finite trace fragments τ̂1 , . . . , τ̂N of T1 , . . . , TN ; finite state sequences ρ̂1 , . . . , ρ̂N of B1 , . . . , BN ; and a
maximal progressive function value VP,max
1: compute the partition I = {I1 , . . . , IM } (Def. 5)
2: for all ` ∈ {1, . . . , M } do
3:
construct Ah (Def. 6) and construct P H (Def. 8)
4:
find a maximally progressive state qmax in P H
5:
if VP (qmax ) > VP,max then
6:
find the shortest path % to qmax and update VP,max
7:
for all i` ∈ I` do
8:
τ̂i` := τ̂i` (%) and ρ̂i` := ρ̂i` (%) (Def. 9)
9:
end for
10:
else
11:
remain τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N , VP,max unchanged
12:
end if
13: end for
14: return τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N , VP,max

4.3

Algorithm 2 Stepwise solution to Prob. 1
Input: a set of agents N = {1, . . . , N }, their models
M1 , . . . , MN ; BAs B1 , . . . , BN ; and horizons h, H ∈ N
Output: traces τ1 , . . . , τN and synchronization sequences
γ1 , . . . , γN that are a solution to Problem 1, and sequences ρ1 , . . . , ρn of states of BAs B1 , . . . , BN .
1: for all i ∈ N do
2:
initialize ≺ := (1, . . . , N ); si := sinit,i qi := qinit,i
3:
initialize τ̂i := empty; ρ̂i := empty; VP,max := (0, 0)
4:
initialize synchronization sequence γi (Sec. 4.1)
5:
send ri,1 := sync i and wait for sync i0 from all i0 ∈ N
6:
ji := 2
7: end for
8: while true do
9:
τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N , VP,max : = short horizon plan
10:
for all i ∈ N do
11:
execute αi,1 , provide L(αi,1 ); si := si,2 ; qi := qi,2
12:
if qi ∈ Fi then
13:
reorder ≺, s.t. i0 ≺ i, for all i0 ∈ {1, . . . , N } \ {i}
14:
VP,max := (0, 0)
15:
end if
16:
send ri,ji := sync i , wait for sync i0 from all i0 ∈ N
17:
ji := ji + 1
18:
end for
19: end while
20: return τ1 , . . . , τN , γ1 , . . . , γn , ρ1 , . . . , ρn

Infinite Horizon Replanning

To complete the solution, we discuss the infinite, iterative execution and recomputation of the finite horizon
plans. We present two recomputation strategies: a stepwise one, and later on in Sec. 4.3.2 an event-triggered
one, where we adjust the preliminary synchronization
sequences to reduce the synchronization frequency.
4.3.1

Stepwise Solution
The motivation for replanning after every iteration on
line 11 of Alg. 2 is to gradually shift the planning horizon in order to keep the planning procedure sufficiently
informed about the future possibilities. Less frequent replanning may be more efficient in terms of computational
demands, at the cost of inefficiency of the resulting plans.
Although the TSs and the BAs are finite and hence there
are a finite number of different finite horizon problems
to solve, the considered LTL formulas are interpreted
over infinite time and the number of iterations cannot
be generally upper-bounded due to the arbitrary transition durations. An alternative to the infinite number of
executions would be to remember how the finite horizon
problem has been resolved for every single combination
of the TSs and BAs states; however, this is generally not
feasible due to the fact that the number of these combinations grows quickly with the number of agents, the
size of the environment and the complexity of the tasks.

In each iteration of the stepwise solution, the finite
horizon plans are executed as summarized in Alg. 2.
Each agent i ∈ N first sets its preliminary synchronization sequence γi = ri,1 ri,2 . . . and synchronizes with
the other agents, i.e., sends ri,1 = sync i , and waits
for the reception of sync i0 from all i0 ∈ N . Second, it
computes the finite horizon plans by Alg. 1.Third, it executes the first action αi,1 of the planned trace fragment
τ̂i = si αi,1 si,2 . . . si,m−1 αi,m−1 si,m along with the first
silent or non-silent service set L(αi,1 ). It transitions to
state si,2 and the current state si is updated. The previous synchronization through ri,1 has ensured that each
agent i0 ∈ I` executes its respective action αi0 ,1 simultaneously. At the same time, the current state of the BAs
Bi , is updated to the second state qi,2 of the run fragment
ρ̂i . Note, that if L(αi,1 ) = εi , then qi,2 = qi,1 by Def. 6
and Def. 8. Furthermore, if qi,2 ∈ Fi , then we update

9

4.3.2

Algorithm 3 Event-triggered solution to Prob. 1

Event-Triggered Solution

Input: a set of agents N = {1, . . . , N }, their models
M1 , . . . , MN ; BAs B1 , . . . , BN ; and horizons h, H ∈ N
Output: traces τ1 , . . . , τN and synchronization sequences
γ1 , . . . , γN that are a solution to Problem 1, and sequences ρ1 , . . . , ρn of states of BAs B1 , . . . , BN .
1: for all i ∈ N do
2:
initialize ≺ := (1, . . . , N ); si := sinit,i qi := qinit,i
3:
initialize τ̂i := empty; ρ̂i := empty; VP,max := (0, 0)
4:
initialize synchronization sequence γi (Sec. 4.1)
5:
send ri,1 := sync i and wait for sync i0 from all i0 ∈ N
6:
ji := 2
7: end for
8: while true do
9:
τ̂1 , . . . , τ̂N , ρ̂1 , . . . , ρ̂N : = short horizon plan
10:
for all i ∈ N do
11:
execute αi,1 and provide service set L(αi,1 )
12:
si := si,2 ; qi := qi,2 ; ki := 2
13:
while L(αi,ji ) = εi and qi 6∈ Fi and qi is not the
last element of ρ̂i and sync i0 was not received from
any i0 ∈ N \ {i} during the last iteration do
14:
send ri,ji := nosync i ; ji := ji + 1
15:
execute αi,ki and provide service set L(αi,ki )
16:
si := si,ki +1 ; qi := qi,ki +1 ; ki := ki + 1
17:
end while
18:
if qi ∈ Fi then
19:
reorder ≺, s.t. j ≺ i, for all j ∈ {1, . . . , N } \ {i}
20:
VP,max := (0, 0)
21:
end if
22:
send ri,ji := sync i , wait for sync i0 from all i0 ∈ N
23:
ji := ji + 1
24:
end for
25: end while
26: return τ1 , . . . , τN , γ1 , . . . , γn , ρ1 , . . . , ρn

In the stepwise solution, the synchronization takes place
after every single transition of every agent, which might
be more frequently than necessarily needed. For example, if the first m actions in the planned trace fragment
τ̂i of an agent i are all associated with silent services,
then this agent does not need to synchronize with the
others nor to recompute its planned trace fragment. In
what follows, we adapt the preliminary synchronization
sequence so that the synchronization and recomputation
are triggered by the need of collaboration.
Assume that for agent i the procedure short horizon plan
executed on line 9 of Alg. 2 has returned a trace and a
run fragment denoted by τ̂i = si,1 αi,1 si,2 αi,2 . . . si,m and
ρ̂i = qi,1 qi,2 . . . qi,m , for some m ≥ 2. The main idea is to
postpone the synchronization with the others from after
the execution of αi,1 till the time tsi,j right before the
execution of the action αi,j , j > 1 with one of the following properties: L(αi,j ) is non-silent, or qi,j is accepting,
or qi,j = qi,m , or there exists an agent i0 , such that sync i0
has been received during (tαi,j−1 , tsi,j ]. If one of the conditions is met, the agent sends sync i , and waits for receiving sync i0 , from all i0 ∈ N . The finite horizon plans
are recomputed and the event-triggered recomputation
procedure repeats. On the other hand, if none of the conditions is met, the agent i substitutes the synchronization action sync i planned within the preliminary synchronization sequence γi with nosync i . Note that thanks
to the enforced compatibility of the behaviors, a deadlock is prevented. The solution is summarized in Alg. 3.

taken in Alg. 2, the state qmax is also present in P H at
time tsi,j+1 , hence if condition on line 5 is not satisfied,
this state remains the progressive goal. Now, let %0 be
0
of P H
the path to a maximally progressive state qmax
0
0
ˆ
at time tsi,j +1 and let τˆi and ρi be the corresponding
finite trace prefix of Ti , and the state sequence of Bi . If
0
0
0
is,
) > VP (qmax ) and qmax
6= qmax , then VP (qmax
qmax
loosely speaking, closer to reaching an accepting state of
Bi . Thanks to Assump. 1 and Assump. 2 and the finite
number of states of P H , by repetitive reasoning we get
that there exists time tsi,m , when a state q ∗ of PH is
reached, such that VP (q ∗ ) ≥ VP (qmax ). Inductively, a
state qf of P H that projects onto an accepting state of Bi
will eventually be reached. Similar holds even if the dependency partition I has changed at time tsi,j+1 and i is
present in a dependency class I`0 6= I` . The state qmax =
(s1` ,m , . . . , sn` ,m , (q1` ,m , . . . , qn` ,m , km )) can be mapped
onto a state of the new P H at time tsi,j+1 , i.e., onto
qmax ,`0 = (s1`0 ,m0 , . . . , sn`0 ,m0 , (q1`0 ,m0 , . . . , qn`0 ,m0 , km0 )),
where si0 ,m = si0 ,m0 , and qi0 ,m = qi0 ,m0 , for all
i0 ∈ I` ∩ I`0 . The remainder of the proof is analogous to
the above. Finally, it is ensured that at least one nonsilent service is provided by Ti on the executed path to
qf . Lines 12–15 of Alg. 2 ensure that each i ∈ N will
repeatedly become the most prioritized one. Altogether,
φi contains infinitely many states fi ∈ Fi , for all i ∈ N .

Remark 3 In Remark 1, we introduced parametrized
synchronization requests. Assume that I = {I1 , . . . , IM }
is an offline dependency partition from Sec. 3. Then for
each agent i ∈ I` , we can replace sync i with sync i (I` ),
and every nosync i with sync i ({i}). However, an analogous step cannot be applied in the case of dynamic classes.

5

Solution Analysis and Discussion

Lemma 4 Let τ1 , . . . , τN , γ1 , . . . , γn , ρ1 , . . . , ρn be the
traces, the synchronization sequences and the corresponding state sequences returned by Alg. 2. Then ρi
contains infinitely many states fi ∈ Fi , for all i ∈ N .
Proof. Denote τi = si,1 si,2 . . ., ρi = qi,1 qi,2 . . ., and
T(τi ) = tsi,1 tsi,2 . . ., for all i ∈ N . Consider a time instance tsi,j , where j ≥ 1 and assume that i is the most
prioritized agent at tsi,j , i.e., that i ≺ i0 , for all i0 ∈ N .
Let % be the path to a maximally progressive state qmax
of P H at time tsi,j computed on line 4 of Alg. 1 and
let τˆi and ρˆi be the corresponding finite trace prefix of
Ti , and the state sequence of Bi computed on lines 7–9.
Assume for a moment that the dependency partition I
remains the same at time tsi,j+1 . Regardless of the steps

10

i0 ∈ I`0 ∩ I` . We propose %`0 to be the path whose projections onto the states of Ti0 and Bi0 are the respective sequences si0 . . . si0 ~τi0 and qi0 . . . qi0 ρ
~i0 , such that the length
of these two sequences, and hence also the length of %`0 ,
equals to the length of the suffix ~τi00 that is the longest
one among the agents agents i00 ∈ I`0 ∩ I` . This path is
strictly shorter than %` . At the same time, it exists in P`H0
α
due to the assumption that s −
→ s, for all s ∈ Si0 , i0 ∈ N ,
and some α ∈ Ai0 . The existence of %`0 ensures that a
progress towards some fi ∈ Fi . Thanks to Assump. 1 and
Assump. 2 and the finite number of states of the the product system, by repetitive reasoning we get that during the
execution of Alg. 3, since a certain moment on, the last
state of %0` will be the maximally progressive state qmax ,`0
in P`H0 , until this state is reached. Inductively, a state qf
that projects onto an accepting state of Bi will eventually be reached. At the same time, at least one non-silent
service is provided by Ti on the path to qf . Furthermore,
lines 18–21 of Alg. 3 ensure, that each i ∈ N will repeatedly become the most prioritized one. Altogether, we ρi
contains infinitely many states fi ∈ Fi , for all i ∈ N .

In summary, Lemma 1 gives us the existence of compatible behaviors regardless of the traces of the agent TSs
and the transition time durations. Lemma 4 together
with Lemmas 2, and 3, and Def. 8 yield that τ1 , . . . , τN
produce words that are accepted by each Bi .
Theorem 1 The traces τ1 , . . . , τN together with the synchronization sequences γ1 , . . . , γN returned by Alg. 2 provide a solution to Prob. 1.
To prove the correctness of the event-triggered solution,
we have to prove that the computed traces and synchronization sequences (i) yield compatible behaviors and
(ii) locally satisfy the LTL formulas:
Lemma 5 The traces τ1 , . . . , τN , where τi = si,1 αi,1 . . .,
for all i ∈ N , together with the synchronization sequences
γ1 , . . . , γN returned by Alg. 3 yield compatible behaviors
regardless of the values of the transition time durations
∆αi,1 , ∆αi,2 . . ..
Proof. Follows immediately from the condition of the
while loop on line 13 of Alg. 3.

Theorem 2 The traces τ1 , . . . , τN together with the synchronization sequences γ1 , . . . , γN returned by Alg. 2 provide a solution to Prob. 1.

Lemma 6 Let τ1 , . . . , τN , γ1 , . . . , γN , ρ1 , . . . , ρN be the
traces, the synchronization sequences and the corresponding state sequences returned by Alg. 3. Then ρi contains infinitely many states fi ∈ Fi , for all i ∈ N .
Proof. Denote τi = si,1 αi,1 . . ., ρi = qi,1 qi,2 . . ., and
Ti = tsi,1 tαi,1 tsi,2 tαi,2 . . ., for all i ∈ N . To prove the
lemma, we prove that at each time t, it holds that an accepting state fi ∈ Fi will be eventually reached for the
most prioritized agent i at time t. First, consider t = 0.
Without loss of generality, assume that i ≺ i0 , for all
i0 ∈ N . Denote I` ∈ I the dependency class i belongs
to. Let τ̂1 , . . . , τ̂N and ρ̂1 , . . . , ρ̂N be the finite trace prefixes of T1 , . . . , TN , and the state sequences of B1 , . . . , BN
computed on line 9 of Alg. 3, respectively. Specifically for
I` , these were obtained from the projections of the shortest path %` that leads to a maximally progressive state
qmax ,` = (s1` ,m . . . sn` ,m , (q1` ,m , . . . , qn` ,m , km )) of the
product system P`H computed on line 4 of Alg. 1. Let the
execution proceed as described in Alg. 3 and let ts denote
the first time instance after t = 0 with one of the properties triggering the synchronization, i.e., with one of the
conditions of line 13 of Alg. 3 being false. Note that ts
is finite and after the requested synchronization is performed, the time tα equals to some tsi0 ,j in Ti0 , for all
i0 ∈ N . Let si0 and qi0 denote the respective states of Ti0
and Bi0 at time tα , and let ~τi0 and ρ
~i0 denote the respective suffixes of τ̂i0 and ρ̂i0 starting at si0 and qi0 , for all
i0 ∈ N . Denote by I`0 the dependency class i belongs to at
time tα and by P`H0 the corresponding product system. We
now show the existence of a mapping between the suffixes
~τi0 and ρ
~i0 of agents i0 ∈ I`0 ∩ I` onto a single finite path
%`0 in P`H0 , whose length is strictly smaller than the length
of %` in P`H . Trivially, if si0 ,m = si0 , for all i0 ∈ I`0 ∩ I` ,
the path %`0 is empty. Suppose that si0 ,m 6= si0 , for some

The complexity of one iteration of the solution is linear with respect to the size of P H , as the applied graph
search algorithms are linear (see, e.g. [5]). The size of
the intersection automaton Ah is in O(n|I` |+1 ), where
n is the maximal set of states reachable in some Bi ,
i ∈ I` within horizon h. The size of the product P H is
O(n|I` |+1 ), where n is the maximal set of states reachable in some Bi or Ti , i ∈ I` within the horizon H. In
the worst case, when n reaches the sizes of Bi or Ti respectively, and when the number of dependency classes
n` = 1, the complexity of one iteration reaches the one
of the straightforward solution,
i.e., the complexity of
Q
one iteration is in O(N · i∈N |Ti | · |Bi |), where |Ti | and
|Bi | is the size of Ti and Bi , respectively. However, as we
demonstrate in Sec. 6, a dramatic improvement of computational times can be achieved in practice.
Assump. 1 may be violated for two different reasons:
First, if the selected horizon h is too short, and although
FA = ∅ in Ah , there exists h0 > h, such that FA 6= ∅ in
0
Ah . Second, if FA = ∅ even for h → ∞. We propose to
systematically extend the horizon h and update the automaton Ah until a set of states FA becomes nonempty,
or until the extension does not change the automaton
Ah any more. In the former case, the automaton Ah
with the extended horizon satisfies Assump. 1 and thus
is used in constructing P H , maintaining the remainder
of the solution as described in Sec. 4.2 and 4.3. In the
latter case the specification has become infeasible, indicating that a wrong step has been made in past. Therefore, we backtrack along the executed solution to a point

11

to be efficiently handled. The goal is to select a horizon
to achieve a reasonable size of the intersection automaton (according to our experience, hundreds to thousands
of states maximally) while containing as many actions
labeled with non-silent services as possible.

when another service could have been executed instead
of the one that has been already done. Intuitively, we
“undo” the service and mark this service as forbidden in
the specification automata. The backtracking procedure
is roughly summarized in Alg. 4. In order to perform the
backtracking, the system execution prefixes have to be
remembered. To reduce the memory requirements, note
that cycles between two exact same system execution
states can be removed from the system execution prefixes without any harm. As there are only finitely many
transitions possible in each system state of each TS and
each BA, the backtracking procedure will ensure that
eventually, the agents’ trace prefixes will be found by
Alg. 1 without further backtracking. Once Assump. 1
holds, there is only one reason for violation of Assump. 2,
which is that the planning horizon H is not long enough.
To cope with this, we systematically extend the horizon
H similarly as we extended h in the BA. Eventually, a
progressive state will be found.

6

Example

To demonstrate our approach and its benefits, we consider the system from Example 1. We have implemented
the proposed solution in MATLAB, and we illustrate
snapshots of the resulting trace under stepwise synchronization in Fig. 4 (A)-(D). It can be seen that the agents
make progress towards satisfaction of their respective
formulas. In the computation, the default values of planning horizons were h = 3, and H = 5. In several cases,
the latter value had to be extended as described in Sec.5.
The maximum value needed in order to find a solution
was H = 9. The sizes of the product automata handled
in each iteration of the algorithm have significantly reduced in comparison to the straightforward centralized
solution from Sec. 3, where all three agents belong to
the dependency class yielding thus a synchronized TS
with 1443 ≈ 3 million states. With our dynamic decomposition, at most two agents belong to the same dependency class at the time, resulting into product automata
sizes in order of thousands states and the computation
of each iteration took seconds. When the agents are not
dependent on each other within h the sizes of product
automata are tens to hundreds states and the computation of each iteration took seconds to minutes. The
durations of all agents’ transitions were randomly generated from {5, ..., 10} time units. The first 7 services
in the plan of agent 2 have been completed after 54 iterations, with average duration of ≈ 477.1 time units.
In the event-triggered solution, the individual resulting
traces did not change, however, as indicated in Fig 4.(E),
the randomized transition durations caused some of the
agents progress more and some of them less in comparison to the stepwise solution. Average number of iterations to provide the 7 services of agent 2 was 30.3, and
average time of completion was 494.2 time units (computed from 20 simulation cases). Finally, Fig 4.(F) shows
the outcome of the event-triggered solution after 477
time units when the duration of transitions of agent 2
was changed to a random number between in {1, . . . , 5}.
The average number of iterations to provide the first 7
services of agent 2 was 26.3, and average time of completion was 355.6 time units (from 20 simulations). The
outcome of the stepwise solution for this case did not
change, except for the average time of completion, which
is now ≈ 457.5. This case thus demonstrates better suitability of the event-triggered solution for heterogeneous
multi-agent systems.

Algorithm 4 Backtracking
Input: Transition systems T1 , . . . , TN ; BAs B1 , . . . , BN ;
t
, ρt1 , . . . , ρtN ) up to
System execution prefix (τ1t , . . . , τN
the current time t, where τit = si,1 $i,1 . . . $i,t−1 si,t , and
ρti = ρi,1 . . . ρi,t , for all i ∈ {1, . . . N }.
Output: Updates to BAs B1 , . . . , BN
1: k := t
2: while solution not found do
3:
k := k − 1
S
4:
Check, if the execution of 1∈{1,...,N } $i,k can lead to
a different set of states of BAs than to q1,t , . . . , qN,t .
If so, apply
S the change and goto line 6.
5:
Forbid 1∈{1,...,N } $i,k in the states q1,k , . . . , qN,k of
each respective automaton B1 , . . . , BN
6:
Execute one iteration of Alg. 1 from s1 =
s1,k , . . . , sN = sN,k , q1 = q1,k , . . . , qN = qN,k
7:
If a plan was found in line 5, continue with execution
of Alg. 1, otherwise goto line 2 of Backtracking.
8: end while

Note, that Assump. 1 and 2 can be enforced by the selection a large enough h and H, respectively. Particularly, h ≥ maxi∈N |Qi |, and H ≥ maxi∈N |Si | ensures
the completeness of our approach. However, in such a
case, the complexity of the proposed approach meets the
complexity of the straightforward solution in Sec 3. A
good guidance criterion for the choice of appropriate size
of the receding horizon is the maximum, the average,
or the mean of the shortest distance (i.e., the smallest
number of transitions) between two actions labeled with
non-silent service sets in the given TSs. If the selected
horizon is too short, there is frequently no action labeled
with a non-silent service set present in the intersection
automaton, and the horizon gets frequently extended by
the algorithm from Sec. 4.5.1. If the horizon is slightly
longer, the resulting intersection automata contain only
a few actions labeled with non-silent service sets, and
the backtracking from Sec. 4.5.2 might take place quite
often. On the other hand, if the selected horizon is too
long, then the intersection automaton might be too large

12

𝑙𝐻

𝑙𝐻

𝑢𝐻

𝑙𝐻
𝑢𝐴

ℎ𝐻

ℎ𝐻

𝑢𝐻

𝑠2
𝑡3
𝑠5

𝑡2

𝑠4

(A)
𝑙𝐻

𝑡3

𝑙𝐻
𝑢𝐴 𝑙𝐵

𝑡4

𝑡1

𝑢𝐵
𝑠2

𝑡2

𝑙𝐴

𝑡1

𝑡3

𝑠4 𝑠5
𝑠5

𝑡1

𝑠2

𝑡2

𝑙𝐴

(D)

𝑢𝐵

𝑠4

𝑡5

(E)

𝑠5

𝑢𝐻
𝑢𝐴 𝑙𝐵

ℎ𝐻

𝑙𝐴

𝑠4 𝑠5
𝑠4

𝑡5

𝑠4 𝑠5

𝑙𝐴

𝑙𝐻
𝑢𝐴 𝑙𝐵

𝑡4

𝑙𝐴

(C)

𝑢𝐻
ℎ𝐻

𝑙𝐴

𝑠4

𝑡5

𝑡2

(B)

𝑢𝐻
ℎ𝐻

𝑠5

𝑢𝐵
𝑠2

𝑡4

𝑡3

𝑠5

𝑙𝐴

𝑡1

𝑢𝐴 𝑙𝐵

ℎ𝐻

𝑡3
𝑠5

𝑡1

𝑡4

𝑠2

𝑡2

𝑙𝐴

𝑢𝐵
𝑠4 𝑠5
𝑠4

𝑡5

𝑙𝐴

𝑠5

(F)

Fig. 4. Trace prefixes of agent 1 (green/light), agent 2 (pink/medium), and agent 3 (blue/dark). The initial position of the agents are in
the bottom left corner of R1 , in the top left corner of R3 , and in the bottom right corner of R5 , respectively. The services are depicted
as squares, the current position of the agents at the moment of the snapshot are indicated with arrows. In all figures, services lH and
hH , and t5 and s4 are provided at the same time. Specifically, (A) depicts the moment when lH and hH are provided and (C) depict
the moment when t5 and s4 are provided. (A)-(D): the outcome of the stepwise solution after 1, 4, 6, and 7 services of agent 2 are
provided, which is after 5, 22, 48, and 54 iterations, respectively; (E) an example outcome of the event-triggered solution after 7 services
of agent 2, which is after 24 iterations; (F) an example outcome of the event-triggered solution after 477 time units in case agent 2 is
faster in executing its transitions than the other two; 9 services were completed by agent 2 in 37 iterations.

7

Summary and Future Work

[2] C. Belta and L. C. G. J. M. Habets. Control of a class
of nonlinear systems on rectangles. IEEE Transactions on
Automatic Control, 51(11):1749–1759, 2006.

We have proposed an automata-based receding horizon approach to solve the multi-agent planning problem
from local LTL specifications. The solution decomposes
the infinite horizon planning problem into finite horizon planning problems that are solved iteratively. It enables each agent to restrict its focus only on the agents
that are constrained by its formula within a limited horizon, and hence to decentralize the planning procedure.
Moreover, via considering the finite horizon, we reduce
the size of handled state space. Stepwise synchronization
can be substituted with less frequent event-based synchronization, increasing the independence of the agents
during the plan execution. Future research directions include involving various optimality requirements, or robustness to small perturbations as well as evaluation of
the approach using mobile robots.

[3] A. Bhatia, M. R. Maly, L. E. Kavraki, and M. Y. Vardi.
Motion planning with complex goals.
IEEE Robotics
Automation Magazine, 18(3):55 –64, 2011.
[4] 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.
[5] T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson.
Introduction to Algorithms. McGraw-Hill Higher Education,
2nd edition, 2001.
[6] X. C. Ding, C. Belta, and Cassandras C. G. Receding horizon
surveillance with temporal logic specifications. In IEEE
Conference on Decision and Control, pages 256–261, 2010.
[7] I.
Filippidis,
D.V.
Dimarogonas,
and
K.J. Kyriakopoulos. Decentralized multi-agent control from
local LTL specifications. In IEEE Conference on Decision
and Control, pages 6235–6240, 2012.
[8] M. Guo and D. V. Dimarogonas.
Multi-agent plan
reconfiguration under local LTL specifications. International
Journal of Robotics Research, 34(2):218–235, 2015.

Acknowledgements

[9] G. Jing, C. Finucane, V. Raman, and H. Kress-Gazit. Correct
high-level robot control from structured english. In IEEE
International Conference on Robotics and Automation, pages
3543–3544, 2012.

The authors are with the ACCESS Linnaeus Center,
School of Electrical Engineering, KTH Royal Institute
of Technology, SE-100 44, Stockholm, Sweden and with
the KTH Centre for Autonomous Systems. This work
was supported by the EU STREP RECONFIG, and by
the H2020 ERC Starting Grant BUCOPHSYS.

[10] 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.

References

[11] 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.

[1] C. Baier and J.-P. Katoen. Principles of Model Checking.
MIT Press, 2008.

[12] M. Kloetzer, X. C. Ding, and C. Belta.
Multirobot deployment from LTL specifications with reduced

13

communication. In IEEE Conference on Decision and
Control and European Control Conference, pages 4867–4872,
2011.
[13] H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal
logic-based reactive mission and motion planning. IEEE
Transactions on Robotics, 25(6):1370–1381, 2009.
[14] S. M. LaValle. Planning Algorithms. Cambridge University
Press, 2006.
[15] S. G. Loizou and K. J. Kyriakopoulos. Automated planning
of motion tasks for multi-robot systems. In IEEE Conference
on Decision and Control, pages 78 – 83, 2005.
[16] M.M. Quottrup, T. Bak, and R.I. Zamanabadi. Multirobot planning : a timed automata approach. In IEEE
International Conference on Robotics and Automation,
volume 5, pages 4417–4422, 2004.
[17] M. Svorenova, J. Tumova, J. Barnat, and I. Cerna.
Attraction-based receding horizon path planning with
temporal logic constraints. In IEEE Conference on Decision
and Control, pages 6749–6754, 2012.
[18] J. Tumova and D. Dimarogonas. A receding horizon approach
to multi-agent planning from local LTL specifications. In
American Control Conference, pages 1775–1780, 2014.
[19] 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.
[20] C. Wiltsche, F. A. Ramponi, and J. Lygeros. Synthesis of an
asynchronous communication protocol for search and rescue
robots. In European Control Conference, pages 1256–1261,
2013.
[21] T. Wongpiromsarn, U. Topcu, and R. M. Murray. Receding
horizon control for temporal logic specifications. In Hybrid
systems: Computation and Control, pages 101–110, 2010.

14

