Temporal Logic Task Planning and Intermittent
Connectivity Control of Mobile Robot Networks
Yiannis Kantaros, Student Member, IEEE, Meng Guo, Student Member, IEEE, and
Michael M. Zavlanos, Member, IEEE
Abstract—In this paper, we develop a distributed intermittent
communication and task planning framework for mobile robot
teams. The goal of the robots is to accomplish complex tasks,
captured by local Linear Temporal Logic formulas, and share
the collected information with all other robots and possibly
also with a user. Specifically, we consider situations where the
robot communication capabilities are not sufficient to form
reliable and connected networks while the robots move to
accomplish their tasks. In this case, intermittent communication
protocols are necessary that allow the robots to temporarily
disconnect from the network in order to accomplish their tasks
free of communication constraints. We assume that the robots
can only communicate with each other when they meet at
common locations in space. Our distributed control framework
jointly determines local plans that allow all robots fulfill their
assigned temporal tasks, sequences of communication events that
guarantee information exchange infinitely often, and optimal
communication locations that minimize red a desired distance
metric. Simulation results verify the efficacy of the proposed
controllers.
Index Terms—Multi-robot networks, intermittent communica-
tion, distributed LTL-based planning.
I. INTRODUCTION
R
ECENTLY, there has been a large amount of work fo-
cused on designing controllers that ensure point-to-point
or end-to-end network connectivity of mobile robot networks
for all time. Such controllers either rely on graph theoretic
approaches [1]–[5] or employ more realistic communication
models that take into account path loss, shadowing, and multi-
path fading as well as optimal routing decisions for desired
information rates [6]–[10]. However, due to the uncertainty
in the wireless channel, it is often impossible to ensure all-
time connectivity in practice. Moreover, such methods often
prevent the robots from accomplishing their tasks, as motion
planning is always restricted by connectivity constraints on
the network. Therefore, a much preferred solution is to allow
robots to communicate in an intermittent fashion and operate
in disconnect mode the rest of the time.
Intermittent communication in multi-agent systems has been
studied in consensus problems [11], coverage problems [12],
and in delay-tolerant networks [13], [14]. The common as-
sumption in these works is that the communication network is
connected over time, infinitely often. Relevant is also the work
Yiannis
Kantaros,
Meng
Guo,
and
Michael
M.
Zavlanos
are
with
the
Department
of
Mechanical
Engineering
and
Materials
Science,
Duke
University,
Durham,
NC
27708,
USA.
{yiannis.kantaros, meng.guo, michael.zavlanos}@duke.edu.
This
work
is supported in part by NSF under grant CNS #1302284 and by ONR under
grant #N000141812374.
on event-based network control [15], [16] where, although the
network is assumed to be connected for all time, messages
between the agents are exchanged intermittently when certain
events take place. In this paper, we lift all connectivity
assumptions and, instead, control the communication network
itself so that it is guaranteed to be intermittently connected,
infinitely often. Specifically, we assume that robots can only
communicate when they are physically close to each other.
The intermittent connectivity requirement is captured by a
global Linear Temporal Logic (LTL) statement that forces
small groups of robots, also called teams, to meet infinitely
often at locations in space that are common for each team, but
possibly different across teams. We assume that every robot
belongs to at least one team and that there is a path, i.e., a
sequence of teams where consecutive teams have non-empty
intersections, connecting every two teams of robots, so that
information can propagate in the network.
In addition to the intermittent communication requirement,
we also assume that the robots are responsible for accom-
plishing independent tasks that are specified by local LTL
formulas. These tasks can be, e.g., gathering of information
in the environment that needs to reach all other robots and
possibly a user through the proposed intermittently connected
network. Given the global LTL statement comprised of the in-
termittent communication requirement and the local LTL tasks,
existing control synthesis approaches for global LTL specifi-
cations [17]–[19] that rely on transition systems to abstract
robot mobility can be used to obtain correct-by-construction
controllers. Nevertheless, such approaches do not optimize
task performance. Optimal control synthesis algorithms for
mobile robot networks under global LTL specifications are
proposed in [20]–[23]. Common in [20], [21] is that they
rely on the construction of a synchronous product automaton
among all robots and the application of graph search methods
to synthesize optimal plans. Therefore, these approaches are
resource demanding and scale poorly with the number of
robots. Sampling-based optimal control synthesis methods un-
der global LTL specifications have also been proposed by the
authors in [22] that scale better than the methods in [20], [21].
The methods proposed in [20]–[22] are all centralized and
offline and, therefore, not reactive to new tasks. Moreover, they
require as an input the B¨uchi automaton that corresponds to the
global LTL formula, which is generated by a computationally
expensive process. A distributed implementation of [22] that
can optimize feasible motion plans online is presented in [23].
However, [23] requires an all-time connected communication
network which is not the case here. A new logic, called
arXiv:1706.00765v3  [cs.RO]  24 Jun 2018
counting linear temporal logic, is proposed in [24] that can be
used for coordination of large collections of agents. However,
this approach is centralized, offline, and assumes that the
identity of the agents is not important for the successful
accomplishment of the task, which is not the case here due to
the intermittent connectivity requirement.
In this work, our goal is to synthesize motion plans
for all robots so that both the local LTL tasks and the
global LTL formula capturing the intermittent connectivity
requirement are satisfied, while minimizing a desired distance
metric. To achieve that, we avoid the construction of the
product automaton altogether and instead propose an online
and distributed framework to design correct-by-construction
controllers for the robots. In particular, we first focus on
the intermittent connectivity requirement and propose a new
distributed framework to design sequences of communication
events, also called communication schedules, for all teams of
robots. Then, we develop discrete plans for the robots that
satisfy the local LTL tasks while ensuring that teams can
communicate according to the predetermined schedules. The
locations of the communication events in these discrete plans
are selected so that they optimize a desired distance metric.
The proposed controllers are synthesized in a distributed and
online fashion, and can be executed asynchronously, which is
not the case in most relevant literature as, e.g., in [22]–[26].
To the best of our knowledge, the most relevant works to
the one proposed here are recent works by the authors [27]–
[30]. Specifically, [27] proposes an asynchronous distributed
intermittent communication framework that is a special case
of the one proposed here in that every robot belongs to
exactly two teams and the robots in every team can only
meet at a single predetermined location. This framework is
extended in [28], where robots can belong to any number of
teams and every team can select among multiple locations
to meet, same as in the work considered here. Nevertheless,
neither of the approaches in [27], [28] consider concurrent
task planning. Intermittent communication control and task
planning is considered in [29] that relies on the construction
of a synchronous product automaton among all robots and,
therefore, this approach is centralized and does not scale well
with the number of robots. A distributed online approach to
this problem is proposed in [30]. The method proposed here
is more general in that it can handle the data gathering tasks
and the star communication topology in [30] that considers
information flow only to the root/user. In fact, in the proposed
method, information can flow intermittently between any pair
of robots and possibly a user in a multi-hop fashion. Another
fundamental difference with [30] is that here the robots first
decide how they want to communicate by constructing abstract
schedules of communication events and then decide where
they want to communicate by embedding online and optimally
these schedules in the workspace so that the desired tasks
are also satisfied. In fact, this is a unique feature of the
proposed approach that differentiates it from existing literature
on communication control where communication is always
state-dependent. Other relevant methods that do not rely on
LTL for intermittent communication control are presented in
[31], [32]. However, these methods impose strong restrictions
on the communication pattern that can be achieved, while [31]
also does not consider concurrent task planning. We provide
theoretical guarantees supporting the proposed framework, as
well as numerical simulations showing its ability to solve
very large and complex planning problems that existing model
checking techniques cannot solve. To the best of our knowl-
edge, this is the first distributed, online, and asynchronous
framework for temporal logic path planning and intermittent
communication control that can be applied to large-scale
multi-robot systems.
The rest of this paper is organized as follows. In Sec-
tion II we present some preliminaries in LTL. The problem
formulation is described in Section III. In Section IV, we
design a distributed schedules of communication events that
ensure intermittent connectivity. In Section V, we design
discrete motion plans that satisfy the assigned local LTL
tasks and the intermittent connectivity requirement as per the
communication schedules, while minimizing a distance metric.
Theoretical guarantees of the proposed algorithm are presented
in Section VI. Simulation results are included in Section VII.
II. PRELIMINARIES
The basic ingredients of Linear Temporal Logic are a set of
atomic propositions AP, the boolean operators, i.e., conjunc-
tion ∧, and negation ¬, and two temporal operators, next ⃝
and until U. LTL formulas over a set AP can be constructed
based on the following grammar: φ ::= true | π | φ1 ∧
φ2 | ¬φ |
⃝φ | φ1 U φ2, where π ∈AP. For the
sake of brevity we abstain from presenting the derivations
of other Boolean and temporal operators, e.g., always □,
eventually ♦, implication ⇒, which can be found in [33].
An infinite word σ over the alphabet 2AP is defined as an
infinite sequence σ = π0π1π2 · · · ∈(2AP)ω, where ω denotes
infinite repetition and πk ∈2AP, ∀k ∈N. The language
Words(φ) =

σ ∈(2AP)ω|σ |= φ
	
is defined as the set of
words that satisfy the LTL formula φ, where |=⊆(2AP)ω ×φ
is the satisfaction relation.
Any LTL formula φ can be translated into a Nondetermin-
istic B¨uchi Automaton (NBA) over 2AP denoted by B, which
is defined as follows [34]:
Definition 2.1 (NBA): A Nondeterministic B¨uchi Automa-
ton (NBA) B over 2AP
is defined as a tuple B
=
QB, Q0
B, Σ, →B, FB


, where QB is the set of states, Q0
B ⊆
QB is a set of initial states, Σ = 2AP is an alphabet,
→B⊆QB × Σ × QB is the transition relation, and FB ⊆QB
is a set of accepting/final states.
An infinite run ρB of B over an infinite word σ = π0π1π2 . . . ,
πk ∈Σ = 2AP ∀k ∈N is a sequence ρB = q0
Bq1
Bq2
B . . .
such that q0
B ∈Q0
B and (qk
B, πk, qk+1
B
) ∈→B, ∀k ∈N. An
infinite run ρB is called accepting if Inf(ρB) ∩FB ̸= ∅,
where Inf(ρB) represents the set of states that appear in ρB
infinitely often. The words σ that result in an accepting run
of B constitute the accepted language of B, denoted by LB.
Then it is proven [33] that the accepted language of a NBA B,
associated with an LTL formula φ, is equivalent to the words
of φ, i.e., LB = Words(φ).
III. PROBLEM FORMULATION
Consider N ≥1 mobile robots operating in a workspace
W ⊂Rd, d ∈{2, 3}, containing W > 0 locations of interest
denoted by vj, j ∈I := {1, . . . , W}. Mobility of robot i ∈
N := {1, . . . , N} in W is captured by a weighted Transition
System (wTS) that is defined as follows:
Definition 3.1 (weighted Transition System): A
weighted
Transition
System
for
robot
i,
denoted
by
wTSi
is
a
tuple
wTSi
=
Qi, q0
i , →i, wi, AP, Li


