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. I NTRODUCTION  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. P RELIMINARIES  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   2 AP   is defined as an infinite sequence   σ   =   π 0 π 1 π 2   · · · ∈   (2 AP   ) ω   , where   ω   denotes infinite repetition and   π k   ∈   2 AP   ,   ∀ k   ∈   N . The language  Words ( φ ) =   { σ   ∈   (2 AP   ) ω   | σ   | =   φ }   is defined as the set of words that satisfy the LTL formula   φ , where   | = ⊆   (2 AP   ) ω   ×   φ  is the satisfaction relation. Any LTL formula   φ   can be translated into a Nondetermin- istic B  ̈ uchi Automaton (NBA) over   2 AP   denoted by   B , which is defined as follows [34]:  Definition 2.1 (NBA):   A   Nondeterministic B  ̈ uchi Automa- ton   (NBA)   B   over   2 AP   is   defined   as   a   tuple   B   = ( Q B   ,   Q 0  B   ,   Σ ,   → B   ,   F B  ) , where   Q B   is the set of states,   Q 0  B   ⊆ Q B   is a set of initial states,   Σ   =   2 AP   is an alphabet,  → B   ⊆ Q B   ×   Σ   × Q B   is the transition relation, and   F B   ⊆ Q B  is a set of accepting/final states. An   infinite run   ρ B   of   B   over an infinite word   σ   =   π 0 π 1 π 2   . . .   ,  π k   ∈   Σ = 2 AP   ∀ k   ∈   N   is a sequence   ρ B   =   q 0  B   q 1  B   q 2  B   . . .  such that   q 0  B   ∈ Q 0  B   and   ( q k B   , π k , q k +1  B   )   ∈→ B   ,   ∀ k   ∈   N . An infinite run   ρ B   is called   accepting   if   Inf ( ρ B   )   ∩ F B   6   =   ∅ , 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   L B   . 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.,   L B   =   Words ( φ ) .
III. P ROBLEM   F ORMULATION  Consider   N   ≥   1   mobile robots operating in a workspace  W ⊂   R d ,   d   ∈ { 2 ,   3 } , containing   W >   0   locations of interest denoted by   v j   ,   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   wTS i   is a   tuple   wTS i   =   ( Q i , q 0  i   ,   → i , w i ,   AP , L i  )   where   (a)  Q i   =   { q v j  i   , j   ∈ I}   is the set of states, where a state   q v j  i  indicates that robot   i   is at location   v j   ∈ W ; (b)   q 0  i   ∈ Q i  is the initial state of robot   i ; (c)   → i ⊆ Q i   × Q i   is a given transition relation such that   ( q v j  i   , q v e  i   )   ∈→ i   if there exists a controller that can drive robot   i   from location   v j   to   v e   in finite time without going through any other location   v c ; (d)  w i   :   Q i   × Q i   →   R +   is a weight function that captures the distance that robot   i   needs to travel to move from   v j   to   v e ; 1  (e)   AP   =   {{ π v j  i   } N i =1 } j ∈I   is the set of atomic propositions associated with each state; and (f)   L i   :   Q i   → AP   is defined as   L i ( q v j  i   ) =   π v j  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   v j   ,   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   =   {{ π v j  i   } N i =1 } j ∈I   , where   π v j  i   = 1   if   ‖ x i   −   v j   ‖ ≤    , for a sufficiently small    >   0 , and 0 otherwise, for all   i   ∈ N   and  j   ∈ I . 2   Namely, the atomic proposition   π v j  i   is true if robot   i   is sufficiently close to location   v j   . For example, an LTL −©   task for robot   i   can be:   φ i   = ( ♦ π v 4  i   )   ∧   (( ¬ π v 4  i   ) U π v 8  i   )   ∧   ( ♦ π v 5  i   )   ∧  (  ¬ π v 3  i   ) ∧ ( ♦ π v 1  i   ) , which requires robot   i   to (i) visit location  v 4   infinitely often, (ii) never visit location   v 4   until location   v 8  is visited, (iii) eventually visit location   v 5 , (iv) always avoid an obstacle located at   v 3 , and (v) visit location at   v 1   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   T m , for all   m   ∈ M   :=   { 1 ,   2 , . . . , M   } . We define the set that collects the indices of teams that robot   i   belongs to as   M i   =   { m | i   ∈ T m , 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   N i   =   { j | j   ∈ T m ,   ∀ m   ∈ M i } \ { i } ,   ∀ i   ∈ N   . Given the robot teams   T m , for all   m   ∈ M , we can define the graph over these teams as follows.  1 Note 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  v j   to   v e .  2 The 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   G T   ):   The   graph over the teams   T m ,   m   ∈ M   is defined as   G T   = ( V T   ,   E T   ) , where the set of nodes   V T   =   M   is indexed by the teams   T m  and set of edges   E T   is defined as   E T   =   { ( m, n ) |T m   ∩ T n   6   =  ∅ ,   ∀ m, n   ∈ M , m   6   =   n } . Given the team membership graph   G T   , we can also de- fine the set   N T m   :=   { e   ∈ V T   | ( m, e )   ∈ E T   }   that collects all neighboring teams of team   T m   in   G T   . Since the robots have limited communication capabilities, we assume that the robots in every subgroup   T m   can only communicate if all of them are simultaneously present at a common location   v j   ∈ W , hereafter called a communication point. We assume that there are   R   ≥   1   available communication points in the workspace at locations   v j   ∈   W , where   j   ∈   C   ⊂   I . Among those communication points, the ones that are specifically available to the robotic team   T m   are collected in a finite set   C m   ⊆ C , where the sets   C m   are not necessarily disjoint. When all robots in a team   T m   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   G c ( t ) ):   The com- munication network among the robots is defined as a dynamic undirected graph   G c ( t ) = ( V c ,   E c ( t )) , where the set of nodes  V c   is indexed by the robots, i.e.,   V c   =   N   , and   E c ( t )   ⊆ V c   ×V c  is the set of communication links that emerge among robots in every team   T m , when they all meet at a common com- munication point   v j   , for some   j   ∈ C m   simultaneously, i.e.,  E c ( t ) =   { ( e, i ) ,   ∀   i, e   ∈ T m ,   ∀ m   ∈ M |   x i ( t ) =   x e ( t ) =  v j   ,   for some   j   ∈ C m } . To   ensure   that   information   is   continuously   transmitted across the network of robots, we require that the commu- nication graph   G c ( t )   is   connected over time infinitely often , i.e., that all robots in every team   T m   meet infinitely often at a common communication point   v j   ,   j   ∈ C m , that does not need to be fixed over time. For this, it is necessary to assume that the graph of teams   G T   is connected. Specifically, if   G T   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   G T   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   T m   are   a priori   known and can be selected arbitrarily as long as the graph of teams  G T   is connected. Intermittent   connectivity   of   the   communication   network  G c ( t )   can be captured by the global LTL formula  φ com   =   ∧ m ∈M  ( ♦   ( ∨ j ∈C m   ( ∧ i ∈T m   π v j  i   ) ))   ,   (1) specified over the set of atomic propositions   {{ π v j  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   G c . Given the wTS i , 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 wTS i   [35], i.e., infinite sequences of states in wTS i , such that   τ i (1) =   q 0  i   ,  τ i ( κ )   ∈ Q i , 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 wTS i , 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  J p ( τ 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   |  ∑  κ =1  w i ( τ   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   w i   are the weights defined in Definition 3.1. The cost   J ( τ   pre  i   )   of the prefix part is defined accordingly. In words,   J p ( τ 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   T m ,   m   ∈ M   so that the associated graph   G T   is connected. Determine discrete motion plans   τ i , i.e., sequences of states   q v j  i   ∈ Q i , 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   ∑  i ∈N   J p ( τ 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   G T  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   ∑  i ∈N   J p ( τ 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:   T 1   =   { 1 ,   2 } ,   T 2   =   { 2 ,   3 } , and   T 3   =   { 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   v e   and   v j   . The sets of communications points for each team are defined as   C 1   =   { v 9 ,   v 10 } ,  C 2   =   { v 10 ,   v 11 } , and   C 3   =   { v 12 } .  IV. I NTERMITTENT   C OMMUNICATION   C ONTROL  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   =   T n ,   T m , . . .   . The sequence  S   satisfies two requirements: (i) all teams   T m ,   m   ∈   M  appear in   S ; and (ii) consecutive teams   T n   and   T m   that appear in   S   are neighboring nodes in the graph   G T   , i.e.,  m   ∈ N T n   :=   { e   ∈ V T   | ( n, e )   ∈ E T   } . 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   sched i   for all robots   i   that determine the order in which those robots participate in communication events for teams   T m ,   ∀ m   ∈ M i   and are defined as follows:  Definition 4.2 (Schedule of Communication Events):   The schedule   sched i   of   communication   events   of   robot   i   is
defined as an infinite repetition of the finite sequence  s i   = X, . . . , X,   M i (1) , X, . . . , X,   M i (2) , X, . . . , X,  M i ( |M i | ) , X, . . . , X,   (5) i.e.,   sched i   =   s i , s i ,   · · ·   =   s ω i   , where   ω   stands for the infinite repetition of   s i . In (5),   M i ( e ) ,   e   ∈ { 1 , . . . ,   |M i |}   stands for the   e -th entry of   M i   and represents a communication event for team with index   M i ( e ) , and the discrete states   X   indicate that there is no communication event for robot   i . The length of the sequence  s i   is   `   = max   { d T m   } M m =1   + 1   for all   i   ∈ N   , where   d T m   is the degree of node   m   ∈ V T   . 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   sched i   defines the order in which robot  i   participates in the communication events for the teams   m   ∈ M i , for all robots   i   ∈ N   . Specifically, at a discrete time step   z   ∈   N + , robot   i   either communicates with all robots that belong to team   T m , for   m   ∈ M i   if   sched i ( z ) =   m , or does not need to participate in any communication event if  sched i ( 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   sched i . These schedules are constructed se- quentially across the teams   T m ,   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 )   =   T m , 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   T n   with   n   ∈ N T m   such that   S ( k   −   1) =   T n  and   T m   ∩ T n   6   =   ∅ . Consequently, there exist also robots  j   ∈ T m   ∩ T n   that previously constructed their sequences   s j   . 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 )   =   T m   that is necessary to construct their sequences   s i . Specifically, this robot   j   ∈   S ( k )   ∩   S ( k   −   1)   first notifies the robots in team   S ( k ) =   T m   that it is their turn to construct their communication schedules. 3   Second, robot   j   transmits to robots   i   ∈ T m   all sequences   s b   that were have been constructed so far by the robots in teams   S (1) , . . . , S ( k   −   1) . Among all those sequences   s b , robots   i   ∈ T m   use only the sequences of robots   b   ∈ N i   to construct their sequences   s i . 4   As a result, all robots   i   ∈ T m   that have not constructed   s i   yet, are aware of the indices   n T g  b   that point to entries in   s b   associated with some communication events   g . These indices satisfy   s b ( n T g  b   ) =   g ,  3 Note that if the teams in   S   were not necessarily neighboring teams, then robot   j   ∈   S ( k   −   1) =   T n   would have to know who the members of team  S ( k ) =   T m ,   m   / ∈ M j   , 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  T m ,   m   ∈ M j   .  4 Note that robot   j   is not aware of the sets   N i   and, therefore, it transmits all the sequences   s b   that have already been constructed to robots   i   ∈ T m .  b   ∈ N i . 5   Notice that this means that robots   i   ∈ T m   are also aware of the indices   n T m  b   . Using this information, every robot  i   ∈ T m   constructs the sequence   s i   based on the following two rules that determine the indices   n T g  i   that point to entries in   s i   where the communication event   g   will be placed, i.e.,  s i ( n T g  i   ) =   g , for all   g   ∈ M i . 1)   First rule:   Let   n T g  i   denote the index of the entry at which the communication event   g   ∈ M i   will be placed into  s i . If there exists a robot   b   ∈ N i   that has selected   n T g  b  so that   s b ( n T g  b   ) =   g , then   n T g  i   =   n T g  b   . In this way, all robots   b   ∈ T g   , including robot   i   ∈ T m   ∩ T g   will select the same index   n T g  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   ∈ N i   that have selected indices   n T g  b   , for communication event   g   ∈ M i , then the communication event   g   can be placed at any available entry   n T g  i   of   s i   that satisfies the following requirement. The entry   n T g  i   in all sequences   s j   of robots  j   ∈ N i   that have already been constructed should not contain communication events   h   such that   h   ∈ N T g   ; see line 6, Alg. 1. Note that the index   n T m  i   will always be determined by the first rule, since robot   j   ∈   S ( k )   ∩   S ( k   −   1)   has already constructed its sequence   s j   by placing the event   m   at an entry of   s j   with index   n T m  j   . To highlight the role of the second rule assume that   h   ∈ N T g   . Then, this means that there exists at least one robot   r   ∈ T h   ∩ T g   . Notice that without the second rule, at a subsequent iteration of this procedure, robot   r   ∈ T h   ∩T g   would have to place communication events for teams   T g   and   T h   at a common entry of   s r   , i.e.,   n T g  r   =   n T h  r   , due to the first rule and, therefore, a conflicting communication event in schedule  sched r   would occur. In all the remaining entries of   s i ,   X ’s are placed; see line 7, Alg. 1. By construction of   s i , there are  `   − |M i |   X ’s in   s i . Once all robots   i   in team   S ( k )   have constructed the se- quences   s i , 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   T 1   =   { 1 ,   2 } ,  T 2   =   { 2 ,   3 } , and   T 3   =   { 3 ,   1 } . Let the sequence   S   be  S   =   T 1 ,   T 2 ,   T 3 . Hence, initially the robots 1 and 2 in team   T 1  coordinate to construct their respective sequences   s i . Assume that initially robot   1   constructs the sequence   s 1   of length equal to   `   =   max   { d T m   } 3  m =1   + 1 = 3 . Robot   1   belongs to teams   T 1   and   T 2   and it arbitrarily constructs   s 1   as follows:  s 1   = 1 ,   3 , X . Then the sequence   s 1   is transmitted to robot   2  that belongs to teams   T 1   and   T 2 . Now robot   2   is responsible for constructing the sequence   s 2 . To construct   s 2 , according  5 Note that the discrete time instants at which the communication event  g   ∈ M i   will take place are   n T g  i   +   z` , where   z   ∈   N , by definition of  sched i .
Algorithm 1:   Distributed construction of sequence   s i ,   i   ∈ T m  Input:   Already constructed sequences   s b ,   ∀ b   ∈ N i .  Output:   Schedule of meeting events:   sched i   = [ s i ] ω  1   Construct an empty finite sequence   s i   of length   ` . ;  2   for   g   ∈ M i   do  3   if   there exist constructed sequences   s b ,   b   ∈ T g   then  4   s i ( n T g  i   ) :=   g , where   n T g  i   :=   n T g  b   ,   ∀ b   ∈ T g   ;  .   First   rule  5   else  6   Choose an available   n T g  i   ∈ { 1 , . . . , ` }   such that it holds either   s j   ( n T g  i   ) :=   X , or   s j   ( n T g  i   ) :=   h   with  h / ∈ N T g   ,   ∀ j   ∈ N i . Then set   s i ( n T g  i   ) :=   g . ;  .   Second   rule  7   Put   X   in the remaining entries; to the first rule, team   T 1   is placed at the first entry of   s 2 , i.e.,  n T 1  2   =   n T 1  1   = 1 . Next, the index   n T 2  2   is determined by the second rule. Specifically, notice that among the two available entries in   s 2   for team   T 3   the entry   n T 3  2   = 2   is invalid, since robot   1   ∈ T 1   has already constructed its sequence   s 1   so that  n T 3  1   = 2   and for teams   T 3   and   T 2   it holds that   3   ∈ N T 2   . Therefore, robot   2   selects   n T 2  2   = 2   and constructs the sequence  s 2   = 1 , X,   2 . At the next iteration of Algorithm 1 the robots 2 and 3 in team   T 2   coordinate to construct their sequences  s i . Robot   2   has already constructed the sequence   s 2   at the previous iteration and it transmits its constructed sequence   s 2  and the previously constructed sequence   s 1   to robot   3 . Thus robot   3   has now access to all already constructed sequences   s e , for   e   ∈ N 3   =   { 1 ,   2 } . Robot   3   constructs   s 3   =   X,   3 ,   2   using the first rule. Finally, the robots in the third team   T 3   =   { 3 ,   1 }   have already constructed their finite paths at previous iterations. In the following proposition we show that Algorithm 1 can always construct sequences   s i   if the length   `   of   s i   is selected as   `   =   max   { d T m   } M m =1   + 1 .  Proposition 4.4:   Algorithm   1   can   always   construct   se- quences   s i , for all   i   ∈ N   , if the length   `   of   s i   is selected as   `   =   max   { d T m   } M m =1   + 1 .  Proof:   The proof is based on contradiction. Assume that a robot   i   requires a sequence   s i   of length greater than   `   = max   { d T e   } M e =1   + 1   when Algorithm 1 is applied. This means that there is team   T m ,   m   ∈ M i , which cannot be placed at any of the first   `   entries of   s i . By construction of Algorithm 1, this means that the team   T m   has at least   `   neighbors in graph  G T   , i.e.,   d T m   ≥   ` , 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   G T   , it is possible that a team   T m   may appear more than once in   S , depending on the structure of the graph  G T   . In this case, robots   i   ∈   T m   construct the sequences  s i   only the first time that team   T m   appears in   S . Also, at the first iteration of Algorithm 1, robots of team   S (1)  have to construct their sequences   s i ,   i   ∈   S (1) . In this case, a randomly selected robot   j   ∈   S (1)   creates arbitrarily its sequence   s j   by placing the teams   m   ∈ M j   at the   n T m  j   -th entry of   s j   . Then the procedure described in Algorithm 1 follows.  Remark 4.6 (Discrete states   X ):   In the schedules   sched i , 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   T m ,   m   ∈ M , is the same for all robots   i   ∈ T m ; 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  sched i   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. I NTEGRATED   T ASK   P LANNING AND   I NTERMITTENT  C OMMUNICATION   C ONTROL  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  τ   n i  i   =   path 0  i   | path 1  i   |   . . .   | [ path n i  i   ] ω   ,   (6) where   n i   ∈   N   is the iteration index associated with robot  i ,   path n i  i   is a finite sequence of states in wTS i ,   |   denotes the concatenation of discrete paths   path n i  i   , and   ω   denotes the infinite repetition. Each path   path n i  i   is constructed so that (i) execution of   path n i  i   , for a every given   n i   ensures that robot   i   will communicate exactly once with all teams  T m ,   m   ∈ M i   in an order that respects the schedules   sched i  designed in Section IV, and (ii) execution of   τ   n i  i   guarantees that the assigned local LTL −©   tasks   φ i   are satisfied. In Section V-A, we discuss the distributed construction of the initial paths   path 0  i   given the communication schedules   sched i . In Section V-B, we present the distributed construction of all subsequent paths   path n i  i   that occurs online as the robots navigate the worskpace.  A. Construction of Initial Paths  Once robot   i   constructs its schedule   sched i , it locally designs the initial path   path 0  i   . To do this, feasible initial communication points for all teams   T m ,   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   comb b   denote any candidate combination of communication points that can be assigned to all teams   T m ,  m   ∈ M , where   b   ∈   { 1 , . . . ,   ∏  m ∈M   |C m | } . Given the com- munication points   v j   ,   j   ∈ C m , in the candidate combination  comb b , every robot constructs the NBA   B i   that corresponds to the following LTL formula  ψ i   =   φ i  ︸︷︷︸  task  ∧   φ com ,i  ︸ ︷︷ ︸  communication  ,   (7)
where  φ com ,i   =   ∧ m ∈M i   ( ♦ v j ∈C m   ) ,   (8) In words, the LTL formula   φ com ,i   requires robot   i   to visit in- finitely often the candidate communication points   v j   ,   j   ∈ C m , of all teams   T m ,   m   ∈ M i , that are specified in   comb b . Then, given the wTS i   and the NBA   B i , every robot can synthesize a motion plan    ̃ τ   0  i   | =   ψ i , if it exists, which will be used to construct the initial path   path 0  i   . This process is repeated for all   b   ∈   { 1 , . . . ,   ∏  m ∈M   |C m | }   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  comb b   reducing in this way the computational cost of finding a feasible plan    ̃ τ   0  i   . Specifically, given candidate initial communication points for all teams   T m ,   m   ∈   M i , the motion plan    ̃ τ   0  i   can be constructed by checking the non-emptiness of the language of the   Product B  ̈ uchi Automaton   (PBA)   P i   =   wTS i   ⊗   B i , defined as follows [33]:  Definition 5.1 (Product B  ̈ uchi Automaton):  Given   the   weighted   transition   system   wTS i   = ( Q i , q 0  i   ,   → i , w P i   ,   AP , L i  )   and   the   NBA   B i   = ( Q B i   ,   Q 0  B i   ,   2 AP   ,   → B i   ,   F B i  ) , the   Product B  ̈ uchi Automaton  P i   =   wTS i   ⊗ B i   is a tuple   ( Q P i   ,   Q 0  P i   ,   −→ P i   , w P i   ,   F P i  )   where (a)   Q P i   =   Q i   × Q B i   is the set of states; (b)   Q 0  P i   =   q 0  i   × Q 0  B i  is a set of initial states; (c)   −→ P i   ⊆   Q P i   × Q P i   is the transition   relation.   Transition   ( q P   , q ′  P   )   ∈→ P i   ,   where  q P   =   ( q v j  i   , q B   )   ∈   Q P i   and   q ′  P   =   ( q v e  i   , q ′  B   )   ∈   Q P i   , exists if   ( q v j  i   , q v e  i   )   ∈→ i   and   ( q B   , L i ( q v j  i   ) , q ′  B   )   ∈→ B   ; (d)  w P i   :   Q P i   × Q P i   →   R +   is the weight function, defined as:   w P i   (( q v j  i   , q B   ) ,   ( q v e  i   , q ′  B   ))   =   w i ( q v j  i   , q v e  i   ) ;   and   (e)  F P i   =   Q i   × F B i   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   P i , which can be viewed as a weighted graph   G P i   =   {V P i   ,   E P i   , w P i   } , where  V P i   =   Q P i   , the set of edges   E P i   is determined by the transition relation   −→ P i   , and the weight function   w P i   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   G P i   (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  P i   = ρ pre , 0  P i  [  ρ suf , 0  P i  ] ω  = ( q 0  wTS i   , q 0  B i   )  ︸   ︷︷   ︸  ∈Q 0  Pi  ( q 1  wTS i   , q 1  B i   )   . . .   ( q F  wTS i   , q F B i   )  ︸   ︷︷   ︸  = q F Pi   ∈F Pi  [ ( q F  wTS i   , q F B i   )   . . .   ( q L  wTS i   , q L B i   ) ] ω   ,   (9) where   with   slight   abuse   of   notation,   q β  wTS i   and   q β B i   de- note   a   state   of   wTS i   and   B i ,   respectively,   for   all   β   ∈ { 0 , . . . , F, . . . , L } . The projection of   ρ 0  P i   onto the state-space of wTS i , denoted by   Π | wTS i   ρ 0  P i   , results in the desired prefix- suffix motion plan   ̃ τ   0  i   = Π | wTS i   ρ 0  P i   =  ̃ τ   pre , 0  i  [   ̃ τ   suf , 0  i  ] ω  =   [ q 0  wTS i   . . . q F  wTS i  ] [ q F  wTS i   . . . q L  wTS i  ] ω   ,   (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   path n i  i   will get optimized online. Given the motion plans    ̃ τ   0  i   =  ̃ τ   pre , 0  i   [ ̃ τ   suf , 0  i   ] ω   , we design the discrete paths   path 0  i   as follows. First, we initialize   path 0  i  as   path 0  i   =    ̃ τ   pre , 0  i   |  ̃ τ   suf , 0  i   . Recall that all paths   path 0  i   are designed so that if executed, then robot   i   will communicate once with all teams   T m ,   m   ∈ M i , in an order that respects the schedules   sched i . Therefore, the state   q v j  i   corresponding to the candidate communication point   v j   ,   j   ∈ C m , appears at least once in the suffix part of    ̃ τ   0  i   , by definition of   ψ i , for   all   m   ∈   M i .   However,   these   communication   states may not appear in   path 0  i   =    ̃ τ   pre , 0  i   |  ̃ τ   suf , 0  i   in an order that respects the schedules   sched i , as this is not required by the LTL formula   ψ i   in (7). Therefore, we append at the end of  path 0  i   the suffix part    ̃ τ   suf , 0  i   enough times so that   path 0  i   =  ̃ τ   pre , 0  i   |  ̃ τ   suf , 0  i   |   . . .   |  ̃ τ   suf , 0  i   respects the schedule   sched i , i.e., there exists a sequence of indices   κ m i   that point to entries in   path 0  i  corresponding to states   q v j  i   with   v j   ,   j   ∈ C m , that satisfy  κ m i   < κ h i   , if the communication event for team   T m   appears before the communication event for team   T h   in   sched i , for all teams   T m ,   T h ,   m, h   ∈ M i ; see also Example 5.3. Note that since the state   q v j  i   ,   j   ∈ C m , appears at least once in the suffix part of    ̃ τ   0  i   , for all   m   ∈ M i , the suffix part    ̃ τ   suf , 0  i   will be appended to   path 0  i   at most   |M i | −   1   times. With slight abuse of notation, the initial path   τ   0  i   in (6) is defined using only   path 0  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   comb b   that is needed to determine initial plans    ̃ τ   0  i   , the robots can search locally in the set of   ∏  m ∈M   |C m |   possible combinations of communication points by solving at most   ∏  m ∈M i   |C m |   control synthesis problems each, instead of   ∏  m ∈M   |C m | . To see this, observe that, for any robot   i   ∈ N   , there exist multiple combinations  comb b   that share the same communication points for all teams   T m ,   m   ∈ M i , and only differ in the communication points for teams   T m ,   m   ∈ M \ M i . 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   ∏  m ∈M i   |C m |   control synthesis problems, then all combinations   comb b   will be exhaustively explored. By combining the feasible local combinations of communication points   comb i b i   that can be assigned to teams   T m ,   m   ∈ M i , where   b i   ∈ { 1 , ...,   ∏  m ∈M i   |C m |} , that are identified by all robots   i , it it easy to obtain feasible global combinations  comb b . Note that, in general, it holds that   ∏  m ∈M i   |C m | ≤ ∏  m ∈M   |C m | , where the equality holds if   M i   =   M   or if  |C m |   = 1 , for all   m   ∈ M \ M i . Moreover,   ∏  m ∈M i   |C m |   is smaller for sparse graphs   G T   , given a fixed number of teams and fixed sets   C m .  Lemma 5.2 (Complexity of initialization):   Let   comb i b i  with   b i   ∈   { 1 , . . . ,   ∏  m ∈M i   |C m | }   denote   a   combination of   communication   points   that   can   be   assigned   to teams   T m ,   m   ∈ M i . Moreover, assume that every robot   i   ∈ N
solves   ∏  m ∈M i   |C m |   control synthesis   problems using the LTL formula (7), one for every combination   comb i b i   . Then, the robots can collectively detect any feasible combination of communication points   comb b ,   b   ∈   { 1 , . . . ,   ∏  m ∈M   |C m | } , if it exists, that can be assigned to all teams   T m ,   m   ∈ M .  Proof:   In what follows, we show by contradiction that under this local construction of   comb b , the robots can detect all feasible combinations   comb b . Assume that there exists a feasible combination   comb b , that cannot be detected if all robots solve their respective   ∏  m ∈M i   |C m |   control synthesis problems. Also, let   Π | M i   comb b   denote the combination of communication points in   comb b   that correspond to all teams  T m ,   m   ∈ M i . Since   comb b   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   Π | M i   comb b  or did not consider the combination   Π | M i   comb b . The first case contradicts the assumption that   comb b   is a feasible combination of communication points that can be assigned to all teams   T m ,   m   ∈ M , while the second case contradicts the assumption that every robot   i   ∈   N   searches over all combinations   comb i b i   , completing the proof.  Example 5.3 (Construction of   path 0  i   ):   Consider   a   robot  i   with   M i   =   { 2 ,   3 ,   4 ,   5 }   and   communication   schedule  sched i   = [2 ,   3 , X,   4 ,   5] ω   . Consider also the motion plan    ̃ τ   0  i   =  ̃ τ   pre , 0  i   [ ̃ τ   suf , 0  i   ] ω   =   q v 1  i   q v 6  i   q v 4  i   q v 5  i   q v 2  i   q v 3  i   [ q v 3  i   q v 5  i   q v 4  i   q v 6  i   q v 2  i   ] ω   , where   v 2 ,   v 3 ,   v 4   are the candidate communication points for   teams   T 2 ,   T 3 ,   T 4 ,   respectively.   The   path   path 0  i   is initialized as   path 0  i   =  ̃ τ   pre , 0  i   |  ̃ τ   suf , 0  i   . To ensure the existence of   indices   κ m i   in   path 0  i   for   all   teams   T m ,   m   ∈   M i , that   respect   the   schedule   sched i ,   the   suffix   part   needs to   be   appended   to   path 0  i   once   more,   i.e.,   path 0  i   =  q v 1  i   q v 6  i   q v 4  i   q v 5  i   q v 2  i   q v 3  i   [ q v 3  i   q v 5  i   q v 4  i   q v 6  i   q v 2  i   ][ q v 3  i   q v 5  i   q v 4  i   q v 6  i   q v 2  i   ] , where the sequence of states in brackets stands for the suffix part   τ   suf , 0  i   . Observe that in   path 0  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   sched i .  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   v j   ,  j   ∈ C m , that (i) does not appear in the atomic propositions  π v e  i   that capture the tasks   φ i   assigned to robots   i   ∈ T m , and (ii) is directly connected to all locations   v e ,   e   ∈ I , that robots  i   ∈ T m   should visit to accomplish their tasks, i.e., the atomic propositions   π v e  i   appear in the tasks   φ i ,   i   ∈ T m . Then,   v j   ,  j   ∈ C m , is a feasible communication point for team   T m , since it does not violate the tasks   φ i   for all   i   ∈ T m   and it does not affect the communication points the other teams can select due to (i). Also, due to (ii) robots   i   ∈ T m   can visit   v j   directly from any location   v e   without passing through locations that may violate   φ i . Finally, if the negation operator does not appear in the tasks   φ i   of all robots   i   ∈ T m , then any communication point   v j   ,   j   ∈ C m , assigned to team   T m   is feasible.  Remark 5.5 (Formula   φ com ,i ):   An alternative selection for  φ com ,i , defined in (8), is   φ ′  com ,i   =    ( ♦ v j ∈C m   ∧   ( ♦ v e ∈C h   ∧  ( ♦ v d ∈C g   ∧   . . .   )))   that requires robot   i   to visit communication points for all teams   T m ,   m   ∈ M i   in an given order that respects the schedules   sched i . However, using this formula,  Algorithm 2:   Distributed construction of   path n i +1  i   ,   ∀ i   ∈ T m ,   ∀ n i   ∈   N .  Input:   Set   C m , wTS i ,   n i  Output:   Paths:   path n i +1  i   ,   ∀ i   ∈ T m  1   Initialize   c i   = 1 ;  2   while   c i   ≤ |M i |   do  3   if   team   T m   with   m   =   M i ( c i )   communicates   then  4   for   j   ∈ C m   do  5   Define   ψ i   by (7) given (i)   v j   for team   T m  and (ii) the selected communication points for other teams   T h ,   h   ∈ M i   \ { m } ;  6   Construct   P i   and synthesize a suffix loop  ρ suf ,j P i   (if it exists) around   q F P i   defined in (9) that minimizes   J (Π | wTS i   ρ suf ,j P i   ) ;  7   Compute    ̃ τ   suf ,j i   = Π | wTS i   ρ suf ,j P i   ;  8   Define   Cost j   =   ∑  r ∈T m   J ( ̃ τ   suf ,j r   ) , for all   j   ∈ C m ;  9   Compute   j ∗   = argmin j ∈C m   { Cost j   } j ∈C m   ;  10   Initialize paths   path n i +1 ,c i  i   =  ̃ τ   suf ,j ∗  i   , for all   i   ∈ T m ;  11   while   path n i +1 ,c i  i   does not respect   sched i   do  12   Update   path n i +1 ,c i  i   =   path n i +1 ,c i  i   |  ̃ τ   suf ,j ∗  i  13   Update   c i   =   c i   + 1 ;  14   Return path   path n i +1  i   =   path n i +1 , |M i |  i   ; there is still no guarantee that all communication points will appear   in   the   suffix   part    ̃ τ   suf , 0  i   in   an   order   that   respects  sched i , as this depends on the structure of the LTL formula  φ i   and the wTS i . 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   path n i  i   occurs online and in an iterative fashion, for all   n i   ∈   N + , as the robots navigate the workspace. Specifically,   path n i +1  i   is constructed and updated every time robot   i   participates at communication events, as it executes   path n i  i   . Hereafter, we denote by   path n i +1 ,c i  i  the path constructed when robot   i   participates at the   c i - th communication event in   path n i  i   . The iteration index   c i  is initialized as   c i   =   1   at the beginning of execution of  path n i  i   and   is   updated   as   c i   =   c i   + 1   when   the   path  path n i +1 ,c i  i   is constructed. Once robot   i   has participated in  |M i |   communication events, i.e.,   c i   =   |M i | , then the next path   path n i +1  i   =   path n i +1 , |M i |  i   has been constructed and will be executed after the execution of   path n i  i   . In what follows, we present the distributed construction of  path n i +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   M i   are ordered as per the respective schedules   sched i . This means that if the robots in team   T m ,   m   =   M i ( c i ) , communicate then the next communication event that robot  i   needs to participate during the execution of   path n i  i   is  M i ( c i   + 1) . Assume that the robots   i   ∈ T m ,   m   =   M i ( c i ) , communicate during the execution of the paths   path n i  i   . To
(a) Communication within   T 1   (b) Selection of new   v j   ,   j   ∈ C 1  Fig.   2.   Illustration   of   Algorithm   2   for   network   of   N   =   3   robots (colored dots) with schedules   sched 1   = [ X,   2] ω   ,   sched 2   = [1 ,   2] ω   , and  sched 3   = [1 , X ] ω   . All robots currently execute paths   path n i  i   constructed by Algorithm 2. Figure 2(a) illustrates the communication events within team  T 1 . The corresponding paths   path n i +1 ,c i  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   path n 3 +1 3   since   |M 3 |   = 1 . The gray square denotes the state   Π | wTS i   q F P i   .  design the paths   path n i +1 ,c i  i   , the robots   i   ∈ T m   need to select a new communication point   v j   ,   j   ∈ C m   and possibly update the waypoints   v j   ,   j   ∈ I   so that the LTL −©   tasks   φ i   are satisfied. The paths   path n i +1 ,c i  i   are constructed in a similar way as the paths   path 0  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   T m   given the already selected communication points for all other teams. Specifically, all robots   i   ∈ T m   perform in parallel the following two steps for all candidate new communication points   v j   ,   j   ∈ C m , for team  T m   [lines 2-4, Alg. 2]. First, every robot   i   ∈ T m   constructs the LTL formula   ψ i , defined in (7), for every candidate new communication point   v j   ,   j   ∈ C m   for team   T m , and given the already selected communication points for all other teams   T h ,  h   ∈ M i   \ { m } ; see (7) [line 5, Alg. 2]. Second, given the wTS i   and the NBA   B i   that corresponds to   ψ i , every robot  i   ∈ T m   constructs the corresponding PBA   P i   =   wTS i   ⊗   B i  and computes the   optimal   suffix loop, denoted by   ρ suf ,j P i   , around the same PBA final state   q F P i   = ( q F  wTS i   , q F B   )   that was used to construct the initial suffix loop of   ρ 0  P i   in (9). Note that by optimal suffix loop   ρ suf ,j P i   , we refer to the path that minimizes the cost   J (Π | wTS i   ρ suf ,j P i   ) . The projection of this optimal suffix loop   ρ suf ,j P i   on the state-space of wTS i   is denoted by    ̃ τ   suf ,j i  [lines 6-7, Alg. 2]. Once all robots   i   ∈ T m   have constructed the suffix parts   ̃ τ   suf ,j i   for all   j   ∈ C m , they compute the total cost   Cost j   = ∑  i ∈T m   J ( ̃ τ   suf ,j i   )   [line 8, Alg. 2]. This cost captures the dis- tance that all robots   i   ∈ T m   need to travel during a single execution of the suffix parts    ̃ τ   suf ,j i   if the new communication point for team   T m   is   v j   ,   j   ∈ C m . Among all the suffix parts   ̃ τ   suf ,j i   , all robots   i   ∈ T m   select the suffix part    ̃ τ   suf ,j ∗  i   , with  j ∗   = argmin j   { Cost j   } j ∈C m   [line 9, Alg. 2]. Given   the   optimal   suffix   part    ̃ τ   suf ,j ∗  i   ,   we   construct  path n i +1 ,c i  i   exactly as the initial paths   path 0  i   . Specifically, first, the paths   path n i +1 ,c i  i   are initialized as   path n i +1 ,c i  i   =  ̃ τ   suf ,j ∗  i   [line   10,   Alg.   2].   Then,   we   append    ̃ τ   suf ,j ∗  i   to  path n i +1 ,c i  i   as many times as needed to satisfy the schedules  sched i   [lines 11-12, Alg. 2]. Note that since the state   q v j  i   ,  j   ∈ C m   appears at least once in the suffix part of    ̃ τ   suf ,j ∗  i   , for all   m   ∈ M i , the suffix part    ̃ τ   suf ,j ∗  i   will be appended at most   |M i | −   1   times to   path n i +1 ,c i  i   . After the construction of   path n i +1 ,c i  i   , the iteration index   c i   is updated as   c i   =  c i   + 1   and points to the next path   path n i +1 ,c i  i   that will be constructed when robot   i   communicates with the robots in team   T h ,   h   =   M i ( c i )   [line 12, Alg. 2].   6   If   c i   =   |M i | , then this corresponds to the last communication event that robot   i   needs to participate during the execution of   path n i  i  and, therefore, the construction of   path n i +1  i   is finalized, i.e.,  path n i +1  i   =   path n i +1 , |M i |  i   [line 14, Alg. 2]. In this case,   c i  is re-initialized as   c i   = 1   [line 1, Alg. 2].  Remark 5.6 (Implicit synchronization across robots):  While   the   robots   transition   from   path n i  i   to   path n i +1  i  asynchronously, there is an implicit synchronization in the system since, for any iteration   n   ∈   N + , the robots that finish the execution of   path n i   , first cannot finish the execution of  path n +1  i   until all other robots   r   have finished the execution of their paths   path n r   . The reason is that (i) every robot  i   has to participate in   |M i |   communication events during the execution of   path n i   and (ii) the graph of teams   G T   is connected by construction of the teams. Therefore, if there exist robots   i   and   r   where robot   i   executes the path   path n +2  i  and robot   r   executes the path   path n r   it must be the case that robot   i   has skipped at least one communication event during the execution of   path n +1  i   , which cannot happen by construction of the proposed algorithm. Therefore, there exist time instants   t n   so that   path n i  i   =   path n i   , for every   n   ∈   N +  and for all   i   ∈ N   .  Remark 5.7 (Computational Cost):   Note that to design the path   path n i +1 ,c i  i   , every robot   i   needs to solve   |C m |   optimal control synthesis problems. Therefore, the computational cost of Algorithm 2 increases with   |C m | . To reduce the compu- tational burden, Algorithm 2 can be executed over subsets   ̄ C m   ⊆ C m   that can change with iterations   n i   but always include the current communication point for team   T m . The latter is required to ensure that paths   path n i  i   can be synthesized for all   n i   >   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   path n i  i  is eventually detected, for all   i   ∈ N   . This means that the computational cost is bounded.  Remark 5.8 (Fixed final state   q F P i   ):   Recall   that   the   fixed PBA final state   q F P i   , defined in (9), is used to construct the paths   path n i +1  i   , for all   n i   ∈   N   and for all   i   ∈ N   , This re- quirement can be relaxed by defining the paths   path n i +1 ,c i  i   as  path n i +1 ,c i  i   = Π wTS i   ρ c i   , where   ρ c i   =   ρ c i , 1 | ρ c i , 2 |   . . . ,   | ρ c i ,K  is a feasible path in the state-space of   P i ,   ρ c i ,k   a feasible path in the state-space of   P i   that connects two possibly different  6 Note that the next communication event   M i ( c i )   respects the schedules  sched i , by construction of   M i .
PBA final states, for all   k   ∈ { 1 , . . . , K } , and   K   <   |M i |  is determined so that execution of   path n i +1 ,c i  i   , for any   c i , ensures that robot   i   will communicate exactly once with all teams   T m ,   m   ∈ M i . 7   In this case   path n i +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   path n i +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   P i .  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   path n i  i   . To the contrary, here the discrete plans  path n i  i   are executed asynchronously across the robots, as per Algorithm 3. In Algorithm 3,   path n i  i   ( κ i )   stands for the   κ i -th state of the discrete path   path n i  i   . The different indices   κ i   for the robots’s states in the plans   path n i  i   allow us to model the situation where the robots pick asynchronously their next states in wTS i . Also, in Algorithm 3, the set   K n i  i   collects an index   κ m i  for all teams   T m ,   m   ∈ M i   that (i) satisfy   path n i  i   ( κ m i   ) =   q v j  i   , where   q v j  i   is   associated   with   a   communication   point   v j   ,  j   ∈ C m ,   m   ∈ M i   and (ii) respect the schedules as described in Section V-A. Note that such indices   κ m i   exist by construction of the paths   path n i  i   . According to Algorithm 3, when the state of robot   i   is   path n i  i   ( κ i ) =   q v j  i   ,   j   ∈ I   i.e., when robot   i  arrives at a location   v j   in the workspace, it checks if   κ i   ∈ K n i  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   v j   ,  j   ∈   C m ,   m   ∈   M i , selected by Algorithm 2 waits there indefinitely, or until all other robots in the team arrive. When all the other robots of team   T m   arrive at the com- munication location   v j   ,   j   ∈ C m , communication for team   T m  occurs and Algorithm 2 is executed to synthesize   path n i +1 ,c i  i  [lines 6-7, Alg. 3]. After that, robot   i   moves towards the next state   path n i  i   ( κ i   + 1)   [line 2, Alg. 3]. In line 2 of Alg. 3,  K n i  i   denotes the number of waypoints/states in   path n i  i   . This process is repeated until robot   i   visits all locations in   path n i  i   . Once robot   i   visit all waypoints of   path n i  i   , it starts executing the path   path n i +1  i   [line 8, Alg. 3]. If   n i   is the last iteration of Algorithm 2, then   path n i  i   is executed indefinitely. VI. A LGORITHM   A NALYSIS  In this section, we present results pertaining to completeness and optimality of the proposed distributed control framework.  7 Observe that if all paths   ρ c i ,k   are defined as the shortest loops around  q F P i   , then   ρ c i ,k   coincides with the   ρ suf ,j P i   , for all   k   ∈ { 1 , . . . , K } .  Algorithm 3:   Asynchronous execution of   path n i  i  Input:   Discrete path   path 0  i   and set   K 0  i  1   n i   = 0 ;  2   for   κ i   = 1 :   K n i  i   do  3   Move towards the state   path n i  i   ( κ i ) ;  4   if   κ i   ∈ K n i  i   then  5   Wait   at communication point   v j   ,   j   ∈ C m  [Definition 5.9];  6   if   all robots in   T m   are present at node   v j   then  7   Communication occurs within team   T m   and execution of Algorithm 2 ;  8   Execute the next path   path n i +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   τ   n i  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   n i   ≥   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   path n i  i   i.e., feasible loops   ρ n i  P i  defined over the state-space of the corresponding PBA   P i , can be designed, for all   n i   ∈   N . This implies that Algorithm 2 can generate plans   τ   n i  i   , for any   n i   ≥   0   and that robots   i   in any team   T m , for   m   ∈ M i , can stop executing Algorithm 2 at any iteration   n m i   ≥   0 .  Proposition 6.1 (Feasibility):   Assume   that   there   exists   a solution to Problem 1. Then, feasible plans   path n i  i   can be constructed for all   n i   ≥   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   T m ,   m   ∈ M , as shown in Lemma 5.2. Therefore, initial feasible paths   path 0  i   can be constructed. Then, to prove this result, it suffices to show that if there exists a feasible path   path n i  i   , then Algorithm 2 can construct a feasible path   path n i +1  i   for all   n i   ≥   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   path n i  i   then, Algorithm 2 will construct feasible paths   path n i +1 ,c i  i   for all   c i   ∈ { 1 , . . . ,   |M i |}   and, conse- quently, it will construct a feasible path   path n i +1 , |M i |  i   =  path n i +1  i   for all   n i   ≥   0 . To show this, we first define the sets   F n i +1  c i   that collect the suffix parts    ̃ τ   suf ,j i   constructed by
Algorithm 2 during the construction of   path n i +1 ,c i  i   , for all  c i   ∈ { 1 , . . . ,   |M i |} . Now, assume that there exists a feasible path   path n i  i   . This means that   F n i +1 0   :=   {  ̃ τ   suf ,j ∗   ,n i  i   } 6   =   ∅ , where    ̃ τ   suf ,j ∗   ,n i  i   is the suffix part used for the construction of the path   path n i  i   . First, we show that   F n i +1 1   6   =   ∅ , i.e., that Algorithm 2 will construct a feasible plan   path n i +1 , 1  i   . Note that the only difference between the paths   path n i +1 , 1  i   and  path n i  i   =   path n i , |M i |  i   , in terms of the selected commu- nication points for teams   T m ,   m   ∈ M i , lies in the selected communication point of exactly one team   T m ,   m   ∈ M i . Also, recall that Algorithm 2 searches over all communication points  j   ∈ C m , including the current communication point of   T m   that appears in   path n i  i   , to select the new communication point for team   T m . Therefore, there exists an optimal control synthesis problem that is solved by Algorithm 2 during the computation of   path n i +1 , 1  i   such that the LTL formula   ψ i   is defined over the   communication   points   selected   in   path n i , |M i |  i   .   Since this optimal control synthesis problem is feasible, by the assumption that   path n i  i   is a feasible path, the generated suffix part, which was also used to construct   path n i , |M i |  i   , belongs to  F n i +1 1   , i.e.,   F n i +1 1   6   =   ∅ . The inductive step follows. Assume that   F n i +1  c i   6   =   ∅ . Then, following the same logic as before we can show that the feasible suffix path used to construct  path n i +1 ,c i  i   belongs to   F n i +1  c i +1   , i.e.,   F n i +1  c i +1   6   =   ∅ . By induction we conclude that if   F n i +1 0   6   =   ∅ , i.e., if there exists a feasible path   path n i  i   , then   F n i +1  c i   6   =   ∅   for all   c i   ∈ { 1 , . . . ,   |M i |}   and all   n i   ≥   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   path n i  i   are executed according to Algorithm 3. Specifically, we assume that there is a   deadlock , if there are robots of any team   T m   that are waiting forever at a communication point, selected by Algorithm 2, for the arrival of all other robots of team   T m   due to the control policy in Definition 5.9.  Proposition 6.2 (Deadlock-free):   The mobile robot network is   deadlock-free   when   the   paths   τ   n i  i   in   (6)   are   executed according to Algorithm 3.  Proof:   Let   W v e   ⊂ T m   denote the set of robots that are waiting at communication point   v e ,   e   ∈   C m , selected by Algorithm 2, for the arrival of the other robots that belong to team   T m . Assume that the robots in   T m \W v e   never arrive at that node so that communication at node   v e   for team   T m  never occurs. This means that the robots in   T m \W v e   are waiting indefinitely at communication locations   v j   ∈   C n ,  j   6   =   e ,   n   6   =   m ,   n   ∈   N T m   , selected by Algorithm 2, to communicate with robots in team   T n . The fact that there are robots that remain indefinitely at node   v j   ∈ C n   means that a communication within team   T n   never occurs by construction of Algorithm 3. Following an argument similar to the above, we conclude that the robots in   T n \W v j   are waiting indefinitely at nodes   v k 6   = j   ∈ C f   to communicate with robots that belong to a team   T f   ,   f   ∈   N T n   . Therefore, if a communication event never occurs for team   T m , 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   sched i , constructed by Algorithm 1, as per Algorithm 3. Specifically, we introduce discrete time steps   z i  that are initialized as   z i   = 1   and are updated as   z i   =   z i   + 1  asynchronously across the robots as follows. If at the current discrete time step   z i   robot   i   participates in the communication event   sched i ( z i ) =   m , for some   z i   ∈   N +   and   m   ∈ M i , then robot   i   ∈ T m   waits until all the other robots in team  T m   are available to communicate. Once all robots in   T m   are available, the discrete time step   z i   is updated as   z i   =   z i   + 1 . If   sched i ( z i ) =   X , then robot   i   updates   z i   =   z i   + 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   T m   that missed a communication event at node   v e ,   e   ∈ C m , at a previous time instant, which cannot happen by construction of Algorithm 3. Consider that there is an arbitrary time instant   t 0   at which the network is at a stationary configuration and let the current communication event for all robots   i   ∈   T m   be   sched i ( n T m  i   ( t 0 ))   =   m  for   some   m   ∈   M i ,   where   the   indices   n T m  i   were   de- fined   in   Algorithm   1.   Define   also   the   set   N min ( t 0 )   =  {  n T m  i   ( t 0 ) | n T m  i   ( t 0 ) = min { n T g  e   ( t 0 )  } N e =1  , g   ∈ M e }   that col- lects the smallest indices   n T m  i   ( t 0 )   among all robots. Also let   n T g  e   ( t 0 )   be an index such that   n T g  e   ( t 0 )   ∈ N min ( t 0 ) . By assumption there are robots   e   ∈ T g   and   r   ∈ T z   ,   g   ∈ N T z   , such that   e   ∈ W v f   ( t 0 ) ,   v f   ∈ T g   and   r   ∈ W v d   ( t 0 ) ,   v d   ∈ T z   , and, therefore, the events that are taking place for these two robots according to their assigned schedules of meeting events are   sched e ( n T g  e   ( t 0 )) =   g   and   sched r   ( n T z  r   ( t 0 )) =   z . Since  n T g  e   ( t 0 )   ∈ N min ( t 0 )   we have that   n T g  e   ( t 0 )   ≥   n T z  r   ( t 0 ) , which along with the fact that   g   ∈ N T z   results in   n T g  e   ( t 0 )   > n T z  r   ( t 0 )  by construction of Algorithm 1. This leads to the following contradiction. The fact that   n T g  e   ( t 0 )   > n T z  r   ( t 0 )   means that there exists a time instant   t < t 0   at which the event that took place for robots   a   ∈ T g   ∩ T z   was   sched a ( n T g  r   ( t )) =   g   and at least one of these robots did not wait for the arrival of all other robots in team   T g   , since at the current time instant   t 0   there are still robots in team   T g   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   sched i   as per Algorithm 3 is deadlock-free. Recall now that the paths (6) respect the schedules   sched i   and that it is not possible that there exist robots in any team   T m   that wait for other robots in the same team at different communication points   v j   ,   j   ∈ C m . 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   τ   n i  i   in (6) as per Algorithm 3, satisfies the LTL −©   statements   φ i , i.e.,   τ   n i  i   | =   φ i , for any   n i   ≥   0   and all robots   i   ∈ N   .  Proof:   First observe that Algorithm 2 can design feasible paths   path n i  i   , for any   n i   ≥   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   τ   n i  i   are bounded by Proposition 6.2. Therefore, the infinite paths   τ   n i  i  will be executed without any deadlocks. This is necessary to satisfy   φ i , as LTL formulas are satisfied by infinite sequences of states in wTS i . To prove this result, first we need to show that all transitions in wTS i   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   ρ B i   of the NBA   B i   that corresponds to  φ i   over the words   σ n i  i   generated during the execution of   τ   n i  i  is accepting, i.e.,   8  Inf ( ρ B i   )   ∩ F B i   6   =   ∅ .   (12) First, we show that all transitions in wTS i   that are due to the plans in (6) respect the transition rule   → i . Notice that all transitions incurred by the finite path   path n i  i   respect the transition rule   → i , for all   n i   ∈   N , by construction; see Algorithm 2. Next, we show that the transition from the last state in   path n i  i   to the first state in   path n i +1  i   also respects the transition rule   → i , for all   n i   ∈   N . To show this, observe that the last state in   path n i  i   is the last state in the suffix part   ̃ τ   suf ,j ∗  i   used to construct   path n i  i   , for all   n i   ∈   N . Also, notice that the first state in   path n i +1  i   is the state   Π | wTS i   q F P i   , for all   n i   ∈   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  path n i  i   to the first state in   path n i +1  i   respects   → i , for all  n i   ∈   N . Consequently, the plans in (6) respect   → i . Next, we show that (12) holds for the plans   τ   n i  i   in (6), for all  n i   ≥   1 . The same logic also applies to the plans   τ   0  i   in (11). To show this result, recall that the paths   path n i  i   , for all   n i   ≥   1  are designed by (i) constructing a suffix path   ρ suf ,j ∗  P i   that lives in the state-space   Q P i   around the fixed PBA final state   q F P i  defined in (9), and initializing   path n i  i   = Π | wTS i   ρ suf ,j ∗  P i   , (ii) appending the path   Π | wTS i   ρ suf ,j ∗  P i   as many times as needed so that   path n i  i   respects the schedule   sched i . Thus,   path n i  i   can be written as the projection onto wTS i   of the finite path   p n i  i   =  ρ suf ,j ∗  P i   | ρ suf ,j ∗  P i   |   . . .   | ρ suf ,j ∗  P i   , which means that   p n i  i   visits the fixed PBA final state   q F P i   a finite number of times. Consequently, since the plans in (6) are defined as infinite sequences of paths  path n i  i   , we get that   q F P i   is visited infinitely often, i.e., (12) holds, completing the proof.  8 The   generated   word   σ n i  i   ,   called   also   trace   of   τ i   [35]   and   de- noted   by   trace ( τ i ) ,   is   defined   as   σ n i  i   =   trace ( τ   n i  i   )   :=  L i ( τ   n i  i   (1)) L i ( τ   n i  i   (2))   . . .   , where   L i   is the labeling function defined in Definition 3.1.  Theorem 6.5 (Intermittent Communication):   The asynchronous   execution   of   the   motion   plans   τ   n i  i   in   (6) as per Algorithm 3, satisfies the intermittent communication requirement   captured   by   the   global   LTL   statement   φ com , for all   n i   ≥   0 .  Proof:   By construction of the paths   path n i  i   every robot   i  will communicate once with all teams   T m ,   m   ∈ M i , during a single execution of the path   path n i  i   . Moreover, by Proposition 6.2, there are no deadlocks during the execution of the plans  τ   n i  i   . Consequently, all robots   i   communicate infinitely often with all teams   T m ,   m   ∈ M i   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   τ   n i  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   n i   ≥   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  t n   when all robots execute the path   path n i   . In the following proposition, we examine the optimality of the paths   path n i   in terms of the total cost   ∑  i ∈N   J ( path n i   ) , for any   n   ∈   N .  Proposition 6.7 (Optimality):   Algorithm   2   generates   dis- crete paths   path n +1  i   so that  ∑  i ∈N  J ( path n i   )   ≤   ∑  i ∈N  J ( path n +1  i   ) ,   (13) for all   n   ≥   0 .  Proof:   Consider the discrete paths   path n i   , for some fixed   n   ≥   0 . Recall that the robots may start executing the paths   path n 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  R n − 1 ( t )   the robots that execute the paths   path n − 1  i   at a time  t . Next, we collect in the set   R n  new ( t )   the robots that are new to executing the path   path n i   and have not participated in any communication event contained in   path n i   yet. Notice that the robots in   R n − 1 ( t )   and   R n  new ( t )   have not constructed yet any path   path n +1 ,c i  i   . Also, we collect in the set   R n  com ( t )   the robots of all teams   T m ,   m   ∈ M , that communicate at time   t   while executing the paths   path n i   . All other robots that at time   t  execute the path   path n i   but they do not participate in any communication event are collected in the set   R n  com ( t ) . Finally, the robots that have already finished the execution of the paths  path n i   at time   t   are collected in the set   R n +1 ( t ) . Observe that  N   =   R n − 1 ( t )   ∪ R n  new ( t )   ∪ R n  com ( t )   ∪ R n  com ( t )   ∪ R n +1 ( t ) ,   for all   t   ≥   0 , for some   n   ≥   0 . Also observe that if   R n +1 ( t )   6   =   ∅ , then   R n − 1 ( t ) =   ∅ , as discussed in Remark 5.6.
To prove the inequality (13), we need to define the following cost function:  cost ( t ) =   ∑  i ∈R n  new ( t ) ∪R n − 1 ( t )  J ( path n i   )+   (14)  ∑  i ∈R n  com   ( t )  J ( path n +1 ,c i ( t )  i   )+  ∑  i ∈R n  com   ( t )  J ( path n +1 ,c i ( t )  i   ) +   ∑  i ∈R n +1 ( t )  J ( path n +1  i   ) ,  where   path n +1 ,c i ( t )  i   denotes the path that has been con- structed by Algorithm 2 by the time instant   t . Also, note that the robots   i   ∈ R n − 1 ( t )   may not have completed the construction of the paths   path n i   yet. Therefore, in the first summation in (14), the paths   path n i   for   i   ∈ R n − 1 ( t ) , are the ones that these robots will create once they complete their construction. Moreover, we define the finite sequence of time instants { t n  0   , t n  1   , . . . , t n F   − 1 , t n F  } , where (i)   t n  0   <   · · ·   <   t n F   , (ii)   t n  0  is an arbitrarily selected time instant such that   R n  new ( t )   ∪ R n − 1 ( t )   =   N   , (ii) (iii)   t n F   is the time instant when all robots have completed construction of the paths   path n +1  i   , i.e.,   R n +1 ( t n F   ) =   N   , and (iv)   t n  1   <   · · ·   < t n F   − 1   are the time instants corresponding to communication events during the execution of any of the paths   path n i   . 9   To prove (13), we need to show that  cost ( t n k +1 )   ≤   cost ( t n k   ) ,   (15) for all   k   ∈ { 0 , . . . , F   } . Since the robots   i   ∈ R n  new ( t n k +1 )   ∪ R n − 1 ( t n k +1 )   have not constructed yet any path   path n i +1 ,c i  i   , these robots cannot af- fect the cost   cost ( t n k   ) . Also, notice that   path n +1 ,c i ( t n k +1 )  i   =  path n +1 ,c i ( t n k   )  i   ,   for   all   robots   i   ∈   R n  com ( t n k +1 ) ,   since these robots do not communicate and, therefore, they do not   execute   Algorithm   2   at   t n k +1 .   Thus,   the   robots   i   ∈ R n  com ( t n k +1 )   cannot   affect   the   cost   cost ( t n k   )   either.   The same   holds   for   the   robots   i   ∈   R n +1 ( t n k +1 ) .   There- fore,   for   all   robots   that   do   not   communicate   at   time  t n k +1   it holds that   ∑  i ∈N \R n  com   ( t n k +1 )   J ( path n +1 ,c i ( t n k +1 )  i   )   =  ∑  i ∈N \R n  com   ( t n k +1 )   J ( path n +1 ,c i ( t n k   )  i   ) . In fact, only the robots  i   ∈ R n  com ( t n k +1 )   that communicate at time   t n k +1   design new paths such that   path n +1 ,c i ( t n k +1 )  i   6   =   path n +1 ,c i ( t n k   )  i   . Since  R n  com ( t n k +1 )   contains all robots that communicate at   t n k +1   the expression   ∑  i ∈R n  com   ( t n k +1 )   J ( path n +1 ,c i ( t n k +1 )  i   )   can be rewrit-  9 Note that the time instant   t n  0   exists, since it corresponds to a time when the robots either execute paths   path n i − 1  i   or paths   path n i  i   without having participated in any communication events yet; see also Remark 5.6. Also, the sequence  {  t n  1   , . . . , t n F   − 1 , t n F  }  for any   n   ≥   0   exists because the network is deadlock-free, as shown in Proposition 6.2.  ten as follows 10  ∑  i ∈R n  com   ( t n k +1 )  J ( path n +1 ,c i ( t n k +1 )  i   ) =  ∑  m ∈A ( t n k +1 )  ∑  i ∈T m  J ( path n +1 ,c i ( t n 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  path n +1 ,c i ( t n k   )  i   is   a   feasible   path   returned   by   Algorithm 2   as   a   candidate   path   for   path n +1 ,c i ( t n k +1 )  i   ;   it   will become   path n +1 ,c i ( t n k +1 )  i   if   it   also   the   optimal   one. Therefore,   we   get   that   ∑  i ∈T m   J ( path n +1 ,c i ( t n k +1 )  i   )   ≤  ∑  i ∈T m   J ( path n +1 ,c i ( t n k   )  i   ) ,   for   all   m   ∈   A ( t n k +1 ) , which   implies   ∑  i ∈R n  com ( t n k +1 )   J ( path n +1 ,c i ( t n k +1 )  i   )   ≤  ∑  i ∈R n  com   ( t n k +1 )   J ( path n +1 ,c i ( t n 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  path P i   ,   path P   +1  i   , . . . ,   path C i   is   repeated   indefinitely for all   n i   ≥   C   and all   i   ∈ N   .  Proof:   To show this result, notice that the sets of commu- nication points   C m   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   path n 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   path C i  have already appeared in a previous path   path P   − 1  i   , for some  P   ≤   C   and for all   i   ∈ N   . Since the selected communication points in the paths   path P   − 1  i   and   path C i   are the same, we have that Algorithm 2 generates the same optimal suffix path   ̃ τ   suf ,j ∗  i   to synthesize both   path P   − 1  i   and   path C i   . Therefore, we get that   path P   − 1  i   =   path C i   . Consequently, the path  path C +1  i   will be the same as the path constructed at iteration  P   , i.e.,   path C +1  i   =   path P i   , since the optimal control synthe- sis problems that are solved to construct the path   path C +1  i  and   path P i   are the same, for all robots   i   ∈ N   . Similarly, we have that   path C +2  i   =   path P   +1  i   . By inspection of the repetitive pattern, we conclude that for any   n   ∈   N   it holds that   path C + n i   =   path C + n − ( b ( C + n ) / ( C − P   +1) c− 1)( C − P   +1)  i   , where   b·c   stands for the floor function. We conclude that  10 Note that it is possible that two teams   T m   and   T h   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   ∈ T m   ∩ T h   has a schedule has the form   sched i   = [ m, h, X ] ω   and   C m   ∩ C h   6   =   ∅ . 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  path n +1 ,c i ( t )  i   .
the sequence   path P i   ,   path P   +1  i   , . . . ,   path C i   is repeated in- definitely for all iterations   n i   ≥   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   J p ( τ i )   =   α   ∑  i ∈N   J ( τ   pre  i   ) + (1   −   α )   ∑  i ∈N   J ( τ   suf  i   ) . Instead they only ensure that the total cost   ∑  i ∈N   J ( path n i   )  decreases   with   every   iteration   n   until   n   =   P   ,   when ∑  i ∈N   J ( path P i   )   =   ∑  i ∈N   J ( path P   +1  i   )   =   · · ·   = ∑  i ∈N   J ( path C i   )   while   for   all   iterations   n i   ≥   C   the sequence of paths   path P i   ,   path P   +1  i   , . . . ,   path C i   is repeated indefinitely. Therefore, the best plans   τ   n i  i   (6) are obtained for any   n i   ≥   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   T m   are fixed and never change. Note that the total cost of the plans   τ   n i  i   can be further minimized if the robots in every team   T m   update not only the communication point   v j   ,   j   ∈ C m , but also the teams they belong to. Optimal design of the teams is part of our future work. VII. S IMULATION   S TUDIES  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:   T 1   =   { 1 ,   2 ,   9 } ,   T 2   =   { 3 ,   4 ,   5 } ,  T 3   =   { 3 ,   6 } ,   T 4   =   { 1 ,   3 } ,   T 5   =   { 2 ,   5 ,   6 ,   11 } ,   T 6   =   { 4 ,   12 } ,  T 7   =   { 5 ,   9 } ,   T 8   =   { 4 ,   9 ,   12 } ,   T 9   =   { 6 ,   7 ,   10 } ,   T 10   =  { 7 ,   8 ,   11 } ,   T 11   =   { 8 ,   10 ,   11 ,   12 } , and   T 12   =   { 7 ,   10 } . Notice that the construction of teams   T m   results in a connected graph  G T   with   max { d T m   } M m =1   = 7 , as discussed in Section III. Mobility of each robot in the workspace is captured by a wTS with   |Q i |   = 300   states that represent   W   = 300   locations of interest and weights   w i   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   ≤ |C m | ≤   6   communication points while  C m   ∩ C n   =   ∅ , 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   v e   to   v j   , with   ( q v e  i   , q v j  i   )   ∈→ i , is generated by a uniform distribution on   [1 ,   2] , at the moment when robot   i  arrives at location   v e . The LTL −©   tasks for robots   1 , and   3   are   φ 1   =   ♦ ( π v 20  1   ∨  π v 10  1   ∨   π v 11  1   )   ∧   ♦ ( π v 61  1   )   ∧   ♦ ( π v 91  1   ∨   π v 100  1   ∨   π v 5  1   ∨   π v 60  1   )   ∧   ( ¬ π v 44  1   )   ∧   ♦ ( π v 6  1   ∨   π v 7  1   ∨   π v 133  1   )   and   φ 3   =   ♦ ( ξ 1 3   ∨   ξ 2 3   )   ∧  [ ♦ ( ξ 3 3   )]   ∧   ♦ [ ξ 2 3   →    ( ¬ ξ 1 3   )]   ∧   ( ¬ ξ 3 3   U ξ 1 3   ) , respectively, where  ξ 1 3   =   π v 81  3   ∨   π v 91  3   ,   ξ 2 3   =   π v 120  3   ∨   π v 91  3   ∨   π v 31  3   , and   ξ 3 3   =   π v 91  3   ∨  π v 110  3   ∨ π v 15  3   ∨ π v 130  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   v 81   or   v 91 . The Boolean formulas   ξ 2 3  and   ξ 3 3   are interpreted similarly. Also, note that robot   1   is responsible for visiting a user located at   v 61   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 { d T m   } 12  m =1   + 1 = 8 .  sched 1   = [1 ,   4 , X, X ] ω   ,   sched 7   = [9 ,   12 ,   10 , X ] ω   ,  sched 2   = [1 ,   5 , X, X ] ω   ,   sched 8   = [ X, X,   10 ,   11] ω   ,  sched 3   = [2 ,   4 ,   3 , X ] ω   ,   sched 9   = [1 , X,   8 ,   7] ω   ,  sched 4   = [2 ,   6 ,   8 , X ] ω   ,   sched 10   = [ 9 ,   12 , X,   11] ω   ,  sched 5   = [2 ,   5 , X,   7] ω   ,   sched 11   = [ X,   5 ,   10 ,   11] ω   .  sched 6   = [9 ,   5 ,   3 , X ] ω   ,   sched 12   = [ X,   6 ,   8 ,   11] ω   .  Then,   given   the   above   schedules,   feasible   initial   paths  path 0  i   are constructed for all robots in   3   seconds approxi- mately using [22]. Specifically, given communication points for all teams   T m ,   m   ∈ M i , [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   path n i  i   with  P   =   C   = 5 . The size of the NBA   B i   that corresponds to   ψ i   in (7) satisfies   7   ≤ |Q B i   | ≤   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   ≤ |C m | ≤   6 , for all   m   ∈ C m , the average runtime of Algorithm 2 per iteration   c i   is between   4   ×   45 = 180  seconds and   6   ×   45 = 270   seconds. Note that this runtime depends only on the size of the sets   C m   and not on the size of the teams   T m . 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   path n i  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  G c . Specifically, we assume that initially all robots generate a random number   v i ( t 0 )   and when all robots   i   ∈ T m   meet at a communication point   j   ∈ C m   they perform the following con- sensus update   v i ( t ) =   1  |T m |  ∑  e ∈T m   v e ( t ) . Figure 3(a) shows that eventually all robots reach a consensus on the numbers  v i ( 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   v i ( t ) . Figure 3(b) illustrates the time instants when the robots   1 ,   2 ,   and   3   started executing the paths   path n 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   path 2 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   T 1   (Figure 4(a)) and   T 4   (Figure 4(b)) with respect to time.  started executing the paths   path n i   , for all   n   ∈ { 1 , . . . ,   14 } . Observe in Figure 3(b) that there exist time instants   t n   when all three robots are executing their respective paths   path n i  for a common   n , for all   n   ∈ { 1 , . . . ,   14 } , as discussed in Remark 5.6. The communication events over time for teams  T 1   and   T 5   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 ∑ N i =1   J ( path n 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   |Q PTS |   =  × ∀ i |Q i |   =   W   | N   |   = 300 12   = 5 . 3144   ×   10 29 . 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  |Q PBA |   =   |Q PTS | × |Q B   |   = 5 . 3144   ×   10 29   × |Q B   |   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   ∑ 12  i =1   J ( path n i   )   with respect to iterations  n . Note that there is also a slight decrease in   ∑ 12  i =1   J ( path n i   )   from   n   = 4  to   n   = 5 . After   n   = 5 , a repetitive pattern in   path n i   is detected giving rise to motion plans   τ i   in a prefix-suffix form.  VIII. C ONCLUSION  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. R EFERENCES [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.