where
(a)
Qi = {qvj
i , j ∈I} is the set of states, where a state qvj
i
indicates that robot i is at location vj ∈W; (b) q0
i ∈Qi
is the initial state of robot i; (c) →i⊆Qi × Qi is a given
transition relation such that (qvj
i , qve
i ) ∈→i if there exists a
controller that can drive robot i from location vj to ve in
finite time without going through any other location vc; (d)
wi : Qi × Qi →R+ is a weight function that captures the
distance that robot i needs to travel to move from vj to ve;1
(e) AP = {{πvj
i }N
i=1}j∈I is the set of atomic propositions
associated with each state; and (f) Li : Qi →AP is defined
as Li(qvj
i ) = πvj
i , for all i ∈N and j ∈I.
Every robot i ∈N is responsible for accomplishing high-
level tasks associated with some of the locations vj, j ∈I.
Hereafter, we assume that the tasks assigned to the robots
are independent from each other. Specifically, we assume that
the task assigned to robot i is captured by a local LTL−⃝
formula φi [35] specified over the set of atomic propositions
AP = {{πvj
i }N
i=1}j∈I, where πvj
i
= 1 if ∥xi −vj∥≤ϵ, for
a sufficiently small ϵ > 0, and 0 otherwise, for all i ∈N and
j ∈I.2 Namely, the atomic proposition πvj
i
is true if robot i is
sufficiently close to location vj. For example, an LTL−⃝task
for robot i can be: φi = (□♦πv4
i )∧((¬πv4
i )Uπv8
i )∧(♦πv5
i )∧
(□¬πv3
i )∧(□♦πv1
i ), which requires robot i to (i) visit location
v4 infinitely often, (ii) never visit location v4 until location v8
is visited, (iii) eventually visit location v5, (iv) always avoid
an obstacle located at v3, and (v) visit location at v1 infinitely
often. Together with accomplishing local tasks, robots are also
responsible for communicating with each other so that any
information that is collected as part of these tasks is propagated
in the network and, possibly, eventually reaches a user.
To define a communication network among the robots, we
first partition the robot team into M ≥1 robot subgroups,
called also teams, and require that every robot belongs to at
least one subgroup. The indices i of the robots that belong to
the m-th subgroup are collected in a set denoted by Tm, for
all m ∈M := {1, 2, . . . , M}. We define the set that collects
the indices of teams that robot i belongs to as Mi = {m|i ∈
Tm, m ∈M}. Also, for robot i we define the set that collects
the indices of all other robots that belong to common teams
with robot i as Ni = {j|j ∈Tm, ∀m ∈Mi} \ {i}, ∀i ∈N.
Given the robot teams Tm, for all m ∈M, we can define the
graph over these teams as follows.
1Note that alternative weights can be assigned to the transitions of the wTSs
that can capture e.g.,the time, or energy required for robot i to move from
vj to ve.
2The syntax of LTL−⃝is the same as the syntax of LTL excluding the
‘next’ operator. The choice of LTL−⃝over LTL is motivated by the fact that
we are interested in the continuous time execution of the synthesized plans,
in which case the next operator is not meaningful. This choice is common in
relevant works, see, e.g., [36] and the references therein.
Definition 3.2 (Team Membership Graph GT ): The
graph
over the teams Tm, m ∈M is defined as GT = (VT , ET ),
where the set of nodes VT = M is indexed by the teams Tm
and set of edges ET is defined as ET = {(m, n)|Tm ∩Tn ̸=
∅, ∀m, n ∈M, m ̸= n}.
Given the team membership graph GT , we can also de-
fine the set NTm := {e ∈VT |(m, e) ∈ET } that collects all
neighboring teams of team Tm in GT . Since the robots have
limited communication capabilities, we assume that the robots
in every subgroup Tm can only communicate if all of them
are simultaneously present at a common location vj ∈W,
hereafter called a communication point. We assume that there
are R ≥1 available communication points in the workspace
at locations vj ∈W, where j ∈C ⊂I. Among those
communication points, the ones that are specifically available
to the robotic team Tm are collected in a finite set Cm ⊆C,
where the sets Cm are not necessarily disjoint. When all robots
in a team Tm have arrived at a communication location, we
assume that communication happens and the robots leave to
accomplish their tasks or communicate with other teams. This
way, a dynamic robot communication network is constructed,
defined as follows:
Definition 3.3 (Communication Network Gc(t)): The com-
munication network among the robots is defined as a dynamic
undirected graph Gc(t) = (Vc, Ec(t)), where the set of nodes
Vc is indexed by the robots, i.e., Vc = N, and Ec(t) ⊆Vc×Vc
is the set of communication links that emerge among robots
in every team Tm, when they all meet at a common com-
munication point vj, for some j ∈Cm simultaneously, i.e.,
Ec(t) = {(e, i), ∀i, e ∈Tm, ∀m ∈M | xi(t) = xe(t) =
vj, for some j ∈Cm}.
To ensure that information is continuously transmitted
across the network of robots, we require that the commu-
nication graph Gc(t) is connected over time infinitely often,
i.e., that all robots in every team Tm meet infinitely often at
a common communication point vj, j ∈Cm, that does not
need to be fixed over time. For this, it is necessary to assume
that the graph of teams GT is connected. Specifically, if GT is
connected, then information can be propagated intermittently
across teams through robots that are common to these teams
and, in this way, information can reach all robots in the
network. Connectivity of GT and the fact that robots can
be members of only a few teams means that information
can be transferred over long distances, possibly to reach a
remote user, without requiring that the robots leave their
assigned regions of interest defined by their assigned tasks and
communication points corresponding to the teams they belong
to. Moreover, we assume that the teams Tm are a priori known
and can be selected arbitrarily as long as the graph of teams
GT is connected.
Intermittent connectivity of the communication network
Gc(t) can be captured by the global LTL formula
φcom = ∧m∈M
□♦
∨j∈Cm(∧i∈Tmπvj
i )



,
(1)
specified over the set of atomic propositions {{πvj
i }N
i=1}j∈C.
Composing φcom with the local LTL−⃝formulas φi, yields
the following global LTL statement
φ = (∧i∈N φi) ∧φcom,
(2)
that captures the local tasks assigned to every robot and
intermittent connectivity of the communication network Gc.
Given the wTSi, for all robots i ∈N, and the global LTL
formula (2), the goal is to synthesize motion plans τi, for all
i ∈N, whose execution satisfies the global LTL formula (2).
Typically, such motion plans are infinite paths in wTSi [35],
i.e., infinite sequences of states in wTSi, such that τi(1) = q0
i ,
τi(κ) ∈Qi, and (τi(κ), τi(κ + 1)) ∈→i, ∀κ ∈N+. In this
form, they cannot be manipulated in practice. This issue can
be resolved by representing these plans in a prefix-suffix form
[34], i.e., τi = τ pre
i

τ suf
i
ω, where the prefix part τ pre
i
and suffix
part τ suf
i
are both finite paths in wTSi, for all robots i ∈N.
The prefix τ pre
i
is executed once and the suffix τ suf
i
is repeated
indefinitely. The cost associated with a plan τi = τ pre
i

τ suf
i
ω
is defined as
Jp(τi) = αJ(τ pre
i ) + (1 −α)J(τ suf
i ),
(3)
where J(τ pre
i ) and J(τ suf
i ) represent the cost of the prefix and
the suffix part, respectively, and α ∈[0, 1] is a user-specified
parameter. The cost J(τ suf
i ) of the suffix part is defined as
J(τ suf
i ) =
|τ suf
i |
X
κ=1
wi(τ suf
i (κ), τ suf
i (κ + 1)),
(4)
where |τ suf
i | stands for the number of states in the finite path
τ suf
i , τ suf
i (κ) denotes the κ-th state in τ suf
i , and wi are the
weights defined in Definition 3.1. The cost J(τ pre
i ) of the
prefix part is defined accordingly. In words, Jp(τi) captures the
distance that robot i needs to travel during a single execution
of the prefix and suffix part weighted by a user-specified
parameter α > 0.
The problem that is addressed in this paper can be summa-
rized as follows:
Problem 1: Consider any initial configuration of a network
of N mobile robots in their respective wTSs, and any partition
of the network in M subgroups Tm, m ∈M so that the
associated graph GT is connected. Determine discrete motion
plans τi, i.e., sequences of states qvj
i
∈Qi, in prefix-suffix
structure, for all robots such that the LTL specification φ
defined in (2) is satisfied, i.e., (i) the local LTL−⃝tasks φi are
satisfied, for all i ∈N, (ii) intermittent communication among
robots captured by φcom is ensured infinitely often, and (iii)
the distance metric P
i∈N Jp(τi) is minimized.
To solve Problem 1, we propose a distributed algorithm that
consists of two main parts. First, we design offline schedules
of communication events for all robots, independently of their
assigned tasks, that ensure intermittent communication among
robots in every team infinitely often; see Section IV. These
communication events depend on the structure of the graph GT
and are not associated with specific locations in space. Then,
in Section V we design online discrete plans for the robots that
satisfy their local tasks while ensuring that the robots in each
team communicate as per the schedules defined in Section IV.
The location of these communication events are selected so
that the distance metric P
i∈N Jp(τi) is minimized.
1
2
3
Fig. 1.
A graphical illustration of the problem formulation. A network of
N = 3 robots (black dots) divided into M = 3 teams is depicted. The robot
teams are selected to be: T1 = {1, 2}, T2 = {2, 3}, and T3 = {3, 1}. The
set I consists of locations represented by red and green squares. Red squares
comprise set C and represent communication points. Black dashed lines stand
for paths in the workspace W that connect locations ve and vj. The sets
of communications points for each team are defined as C1 = {v9, v10},
C2 = {v10, v11}, and C3 = {v12}.
IV. INTERMITTENT COMMUNICATION CONTROL
In this section we construct infinite sequences of commu-
nication events (also called communication schedules) so that
intermittent connectivity infinitely often as per (1) is guar-
anteed. Construction of the communication schedules occurs
offline i.e., before the robots are deployed in the workspace
to satisfy the assigned LTL−⃝tasks φi, and requires that the
robots are connected so that they can share information with
each other. Then, in Section V, these schedules are integrated
online with task planning to synthesize discrete motion plans
that ensure that the local tasks are satisfied, the network is
intermittently connected as per the designed schedules, and
the cost function defined in Section III is minimized.
Since every robot can be a member of more than one team,
the objective in designing the proposed communication sched-
ules is that no teams that share common robots communicate
at the same time, as this would require that the shared robots
are present at more than one possibly different communication
points at the same time. We call such schedules conflict-free.
To construct such conflict-free schedules of communication
events we define a sequence S of teams that determines the
order in which the robots construct their schedules.
Definition 4.1 (Sequence S): The finite sequence S is a
sequence of teams defined as S = Tn, Tm, . . . . The sequence
S satisfies two requirements: (i) all teams Tm, m ∈M
appear in S; and (ii) consecutive teams Tn and Tm that
appear in S are neighboring nodes in the graph GT , i.e.,
m ∈NTn := {e ∈VT |(n, e) ∈ET }.
In what follows, we assume that the sequence S is user-
defined and known by all robots. Moreover, we denote by
S(k) the k-th team in S, ∀k ∈{1, . . . , |S|} where |S| stands
for the length of S. Using the sequence S we construct com-
munication schedules schedi for all robots i that determine
the order in which those robots participate in communication
events for teams Tm, ∀m ∈Mi and are defined as follows:
Definition 4.2 (Schedule of Communication Events): The
schedule schedi of communication events of robot i is
defined as an infinite repetition of the finite sequence
si =X, . . . , X, Mi(1), X, . . . , X, Mi(2), X, . . . , X,
Mi(|Mi|), X, . . . , X,
(5)
i.e., schedi = si, si, · · · = sω
i , where ω stands for the infinite
repetition of si.
In (5), Mi(e), e ∈{1, . . . , |Mi|} stands for the e-th entry
of Mi and represents a communication event for team with
index Mi(e), and the discrete states X indicate that there is no
communication event for robot i. The length of the sequence
si is ℓ= max {dTm}M
m=1 + 1 for all i ∈N, where dTm is
the degree of node m ∈VT . It is shown in Proposition 4.4
that this length ℓis sufficient for the construction of conflict-
free communication schedules as per the algorithm described
bellow. The schedule schedi defines the order in which robot
i participates in the communication events for the teams m ∈
Mi, for all robots i ∈N. Specifically, at a discrete time
step z ∈N+, robot i either communicates with all robots that
belong to team Tm, for m ∈Mi if schedi(z) = m, or
does not need to participate in any communication event if
schedi(z) = X.
In what follows we present a distributed process that relies
on two rules that the robots execute in order to construct
the schedules schedi. These schedules are constructed se-
quentially across the teams Tm, m ∈M, in an order that
is determined by the sequence S. In other words, robots in
team S(k) will construct their respective schedules, only if all
robots in team S(k−1) have already designed their schedules.
Assume that according to the sequence S, robots in team
S(k) = Tm, for some k ≥1 are due to construct their
schedules. By construction of the sequence S, consecutive
teams in S are always neighboring teams, which means that
there exists a team Tn with n ∈NTm such that S(k−1) = Tn
and Tm ∩Tn ̸= ∅. Consequently, there exist also robots
j ∈Tm ∩Tn that previously constructed their sequences sj.
These robots j never re-construct their schedules. Instead, one
of the robots j ∈S(k) ∩S(k −1) is tasked with providing
information to the other robots i ∈S(k) = Tm that is
necessary to construct their sequences si.
Specifically, this robot j ∈S(k) ∩S(k −1) first notifies
the robots in team S(k) = Tm that it is their turn to construct
their communication schedules.3 Second, robot j transmits to
robots i ∈Tm all sequences sb that were have been constructed
so far by the robots in teams S(1), . . . , S(k −1). Among all
those sequences sb, robots i ∈Tm use only the sequences of
robots b ∈Ni to construct their sequences si.4 As a result, all
robots i ∈Tm that have not constructed si yet, are aware of
the indices nTg
b
that point to entries in sb associated with some
communication events g. These indices satisfy sb(nTg
b ) = g,
3Note that if the teams in S were not necessarily neighboring teams, then
robot j ∈S(k −1) = Tn would have to know who the members of team
S(k) = Tm, m /∈Mj, are in order to notify them that it is their turn
to construct the communication schedules. Due to the fact that S connects
neighboring teams, every robot j needs to know only the structure of teams
Tm, m ∈Mj.
4Note that robot j is not aware of the sets Ni and, therefore, it transmits
all the sequences sb that have already been constructed to robots i ∈Tm.
b ∈Ni.5 Notice that this means that robots i ∈Tm are also
aware of the indices nTm
b
. Using this information, every robot
i ∈Tm constructs the sequence si based on the following
two rules that determine the indices nTg
i
that point to entries
in si where the communication event g will be placed, i.e.,
si(nTg
i ) = g, for all g ∈Mi.
1) First rule: Let nTg
i
denote the index of the entry at which
the communication event g ∈Mi will be placed into
si. If there exists a robot b ∈Ni that has selected nTg
b
so that sb(nTg
b ) = g, then nTg
i
= nTg
b . In this way, all
robots b ∈Tg, including robot i ∈Tm ∩Tg will select
the same index nTg
b
and will participate in the same
communication event g at the same discrete time instant;
see line 4, Alg. 1.
2) Second rule: If there do not exist robots b ∈Ni that
have selected indices nTg
b , for communication event g ∈
Mi, then the communication event g can be placed at
any available entry nTg
i
of si that satisfies the following
requirement. The entry nTg
i
in all sequences sj of robots
j ∈Ni that have already been constructed should not
contain communication events h such that h ∈NTg; see
line 6, Alg. 1.
Note that the index nTm
i
will always be determined by the first
rule, since robot j ∈S(k) ∩S(k −1) has already constructed
its sequence sj by placing the event m at an entry of sj with
index nTm
j
. To highlight the role of the second rule assume
that h ∈NTg. Then, this means that there exists at least one
robot r ∈Th ∩Tg. Notice that without the second rule, at a
subsequent iteration of this procedure, robot r ∈Th∩Tg would
have to place communication events for teams Tg and Th at
a common entry of sr, i.e., nTg
r
= nTh
r , due to the first rule
and, therefore, a conflicting communication event in schedule
schedr would occur. In all the remaining entries of si, X’s
are placed; see line 7, Alg. 1. By construction of si, there are
ℓ−|Mi| X’s in si.
Once all robots i in team S(k) have constructed the se-
quences si, a robot j ∈S(k) ∩S(k + 1) will notify all robots
in team S(k+1) that it is their turn to compute their respective
schedules. The procedure is repeated sequentially over the
teams in S until all robots have computed their respective
schedules of meeting events. This process is summarized in
Algorithm 1 and it is also illustrated in Example 4.3.
Example 4.3 (Algorithm 1): To illustrate Algorithm 1, con-
sider the network of N = 3 robots shown in Figure 1,
where the teams of robots are designed as T1 = {1, 2},
T2 = {2, 3}, and T3 = {3, 1}. Let the sequence S be
S = T1, T2, T3. Hence, initially the robots 1 and 2 in team T1
coordinate to construct their respective sequences si. Assume
that initially robot 1 constructs the sequence s1 of length
equal to ℓ= max {dTm}3
m=1 + 1 = 3. Robot 1 belongs to
teams T1 and T2 and it arbitrarily constructs s1 as follows:
s1 = 1, 3, X. Then the sequence s1 is transmitted to robot 2
that belongs to teams T1 and T2. Now robot 2 is responsible
for constructing the sequence s2. To construct s2, according
5Note that the discrete time instants at which the communication event
g ∈Mi will take place are nTg
i
+ zℓ, where z ∈N, by definition of
schedi.
Algorithm 1: Distributed construction of sequence si, i ∈
Tm
Input: Already constructed sequences sb, ∀b ∈Ni.
Output: Schedule of meeting events: schedi = [si]ω
1 Construct an empty finite sequence si of length ℓ. ;
2 for g ∈Mi do
3
if there exist constructed sequences sb, b ∈Tg then
4
si(nTg
i ) := g, where nTg
i
:= nTg
b , ∀b ∈Tg ;
▷First rule
5
else
6
Choose an available nTg
i
∈{1, . . . , ℓ} such that it
holds either sj(nTg
i ) := X, or sj(nTg
i ) := h with
h /∈NTg, ∀j ∈Ni. Then set si(nTg
i ) := g. ;
▷Second rule
7 Put X in the remaining entries;
to the first rule, team T1 is placed at the first entry of s2, i.e.,
nT1
2
= nT1
1
= 1. Next, the index nT2
2
is determined by the
second rule. Specifically, notice that among the two available
entries in s2 for team T3 the entry nT3
2
= 2 is invalid, since
robot 1 ∈T1 has already constructed its sequence s1 so that
nT3
1
= 2 and for teams T3 and T2 it holds that 3 ∈NT2.
Therefore, robot 2 selects nT2
2 = 2 and constructs the sequence
s2 = 1, X, 2. At the next iteration of Algorithm 1 the robots
2 and 3 in team T2 coordinate to construct their sequences
si. Robot 2 has already constructed the sequence s2 at the
previous iteration and it transmits its constructed sequence s2
and the previously constructed sequence s1 to robot 3. Thus
robot 3 has now access to all already constructed sequences se,
for e ∈N3 = {1, 2}. Robot 3 constructs s3 = X, 3, 2 using the
first rule. Finally, the robots in the third team T3 = {3, 1} have
already constructed their finite paths at previous iterations.
In the following proposition we show that Algorithm 1 can
always construct sequences si if the length ℓof si is selected
as ℓ= max {dTm}M
m=1 + 1.
Proposition 4.4: Algorithm 1 can always construct se-
quences si, for all i ∈N, if the length ℓof si is selected
as ℓ= max {dTm}M
m=1 + 1.
Proof: The proof is based on contradiction. Assume that
a robot i requires a sequence si of length greater than ℓ=
max {dTe}M
e=1 + 1 when Algorithm 1 is applied. This means
that there is team Tm, m ∈Mi, which cannot be placed at
any of the first ℓentries of si. By construction of Algorithm 1,
this means that the team Tm has at least ℓneighbors in graph
GT , i.e., dTm ≥ℓ, which can never happen, which completes
the proof.
Remark 4.5 (Repeated teams in S and initialization): Due
to the requirement that consecutive teams in S need to be
neighbors in GT , it is possible that a team Tm may appear
more than once in S, depending on the structure of the graph
GT . In this case, robots i ∈Tm construct the sequences
si only the first time that team Tm appears in S. Also,
at the first iteration of Algorithm 1, robots of team S(1)
have to construct their sequences si, i ∈S(1). In this case,
a randomly selected robot j ∈S(1) creates arbitrarily its
sequence sj by placing the teams m ∈Mj at the nTm
j
-th
entry of sj. Then the procedure described in Algorithm 1
follows.
Remark 4.6 (Discrete states X): In the schedules schedi,
defined in Definition 4.2 and constructed using Algorithm 1,
the states X indicate that no communication events occur
for robot i at the corresponding discrete time instants. These
states are used to synchronize the communication events over
the discrete time instants c ∈N+, i.e., to ensure that the
discrete time instant z at which communication happens for
team Tm, m ∈M, is the same for all robots i ∈Tm; see also
Example 4.3. Nevertheless, as it will be shown in Theorem
6.5, in Section VI, it is the order of communication events in
schedi that is critical to ensure intermittent communication,
not the time instants that they take place. This is due to a
communication policy proposed in V-C.
V. INTEGRATED TASK PLANNING AND INTERMITTENT
COMMUNICATION CONTROL
In this section, we propose a distributed and online al-
gorithm to synthesize motion plans for all robots i so that
the global LTL formula (1) is satisfied, i.e., the assigned
local LTL−⃝tasks are accomplished, and the network is
intermittently connected. These plans are generated iteratively
and have the following prefix-suffix structure
τ ni
i
= path0
i |path1
i | . . . |[pathni
i ]ω,
(6)
where ni ∈N is the iteration index associated with robot
i, pathni
i
is a finite sequence of states in wTSi, | denotes
the concatenation of discrete paths pathni
i , and ω denotes
the infinite repetition. Each path pathni
i
is constructed so
that (i) execution of pathni
i , for a every given ni ensures
that robot i will communicate exactly once with all teams
Tm, m ∈Mi in an order that respects the schedules schedi
designed in Section IV, and (ii) execution of τ ni
i
guarantees
that the assigned local LTL−⃝tasks φi are satisfied. In Section
V-A, we discuss the distributed construction of the initial
paths path0
i given the communication schedules schedi.
In Section V-B, we present the distributed construction of
all subsequent paths pathni
i
that occurs online as the robots
navigate the worskpace.
A. Construction of Initial Paths
Once robot i constructs its schedule schedi, it locally
designs the initial path path0
i . To do this, feasible initial
communication points for all teams Tm, m ∈M, need to
be selected first, that do not violate the local tasks φi. These
can be found by exhaustively searching through the set of
possible combinations of communication points for all teams.
Specifically, let combb denote any candidate combination of
communication points that can be assigned to all teams Tm,
m ∈M, where b ∈

1, . . . , Q
m∈M |Cm|
	
. Given the com-
munication points vj, j ∈Cm, in the candidate combination
combb, every robot constructs the NBA Bi that corresponds
to the following LTL formula
ψi = φi
|{z}
task
∧
φcom,i
| {z }
communication
,
(7)
where
φcom,i = ∧m∈Mi(□♦vj∈Cm),
(8)
In words, the LTL formula φcom,i requires robot i to visit in-
finitely often the candidate communication points vj, j ∈Cm,
of all teams Tm, m ∈Mi, that are specified in combb. Then,
given the wTSi and the NBA Bi, every robot can synthesize
a motion plan ˜τ 0
i |= ψi, if it exists, which will be used to
construct the initial path path0
i . This process is repeated for
all b ∈

1, . . . , Q
m∈M |Cm|
	
until feasible plans ˜τ 0
i |= ψi can
be constructed for all robots i ∈N. Later, in Lemma 5.2, we
show that the robots can search locally over the combinations
combb reducing in this way the computational cost of finding
a feasible plan ˜τ 0
i .
Specifically, given candidate initial communication points
for all teams Tm, m ∈Mi, the motion plan ˜τ 0
i
can be
constructed by checking the non-emptiness of the language
of the Product B¨uchi Automaton (PBA) Pi = wTSi ⊗Bi,
defined as follows [33]:
Definition 5.1 (Product B¨uchi Automaton):
Given
the
weighted
transition
system
wTSi
=
Qi, q0
i , →i, wPi, AP, Li


and
the
NBA
Bi
=
QBi, Q0
Bi, 2AP, →Bi, FBi


, the Product B¨uchi Automaton
Pi = wTSi⊗Bi is a tuple
QPi, Q0
Pi, −→Pi, wPi, FPi


where
(a) QPi = Qi × QBi is the set of states; (b) Q0
Pi = q0
i × Q0
Bi
is a set of initial states; (c) −→Pi⊆QPi × QPi is the
transition
relation.
Transition
(qP , q′
P )
∈→Pi,
where
qP
= (qvj
i , qB) ∈QPi and q′
P
= (qve
i , q′
B) ∈QPi,
exists if (qvj
i , qve
i ) ∈→i and (qB, Li(qvj
i ), q′
B) ∈→B; (d)
wPi : QPi × QPi →R+ is the weight function, defined
as:
wPi((qvj
i , qB), (qve
i , q′
B))
=
wi(qvj
i , qve
i );
and
(e)
FPi = Qi × FBi is a set of accepting/final states.
More precisely, a motion plan ˜τ 0
i that satisfies ψi can be
derived using graph search techniques on Pi, which can be
viewed as a weighted graph GPi = {VPi, EPi, wPi}, where
VPi = QPi, the set of edges EPi is determined by the transition
relation −→Pi, and the weight function wPi is defined in
Definition 5.1; see e.g., [20]–[23], [37], [38]. Then, a path
from an initial state to an accepting state in GPi (the prefix
path) followed by a cycle around this accepting state (the suffix
path), which is repeated indefinitely, results in an accepting run
of the PBA that has the following prefix-suffix structure
ρ0
Pi =ρpre,0
Pi
h
ρsuf,0
Pi
iω
= (q0
wTSi, q0
Bi)
|
{z
}
∈Q0
Pi
(q1
wTSi, q1
Bi) . . . (qF
wTSi, qF
Bi)
|
{z
}
=qF
Pi∈FPi

(qF
wTSi, qF
Bi) . . . (qL
wTSi, qL
Bi)
ω ,
(9)
where with slight abuse of notation, qβ
wTSi and qβ
Bi de-
note a state of wTSi and Bi, respectively, for all β
∈
{0, . . . , F, . . . , L}. The projection of ρ0
Pi onto the state-space
of wTSi, denoted by Π|wTSiρ0
Pi, results in the desired prefix-
suffix motion plan
˜τ 0
i = Π|wTSiρ0
Pi = ˜τ pre,0
i
h
˜τ suf,0
i
iω
=

q0
wTSi . . . qF
wTSi
 
qF
wTSi . . . qL
wTSi
ω ,
(10)
that satisfies ψi provided feasible initial communication points
have been selected [34]. To reduce the computational cost of
synthesizing ˜τ 0
i , we only require a feasible plan ˜τ 0
i and not
the optimal one that minimizes (3), especially since subsequent
paths pathni
i
will get optimized online.
Given the motion plans ˜τ 0
i = ˜τ pre,0
i
[˜τ suf,0
i
]ω, we design the
discrete paths path0
i as follows. First, we initialize path0
i
as path0
i = ˜τ pre,0
i
|˜τ suf,0
i
. Recall that all paths path0
i are
designed so that if executed, then robot i will communicate
once with all teams Tm, m ∈Mi, in an order that respects
the schedules schedi. Therefore, the state qvj
i
corresponding
to the candidate communication point vj, j ∈Cm, appears
at least once in the suffix part of ˜τ 0
i , by definition of ψi,
for all m
∈
Mi. However, these communication states
may not appear in path0
i = ˜τ pre,0
i
|˜τ suf,0
i
in an order that
respects the schedules schedi, as this is not required by the
LTL formula ψi in (7). Therefore, we append at the end of
path0
i the suffix part ˜τ suf,0
i
enough times so that path0
i =
˜τ pre,0
i
|˜τ suf,0
i
| . . . |˜τ suf,0
i
respects the schedule schedi, i.e., there
exists a sequence of indices κm
i that point to entries in path0
i
corresponding to states qvj
i
with vj, j ∈Cm, that satisfy
κm
i
< κh
i , if the communication event for team Tm appears
before the communication event for team Th in schedi, for
all teams Tm, Th, m, h ∈Mi; see also Example 5.3. Note
that since the state qvj
i , j ∈Cm, appears at least once in the
suffix part of ˜τ 0
i , for all m ∈Mi, the suffix part ˜τ suf,0
i
will
be appended to path0
i at most |Mi| −1 times. With slight
abuse of notation, the initial path τ 0
i in (6) is defined using
only path0
i as follows:
τ 0
i = ˜τ pre,0
i
[˜τ suf,0
i
| . . . |˜τ suf,0
i
]ω
(11)
In what follows, we show that to find a feasible initial
combination of communication points combb that is needed to
determine initial plans ˜τ 0
i , the robots can search locally in the
set of Q
m∈M |Cm| possible combinations of communication
points by solving at most Q
m∈Mi |Cm| control synthesis
problems each, instead of Q
m∈M |Cm|. To see this, observe
that, for any robot i ∈N, there exist multiple combinations
combb that share the same communication points for all
teams Tm, m ∈Mi, and only differ in the communication
points for teams Tm, m ∈M \ Mi. All these combinations,
correspond to the same formula ψi, which means that that
robot i needs to solve a single control synthesis problem to
determine if they are feasible. Motivated by this observation, in
the following lemma, we show that if every robot i ∈N solves
locally at most Q
m∈Mi |Cm| control synthesis problems, then
all combinations combb will be exhaustively explored. By
combining the feasible local combinations of communication
points combi
bi that can be assigned to teams Tm, m ∈Mi,
where bi ∈{1, ..., Q
m∈Mi |Cm|}, that are identified by all
robots i, it it easy to obtain feasible global combinations
combb. Note that, in general, it holds that Q
m∈Mi |Cm| ≤
Q
m∈M |Cm|, where the equality holds if Mi = M or if
|Cm| = 1, for all m ∈M \ Mi. Moreover, Q
m∈Mi |Cm| is
smaller for sparse graphs GT , given a fixed number of teams
and fixed sets Cm.
Lemma 5.2 (Complexity of initialization): Let
combi
bi
with bi
∈

1, . . . , Q
m∈Mi |Cm|
	
denote a combination
of
communication
points
that
can
be
assigned
to
teams Tm, m ∈Mi. Moreover, assume that every robot i ∈N
solves Q
m∈Mi |Cm| control synthesis problems using the
LTL formula (7), one for every combination combi
bi. Then,
the robots can collectively detect any feasible combination of
communication points combb, b ∈

1, . . . , Q
m∈M |Cm|
	
, if
it exists, that can be assigned to all teams Tm, m ∈M.
Proof: In what follows, we show by contradiction that
under this local construction of combb, the robots can detect
all feasible combinations combb. Assume that there exists a
feasible combination combb, that cannot be detected if all
robots solve their respective Q
m∈Mi |Cm| control synthesis
problems. Also, let Π|Micombb denote the combination of
communication points in combb that correspond to all teams
Tm, m ∈Mi. Since combb cannot be detected by the robots,
this means that there exists at least one robot i that either
could not find a feasible solution to the control synthesis
problem that corresponds to the combination Π|Micombb
or did not consider the combination Π|Micombb. The first
case contradicts the assumption that combb is a feasible
combination of communication points that can be assigned
to all teams Tm, m ∈M, while the second case contradicts
the assumption that every robot i ∈N searches over all
combinations combi
bi, completing the proof.
Example 5.3 (Construction of path0
i ): Consider a robot
i with Mi
=
{2, 3, 4, 5} and communication schedule
schedi = [2, 3, X, 4, 5]ω. Consider also the motion plan ˜τ 0
i =
˜τ pre,0
i
[˜τ suf,0
i
]ω
=
qv1
i qv6
i qv4
i qv5
i qv2
i qv3
i [qv3
i qv5
i qv4
i qv6
i qv2
i ]ω,
where v2, v3, v4 are the candidate communication points
for teams T2,
T3,
T4, respectively. The path path0
i
is
initialized as path0
i = ˜τ pre,0
i
|˜τ suf,0
i
. To ensure the existence
of indices κm
i
in path0
i for all teams Tm, m ∈Mi,
that respect the schedule schedi, the suffix part needs
to be appended to path0
i
once more, i.e., path0
i
=
qv1
i qv6
i qv4
i qv5
i qv2
i qv3
i [qv3
i qv5
i qv4
i qv6
i qv2
i ][qv3
i qv5
i qv4
i qv6
i qv2
i ],
where the sequence of states in brackets stands for the suffix
part τ suf,0
i
. Observe that in path0
i there exists indices κ2
i = 5,
κ3
i = 6, κ4
i = 9 and κ5
i = 13, so that κ2
i < κ3
i < κ4
i < κ5
i
as dictated by schedi.
Remark 5.4 (Initialization): Note that there are cases where
feasible initial communication points can be easily identified
by inspection, e.g., if there exists a communication point vj,
j ∈Cm, that (i) does not appear in the atomic propositions
πve
i
that capture the tasks φi assigned to robots i ∈Tm, and
(ii) is directly connected to all locations ve, e ∈I, that robots
i ∈Tm should visit to accomplish their tasks, i.e., the atomic
propositions πve
i
appear in the tasks φi, i ∈Tm. Then, vj,
j ∈Cm, is a feasible communication point for team Tm, since
it does not violate the tasks φi for all i ∈Tm and it does not
affect the communication points the other teams can select due
to (i). Also, due to (ii) robots i ∈Tm can visit vj directly from
any location ve without passing through locations that may
violate φi. Finally, if the negation operator does not appear
in the tasks φi of all robots i ∈Tm, then any communication
point vj, j ∈Cm, assigned to team Tm is feasible.
Remark 5.5 (Formula φcom,i): An alternative selection for
φcom,i, defined in (8), is φ′
com,i = □(♦vj∈Cm ∧(♦ve∈Ch ∧
(♦vd∈Cg ∧. . . ))) that requires robot i to visit communication
points for all teams Tm, m ∈Mi in an given order that
respects the schedules schedi. However, using this formula,
Algorithm 2: Distributed construction of pathni+1
i
, ∀i ∈
Tm, ∀ni ∈N.
Input: Set Cm, wTSi, ni
Output: Paths: pathni+1
i
, ∀i ∈Tm
1 Initialize ci = 1;
2 while ci ≤|Mi| do
3
if team Tm with m = Mi(ci) communicates then
4
for j ∈Cm do
5
Define ψi by (7) given (i) vj for team Tm
and (ii) the selected communication points
for other teams Th, h ∈Mi \ {m};
6
Construct Pi and synthesize a suffix loop
ρsuf,j
Pi
(if it exists) around qF
Pi defined in (9)
that minimizes J(Π|wTSiρsuf,j
Pi );
7
Compute ˜τ suf,j
i
= Π|wTSiρsuf,j
Pi ;
8
Define Costj = P
r∈Tm J(˜τ suf,j
r
), for all j ∈Cm;
9
Compute j∗= argminj∈Cm{Costj}j∈Cm ;
10
Initialize paths pathni+1,ci
i
= ˜τ suf,j∗
i
, for all i ∈Tm;
11
while pathni+1,ci
i
does not respect schedi do
12
Update pathni+1,ci
i
= pathni+1,ci
i
|˜τ suf,j∗
i
13
Update ci = ci + 1;
14 Return path pathni+1
i
= pathni+1,|Mi|
i
;
there is still no guarantee that all communication points will
appear in the suffix part ˜τ suf,0
i
in an order that respects
schedi, as this depends on the structure of the LTL formula
φi and the wTSi. Therefore, we have chosen (8), instead of
φ′
com,i, since (8) corresponds to a much smaller NBA that
makes the proposed algorithm more computationally efficient.
B. Online Construction of Paths
The construction of the paths pathni
i
occurs online and in
an iterative fashion, for all ni ∈N+, as the robots navigate the
workspace. Specifically, pathni+1
i
is constructed and updated
every time robot i participates at communication events, as
it executes pathni
i . Hereafter, we denote by pathni+1,ci
i
the path constructed when robot i participates at the ci-
th communication event in pathni
i . The iteration index ci
is initialized as ci = 1 at the beginning of execution of
pathni
i
and is updated as ci = ci + 1 when the path
pathni+1,ci
i
is constructed. Once robot i has participated in
|Mi| communication events, i.e., ci = |Mi|, then the next
path pathni+1
i
= pathni+1,|Mi|
i
has been constructed and
will be executed after the execution of pathni
i .
In what follows, we present the distributed construction of
pathni+1
i
, which is also summarized in Algorithm 2 and
illustrated in Figure 2. Also, in Algorithm 2, for simplicity
of notations, we assume that the indices of the teams in the
sets Mi are ordered as per the respective schedules schedi.
This means that if the robots in team Tm, m = Mi(ci),
communicate then the next communication event that robot
i needs to participate during the execution of pathni
i
is
Mi(ci + 1). Assume that the robots i ∈Tm, m = Mi(ci),
communicate during the execution of the paths pathni
i . To
(a) Communication within T1
(b) Selection of new vj, j ∈C1
Fig. 2.
Illustration of Algorithm 2 for network of N
=
3 robots
(colored dots) with schedules sched1 = [X, 2]ω, sched2 = [1, 2]ω, and
sched3 = [1, X]ω. All robots currently execute paths pathni
i
constructed
by Algorithm 2. Figure 2(a) illustrates the communication events within team
T1. The corresponding paths pathni+1,ci
i
constructed at this communication
event is depicted in Figure 2(b). Observe in Figure 2(b) that robots 3 has
finalized the construction of the paths pathn3+1
3
since |M3| = 1. The gray
square denotes the state Π|wTSiqF
Pi.
design the paths pathni+1,ci
i
, the robots i ∈Tm need to select
a new communication point vj, j ∈Cm and possibly update
the waypoints vj, j ∈I so that the LTL−⃝tasks φi are
satisfied. The paths pathni+1,ci
i
are constructed in a similar
way as the paths path0
i in Section V-A. The only difference
lies in the definition of the LTL formula ψi in (7), since
now the robots need to autonomously select a new optimal
communication point for team Tm given the already selected
communication points for all other teams. Specifically, all
robots i ∈Tm perform in parallel the following two steps for
all candidate new communication points vj, j ∈Cm, for team
Tm [lines 2-4, Alg. 2]. First, every robot i ∈Tm constructs
the LTL formula ψi, defined in (7), for every candidate new
communication point vj, j ∈Cm for team Tm, and given the
already selected communication points for all other teams Th,
h ∈Mi \ {m}; see (7) [line 5, Alg. 2]. Second, given the
wTSi and the NBA Bi that corresponds to ψi, every robot
i ∈Tm constructs the corresponding PBA Pi = wTSi ⊗Bi
and computes the optimal suffix loop, denoted by ρsuf,j
Pi , around
the same PBA final state qF
Pi = (qF
wTSi, qF
B) that was used to
construct the initial suffix loop of ρ0
Pi in (9). Note that by
optimal suffix loop ρsuf,j
Pi , we refer to the path that minimizes
the cost J(Π|wTSiρsuf,j
Pi ). The projection of this optimal suffix
loop ρsuf,j
Pi
on the state-space of wTSi is denoted by ˜τ suf,j
i
[lines 6-7, Alg. 2].
Once all robots i ∈Tm have constructed the suffix parts
˜τ suf,j
i
for all j ∈Cm, they compute the total cost Costj =
P
i∈Tm J(˜τ suf,j
i
) [line 8, Alg. 2]. This cost captures the dis-
tance that all robots i ∈Tm need to travel during a single
execution of the suffix parts ˜τ suf,j
i
if the new communication
point for team Tm is vj, j ∈Cm. Among all the suffix parts
˜τ suf,j
i
, all robots i ∈Tm select the suffix part ˜τ suf,j∗
i
, with
j∗= argminj{Costj}j∈Cm [line 9, Alg. 2].
Given
the
optimal
suffix
part
˜τ suf,j∗
i
,
we
construct
pathni+1,ci
i
exactly as the initial paths path0
i . Specifically,
first, the paths pathni+1,ci
i
are initialized as pathni+1,ci
i
=
˜τ suf,j∗
i
[line 10, Alg. 2]. Then, we append
˜τ suf,j∗
i
to
pathni+1,ci
i
as many times as needed to satisfy the schedules
schedi [lines 11-12, Alg. 2]. Note that since the state qvj
i ,
j ∈Cm appears at least once in the suffix part of ˜τ suf,j∗
i
,
for all m ∈Mi, the suffix part ˜τ suf,j∗
i
will be appended at
most |Mi| −1 times to pathni+1,ci
i
. After the construction
of pathni+1,ci
i
, the iteration index ci is updated as ci =
ci + 1 and points to the next path pathni+1,ci
i
that will be
constructed when robot i communicates with the robots in
team Th, h = Mi(ci) [line 12, Alg. 2]. 6 If ci = |Mi|,
then this corresponds to the last communication event that
robot i needs to participate during the execution of pathni
i
and, therefore, the construction of pathni+1
i
is finalized, i.e.,
pathni+1
i
= pathni+1,|Mi|
i
[line 14, Alg. 2]. In this case, ci
is re-initialized as ci = 1 [line 1, Alg. 2].
Remark 5.6 (Implicit synchronization across robots):
While the robots transition from pathni
i
to pathni+1
i
asynchronously, there is an implicit synchronization in the
system since, for any iteration n ∈N+, the robots that finish
the execution of pathn
i , first cannot finish the execution of
pathn+1
i
until all other robots r have finished the execution
of their paths pathn
r . The reason is that (i) every robot
i has to participate in |Mi| communication events during
the execution of pathn
i and (ii) the graph of teams GT is
connected by construction of the teams. Therefore, if there
exist robots i and r where robot i executes the path pathn+2
i
and robot r executes the path pathn
r it must be the case
that robot i has skipped at least one communication event
during the execution of pathn+1
i
, which cannot happen by
construction of the proposed algorithm. Therefore, there exist
time instants tn so that pathni
i
= pathn
i , for every n ∈N+
and for all i ∈N.
Remark 5.7 (Computational Cost): Note that to design the
path pathni+1,ci
i
, every robot i needs to solve |Cm| optimal
control synthesis problems. Therefore, the computational cost
of Algorithm 2 increases with |Cm|. To reduce the compu-
tational burden, Algorithm 2 can be executed over subsets
¯Cm ⊆Cm that can change with iterations ni but always include
the current communication point for team Tm. The latter is
required to ensure that paths pathni
i
can be synthesized for
all ni > 0, if a solution to Problem 1 exists; see Proposition
6.1. Moreover, sampling-based approaches can be used to
synthesize the suffix parts ˜τ suf,j
i
that do not require the explicit
construction of the PBA or the application of computationally
expensive graph-search methods [22]. Finally, in Proposition
6.8, we show that Algorithm 2 terminates after a finite number
of iterations, i.e., a repetitive pattern in the paths pathni
i
is eventually detected, for all i ∈N. This means that the
computational cost is bounded.
Remark 5.8 (Fixed final state qF
Pi): Recall that the fixed
PBA final state qF
Pi, defined in (9), is used to construct the
paths pathni+1
i
, for all ni ∈N and for all i ∈N, This re-
quirement can be relaxed by defining the paths pathni+1,ci
i
as
pathni+1,ci
i
= ΠwTSiρci, where ρci = ρci,1|ρci,2| . . . , |ρci,K
is a feasible path in the state-space of Pi, ρci,k a feasible path
in the state-space of Pi that connects two possibly different
6Note that the next communication event Mi(ci) respects the schedules
schedi, by construction of Mi.
PBA final states, for all k ∈{1, . . . , K}, and K < |Mi|
is determined so that execution of pathni+1,ci
i
, for any ci,
ensures that robot i will communicate exactly once with all
teams Tm, m ∈Mi.7 In this case pathni+1
i
is not a periodic
path that can be executed infinitely and, therefore, (6) cannot
be used to model the solution of Algorithm 2, which will
now be an infinite aperiodic sequence of states. Also, allowing
the paths pathni+1
i
to be associated with multiple PBA final
states would increase the computational burden of Algorithm
2, as it requires the computation of K paths in the PBA Pi.
C. Asynchronous Execution
In the majority of global LTL-based motion planning,
robots are assumed to execute their assigned motion plans
synchronously, i.e., all the robots pick synchronously their
next states, see e.g., [25], [29]. However, assuming that robot
motion is performed in a synchronous way is conservative
due to, e.g., uncertainty and exogenous disturbances in the
arrival times of the robots at their next locations as per the
discrete path pathni
i . To the contrary, here the discrete plans
pathni
i
are executed asynchronously across the robots, as per
Algorithm 3.
In Algorithm 3, pathni
i (κi) stands for the κi-th state of the
discrete path pathni
i . The different indices κi for the robots’s
states in the plans pathni
i
allow us to model the situation
where the robots pick asynchronously their next states in
wTSi. Also, in Algorithm 3, the set Kni
i
collects an index κm
i
for all teams Tm, m ∈Mi that (i) satisfy pathni
i (κm
i ) = qvj
i ,
where qvj
i
is associated with a communication point vj,
j ∈Cm, m ∈Mi and (ii) respect the schedules as described in
Section V-A. Note that such indices κm
i
exist by construction
of the paths pathni
i . According to Algorithm 3, when the
state of robot i is pathni
i (κi) = qvj
i , j ∈I i.e., when robot i
arrives at a location vj in the workspace, it checks if κi ∈Kni
i
[lines 3-4, Alg. 3]. If so, then robot i performs the following
control policy [line 5, Alg. 3]:
Definition 5.9 (Control policy at communication locations):
Every robot i that arrives at a communication location vj,
j ∈Cm, m ∈Mi, selected by Algorithm 2 waits there
indefinitely, or until all other robots in the team arrive.
When all the other robots of team Tm arrive at the com-
munication location vj, j ∈Cm, communication for team Tm
occurs and Algorithm 2 is executed to synthesize pathni+1,ci
i
[lines 6-7, Alg. 3]. After that, robot i moves towards the next
state pathni
i (κi + 1) [line 2, Alg. 3]. In line 2 of Alg. 3,
Kni
i
denotes the number of waypoints/states in pathni
i . This
process is repeated until robot i visits all locations in pathni
i .
Once robot i visit all waypoints of pathni
i , it starts executing
the path pathni+1
i
[line 8, Alg. 3]. If ni is the last iteration
of Algorithm 2, then pathni
i
is executed indefinitely.
VI. ALGORITHM ANALYSIS
In this section, we present results pertaining to completeness
and optimality of the proposed distributed control framework.
7Observe that if all paths ρci,k are defined as the shortest loops around
qF
Pi, then ρci,k coincides with the ρsuf,j
Pi , for all k ∈{1, . . . , K}.
Algorithm 3: Asynchronous execution of pathni
i
Input: Discrete path path0
i and set K0
i
1 ni = 0;
2 for κi = 1 : Kni
i
do
3
Move towards the state pathni
i (κi);
4
if κi ∈Kni
i
then
5
Wait at communication point vj, j ∈Cm
[Definition 5.9];
6
if all robots in Tm are present at node vj then
7
Communication occurs within team Tm and
execution of Algorithm 2 ;
8 Execute the next path pathni+1
i
;
Specifically, in Section VI-A, we show that if there exists a
solution to Problem 1, then the proposed distributed framework
will generate prefix-suffix plans τ ni
i , defined in (6), that can
be executed asynchronously according to Algorithm 3, and
satisfy the assigned LTL tasks and the intermittent connectivity
requirement, for every iteration ni ≥0. Then, in Section VI-B
we show that the cost of the suffix part of the plans in (6)
decreases with every iteration of Algorithm 2 while in Section
VI-C we show that these plans converge in a finite number of
iterations. Note that since the proposed algorithm is online,
synthesis and execution take place concurrently and this is
reflected in the subsequent results.
A. Completeness
First, we show that if there exists a feasible solution to
Problem 1 then, feasible paths pathni
i
i.e., feasible loops ρni
Pi
defined over the state-space of the corresponding PBA Pi, can
be designed, for all ni ∈N. This implies that Algorithm 2 can
generate plans τ ni
i , for any ni ≥0 and that robots i in any
team Tm, for m ∈Mi, can stop executing Algorithm 2 at any
iteration nm
i ≥0.
Proposition 6.1 (Feasibility): Assume that there exists a
solution to Problem 1. Then, feasible plans pathni
i
can be
constructed for all ni ≥0.
Proof: First observe that if there exists a solution to
Problem 1, then feasible initial paths ˜τ 0
i that satisfy ψi in (7),
for all robots i ∈N, will be detected since at initialization
we exhaustively search through all available communication
points assigned to the teams Tm, m ∈M, as shown in Lemma
5.2. Therefore, initial feasible paths path0
i can be constructed.
Then, to prove this result, it suffices to show that if there
exists a feasible path pathni
i , then Algorithm 2 can construct
a feasible path pathni+1
i
for all ni ≥0. This means that
Algorithm 2 will not deadlock. Note that Algorithm 2 does
not search over all combinations of communication points
assigned to the teams.
In what follows, we show by induction that if there exists a
feasible path pathni
i
then, Algorithm 2 will construct feasible
paths pathni+1,ci
i
for all ci ∈{1, . . . , |Mi|} and, conse-
quently, it will construct a feasible path pathni+1,|Mi|
i
=
pathni+1
i
for all ni ≥0. To show this, we first define the
sets Fni+1
ci
that collect the suffix parts ˜τ suf,j
i
constructed by
Algorithm 2 during the construction of pathni+1,ci
i
, for all
ci ∈{1, . . . , |Mi|}. Now, assume that there exists a feasible
path pathni
i . This means that Fni+1
0
:= {˜τ suf,j∗,ni
i
} ̸= ∅,
where ˜τ suf,j∗,ni
i
is the suffix part used for the construction of
the path pathni
i . First, we show that Fni+1
1
̸= ∅, i.e., that
Algorithm 2 will construct a feasible plan pathni+1,1
i
. Note
that the only difference between the paths pathni+1,1
i
and
pathni
i
= pathni,|Mi|
i
, in terms of the selected commu-
nication points for teams Tm, m ∈Mi, lies in the selected
communication point of exactly one team Tm, m ∈Mi. Also,
recall that Algorithm 2 searches over all communication points
j ∈Cm, including the current communication point of Tm that
appears in pathni
i , to select the new communication point for
team Tm. Therefore, there exists an optimal control synthesis
problem that is solved by Algorithm 2 during the computation
of pathni+1,1
i
such that the LTL formula ψi is defined over
the communication points selected in pathni,|Mi|
i
. Since
this optimal control synthesis problem is feasible, by the
assumption that pathni
i
is a feasible path, the generated suffix
part, which was also used to construct pathni,|Mi|
i
, belongs to
Fni+1
1
, i.e., Fni+1
1
̸= ∅. The inductive step follows. Assume
that Fni+1
ci
̸= ∅. Then, following the same logic as before
we can show that the feasible suffix path used to construct
pathni+1,ci
i
belongs to Fni+1
ci+1 , i.e., Fni+1
ci+1 ̸= ∅. By induction
we conclude that if Fni+1
0
̸= ∅, i.e., if there exists a feasible
path pathni
i , then Fni+1
ci
̸= ∅for all ci ∈{1, . . . , |Mi|} and
all ni ≥0 completing the proof.
To prove task satisfaction and intermittent communication,
we also need to show that the network is deadlock-free when
the paths pathni
i
are executed according to Algorithm 3.
Specifically, we assume that there is a deadlock, if there
are robots of any team Tm that are waiting forever at a
communication point, selected by Algorithm 2, for the arrival
of all other robots of team Tm due to the control policy in
Definition 5.9.
Proposition 6.2 (Deadlock-free): The mobile robot network
is deadlock-free when the paths τ ni
i
in (6) are executed
according to Algorithm 3.
Proof: Let Wve ⊂Tm denote the set of robots that are
waiting at communication point ve, e ∈Cm, selected by
Algorithm 2, for the arrival of the other robots that belong
to team Tm. Assume that the robots in Tm\Wve never arrive
at that node so that communication at node ve for team Tm
never occurs. This means that the robots in Tm\Wve are
waiting indefinitely at communication locations vj ∈Cn,
j ̸= e, n ̸= m, n ∈NTm, selected by Algorithm 2, to
communicate with robots in team Tn. The fact that there are
robots that remain indefinitely at node vj ∈Cn means that a
communication within team Tn never occurs by construction
of Algorithm 3. Following an argument similar to the above,
we conclude that the robots in Tn\Wvj are waiting indefinitely
at nodes vk̸=j ∈Cf to communicate with robots that belong
to a team Tf, f ∈NTn. Therefore, if a communication
event never occurs for team Tm, then all robots i ∈N
need to be waiting at communication locations selected by
Algorithm 2 and, consequently, there is no communication
location where all robots are present, i.e., there is no team
within which communication will ever occur. Throughout the
rest of the proof we will refer to this network configuration
as a stationary configuration.
In what follows, we show by contradiction that the network
can never reach a stationary configuration when the paths in
(6) are executed asynchronously as per Algorithm 3. To show
this result, we we first model the asynchronous execution of
the schedules schedi, constructed by Algorithm 1, as per
Algorithm 3. Specifically, we introduce discrete time steps zi
that are initialized as zi = 1 and are updated as zi = zi + 1
asynchronously across the robots as follows. If at the current
discrete time step zi robot i participates in the communication
event schedi(zi) = m, for some zi ∈N+ and m ∈Mi,
then robot i ∈Tm waits until all the other robots in team
Tm are available to communicate. Once all robots in Tm are
available, the discrete time step zi is updated as zi = zi + 1.
If schedi(zi) = X, then robot i updates zi = zi + 1 without
waiting.
Using this model to describe asynchronous execution of the
schedules, we now show by contradiction that if the network
gets trapped at a stationary configuration, then there exist
robots of some team Tm that missed a communication event
at node ve, e ∈Cm, at a previous time instant, which cannot
happen by construction of Algorithm 3. Consider that there
is an arbitrary time instant t0 at which the network is at a
stationary configuration and let the current communication
event for all robots i ∈Tm be schedi(nTm
i
(t0)) = m
for some m
∈
Mi, where the indices nTm
i
were de-
fined in Algorithm 1. Define also the set Nmin(t0)
=
n
nTm
i
(t0)|nTm
i
(t0) = min{nTg
e (t0)
oN
e=1 , g ∈Me} that col-
lects the smallest indices nTm
i
(t0) among all robots. Also
let nTg
e (t0) be an index such that nTg
e (t0) ∈Nmin(t0). By
assumption there are robots e ∈Tg and r ∈Tz, g ∈NTz,
such that e ∈Wvf (t0), vf ∈Tg and r ∈Wvd(t0), vd ∈Tz,
and, therefore, the events that are taking place for these two
robots according to their assigned schedules of meeting events
are schede(nTg
e (t0)) = g and schedr(nTz
r (t0)) = z. Since
nTg
e (t0) ∈Nmin(t0) we have that nTg
e (t0) ≥nTz
r (t0), which
along with the fact that g ∈NTz results in nTg
e (t0) > nTz
r (t0)
by construction of Algorithm 1. This leads to the following
contradiction. The fact that nTg
e (t0) > nTz
r (t0) means that
there exists a time instant t < t0 at which the event that took
place for robots a ∈Tg ∩Tz was scheda(nTg
r (t)) = g and at
least one of these robots did not wait for the arrival of all other
robots in team Tg, since at the current time instant t0 there are
still robots in team Tg waiting for the arrival of other robots.
However, such a scenario is precluded by construction of
Algorithm 3. Consequently, the asynchronous execution of the
schedules schedi as per Algorithm 3 is deadlock-free. Recall
now that the paths (6) respect the schedules schedi and that it
is not possible that there exist robots in any team Tm that wait
for other robots in the same team at different communication
points vj, j ∈Cm. Thus, we conclude that the network is
deadlock-free when the plans (6) are executed asynchronously,
as per Algorithm 3, which completes the proof.
Remark 6.3 (Bounded waiting times): Proposition
6.2
shows also that the waiting times introduced by Algorithm 3
are bounded.
In Theorems 6.4-6.5, we show that the assigned local tasks
φi and the intermittent connectivity requirement captured by
(1) are satisfied.
Theorem 6.4 (Task satisfaction): The asynchronous execu-
tion of the motion plans τ ni
i
in (6) as per Algorithm 3, satisfies
the LTL−⃝statements φi, i.e., τ ni
i
|= φi, for any ni ≥0 and
all robots i ∈N.
Proof: First observe that Algorithm 2 can design feasible
paths pathni
i , for any ni ≥0 as long as there exists a
solution to Problem 1, due to Proposition 6.1. Moreover, the
waiting times at the communication points in the plans τ ni
i
are
bounded by Proposition 6.2. Therefore, the infinite paths τ ni
i
will be executed without any deadlocks. This is necessary to
satisfy φi, as LTL formulas are satisfied by infinite sequences
of states in wTSi.
To prove this result, first we need to show that all transitions
in wTSi that are generated by the plans in (6) respect the
transition rule →i; see Definition 3.1. Next, we need to show
that the infinite run ρBi of the NBA Bi that corresponds to
φi over the words σni
i
generated during the execution of τ ni
i
is accepting, i.e., 8
Inf(ρBi) ∩FBi ̸= ∅.
(12)
First, we show that all transitions in wTSi that are due
to the plans in (6) respect the transition rule →i. Notice
that all transitions incurred by the finite path pathni
i
respect
the transition rule →i, for all ni ∈N, by construction; see
Algorithm 2. Next, we show that the transition from the last
state in pathni
i
to the first state in pathni+1
i
also respects
the transition rule →i, for all ni ∈N. To show this, observe
that the last state in pathni
i
is the last state in the suffix part
˜τ suf,j∗
i
used to construct pathni
i , for all ni ∈N. Also, notice
that the first state in pathni+1
i
is the state Π|wTSiqF
Pi, for
all ni ∈N, which is also the first state in ˜τ suf,j∗
i
. Therefore,
by construction of ˜τ suf,j∗
i
, the transition from the last state in
pathni
i
to the first state in pathni+1
i
respects →i, for all
ni ∈N. Consequently, the plans in (6) respect →i.
Next, we show that (12) holds for the plans τ ni
i
in (6), for all
ni ≥1. The same logic also applies to the plans τ 0
i in (11). To
show this result, recall that the paths pathni
i , for all ni ≥1
are designed by (i) constructing a suffix path ρsuf,j∗
Pi
that lives
in the state-space QPi around the fixed PBA final state qF
Pi
defined in (9), and initializing pathni
i
= Π|wTSiρsuf,j∗
Pi
, (ii)
appending the path Π|wTSiρsuf,j∗
Pi
as many times as needed so
that pathni
i
respects the schedule schedi. Thus, pathni
i
can
be written as the projection onto wTSi of the finite path pni
i
=
ρsuf,j∗
Pi
|ρsuf,j∗
Pi
| . . . |ρsuf,j∗
Pi
, which means that pni
i
visits the fixed
PBA final state qF
Pi a finite number of times. Consequently,
since the plans in (6) are defined as infinite sequences of paths
pathni
i , we get that qF
Pi is visited infinitely often, i.e., (12)
holds, completing the proof.
8The generated word σni
i , called also trace of τi
[35] and de-
noted
by
trace(τi),
is
defined
as
σni
i
=
trace(τ ni
i
)
:=
Li(τ ni
i
(1))Li(τ ni
i
(2)) . . . , where Li is the labeling function defined in
Definition 3.1.
Theorem 6.5 (Intermittent Communication): The
asynchronous execution of the motion plans τ ni
i
in (6)
as per Algorithm 3, satisfies the intermittent communication
requirement captured by the global LTL statement φcom,
for all ni ≥0.
Proof: By construction of the paths pathni
i
every robot i
will communicate once with all teams Tm, m ∈Mi, during a
single execution of the path pathni
i . Moreover, by Proposition
6.2, there are no deadlocks during the execution of the plans
τ ni
i . Consequently, all robots i communicate infinitely often
with all teams Tm, m ∈Mi completing the proof.
Combining the previous results, we can show that the
proposed control scheme is complete.
Theorem 6.6 (Completeness): If there exists a solution to
Problem 1, Algorithm 2 will find motion plans τ ni
i
as in (6)
that, when executed asynchronously as per Algorithm 3, satisfy
the local LTL−⃝tasks φi and the global LTL intermittent
connectivity requirement φcom.
Proof: By Proposition 6.1, we get that if there exists
a solution to Problem 1, then prefix-suffix motion plans as
in (6) will be generated for any ni ≥0. Due to Theorems
6.4 and 6.5, the asynchronous execution of these plans as
per Algorithm 3 satisfies the local LTL−⃝tasks φi and
the intermittent communication requirement captured by the
global LTL statement φcom. This completes the proof.
B. Optimality
As discussed in Remark 5.6, execution of the plans in (6)
is synchronized implicitly so that there exists a time instant
tn when all robots execute the path pathn
i . In the following
proposition, we examine the optimality of the paths pathn
i in
terms of the total cost P
i∈N J(pathn
i ), for any n ∈N.
Proposition 6.7 (Optimality): Algorithm 2 generates dis-
crete paths pathn+1
i
so that
X
i∈N
J(pathn
i ) ≤
X
i∈N
J(pathn+1
i
),
(13)
for all n ≥0.
Proof: Consider the discrete paths pathn
i , for some
fixed n ≥0. Recall that the robots may start executing the
paths pathn
i asynchronously, i.e., at different time instants.
Therefore, given a time instant t, we divide the robots i ∈N
in the following five disjoint sets. First, we collect in the set
Rn−1(t) the robots that execute the paths pathn−1
i
at a time
t. Next, we collect in the set Rn
new(t) the robots that are new
to executing the path pathn
i and have not participated in any
communication event contained in pathn
i yet. Notice that the
robots in Rn−1(t) and Rn
new(t) have not constructed yet any
path pathn+1,ci
i
. Also, we collect in the set Rn
com(t) the robots
of all teams Tm, m ∈M, that communicate at time t while
executing the paths pathn
i . All other robots that at time t
execute the path pathn
i but they do not participate in any
communication event are collected in the set Rn
com(t). Finally,
the robots that have already finished the execution of the paths
pathn
i at time t are collected in the set Rn+1(t). Observe that
N = Rn−1(t) ∪Rn
new(t) ∪Rn
com(t) ∪Rn
com(t) ∪Rn+1(t), for
all t ≥0, for some n ≥0. Also observe that if Rn+1(t) ̸= ∅,
then Rn−1(t) = ∅, as discussed in Remark 5.6.
To prove the inequality (13), we need to define the following
cost function:
cost(t) =
X
i∈Rn
new(t)∪Rn−1(t)
J(pathn
i )+
(14)
X
i∈Rn
com(t)
J(pathn+1,ci(t)
i
)+
X
i∈Rn
com(t)
J(pathn+1,ci(t)
i
) +
X
i∈Rn+1(t)
J(pathn+1
i
),
where pathn+1,ci(t)
i
denotes the path that has been con-
structed by Algorithm 2 by the time instant t. Also, note
that the robots i ∈Rn−1(t) may not have completed the
construction of the paths pathn
i yet. Therefore, in the first
summation in (14), the paths pathn
i for i ∈Rn−1(t), are
the ones that these robots will create once they complete their
construction.
Moreover, we define the finite sequence of time instants

tn
0, tn
1, . . . , tn
F −1, tn
F
	
, where (i) tn
0 < · · · < tn
F , (ii) tn
0
is an arbitrarily selected time instant such that Rn
new(t) ∪
Rn−1(t) = N, (ii) (iii) tn
F is the time instant when all
robots have completed construction of the paths pathn+1
i
,
i.e., Rn+1(tn
F ) = N, and (iv) tn
1 < · · · < tn
F −1 are the
time instants corresponding to communication events during
the execution of any of the paths pathn
i .9 To prove (13), we
need to show that
cost(tn
k+1) ≤cost(tn
k),
(15)
for all k ∈{0, . . . , F}.
Since the robots i ∈Rn
new(tn
k+1) ∪Rn−1(tn
k+1) have not
constructed yet any path pathni+1,ci
i
, these robots cannot af-
fect the cost cost(tn
k). Also, notice that path
n+1,ci(tn
k+1)
i
=
pathn+1,ci(tn
k )
i
, for all robots i
∈
Rn
com(tn
k+1), since
these robots do not communicate and, therefore, they do
not execute Algorithm 2 at tn
k+1. Thus, the robots i ∈
Rn
com(tn
k+1) cannot affect the cost cost(tn
k) either. The
same
holds
for
the
robots
i
∈
Rn+1(tn
k+1).
There-
fore, for all robots that do not communicate at time
tn
k+1 it holds that P
i∈N \Rn
com(tn
k+1) J(path
n+1,ci(tn
k+1)
i
) =
P
i∈N \Rn
com(tn
k+1) J(pathn+1,ci(tn
k )
i
). In fact, only the robots
i ∈Rn
com(tn
k+1) that communicate at time tn
k+1 design new
paths such that path
n+1,ci(tn
k+1)
i
̸= pathn+1,ci(tn
k )
i
. Since
Rn
com(tn
k+1) contains all robots that communicate at tn
k+1 the
expression P
i∈Rn
com(tn
k+1) J(path
n+1,ci(tn
k+1)
i
) can be rewrit-
9Note that the time instant tn
0 exists, since it corresponds to a time when
the robots either execute paths pathni−1
i
or paths pathni
i
without having
participated in any communication events yet; see also Remark 5.6. Also, the
sequence
n
tn
1 , . . . , tn
F −1, tn
F
o
for any n ≥0 exists because the network is
deadlock-free, as shown in Proposition 6.2.
ten as follows10
X
i∈Rn
com(tn
k+1)
J(path
n+1,ci(tn
k+1)
i
) =
X
m∈A(tn
k+1)
X
i∈Tm
J(path
n+1,ci(tn
k+1)
i
),
(16)
where A(t) ⊆M is the set of the teams that communicate
at time t. By the proof of Proposition 6.1, we get that
pathn+1,ci(tn
k )
i
is a feasible path returned by Algorithm
2
as
a
candidate
path
for
path
n+1,ci(tn
k+1)
i
;
it
will
become
path
n+1,ci(tn
k+1)
i
if
it
also
the
optimal
one.
Therefore,
we
get
that
P
i∈Tm J(path
n+1,ci(tn
k+1)
i
)
≤
P
i∈Tm J(pathn+1,ci(tn
k )
i
),
for
all
m
∈
A(tn
k+1),
which
implies
P
i∈Rn
com(tn
k+1) J(path
n+1,ci(tn
k+1)
i
)
≤
P
i∈Rn
com(tn
k+1) J(pathn+1,ci(tn
k )
i
), due to (16). Therefore, we
get that (15) holds, completing the proof.
C. Complexity
In the following proposition, we show that Algorithm 2
terminates after a finite number of iterations and, therefore,
the computational cost is bounded.
Proposition 6.8 (Convergence): There
exist
iterations
P
≤
C
in
Algorithm
2
so
that
the
sequence
pathP
i , pathP +1
i
, . . . , pathC
i
is
repeated
indefinitely
for all ni ≥C and all i ∈N.
Proof: To show this result, notice that the sets of commu-
nication points Cm are finite, for all m ∈M and, therefore, the
number of possible combinations of communication points that
can be assigned to the teams is finite. Therefore, there exists
an index n where the paths pathn
i contain communication
points that have appeared in a previous path n′ ≤n, as well,
for all i ∈N. Let C be the first index n when it holds that
the communication points that appear in the paths pathC
i
have already appeared in a previous path pathP −1
i
, for some
P ≤C and for all i ∈N. Since the selected communication
points in the paths pathP −1
i
and pathC
i
are the same, we
have that Algorithm 2 generates the same optimal suffix path
˜τ suf,j∗
i
to synthesize both pathP −1
i
and pathC
i . Therefore,
we get that pathP −1
i
= pathC
i . Consequently, the path
pathC+1
i
will be the same as the path constructed at iteration
P, i.e., pathC+1
i
= pathP
i , since the optimal control synthe-
sis problems that are solved to construct the path pathC+1
i
and pathP
i
are the same, for all robots i ∈N. Similarly,
we have that pathC+2
i
= pathP +1
i
. By inspection of the
repetitive pattern, we conclude that for any n ∈N it holds
that pathC+n
i
= pathC+n−(⌊(C+n)/(C−P +1)⌋−1)(C−P +1)
i
,
where ⌊·⌋stands for the floor function. We conclude that
10Note that it is possible that two teams Tm and Th that share at least
a robot may be present simultaneously at the same communication point.
This can happen, e.g., if the schedule of robot i ∈Tm ∩Th has a schedule
has the form schedi = [m, h, X]ω and Cm ∩Ch ̸= ∅. In this case, we
assume that communication at the common communication point will happen
sequentially across the teams according to the schedules. This ensures that in
the second summation in (16), we never double count the cost of the paths
pathn+1,ci(t)
i
.
the sequence pathP
i , pathP +1
i
, . . . , pathC
i
is repeated in-
definitely for all iterations ni ≥C of Algorithm 2 and for
all robots i ∈N completing the proof. which completes the
proof.
Remark 6.9 (Optimality of Algorithm 2): Notice
that
Propositions 6.7-6.8 do not guarantee that Algorithm 2
will find the optimal prefix-suffix plan that minimizes the
cost Jp(τi)
=
α P
i∈N J(τ pre
i ) + (1 −α) P
i∈N J(τ suf
i ).
Instead they only ensure that the total cost P
i∈N J(pathn
i )
decreases with every iteration n until n
=
P, when
P
i∈N J(pathP
i )
=
P
i∈N J(pathP +1
i
)
=
· · ·
=
P
i∈N J(pathC
i ) while for all iterations ni
≥
C the
sequence of paths pathP
i , pathP +1
i
, . . . , pathC
i is repeated
indefinitely. Therefore, the best plans τ ni
i
(6) are obtained for
any ni ≥P, for all robots i ∈N. Sub-optimality is due to the
decomposition of Problem 1 into intermittent communication
control (Section IV) and task planning (Section V) that
are solved independently. The optimal plan can be found
by translating the global LTL formula (2) into a NBA,
constructing a product automaton across all robots in the
network as, e.g., in [20], [21], and using graph search methods
to find the optimal plan. However, such centralized methods
are computationally expensive and resource demanding as it
is also discussed in the Introduction. Moreover, recall that
in this work we assume that the teams Tm are fixed and
never change. Note that the total cost of the plans τ ni
i
can
be further minimized if the robots in every team Tm update
not only the communication point vj, j ∈Cm, but also the
teams they belong to. Optimal design of the teams is part of
our future work.
VII. SIMULATION STUDIES
In this section, we present a simulation study, implemented
using MATLAB R2015b on a computer with Intel Core i7
2.2GHz and 4Gb RAM that illustrates our approach for a
network of N
= 12 robots. Robots are categorized into
M = 12 teams as follows: T1 = {1, 2, 9}, T2 = {3, 4, 5},
T3 = {3, 6}, T4 = {1, 3}, T5 = {2, 5, 6, 11}, T6 = {4, 12},
T7 = {5, 9}, T8 = {4, 9, 12}, T9 = {6, 7, 10}, T10 =
{7, 8, 11}, T11 = {8, 10, 11, 12}, and T12 = {7, 10}. Notice
that the construction of teams Tm results in a connected graph
GT with max{dTm}M
m=1 = 7, as discussed in Section III.
Mobility of each robot in the workspace is captured by a wTS
with |Qi| = 300 states that represent W = 300 locations of
interest and weights wi that capture the distance between its
states. Among the W = 300 locations of interest, R = 70
locations correspond to possible communication points. Also,
every team has 4 ≤|Cm| ≤6 communication points while
Cm ∩Cn = ∅, for all m, n ∈M. Also, the parameter α
in (3) is selected as α = 0.5. To model uncertainty in robot
mobility, caused by exogenous disturbances that may affect
the arrival times of the robots at the communication locations,
we assume that the time required for robot i to travel from
location ve to vj, with (qve
i , qvj
i ) ∈→i, is generated by a
uniform distribution on [1, 2], at the moment when robot i
arrives at location ve.
The LTL−⃝tasks for robots 1, and 3 are φ1 = □♦(πv20
1
∨
πv10
1
∨πv11
1
) ∧□♦(πv61
1
) ∧□♦(πv91
1
∨πv100
1
∨πv5
1 ∨πv60
1
) ∧
□(¬πv44
1
) ∧♦(πv6
1
∨πv7
1
∨πv133
1
) and φ3 = □♦(ξ1
3 ∨ξ2
3) ∧
[□♦(ξ3
3)] ∧♦[ξ2
3 →□(¬ξ1
3)] ∧(¬ξ3
3Uξ1
3), respectively, where
ξ1
3 = πv81
3
∨πv91
3
, ξ2
3 = πv120
3
∨πv91
3
∨πv31
3
, and ξ3
3 = πv91
3
∨
πv110
3
∨πv15
3
∨πv130
3
. All other robots are responsible for similar
LTL tasks. For instance, the LTL formula in φ3 requires robot
3 to (i) satisfy infinitely often either the Boolean formula ξ1
3
or ξ2
3; (ii) satisfy infinitely often the Boolean formula ξ3
3; (iii)
never satisfy ξ1
3 if ξ2
3 is ever satisfied; and (iv) never satisfy
ξ3
3 until ξ1
3 is satisfied. The Boolean formula ξ1
3 is satisfied
if robot 3 visits either v81 or v91. The Boolean formulas ξ2
3
and ξ3
3 are interpreted similarly. Also, note that robot 1 is
responsible for visiting a user located at v61 infinitely often
to transmit all collected information.
The schedules of communication events constructed as per
Algorithm 1 have the following form with length ℓ= 4 ≤
max{dTm}12
m=1 + 1 = 8.
sched1 = [1, 4, X, X]ω, sched7 = [9, 12, 10, X]ω,
sched2 = [1, 5, X, X]ω, sched8 = [X, X, 10, 11]ω,
sched3 = [2, 4, 3, X]ω,
sched9 = [1, X, 8, 7]ω,
sched4 = [2, 6, 8, X]ω,
sched10 = [ 9, 12, X, 11]ω,
sched5 = [2, 5, X, 7]ω,
sched11 = [X, 5, 10, 11]ω.
sched6 = [9, 5, 3, X]ω,
sched12 = [X, 6, 8, 11]ω.
Then, given the above schedules, feasible initial paths
path0
i are constructed for all robots in 3 seconds approxi-
mately using [22]. Specifically, given communication points
for all teams Tm, m ∈Mi, [22] can synthesize a feasible
plan ˜τ 0
i that satisfies ψi in 0.35 seconds on average for all
i ∈N. Similar runtimes are reported if off-the-shelf model
checkers, such as NuSMV [39], are employed for initialization.
Moreover, Algorithm 2 constructs online paths pathni
i
with
P = C = 5. The size of the NBA Bi that corresponds to ψi in
(7) satisfies 7 ≤|QBi| ≤16, for all i ∈N while the average
runtime to solve a single optimal control synthesis problem
to generate the optimal suffix path ˜τ suf,j
i
was 45 seconds.
Since 4 ≤|Cm| ≤6, for all m ∈Cm, the average runtime
of Algorithm 2 per iteration ci is between 4 × 45 = 180
seconds and 6 × 45 = 270 seconds. Note that this runtime
depends only on the size of the sets Cm and not on the size of
the teams Tm. Note also that this runtime is higher than the
initialization runtime, since during initialization only feasible
plans are required while for the online construction of pathni
i
optimal suffix paths are created. More computational efficient
methods are discussed in Remark 5.7 that can decrease the
corresponding runtime.
To illustrate that the designed motion plans ensure inter-
mittent communication among the robots infinitely often, we
implement a consensus algorithm over the dynamic network
Gc. Specifically, we assume that initially all robots generate a
random number vi(t0) and when all robots i ∈Tm meet at a
communication point j ∈Cm they perform the following con-
sensus update vi(t) =
1
|Tm|
P
e∈Tm ve(t). Figure 3(a) shows
that eventually all robots reach a consensus on the numbers
vi(t), which means that communication among robots takes
place infinitely often, as proven in Theorem 6.5. Moreover,
Figure 3(b) shows the time instants when robots 1, 2, and 3
0
10
20
30
40
50
60
70
80
90
6
8
10
12
14
16
18
20
(a)
0
500
1000
1500
2000
2500
3000
3500
4000
0
2
4
6
8
10
12
14
(b)
Fig. 3.
Figure 3(a) depicts the consensus of numbers vi(t). Figure 3(b)
illustrates the time instants when the robots 1, 2, and 3 started executing the
paths pathn
i . For instance, the time between the second and the third red
square denotes the time required by robot 1 to travel along the path path2
1.
0
100
200
300
400
500
600
700
800
0
2
4
6
8
10
12
14
16
18
20
(a) Team 1
0
100
200
300
400
500
600
700
800
0
2
4
6
8
10
12
14
16
18
20
(b) Team 4
Fig. 4.
Graphical depiction of communication events for team T1 (Figure
4(a)) and T4 (Figure 4(b)) with respect to time.
started executing the paths pathn
i , for all n ∈{1, . . . , 14}.
Observe in Figure 3(b) that there exist time instants tn when
all three robots are executing their respective paths pathn
i
for a common n, for all n ∈{1, . . . , 14}, as discussed in
Remark 5.6. The communication events over time for teams
T1 and T5 are depicted in Figure 4. Observe in Figure 4 that
the communication time instances do not depend linearly on
time, which means that communication within these teams
is aperiodic. Figure 5 shows that the total traveled distance
PN
i=1 J(pathn
i ) with respect to n ∈N which decreases as
expected due to Proposition 6.7. The corresponding simulation
video can be found in [40].
Note also that due to excessive memory requirements it
would be impossible to generate optimal motion plans τi by
using either the optimal control synthesis methods presented in
[20], [21], [29] that rely on the construction of a synchronous
product automaton or off-the-shelf model checkers [39], [41]
that can construct feasible but not optimal paths. Specifically,
[20], [21], [29] rely on the construction of a product transition
system (PTS), whose state space has dimension |QPTS| =
×∀i|Qi| = W |N| = 30012 = 5.3144 × 1029. This PTS is
combined with the B¨uchi Automaton B that corresponds to
the LTL statement φ = (∧∀i∈N φi) ∧φcom to construct a
Product B¨uchi Automaton whose state space has dimension
|QPBA| = |QPTS| × |QB| = 5.3144 × 1029 × |QB| which
is too large to manipulate in practice let alone searching for
an optimal accepting infinite run. Finally, we validated the
efficacy of the proposed distributed algorithm by experimental
results that are omitted due to space limitations. The video
showing the conducted experiment along with its description
can be found in [42].
0
2
4
6
8
10
12
14
5500
6000
6500
7000
7500
8000
8500
9000
Fig. 5. Evolution of the total cost P12
i=1 J(pathn
i ) with respect to iterations
n. Note that there is also a slight decrease in P12
i=1 J(pathn
i ) from n = 4
to n = 5. After n = 5, a repetitive pattern in pathn
i is detected giving rise
to motion plans τi in a prefix-suffix form.
VIII. CONCLUSION
In this paper, we developed the first distributed and online
intermittent communication framework for networks of mo-
bile robots with limited communication capabilities that are
responsible for accomplishing temporal logic tasks. Our pro-
posed distributed online control framework jointly determines
local plans that allow all robots to fulfill their assigned LTL−⃝
tasks, schedules of communication events that guarantee infor-
mation exchange infinitely often, and optimal communication
locations that minimize a desired distance metric. We showed
that the proposed method can solve optimally very large-scale
problems that are impossible to solve using current off-the-
shelf model-checkers.
REFERENCES
[1] M. M. Zavlanos and G. J. Pappas, “Potential fields for maintaining
connectivity of mobile networks,” IEEE Transactions on Robotics,,
vol. 23, no. 4, pp. 812–816, 2007.
[2] M. Ji and M. B. Egerstedt, “Distributed coordination control of multi-
agent systems while preserving connectedness.” IEEE Transactions on
Robotics, vol. 23, no. 4, pp. 693–703, August 2007.
[3] M. Zavlanos and G. Pappas, “Distributed connectivity control of mobile
networks,” IEEE Transactions on Robotics, vol. 24, no. 6, pp. 1416–
1428, 2008.
[4] L. Sabattini, N. Chopra, and C. Secchi, “Decentralized connectivity
maintenance for cooperative control of mobile robotic systems,” The
International Journal of Robotics Research, vol. 32, no. 12, pp. 1411–
1423, 2013.
[5] M. Zavlanos, M. Egerstedt, and G. Pappas, “Graph theoretic connectivity
control of mobile robot networks,” Proc. of the IEEE, vol. 99, no. 9,
pp. 1525–1540, 2011.
[6] M. M. Zavlanos, A. Ribeiro, and G. J. Pappas, “Network integrity in
mobile robotic networks,” IEEE Transactions on Automatic Control,
vol. 58, no. 1, pp. 3–18, 2013.
[7] Y. Yan and Y. Mostofi, “Robotic router formation in realistic commu-
nication environments,” IEEE Transactions on Robotics, vol. 28, no. 4,
pp. 810–827, 2012.
[8] Y. Kantaros and M. M. Zavlanos, “Distributed communication-aware
coverage control by mobile sensor networks,” Automatica, vol. 63, pp.
209–220, 2016.
[9] Y. Kantaros and M. M. Zavlanos, “Global planning for multi-robot
communication networks in complex environments,” IEEE Transactions
on Robotics, vol. 32, no. 5, pp. 1045–1061, October 2016.
[10] J. Stephan, J. Fink, V. Kumar, and A. Ribeiro, “Concurrent control of
mobility and communication in multirobot systems,” IEEE Transactions
on Robotics, 2017.
[11] G. Wen, Z. Duan, W. Ren, and G. Chen, “Distributed consensus of
multi-agent systems with general linear node dynamics and intermit-
tent communications,” International Journal of Robust and Nonlinear
Control, vol. 24, no. 16, pp. 2438–2457, 2014.
[12] Y. Wang and I. I. Hussein, “Awareness coverage control over large-scale
domains with intermittent communications,” Automatic Control, IEEE
Transactions on, vol. 55, no. 8, pp. 1850–1859, 2010.
[13] A. Lindgren, A. Doria, and O. Schel´en, “Probabilistic routing in in-
termittently connected networks,” ACM SIGMOBILE mobile computing
and communications review, vol. 7, no. 3, pp. 19–20, 2003.
[14] E. P. Jones, L. Li, J. K. Schmidtke, and P. A. Ward, “Practical routing
in delay-tolerant networks,” Mobile Computing, IEEE Transactions on,
vol. 6, no. 8, pp. 943–959, 2007.
[15] D. V. Dimarogonas, E. Frazzoli, and K. H. Johansson, “Distributed
event-triggered control for multi-agent systems,” IEEE Transactions on
Automatic Control, vol. 57, no. 5, pp. 1291–1297, 2012.
[16] P. Tabuada, “Event-triggered real-time scheduling of stabilizing control
tasks,” IEEE Transactions on Automatic Control, vol. 52, no. 9, pp.
1680–1685, 2007.
[17] M. Kloetzer and C. Belta, “Distributed implementations of global
temporal logic motion specifications,” in IEEE International Conference
on Robotics and Automation, Pasadena, CA, USA, May 2008, pp. 393–
398.
[18] Y. Chen, X. C. Ding, and C. Belta, “Synthesis of distributed control and
communication schemes from global LTL specifications,” in 50th IEEE
Conference on Decision and Control and European Control Conference,
Orlando, FL, USA, December 2011, pp. 2718–2723.
[19] Y. Chen, X. C. Ding, A. Stefanescu, and C. Belta, “Formal approach
to the deployment of distributed robotic teams,” IEEE Transactions on
Robotics, vol. 28, no. 1, pp. 158–171, 2012.
[20] A. Ulusoy, S. L. Smith, X. C. Ding, C. Belta, and D. Rus, “Optimality
and robustness in multi-robot path planning with temporal logic con-
straints,” The International Journal of Robotics Research, vol. 32, no. 8,
pp. 889–911, 2013.
[21] A. Ulusoy, S. L. Smith, and C. Belta, “Optimal multi-robot path planning
with ltl constraints: guaranteeing correctness through synchronization,”
in Distributed Autonomous Robotic Systems.
Springer, 2014, pp. 337–
351.
[22] Y. Kantaros and M. M. Zavlanos, “Sampling-based optimal control
synthesis
for
multi-robot
systems
under
global
temporal
tasks,”
IEEE Transactions on Automatic Control, 2017, (accepted). [Online].
Available: https://arxiv.org/pdf/1706.04216.pdf
[23] Y. Kantaros and M. M. Zavlanos, “Distributed optimal control synthesis
for multi-robot systems under global temporal tasks,” in 9th ACM/IEEE
International Conference on Cyber-Physical Systems (ICCPS), Porto,
Portugal, April 2018, pp. 162–173.
[24] Y. E. Sahin, P. Nilsson, and N. Ozay, “Provably-correct coordination
of large collections of agents with counting temporal logic constraints,”
in Proceedings of the 8th International Conference on Cyber-Physical
Systems.
Pittsburgh,PA: ACM, 2017, pp. 249–258.
[25] M. Kloetzer and C. Belta, “Automatic deployment of distributed teams
of robots from temporal logic motion specifications,” IEEE Transactions
on Robotics, vol. 26, no. 1, pp. 48–61, 2010.
[26] G. Pola, P. Pepe, and M. D. Di Benedetto, “Decentralized supervi-
sory control of networks of nonlinear control systems,” arXiv preprint
arXiv:1606.04647, 2016.
[27] Y. Kantaros and M. M. Zavlanos, “Distributed intermittent connectivity
control of mobile robot networks,” Transactions on Automatic Control,
vol. 62, no. 7, pp. 3109–3121, July 2017.
[28] Y. Kantaros and M. M. Zavlanos, “Simultaneous intermittent communi-
cation control and path optimization in networks of mobile robots,” in
Conference on Decision and Control (CDC).
Las Vegas, NV: IEEE,
December 2016, pp. 1794–1795.
[29] Y. Kantaros and M. M. Zavlanos, “Intermittent connectivity control
in mobile robot networks,” in 49th Asilomar Conference on Signals,
Systems and Computers, Pacific Grove, CA, USA, November, 2015, pp.
1125–1129.
[30] M. Guo and M. M. Zavlanos, “Distributed data gathering with buffer
constraints and intermittent communication,” in IEEE Internationtal
Conference on Robotics and Automation (ICRA), Singapore, May-June
2017, pp. 279–284.
[31] M. M. Zavlanos, “Synchronous rendezvous of very-low-range wireless
agents,” in 49th IEEE Conference on Decision and Control (CDC),
Atlanta, GA, USA, December 2010, pp. 4740–4745.
[32] G. Hollinger and S. Singh, “Multi-robot coordination with periodic
connectivity,” in IEEE International Conference on Robotics and Au-
tomation (ICRA), Anchorage, Alaska, May 2010, pp. 4457–4462.
[33] C. Baier and J.-P. Katoen, Principles of model checking.
MIT press
Cambridge, 2008, vol. 26202649.
[34] M. Y. Vardi and P. Wolper, “An automata-theoretic approach to automatic
program verification,” in 1st Symposium in Logic in Computer Science
(LICS).
IEEE Computer Society, 1986.
[35] E. M. Clarke, O. Grumberg, and D. Peled, Model checking. MIT press,
1999.
[36] M. Kloetzer and C. Belta, “A fully automated framework for control of
linear systems from temporal logic specifications,” IEEE Transactions
on Automatic Control, vol. 53, no. 1, pp. 287–297, 2008.
[37] S. L. Smith, J. Tumova, C. Belta, and D. Rus, “Optimal path planning for
surveillance with temporal-logic constraints,” The International Journal
of Robotics Research, vol. 30, no. 14, pp. 1695–1708, 2011.
[38] M. Guo and D. V. Dimarogonas, “Multi-agent plan reconfiguration
under local LTL specifications,” The International Journal of Robotics
Research, vol. 34, no. 2, pp. 218–235, 2015.
[39] A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore,
M. Roveri, R. Sebastiani, and A. Tacchella, “Nusmv 2: An opensource
tool for symbolic model checking,” in International Conference on
Computer Aided Verification.
Springer, 2002, pp. 359–364.
[40] SimulationVideo, https://vimeo.com/274366915, 2018.
[41] G. J. Holzmann, The SPIN model checker: Primer and reference manual.
Addison-Wesley Reading, 2004, vol. 1003.
[42] ExperimentVideo, https://vimeo.com/239508876, 2017.