# Decomposition-based Hierarchical Task Allocation and Planning for Multi-
Robots under Hierarchical Temporal Logic Specifications

Xusheng Luo1, Shaojun Xu2,†, Ruixuan Liu1 and Changliu Liu1 *This work was in
part supported by NSF under grant No. 2144489.1Xusheng Luo, Ruixuan Liu and
Changliu Liu are with Robotics Institute, Carnegie Mellon University,
Pittsburgh, PA 15213, USA (e-mail: {xushengl, ruixuanl,
cliu6}@andrew.cmu.edu)2Shaojun Xu with College of Control Science and
Engineering, Zhejiang University, Hangzhou, 310058, China (e-mail:
sjxu@zju.edu.cn).†Work done during internship at Carnegie Mellon University.

###### Abstract

Past research into robotic planning with temporal logic specifications,
notably Linear Temporal Logic (LTL), was largely based on a single formula for
individual or groups of robots. But with increasing task complexity, LTL
formulas unavoidably grow lengthy, complicating interpretation and
specification generation, and straining the computational capacities of the
planners. A recent development has been the hierarchical representation of LTL
[1] that contains multiple temporal logic specifications, providing a more
interpretable framework. However, the proposed planning algorithm assumes the
independence of robots within each specification, limiting their application
to multi-robot coordination with complex temporal constraints. In this work,
we formulated a decomposition-based hierarchical framework. At the high level,
each specification is first decomposed into a set of atomic sub-tasks. We
further infer the temporal relations among the sub-tasks of different
specifications to construct a task network. Subsequently, a Mixed Integer
Linear Program is used to assign sub-tasks to various robots. At the lower
level, domain-specific controllers are employed to execute sub-tasks. Our
approach was experimentally applied to domains of navigation and manipulation.
The simulation demonstrated that our approach can find better solutions using
less runtimes.

##  I Introduction

The field of temporal logic planning has seen rapid expansion in recent years,
which can manage a more diverse range of tasks beyond the typical point-to-
point navigation, encompassing temporal objectives as well. These tasks
involve sequencing or coverage [2], intermittent communication [3] and
manipulation [4] among others. Here, we focus on Linear Temporal Logic (LTL)
specifications [5]. In the most research that centered on multi-robot systems,
LTL tasks are either assigned locally to individual robots within a team [6,
7, 8, 9], or a global LTL specification is used to capture the collective
behavior of all robots. In the latter approach, tasks can either be explicitly
assigned to each robot, as in [10, 11, 12], or task allocation is considered
without specific assignments, as in [13, 14, 15, 16, 17, 18]. However, except
for [1], all LTL formulas, regardless of whether they are assigned locally or
globally, are in the “flat” structure, meaning a single LTL formula specifies
the behavior of an individual robot or a team of robots. They tend to become
cumbersome for complex tasks. Despite attempts to increase expressivity, such
as inner and outer logics [15, 19], they are task specific and still flat
formulas by syntactically putting all in single formulas.

Studies (e.g., [20]) suggest that humans prefer hierarchical task
specification, which improves interpretability of planning and execution,
making it easier to identify ongoing work and conveniently adjust infeasible
parts without affecting other components. In our prior work [1], we introduced
a hierarchical and interpretable structure for LTL specifications, consisting
of various levels of flat specifications that enhance computational
efficiency. A bottom-up planning approach was developed for simultaneous task
allocation and planning. While this method is efficient, it operates under the
assumption that tasks with temporal dependencies within a flat specification
is allocated to a single robot, hence robots can work independently, limiting
its application in scenarios that require cooperation among multiple robots.

In this work, we developed a decomposition-based hierarchical framework
capable of addressing multi-robot coordination under hierarchical temporal
logic specifications. Temporal logic specifications that do not explicitly
assign tasks to robots generally require decomposition to derive the necessary
task allocation, which can be accomplished in three approaches: The most
common method, used in works such as [14, 21, 22, 17, 23], involves
decomposing a global specification into multiple tasks, leveraging the
transition relations within the automaton, which represents an LTL formula
graphically. Our work is also in line with this approach as graph-based
methods are well-established. As demonstrated in [13, 15], the second approach
creates a Boolean Satisfaction or Integer Linear Programming (ILP) model,
which simultaneously addresses task allocation and implicit task decomposition
in a unified formulation. Another method, e.g., [24], directly interacts with
the syntax tree of LTL formulas, which segments the global specification into
smaller, more manageable sub-specifications.

The proposed framework, built upon work [17], starts at the top level by
breaking down each flat specification into smaller sub-tasks. These sub-tasks
are then organized into a task network, where we deduce the temporal
relationships between them. Subsequently, we use a Mixed Integer Linear
Programming (MILP) approach to assign these sub-tasks to various robots. At
the lower level, we implement domain-specific planning methods to carry out
these sub-tasks. To the best of knowledge, our work is the first one that can
tackle multi-robot collaboration under hierarchical LTL specifications. Our
contributions are as follows:

  1. 1.

We developed an efficient hierarchical planning algorithm that can handle
multi-robot coordination under hierarchical LTL specifications;

  2. 2.

The efficiency and the quality of solutions were demonstrated through
navigation and manipulation tasks.

It is worth noting that hierarchical framework lacks completeness in two
respects. Firstly, for the sake of completeness, [17] makes assumptions about
the single automaton’s structure, assumptions that might not hold across a set
of automatons when examining relationships between hierarchical
specifications. More importantly, without an adequate interface, the high-
level task plans might prove infeasible by the low-level controllers.

##  II Problem Formulation

###  II-A Linear Temporal Logic

Linear Temporal Logic (LTL) is composed of a set of atomic propositions
$\mathcal{AP}$, along with boolean operators such as conjunction ($\wedge$)
and negation ($\neg$), as well as temporal operators like next ($\bigcirc$)
and until ($\mathcal{U}$) [25]. LTL formulas follow the syntax outlined below:

$\displaystyle\phi:=\top~{}|~{}\pi~{}|~{}\phi_{1}\wedge\phi_{2}~{}|~{}\neg\phi~{}|~{}\bigcirc\phi~{}|~{}\phi_{1}~{}\mathcal{U}~{}\phi_{2},$
(1)

where $\top$ is an unconditionally true statement, and $\pi\in\mathcal{AP}$
refers to a boolean valued atomic proposition. Other temporal operators can be
derived from $\mathcal{U}$, such as $\Diamond\phi$ that implies $\phi$ will
ultimately be true at a future time.

An infinite word $w$ over the alphabet $2^{\mathcal{AP}}$, where
$\mathcal{AP}$ is the set of atomic propositions, can be denoted as
$w=\sigma_{0}\sigma_{1}\ldots\in(2^{\mathcal{AP}})^{\omega}$, with $\omega$
signifying infinite repetition, and $\sigma_{k}\in 2^{\mathcal{AP}}$ for
$\forall k\in\mathbb{N}$. The language $\texttt{Words}(\phi)$ is the
collection of words that meet the formula $\phi$. This means, $w$ belongs to
$\texttt{Words}(\phi)$ if and only if $w$ satisfies $\phi$.

We focus on a subset of LTL known as syntactically co-safe formulas, or sc-LTL
for short [26]. It has been established that any LTL formula encompassing only
the temporal operators $\Diamond$ and $\mathcal{U}$ and written in positive
normal form (where negation is exclusively before atomic propositions) is
classified under syntactically co-safe formulas [26]. Sc-LTL formulas can be
satisfied by finite sequences followed by any infinite repetitions. An LTL
formula $\phi$ can be translated into a Nondeterministic B$\ddot{\text{u}}$chi
Automaton (NBA) [25]:

######  Definition II.1 (NBA)

An NBA $B$ is a tuple
$B=\left({\mathcal{Q}},{\mathcal{Q}}_{0},\Sigma,\rightarrow_{B},\mathcal{Q}_{F}\right)$,
where ${\mathcal{Q}}$ is the set of states;
${\mathcal{Q}}_{0}\subseteq{\mathcal{Q}}$ is a set of initial states;
$\Sigma=2^{\mathcal{AP}}$ is an alphabet;
$\rightarrow_{B}\subseteq{\mathcal{Q}}\times\Sigma\times{\mathcal{Q}}$ is the
transition relation; and ${\mathcal{Q}}_{F}\subseteq{\mathcal{Q}}$ is a set of
accepting states.

###  II-B Hierarchical Linear Temporal Logic

######  Definition II.2 (Hierarchical LTL [1])

A hierarchical LTL specification, denoted by $\Phi=\\{\phi({k},{i})\mid
k=1,\ldots,K,i=1,\ldots,|\Phi^{k}|\\}$ where $\phi({k},{i})$ is the $i$-th sc-
LTL specification at level $k$, $\Phi^{k}$ denotes the set of specifications
at level $k$, and $|\cdot|$ denotes the cardinality, includes $K$ levels such
that each specification at level $k$, for $k=1,\ldots,K-1$, is constructed
from specifications at the immediate lower level $k+1$.

We refer to each specification $\phi({k},{i})$ in $\Phi$ as the “flat”
specification. These flat specifications can be organized in a tree-like
specification hierarchy graph, where each node represent a flat sc-LTL
specification. Edges between nodes indicate that one specification encompasses
another as a composite proposition. This composite proposition is, in essence,
another flat sc-LTL formula. Leaf nodes represent leaf specifications at the
$K$-th level that consist only of atomic propositions, while non-leaf nodes
represent non-leaf specifications made up of composite propositions.

######  Example 1 (Multi-Robot Pickup and Delivery (MRPD))

Consider a MRPD problem in a warehouse setting. Here, mobile robots, waiting
at the dock, are assigned to pick up various items from storage shelves and
deliver them to a packing zone. The warehouse is segmented into six areas:
grocery, health, outdoor, pet supplies, furniture, and electronics; see Fig.
1. We consider three types of robots. There are two robots for each of these
types. The specific requirements for task 1 are as follows: 1) Initially, a
robot of type 1 proceeds to the furniture section and waits until the arrival
of a type 3 robot to assist with the loading of a large piece of furniture;
following this, it gathers items from the outdoor and pet sections in no
particular sequence. 2) A type 2 robot should initiate its task by gathering
items from the health section, and only afterward does it move to the grocery
section, ensuring it doesn’t visit the grocery section before visiting the
health section. 3) A type 3 robot moves to the furniture section to assist the
type 1 robot. 4) After the items are delivered to the packing area, all robots
eventually return to the dock. Temporal constraints may arise from item
attributes like weight, fragility, and category. This example extends the
classical MRPD in several aspects: (i) Tasks are defined within temporal logic
specifications, not as predefined point-to-point navigation. (ii) Logical and
temporal constraints between tasks, not considered in typical MRPD, are
included. (iii) A single robot may handle multiple tasks, contrasting with
most MRPD works where each robot performs one task, except for [27, 28]. (iv)
Cooperative behaviors among robots are introduced but not typically included
in MRPD.

Figure 1: Topological map of the supermarket. Various types of robots are
represented in distinct colors.

Let symbols $\pi_{s}^{t}$ represent atomic propositions indicating the need
for a robot of type $t$ to collect items from section $s$. Propositions with
the same second superscript, like $\pi_{s}^{t,j}$ and
$\pi_{s^{\prime}}^{t,j}$, must be executed by the same robot of type $t$. For
instance, $\pi_{\text{furn}}^{1,1},\pi_{\text{outd}}^{1,1}$ and
$\pi_{\text{pet}}^{1,1}$ should be completed by the same robot of type 1. The
hierarchical specification $\Phi$ is:

$\displaystyle L_{1}:\quad$
$\displaystyle\phi({1},{1})=\Diamond\phi({2},{1})\wedge\Diamond\phi({2},{2})$
$\displaystyle L_{2}:\quad$
$\displaystyle\phi({2},{1})=\Diamond\left(\phi({3},{1})\wedge\Diamond\phi({3},{2})\wedge\Diamond(\phi({3},{3})\wedge\Diamond\phi({3},{4}))\right)$
$\displaystyle\phi({2},{2})=\Diamond(\phi({3},{5})\wedge\Diamond\phi({3},{6}))$
$\displaystyle L_{3}:\quad$
$\displaystyle\phi({3},{1})=\Diamond(\pi_{\text{furn}}^{1,1}\wedge\bigcirc(\pi_{\text{furn}}^{1,1}\;\mathcal{U}\;\pi_{\text{furn}}^{3,3}))$
$\displaystyle\phi({3},{2})=\Diamond(\pi_{\text{pack}}^{3,3}\wedge\Diamond\pi_{\text{dock}}^{3,3})$
(2)
$\displaystyle\phi({3},{3})=\Diamond\pi_{\text{outd}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}$
$\displaystyle\phi({3},{4})=\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$
$\displaystyle\phi({3},{5})=\Diamond\pi_{\text{heal}}^{2,2}\wedge\Diamond\pi_{\text{groc}}^{2,2}\wedge\neg\pi_{\text{groc}}^{2,2}\;\mathcal{U}\;\pi_{\text{heal}}^{2,2}$
$\displaystyle\phi({3},{6})=\Diamond(\pi_{\text{pack}}^{2,2}\wedge\Diamond\pi_{\text{dock}}^{2,2}).$

The specification hierarchy graph is shown in Fig. 2. When $\phi({k},{i})$
appears at the right side of a formula, it is referred to as a composite
proposition, while at the left side, it’s a specification. For instance, in
the formula
$\phi({2},{2})=\Diamond(\phi({3},{5})\wedge\Diamond\phi({3},{6}))$,
$\phi({2},{2})$ is a specification, and $\phi({3},{5})$ and $\phi({3},{6})$
are composite propositions. A flat LTL specification of this task can be seen
in Eq. (B-1) in Appendix B. Note that the flat and hierarchical versions of
this task are not strictly equivalent in terms of the set of accepted words.
In the flat form, depicting precedence often necessitates using the sub-
formula $\neg\pi_{a}\,\mathcal{U}\,\pi_{b}$ frequently, especially due to the
multitude of atomic propositions and the mix of independent and dependent
relations. However, in hierarchical LTL, specifications are typically short,
allowing for a simpler expression of precedence using $\Diamond$, which is
less rigid than $\mathcal{U}$. Nevertheless, either form adheres to task
descriptions in natural language, as these descriptions usually don’t express
a preference for a specific type of precedence relation. $\square$

Figure 2: Specification hierarchy graph for Example 1.

###  II-C Problem Formulation

###### Problem 1

Consider an environment $\mathcal{E}$ populated by a set of heterogeneous
robots $\mathcal{R}=\\{r_{1},...,r_{n}\\}$ of different capabilities, and a
task represented by a hierarchical LTL specification $\Phi$ for either
navigation or manipulation. The goal is to generate a plan $\mathcal{P}$ that
allocates tasks to robots and schedules actions in a way that fulfills
specification $\Phi$, provided that such a plan is feasible.

###### Remark II.3

This work primarily addresses the high-level task allocation under
hierarchical specifications. We assume that robot dynamics and their
interactions with the environment are handled by domain-specific low-level
controllers.

##  III Decomposition-based Hierarchical Planning

Our approach builds upon work [17], which decomposes the NBA of a given LTL
specification into sub-tasks (which will be defined in Definition III.1) and
infers their temporal relationships. Next, we deduce the temporal relations
between atomic sub-tasks across all leaf specifications.

We start by presenting the necessary definitions and notations related to NBA.
It is worth noting that the NBA, as defined in Definition II.1, can be
perceived as a graph. For the sake of simplicity, we will refer to the NBA as
the graph ${\mathcal{A}}_{\phi}$. When discussing ${\mathcal{A}}_{\phi}$’s
edges, we don’t consider self-loops as they can be represented by vertices
themselves. The propositional formula $\gamma$ associated with a transition
$v_{1}\xrightarrow{\gamma}v_{2}$ in the NBA ${\mathcal{A}}_{\phi}$ is called a
vertex label if $v_{1}=v_{2}$, and an edge label if not. We denote the
mappings of a vertex and an edge to their respective labels using the
functions $\gamma:{\mathcal{V}}\to\Sigma$ and
$\gamma:{\mathcal{V}}\times{\mathcal{V}}\to\Sigma$, respectively. We then
define an edge-induced sub-task as a series of actions that robots must
perform to trigger a transition in the NBA. To greatly decrease the number of
edge-induced sub-tasks in the NBA, we remove any edge where the label requires
that more than one proposition be true simultaneously, if such a condition is
not required by the corresponding specification.

######  Definition III.1 (Edge-induced sub-task [17])

Given an edge $(v_{1},v_{2})$ in ${\mathcal{A}}_{\phi}$, an edge-induced sub-
task is defined by the edge label $\gamma(v_{1},v_{2})$ and the starting
vertex label $\gamma(v_{1})$.

######  Definition III.2 (Atomic and composite sub-task)

In the NBA ${\mathcal{A}}_{\phi}$, a sub-task $(v_{1},v_{2})$ is classified as
an atomic sub-task if the edge label $\gamma(v_{1},v_{2})$ consists solely of
atomic propositions. Otherwise, it is a composite sub-task if the edge label
consists solely of composite propositions.

Figure 5: (a) The NBA of specification $\phi({1},{1})$ in Eq. (1). The sub-
task $(v_{\text{init}},v_{1})$ implies that the composite proposition
$\phi({2},{1})$ must eventually be true, as indicated by its edge label. The
sub-tasks $(v_{\text{init}},v_{1})$ and $(v_{2},v_{\text{acc}})$ are
equivalent because $\gamma(v_{\text{init}})=\gamma(v_{2})$ and
$\gamma(v_{\text{init}},v_{1})=\gamma(v_{2},v_{\text{acc}})$. Similarly, the
sub-tasks $(v_{\text{init}},v_{2})$ and $(v_{1},v_{\text{acc}})$ are
equivalent. (b) The two sub-tasks $(v_{\text{init}},v_{1})$ and
$(v_{\text{init}},v_{2})$. (c) Concise representation of sub-tasks. The two
sub-tasks are temporally independent, thus no edges exist between them.

Two sub-tasks are equivalent if they have identical starting vertex labels and
edge labels. Note that because each specification consists solely of atomic
propositions (for leaf specifications) or composite propositions (for non-leaf
specifications), all of its sub-tasks should be of the same type.

###### Example 1

continued (Sub-tasks) The NBA of specification $\phi({1},{1})$ and sub-tasks
are shown in Figs. LABEL:fig:par_a and LABEL:fig:par_b.

###  III-A Generate Temporal Relations across Atomic Sub-tasks

The work [17] focuses on a flat LTL specification, extracting edge-induced
sub-tasks from its NBA, and identifying the temporal relationships among these
sub-tasks, i.e., a sub-task must be completed before, after or independently
of another one; an example with specification $\phi({1},{1})$ of task 1 is
illustrated in Fig. LABEL:fig:par_c. The goal here is to create a task network
represented as a Directed Acyclic Graph (DAG). In this DAG, each node
represents an atomic sub-task from a specific leaf specification, and edges
indicate precedence relationships between atomic sub-tasks, as determined by
corresponding non-leaf specifications.

Let $\Phi^{k}$ denote the set of specifications at the $k$-th level, with
$|\Phi^{k}|$ indicating its size. In what follows, we denote the edge-induced
sub-task as $e=(v_{1},v_{2})$ and use $\llbracket\phi\rrbracket$,
$\llbracket\phi\rrbracket_{a}$, and $\llbracket\phi\rrbracket_{c}$ to
represent the sets of all sub-tasks, atomic sub-tasks, and composite sub-tasks
for a given specification $\phi\in\Phi$, respectively. As defined in Def.
III.2, $\llbracket\phi\rrbracket$ equates either to
$\llbracket\phi\rrbracket_{a}$ or $\llbracket\phi\rrbracket_{c}$. For any two
different sub-tasks $e,e^{\prime}\in\llbracket\phi\rrbracket$, we use
$e\bowtie e^{\prime}$ to denote that sub-task $e$ must be completed before
($\prec$), after ($\succ$), or independently ($\|$) of $e^{\prime}$. The
following assumption restricts the relationships between sub-tasks from two
composite propositions.

######  Assumption III.3 (Temporal relation inheritance)

Sub-tasks follow the temporal relations of corresponding specifications. That
is, if $\phi\bowtie\phi^{\prime}$, then $e\bowtie e^{\prime},\forall
e\in\llbracket\phi\rrbracket_{,}\forall
e^{\prime}\in\llbracket\phi^{\prime}\rrbracket$.

Input: Hierarchical LTL specifications $\\{\phi({k},{i})\\}_{k=1}^{K}$

Output: DAG ${\mathcal{G}}$ of atomic sub-tasks

1 ${\mathcal{V}}=\varnothing,{\mathcal{E}}=\varnothing$;

;

$\triangleright$ Same leaf specifications

2 for  _$i\in\\{1,\ldots,|\Phi^{K}|\\}$_ do

3 for  _$e,e^{\prime}\in\llbracket\phi({K},{i})\rrbracket_{a}$_ do

4 if $e\prec e^{\prime}$ then
${\mathcal{E}}={\mathcal{E}}\cup\\{(e,e^{\prime})\\}$;

5 if $e\succ e^{\prime}$ then
${\mathcal{E}}={\mathcal{E}}\cup\\{(e^{\prime},e)\\}$ ;

6 ${\mathcal{V}}={\mathcal{V}}\cup\\{e,e^{\prime}\\}$;

7

;

$\triangleright$ Different leaf specifications

8 for  _$i,i^{\prime}\in\\{1,\ldots,|\Phi^{K}|\\}$_ do

9 if $i==i^{\prime}$ then continue;

10 Get the minimal common predecessor $\mu_{cp}(i,i^{\prime})$;

11 Find sub-tasks $e_{\phi}$ and $e_{\phi^{\prime}}$ in
$\mu_{cp}(i,i^{\prime})$ whose edge labels include $\phi(K,i)$ and
$\phi(K,i^{\prime})$, resp.;

12 for  _$e\in\llbracket\phi({K},{i})\rrbracket_{a}$_ do

13 for  _$e^{\prime}\in\llbracket\phi({K},{i^{\prime}})\rrbracket_{a}$_ do

14 if $e_{\phi}\prec e_{\phi^{\prime}}$ then
${\mathcal{E}}={\mathcal{E}}\cup\\{(e,e^{\prime})\\}$;

15 if $e_{\phi}\succ e_{\phi^{\prime}}$ then
${\mathcal{E}}={\mathcal{E}}\cup\\{(e^{\prime},e)\\}$ ;

16

17return ${\mathcal{G}}=({\mathcal{V}},{\mathcal{E}})$;

Algorithm 1 Construct DAG ${\mathcal{G}}=({\mathcal{V}},{\mathcal{E}})$

The process for creating the DAG ${\mathcal{G}}=({\mathcal{V}},{\mathcal{E}})$
is detailed in Alg. 1, which consists of two parts, based on whether the
atomic sub-tasks belong to the same leaf specification.

####  III-A1 Same leaf specification ${\phi({K},{i})}$

The algorithm iterates through each leaf specification $\phi({K},{i})$. For
any pair of atomic sub-tasks within $\llbracket\phi({K},{i})\rrbracket_{a}$,
an edge is added to the graph ${\mathcal{G}}$ if they have a precedence
relation [lines 1-1]. The method for extracting temporal relations between
sub-tasks is based on the approach described in Section IV.C of [17].

####  III-A2 Different leaf specifications ${\phi({K},{i})}$ and
${\phi({K},{i^{\prime}})}$

For a given specification $\phi({K},{i})$, its predecessor is defined as the
composite proposition that encompasses it at the higher level. The sequence of
predecessors leading up to the root specification, denoted as
${\mathcal{S}}(\phi({K},{i}))$, is established by tracing back to the first
level in the specification hierarchy graph. Note that the sequence of
predecessors also includes the specification itself. When examining two
sequences ${\mathcal{S}}(\phi({K},{i}))$ and
${\mathcal{S}}(\phi({K},{i^{\prime}}))$, let the set
$\Phi_{\wedge}(i,i^{\prime})=\left\\{\phi\,|\,\phi\in{\mathcal{S}}(\phi({K},{i})),\phi\in{\mathcal{S}}(\phi({K},{i^{\prime}}))\right\\}$
collect predecessors that appear in both sequences. A predecessor is defined
as the minimal common predecessor, denoted by $\mu_{cp}(i,i^{\prime})$, if it
is the closest to leaf specifications, that is,
$\mu_{cp}(i,i^{\prime})=\operatornamewithlimits{argmin}_{\phi\in\Phi_{\wedge}(i,i^{\prime})}\texttt{dist}(\phi-\phi({K},{i}))$,
where dist returns the distance between two specifications in terms of the
number of levels [line 1]. The temporal relations between the sets
$\llbracket\phi({K},{i})\rrbracket_{a}$ and
$\llbracket\phi({K},{i^{\prime}})\rrbracket_{a}$ are determined within this
minimal common predecessor. It may happen that $\phi({K},{i})$ or
$\phi({K},{i^{\prime}})$ is not directly included in $\mu_{cp}(i,i^{\prime})$
due to multiple levels separating them. In such cases, we identify the
composite propositions within $\mu_{cp}(i,i^{\prime})$, labelled as $\phi$ and
$\phi^{\prime}$, which act as predecessors to $\phi({K},{i})$ and
$\phi({K},{i^{\prime}})$, respectively [line 1]. Subsequently, we identify a
composite sub-task $e_{\phi}$ within
$\llbracket\mu_{cp}(i,i^{\prime})\rrbracket_{c}$ that contains $\phi$ in its
edge label, without being preceded by the negation operator $\neg$. This sub-
task necessitates fulfilling the composite proposition $\phi$, which in turn
requires satisfying $\phi({K},{i})$. Similarly, we find another composite sub-
task $e_{\phi^{\prime}}$ corresponding to $\phi({K},{i^{\prime}})$ in
$\llbracket\mu_{cp}(i,i^{\prime})\rrbracket_{c}$. The temporal relationship
between $\phi({K},{i})$ and $\phi({K},{i^{\prime}})$ mirrors that between
their associated sub-tasks $e_{\phi}$ and $e_{\phi^{\prime}}$ within
$\mu_{cp}(i,i^{\prime})$. As per Assumption III.3, this relationship extends
to the atomic sub-tasks in $\llbracket\phi({k},{i})\rrbracket_{a}$ and
$\llbracket\phi({k^{\prime}},{i^{\prime}})\rrbracket_{a}$; see lines 1-1.

Figure 6: Task network of task 1. Each sub-task is represented by a node along
with its self-loop. The symbol within each node corresponds to the edge label
of the sub-task. The label $\top$ associated with self-loops is omitted. Nodes
with sub-tasks belonging to the same leaf specification are grouped within a
shaded block, with the leaf specification being marked nearby. Sub-tasks
associated with $\phi({2},{1})$ and $\phi({2},{2})$ are encased in blue boxes,
while those pertaining to the root specification $\phi({1},{1})$ are enclosed
in the red box.

###### Example 1

continued (Temporal relations) The task network of task 1 is shown in Fig. 6.
In terms of the specifications $\phi({3},{1})$ and $\phi({3},{5})$, sequences
of predecessors are
${\mathcal{S}}(\phi({3},{1}))=\\{\phi({3},{1}),\phi({2},{1}),\phi({1},{1})\\},{\mathcal{S}}(\phi({3},{5}))=\\{\phi({3},{5}),\phi({2},{2}),\phi({1},{1})\\}$,
minimal common predecessor is $\mu_{cp}(1,5)=\phi({1},{1})$. Note that
$\phi({3},{1})$ and $\phi({3},{5})$ do not fall within $\mu_{cp}(1,5)$ because
they are separated by two levels. Predecessors in $\mu_{cp}(1,5)$ are
$\phi=\phi({2},{1})$ and $\phi^{\prime}=\phi({2},{2})$, respectively; see Fig.
2. Related composite sub-tasks in $\llbracket\mu_{cp}(1,5)\rrbracket_{c}$ are
$e_{\phi}=(v_{\text{init}},v_{1})$ and
$e_{\phi^{\prime}}=(v_{\text{init}},v_{2})$, respectively. Since they are
temporally independent, we have $\phi({2},{1})\,\|\,\phi({2},{2})$. By
denoting atomic sub-tasks using their respective edge labels, the temporal
relationships between atomic sub-tasks from the two specifications
$\phi({3},{1})$ and $\phi({3},{5})$ are
$\pi_{\text{furn}}^{1,1}\,\|\,\pi_{\text{heal}}^{2,2},\pi_{\text{furn}}^{1,1}\,\|\,\pi_{\text{groc}}^{2,2},\pi_{\text{furn}}^{3,3}\,\|\,\pi_{\text{heal}}^{2,2},\pi_{\text{furn}}^{3,3}\,\|\,\pi_{\text{groc}}^{2,2}$;
see the blocks associated with $\phi({3},{1})$ and $\phi({3},{5})$ in Fig. 6.

###  III-B Formulate MILP to Allocate Sub-tasks

Using the task network ${\mathcal{G}}$, we adapt the MILP formulation from
[17] to assign atomic sub-tasks to robots, which was inspired by the Vehicle
Routing Problem (VRP) with temporal constraints [29]. The difference is that,
for the case of a single specification, all sub-tasks must be completed.
However, in this work, sub-tasks originate from various leaf specifications
and not all are mandatory. For example, in a case where two leaf
specifications are linked by an OR operator in a non-leaf specification (e.g.,
$\phi({1},{1})=\phi({2},{1})\vee\phi({2},{2})$), it is possible for one leaf
specification, like $\phi({2},{1})$, to be false, so all its sub-tasks should
not be fulfilled. The MILP modifications are tailored to accommodate
specification-level constraints, involving two categories of constraints:
logical constraints and temporal constraints. The solution provides a time-
stamped sequential plan including the starting time (when the vertex label is
activated) and the completion time (when the edge label becomes true) of sub-
tasks within ${\mathcal{G}}$.

For any specification $\phi\in\Phi$, considering a sub-task
$(v_{1},v_{2})\in\llbracket\phi\rrbracket$, let $\gamma$ be the propositional
formula associated with its edge or vertex label, i.e.,
$v_{1}\xrightarrow{\gamma}v_{2}$ or $v_{1}\xrightarrow{\gamma}v_{1}$. Assume
this formula is in disjunctive normal form (DNF), i.e.,
$\gamma=\bigvee_{p\in{\mathcal{P}}}\bigwedge_{q\in{\mathcal{Q}}_{p}}(\neg)\pi$
or
$\gamma=\bigvee_{p\in{\mathcal{P}}}\bigwedge_{q\in{\mathcal{Q}}_{p}}(\neg)\phi^{\prime}$,
where the negation operator only precedes the atomic propositions $\pi$ or
composite propositions $\phi^{\prime}$, and ${\mathcal{P}}$ and
${\mathcal{Q}}_{p}$ are suitable index sets. Every propositional formula has
an equivalent DNF form [25]. We define
${\mathcal{C}}_{p}^{\gamma}=\bigwedge_{q\in{\mathcal{Q}}_{p}}(\neg)\pi$ or
${\mathcal{C}}_{p}^{\gamma}=\bigwedge_{q\in{\mathcal{Q}}_{p}}(\neg)\phi^{\prime}$
as the $p$-th clause of $\gamma$ which includes a set ${\mathcal{Q}}_{p}$ of
positive and negative literals with each literal being an atomic or composite
proposition.

####  III-B1 Logical Constraints

Logical constraints mainly encode the logical relation between labels, clauses
and literals, and the realization of literals. We iterate over each
specification $\phi\in\Phi$. Consider a specification $\phi\in\Phi$, for any
edge or vertex label $\gamma$ within its NBA, the necessity to satisfy
$\gamma$ depends on whether the specification $\phi$ should be true. To
incorporate this condition, we introduce a binary variable $b_{\phi}$,
representing the truth of specification $\phi$. By default, the binary
variable for the root specification is assigned a value of 1, i.e.,
$b_{\phi({1},{1})}=1$, which states that the root specification needs to be
satisfied. The condition that $\gamma$ should be true if and only if the
specification $\phi$ is true can be expressed by

$\sum_{p\in{\mathcal{P}}}b_{p}=b_{\phi},\quad\forall\phi\in\Phi,$ (3)

where the binary variable $b_{p}$ denotes whether the $p$-th clause is used
for the satisfaction of $\gamma$. If $b_{\phi}=1$, constraint (3) states that
exactly one clause is used to satisfy $\gamma$. Furthermore, the truth of a
clause determines the truth of positive and negative literals inside it. In
cases where $\phi$ is a non-leaf specification, all literals are essentially
composite propositions. The condition that every positive literal must be true
if its associated clause is true is formulated as

$\sum_{\phi\in\mathsf{lit}^{+}({\mathcal{C}}_{p}^{\gamma})}b_{\phi}=\left|\mathsf{lit}^{+}({\mathcal{C}}_{p}^{\gamma})\right|b_{p},\quad\forall
p\in{\mathcal{P}},$ (4)

where $\mathsf{lit}^{+}({\mathcal{C}}_{p}^{\gamma})$ is the set of positive
literals in the $p$-th clause. Beginning with the root specification, which
must be satisfied ($b_{\phi({1},{1})}=1$), the satisfaction of composite
propositions within $\phi({1},{1})$, i.e., specifications at level 2, is
deduced according to Eq. (3). Their truth will influence the satisfaction of
level 3 specifications, and this procedure continues down to the level of leaf
specifications. At this point, only those atomic sub-tasks linked to leaf
specifications identified as satisfied are assigned and executed. This
assignment and execution process is governed by the following set of
inequality constraints.

####  III-B2 Temporal Constraints

These constraints capture the temporal orders between atomic sub-tasks, which
are represented as linear inequalities. The key idea here is that if the
specification $\phi$ should not be satisfied, the inequality constraints
associated with it should be trivially met. Each of these constraints is
represented by a general linear inequality $g(x)\leq 0$, where $x$ denotes the
decision variables of the MILP. Let $\Phi_{g}$ denote the set of leaf
specifications involved in $g(x)$. The following constraint ensures that
$g(x)$ is trivially satisfied when at least one leaf specification in
$\Phi_{g}$ is false:

$\displaystyle g(x)\leq\sum_{\phi\in\Phi_{g}}M(1-b_{\phi}),$ (5)

where $M$ represents a sufficiently large integer. The inequality is only
active when $b_{\phi}=1,\forall\phi\in\Phi_{g}$. For differentiation, the
notation $\langle\cdot\rangle$ is used when referencing constraints in [17].
Consider constraint $\langle 15\rangle$ stating that the completion time of an
atomic sub-task $e\in\llbracket\phi\rrbracket_{a}$ in the task network should
be later than that of atomic sub-task
$e^{\prime}\in\llbracket\phi^{\prime}\rrbracket_{a}$ if $e^{\prime}$ is
required to be completed before $e$. Let $t_{e}$ be an integer variable
denoting the completion time of sub-task $e$, that is, when its edge label is
satisfied. Now the constraint becomes

$\displaystyle t_{e^{\prime}}+1\leq t_{e}+M(1-b_{\phi})$
$\displaystyle+M(1-b_{\phi^{\prime}}),\quad\text{if}\;e^{\prime}\prec e.$ (6)

The constraint (6) comes into effect, i.e., $t_{e^{\prime}}+1\leq t_{e}$, only
if both $\phi$ and $\phi^{\prime}$ need to be true. The same logic applies to
the other constraints $\langle 13\rangle$, $\langle 17\rangle$, $\langle
18\rangle$, $\langle 19\rangle$, $\langle 23\rangle$ and $\langle 25\rangle$,
which are elaborated in Appendix A.

###### Remark III.4

For navigation tasks, a sequence of Generalized Multi-Robot Path Planning
(GMRPP) problems [17], are set up for each sub-task to create robot paths.
These GMRPP solutions are sequentially organized and evaluated to ensure they
align with the semantics of hierarchical LTL specifications [1]. If this
satisfaction check fails, no solution is presented, resulting in the method’s
soundness. It is worth noting that [17] offers a complete solution for a wide
range of LTL specifications. Leveraging this foundation, our approach is
feasible for many robotic tasks, a claim supported by the following
experiments.

##  IV Numerical Experiments

We use Python 3.10.12 on a computer with 3.5 GHz Apple M2 Pro and 16G RAM. The
Big-M based MILP is solved using the Gurobi solver [30] with $M=10^{5}$. The
simulation video is accessible via https://youtu.be/a8gQCNuoNbM.

###  IV-A Navigation Task

The LTL specifications for task 2 are:

$\displaystyle L_{1}:\quad$
$\displaystyle\phi({1},{1})=\Diamond\left(\phi({2},{1})\wedge\Diamond\left(\phi({2},{2})\wedge\Diamond\left(\phi({2},{3})\wedge\Diamond\phi({2},{4})\right)\right)\right)$
$\displaystyle L_{2}:\quad$
$\displaystyle\phi({2},{1})=\Diamond\pi_{\text{furn}}^{1,1}\wedge\Diamond\pi_{\text{outd}}^{1,1}$
$\displaystyle\phi({2},{2})=\Diamond\pi_{\text{heal}}^{1,1}\wedge\Diamond\pi_{\text{groc}}^{1,1}$
(7)
$\displaystyle\phi({2},{3})=\Diamond\pi_{\text{elec}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}$
$\displaystyle\phi({2},{4})=\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$

These require that 1) A type 1 robot should initiate its task by gathering
items from the furniture and outdoor sections in any order; 2) Following that
the robot gathers items from the health and grocery sections in any order; 3)
Subsequently the robot gathers items from the electronics and pet sections
again without any specific sequence; 4) After delivering all the items to the
packing area, the robot eventually returns to the dock. The LTL specifications
for task 3 are:

$\displaystyle L_{1}:\quad$
$\displaystyle\phi({1},{1})=\Diamond(\phi({2},{1})\wedge\Diamond\phi({2},{2}))\wedge(\Diamond\phi({2},{3})\vee\Diamond\phi({2},{4}))$
$\displaystyle L_{2}:\quad$
$\displaystyle\phi({2},{1})=\Diamond\pi_{\text{heal}}^{1,1}\wedge\Diamond\pi_{\text{groc}}^{1,1}\wedge\Diamond\pi_{\text{elec}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}$
$\displaystyle\phi({2},{2})=\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$
(8)
$\displaystyle\phi({2},{3})=\Diamond(\pi_{\text{outd}}^{2,2}\wedge\Diamond(\pi_{\text{pack}}^{2,2}\wedge\Diamond\pi_{\text{dock}}^{2,2}))$
$\displaystyle\phi({2},{4})=\Diamond(\pi_{\text{outd}}^{3,3}\wedge\Diamond(\pi_{\text{pack}}^{3,3}\wedge\Diamond\pi_{\text{dock}}^{3,3}))$

These require that 1) A type 1 robot gathers items from the health, grocery,
electronics and pet sections in any order; 2) Either a type 2 robot or a type
3 robot gathers items from the outdoor section; 3) After the items are
delivered to the packing area, all robots eventually return to the dock.

The task networks are shown in Fig. LABEL:fig:tasks23. Flat LTL specifications
can be found in Eqs. (B-2) and (B-3) in Appendix B, respectively. We use [17]
to tackle the flat specifications. As far as we know, the only method for
hierarchical LTL is in [1], but it’s unsuitable here. First, [1] assumes
robots work independently within a flat specification, which forbids robot
coordination, like in $\phi({3},{1})$ in Eq. (1). Second, that method requires
that sequential sub-tasks in a flat specification must be completed by the
same robot. Finally, it cannot address specifications that explicitly require
sub-tasks to be performed by the same robot, as in $\phi({2},{1})$ in Eq.
(IV-A).

task | $l_{\text{flat}}$ | $l_{\text{hier}}$ | ${\mathcal{A}}_{\text{flat}}$ | ${\mathcal{A}}_{\text{hier}}$
---|---|---|---|---
1 | 51 | 35 | (387, 13862) | (33, 45)
2 | 45 | 19 | (12, 63) | (20, 28)
3 | 35 | 27 | (113, 1891) | (35, 101)
task | $t_{\text{flat}}$ | $t_{\text{hier}}$ | $c_{\text{flat}}$ | $c_{\text{hier}}$
1 | 126.1$\pm$2.7 | 18.6$\pm$0.8 | 289.3$\pm$3.0 | 237.9$\pm$3.5
2 | 30.8$\pm$0.5 | 23.8$\pm$1.3 | 115.6$\pm$1.9 | 114.9$\pm$1.6
3 | 25.8$\pm$1.8 | 20.1$\pm$0.8 | 148.1$\pm$2.1 | 147.9$\pm$1.9
TABLE I: The length of LTL specifications is represented by $l_{\text{flat}}$
and $l_{\text{hier}}$, while the size of the NBA is denoted by
${\mathcal{A}}_{\text{flat}}$ and ${\mathcal{A}}_{\text{hier}}$, specifying
the number of nodes first, followed by the number of edges. The runtimes are
indicated by $t_{\text{flat}}$ and $t_{\text{hier}}$, and the plan horizons
are indicated by $c_{\text{flat}}$ and $c_{\text{hier}}$.

The length of a LTL specification is quantified by the number of operators it
contains, including both logical and temporal operators [25]. For each task,
we compare between the length of the LTL and the size of the NBA, taking into
account both the flat and hierarchical forms. These NBAs are built using
LTL2BA [31]. In the case of the hierarchical form, the total is the sum of all
the specifications. The initial locations for the robots are randomly sampled
within the dock, and the runtimes and plan horizons are averaged over 20 runs.
The statistical outcomes are displayed in Tab. I. The hierarchical form of LTL
specifications leads to more concise formulas in length and NBAs that are
reduced in size with fewer nodes and edges. The reason is that in these three
tasks, composite sub-tasks, which can encompass several atomic sub-tasks, have
precedence relations between them. While expressing these relationships using
flat specifications can be wordy due to the need for pairwise enumeration,
using hierarchical LTL allows for a much more succinct representation. The
reduction in complexity leads to decreased runtimes and costs, particularly
for task 1, where it notably minimizes both the runtimes and horizons.

###  IV-B Manipulation Task

Two manipulation arms of the same type are tasked to assemble two LEGO models
in the Gazebo simulator. The task specifications are hard to specify by flat
specifications. To create executable trajectories, we use an online planning
approach. Upon the completion of a sub-task, thereby freeing an arm, we
evaluate the subsequent sub-task in the plan allocated to be executed by this
arm. If this sub-task is not preceded by any other ongoing or pending sub-
tasks, it will be carried out by this arm. However, if there are preceding
sub-tasks that are yet to be completed, the sub-task is deferred until all
preceding tasks are finished.

####  IV-B1 Bin packing

We use the LEGO model to replicate a bin packing task, as depicted in Fig.
LABEL:fig:iclltl. This task involves two adjacent stacks of bins, with the
requirement to pack two stacks in any order, ensuring that the second level is
packed only after the first level for each stack:

$\displaystyle L_{1}:\quad$
$\displaystyle\phi({1},{1})=\Diamond\phi({2},{1})\wedge\Diamond\phi({2},{2})$
$\displaystyle L_{2}:\quad$
$\displaystyle\phi({2},{1})=\Diamond\phi({3},{1})\wedge\Diamond\phi({3},{2})\wedge\neg\phi({3},{2})\,\mathcal{U}\,\phi({3},{1})$
$\displaystyle\phi({2},{2})=\Diamond\phi({3},{3})\wedge\Diamond\phi({3},{4})\wedge\neg\phi({3},{4})\,\mathcal{U}\,\phi({3},{3})$
$\displaystyle L_{3}:\quad$
$\displaystyle\begin{rcases}\phi({3},{1})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\pgfsys@color@rgb@stroke{1}{.5}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{.5}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,.5,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad\quad\quad\end{rcases}\text{1st
level of stack 1}$ (9)
$\displaystyle\begin{rcases}\phi({3},{2})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\;\end{rcases}\text{2nd
level of stack 1}$
$\displaystyle\begin{rcases}\phi({3},{3})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{
}\pgfsys@color@gray@fill{.5}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad\quad\quad\end{rcases}\text{1st
level of stack 2}$
$\displaystyle\begin{rcases}\phi({3},{4})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad\quad\quad\end{rcases}\text{2nd
level of stack 2}$

where $\phi({2},{1})$ and $\phi({2},{2})$ represent packing two stacks of
bins, while $\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}$ denotes packing a
bin colored  by any arm. Since both arms are of the same type, the atomic
propositions do not carry a superscript to denote the robot type. There is a
total of 30 states and 44 edges in the NBAs. It took $4.9\pm 0.2$ seconds over
20 runs to generate a task allocation plan.

####  IV-B2 House model

The second task involves constructing a complex house model, level by level,
as shown in Fig. LABEL:fig:house. Since the model is symmetric when viewed
from the front, each arm essentially handles half of the overall workload. The
hierarchical LTL specifications are

$\displaystyle L_{1}:\quad$
$\displaystyle\phi({1},{1})=\Diamond(\phi({2},{1})\wedge\Diamond(\phi({2},{2})\wedge\Diamond(\phi({2},{3})$
$\displaystyle\quad\quad\quad\quad\wedge\Diamond(\phi({2},{4})\wedge\Diamond(\phi({2},{5})\wedge\Diamond\phi({2},{6}))))))$
$\displaystyle L_{2}:\quad$
$\displaystyle\phi({2},{1})=\Diamond\phi({3},{1})\wedge\Diamond\phi({3},{2})$
$\displaystyle\phi({2},{2})=\Diamond\phi({3},{3})\wedge\Diamond\phi({3},{4})$
$\displaystyle\phi({2},{3})=\Diamond\phi({3},{5})\wedge\Diamond\phi({3},{6})$
$\displaystyle\phi({2},{4})=\Diamond\phi({3},{7})$
$\displaystyle\phi({2},{5})=\Diamond(\phi({3},{8})\wedge\Diamond\phi({3},{9}))$
$\displaystyle\phi({2},{6})=\Diamond\phi({3},{10})$ (10) $\displaystyle
L_{3}:\quad$
$\displaystyle\begin{rcases}\phi({3},{1})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1}\\\
\phi({3},{2})=\Diamond\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2}\;\;\;\quad\\\
\end{rcases}\text{1st level}$
$\displaystyle\begin{rcases}\phi({3},{3})=\Diamond(\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{
}\pgfsys@color@gray@fill{.5}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1})\\\
\phi({3},{4})=\Diamond(\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{
}\pgfsys@color@gray@fill{.5}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2})\\\
\phi({3},{5})=\Diamond(\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{
}\pgfsys@color@gray@fill{.5}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1})\\\
\phi({3},{6})=\Diamond(\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@invoke{
}\pgfsys@color@gray@fill{.5}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{.5,.5,.5}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2})\quad\\\
\end{rcases}\text{2nd and 3rd levels}$
$\displaystyle\begin{rcases}\phi({3},{7})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,1,0}\pgfsys@color@rgb@stroke{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad\;\;\;\\\
\end{rcases}\text{4th level}$
$\displaystyle\begin{rcases}\phi({3},{8})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{1}\wedge\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}^{2}\quad\;\;\;\\\
\phi({3},{9})=\Diamond\pi_{\leavevmode\hbox to4pt{\vbox
to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,.5,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,.5,0}\pgfsys@color@rgb@stroke{1}{.5}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{.5}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,.5,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\\\
\end{rcases}\text{5th level}$
$\displaystyle\begin{rcases}\phi({3},{10})=\Diamond\pi_{\leavevmode\hbox
to4pt{\vbox to4pt{\pgfpicture\makeatletter\hbox{\hskip 2.0pt\lower-2.0pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}{}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@moveto{2.0pt}{0.0pt}\pgfsys@curveto{2.0pt}{1.10458pt}{1.10458pt}{2.0pt}{0.0pt}{2.0pt}\pgfsys@curveto{-1.10458pt}{2.0pt}{-2.0pt}{1.10458pt}{-2.0pt}{0.0pt}\pgfsys@curveto{-2.0pt}{-1.10458pt}{-1.10458pt}{-2.0pt}{0.0pt}{-2.0pt}\pgfsys@curveto{1.10458pt}{-2.0pt}{2.0pt}{-1.10458pt}{2.0pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\quad\quad\quad\quad\,\end{rcases}\text{6th
level}$

where the identical superscript represents that blocks are assembled by the
same arm. For instance, leaf specifications $\phi({3},{1})$ and
$\phi({3},{2})$ specify the assembly of the 1st level by assigning two yellow
blocks to each arm, and $\phi({3},{10})$ specify that the red block at the top
can be assembled by any arm. There is a total of 58 states and 59 edges in all
NBAs. It took $4.8\pm 0.2$ seconds over 20 runs to generate a task allocation
plan.

##  V Discussion and Conclusions

In this work, we presented a hierarchical decomposition-based method to
address robotic navigation and manipulation tasks as described by hierarchical
LTL specifications. Although our proposed approach demonstrates effectiveness,
it falls short in terms of completeness. Consequently, developing an approach
that guarantees both completeness and optimality stands as a potential avenue
for future research.

## References

  * Luo and Liu [2024] X. Luo and C. Liu, “Simultaneous task allocation and planning for multi-robots under hierarchical temporal logic specifications,” _arXiv preprint arXiv:2401.04003_ , 2024.
  * Fainekos et al. [2005] G. E. Fainekos, H. Kress-Gazit, and G. J. Pappas, “Temporal logic motion planning for mobile robots,” in _IEEE International Conference on Robotics and Automation (ICRA)_ , Barcelona, Spain, 2005, pp. 2020–2025.
  * Kantaros and Zavlanos [2017] Y. Kantaros and M. M. Zavlanos, “Distributed intermittent connectivity control of mobile robot networks,” _IEEE Transactions on Automatic Control_ , vol. 62, no. 7, pp. 3109–3121, 2017.
  * He et al. [2015] K. He, M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “Towards manipulation planning with temporal logic specifications,” in _2015 IEEE international conference on robotics and automation (ICRA)_. IEEE, 2015, pp. 346–352.
  * Pnueli [1977] A. Pnueli, “The temporal logic of programs,” in _18th Annual Symposium on Foundations of Computer Science (sfcs 1977)_. ieee, 1977, pp. 46–57.
  * Guo and Dimarogonas [2015] 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.
  * Tumova and Dimarogonas [2016] J. Tumova and D. V. Dimarogonas, “Multi-agent planning under local LTL specifications and event-based synchronization,” _Automatica_ , vol. 70, pp. 239–248, 2016.
  * Yu and Dimarogonas [2021] P. Yu and D. V. Dimarogonas, “Distributed motion coordination for multirobot systems under ltl specifications,” _IEEE Transactions on Robotics_ , vol. 38, no. 2, pp. 1047–1062, 2021.
  * Bai et al. [2022] R. Bai, R. Zheng, Y. Xu, M. Liu, and S. Zhang, “Hierarchical multi-robot strategies synthesis and optimization under individual and collaborative temporal logic specifications,” _Robotics and Autonomous Systems_ , vol. 153, p. 104085, 2022.
  * Smith et al. [2011] S. L. Smith, J. Tůmová, 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.
  * Kantaros and Zavlanos [2020] Y. Kantaros and M. M. Zavlanos, “Stylus*: A temporal logic optimal control synthesis algorithm for large-scale multi-robot systems,” _The International Journal of Robotics Research_ , vol. 39, no. 7, pp. 812–836, 2020\.
  * Luo et al. [2021] X. Luo, Y. Kantaros, and M. M. Zavlanos, “An abstraction-free method for multirobot temporal logic optimal control synthesis,” _IEEE Transactions on Robotics_ , vol. 37, no. 5, pp. 1487–1507, 2021.
  * Shoukry et al. [2017] Y. Shoukry, P. Nuzzo, A. Balkan, I. Saha, A. L. Sangiovanni-Vincentelli, S. A. Seshia, G. J. Pappas, and P. Tabuada, “Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming,” in _2017 IEEE 56th Annual Conference on Decision and Control (CDC)_. IEEE, 2017, pp. 1132–1137.
  * Schillinger et al. [2018] P. Schillinger, M. Bürger, and D. V. Dimarogonas, “Simultaneous task allocation and planning for temporal logic goals in heterogeneous multi-robot systems,” _The International Journal of Robotics Research_ , vol. 37, no. 7, pp. 818–838, 2018.
  * Sahin et al. [2019] Y. E. Sahin, P. Nilsson, and N. Ozay, “Multirobot coordination with counting temporal logics,” _IEEE Transactions on Robotics_ , 2019.
  * Leahy et al. [2021] K. Leahy, Z. Serlin, C.-I. Vasile, A. Schoer, A. M. Jones, R. Tron, and C. Belta, “Scalable and robust algorithms for task-based coordination from high-level specifications (scratches),” _IEEE Transactions on Robotics_ , vol. 38, no. 4, pp. 2516–2535, 2021.
  * Luo and Zavlanos [2022] X. Luo and M. M. Zavlanos, “Temporal logic task allocation in heterogeneous multirobot systems,” _IEEE Transactions on Robotics_ , vol. 38, no. 6, pp. 3602–3621, 2022.
  * Li et al. [2023] L. Li, Z. Chen, H. Wang, and Z. Kan, “Fast task allocation of heterogeneous robots with temporal logic and inter-task constraints,” _IEEE Robotics and Automation Letters_ , 2023.
  * Liu et al. [2023] W. Liu, K. Leahy, Z. Serlin, and C. Belta, “Robust multi-agent coordination from catl+ specifications,” in _2023 American Control Conference (ACC)_. IEEE, 2023, pp. 3529–3534.
  * Tenenbaum et al. [2011] J. B. Tenenbaum, C. Kemp, T. L. Griffiths, and N. D. Goodman, “How to grow a mind: Statistics, structure, and abstraction,” _Science_ , vol. 331, no. 6022, pp. 1279–1285, 2011.
  * Luo and Zavlanos [2019] X. Luo and M. M. Zavlanos, “Transfer planning for temporal logic tasks,” in _2019 IEEE 58th Conference on Decision and Control (CDC)_. IEEE, 2019, pp. 5306–5311.
  * Camacho et al. [2019] A. Camacho, R. T. Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith, “LTL and beyond: Formal languages for reward function specification in reinforcement learning,” in _Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI)_ , 2019, pp. 6065–6073.
  * Liu et al. [2024] Z. Liu, M. Guo, and Z. Li, “Time minimization and online synchronization for multi-agent systems under collaborative temporal logic tasks,” _Automatica_ , vol. 159, p. 111377, 2024.
  * Leahy et al. [2023] K. Leahy, M. Mann, and C.-I. Vasile, “Rewrite-based decomposition of signal temporal logic specifications,” in _NASA Formal Methods Symposium_. Springer, 2023, pp. 224–240.
  * Baier and Katoen [2008] C. Baier and J.-P. Katoen, _Principles of model checking_. MIT press Cambridge, 2008.
  * Kupferman and Vardi [2001] O. Kupferman and M. Y. Vardi, “Model checking of safety properties,” _Formal Methods in System Design_ , vol. 19, no. 3, pp. 291–314, 2001.
  * Chen et al. [2021] Z. Chen, J. Alonso-Mora, X. Bai, D. D. Harabor, and P. J. Stuckey, “Integrated task assignment and path planning for capacitated multi-agent pickup and delivery,” _IEEE Robotics and Automation Letters_ , vol. 6, no. 3, pp. 5816–5823, 2021.
  * Xu et al. [2022] Q. Xu, J. Li, S. Koenig, and H. Ma, “Multi-goal multi-agent pickup and delivery,” in _2022 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)_. IEEE, 2022, pp. 9964–9971.
  * Bredström and Rönnqvist [2008] D. Bredström and M. Rönnqvist, “Combined vehicle routing and scheduling with temporal precedence and synchronization constraints,” _European journal of operational research_ , vol. 191, no. 1, pp. 19–31, 2008\.
  * Gurobi Optimization [2018] L. Gurobi Optimization, “Gurobi optimizer reference manual,” 2018. [Online]. Available: http://www.gurobi.com
  * Gastin and Oddoux [2001] P. Gastin and D. Oddoux, “Fast LTL to büchi automata translation,” in _International Conference on Computer Aided Verification_. Springer, 2001, pp. 53–65.

## Appendix A

###  A-A MILP objective

Drawing inspiration from VRP, we construct a routing graph
$({\mathcal{V}}_{r},{\mathcal{E}}_{r})$ in which nodes denote regions (e.g., a
grocery shelf, a brick target location) associated with certain atomic sub-
task, and the traversal of nodes within some duration by appropriate robots
fulfills certain atomic propositions. The goal is to minimize the
$\alpha$-weighted sum of the energy cost and completion time:

$\displaystyle\min_{x_{uvr},t_{e}}\;\alpha\sum_{(u,v)\in{\mathcal{E}}_{r}}\sum_{r\in{\mathcal{M}}(v)}d_{uv}x_{uvr}+(1-\alpha)\sum_{e}t_{e}.$
(11)

Here $x_{uvr}\in\\{0,1\\}$ are routing variables indicating the movement of
robot $r$ between nodes $u$ and $v$ in the routing graph, with robot $r$ being
part of the subset ${\mathcal{M}}(v)$ which assigns a type of robots with the
required skills to a node, and $d_{uv}$ is the energy cost. Additionally, $e$
stands for the atomic sub-tasks within the task network.

We present the concepts of activation and completion times and identify three
categories of temporal constraints.

######  Definition A.1 (Activation and completion time of a sub-task or its
starting vertex label [17])

For a given sub-task $e=(v_{1},v_{2})$, its activation time (or the activation
time of its starting vertex label) is defined as the moment when the vertex
label $\gamma(v_{1})$ become satisfied. Similarly, the completion time of a
sub-task (or the completion time of its starting vertex label) is determined
as the moment when its edge label $\gamma(v_{1},v_{2})$ is satisfied (or
alternatively, the final moment when its starting vertex label $\gamma(v_{1})$
remains true). The span of a sub-task (or its starting vertex label) is the
time period that begins with the activation time and ends with the completion
time.

Let $t^{-}_{ep}$ and $t^{+}_{ep}$ denote the first and last time instants at
which the $p$-th clause in the starting vertex label of sub-task $e$ is
satisfied, respectively. Considering two atomic sub-tasks $e$ and
$e^{\prime}$, let $\phi$ and $\phi^{\prime}$ be their corresponding leaf
specifications. The linear inequality constraints $\langle 13\rangle$,
$\langle 17\rangle$, $\langle 18\rangle$, $\langle 19\rangle$, $\langle
23\rangle$, and $\langle 25\rangle$ are modified with modifications being
highlighted in boxes. Notations are simplified for ease of understanding.

###  A-B Temporal constraints associated with one atomic sub-task

Constraint $\langle 13\rangle$ captures the relation that the completion time
of a sub-task must fall within the duration of its starting vertex label, or
precisely one time step subsequent to the completion of this starting vertex
label, which becomes:

$\displaystyle t_{ep}^{-}$ $\displaystyle\leq t_{e}+\boxed{M(1-b_{\phi})}$
(12a) $\displaystyle t_{e}\leq t_{ep}^{+}+1+M$
$\displaystyle(1-b_{p})+\boxed{M(1-b_{\phi})}.$ (12b)

Constraints are activated only if $b_{\phi}=1$ and $b_{p}=1$, then the
condition $t_{ep}^{-}\leq t_{e}\leq t_{ep}^{+}+1$ come into effect.

###  A-C Temporal constraints associated with the completion of a sub-task and
the activation of the sub-task immediately following it

Constraint $\langle 17\rangle$ reflecting the precedence rule that sub-task
$e$ must be completed at most one time step prior to the activation of its
immediately subsequent sub-task, becomes

$\displaystyle t_{e}+1\leq t_{e^{\prime}}$
$\displaystyle+M(1-b_{ee^{\prime}})$
$\displaystyle+\boxed{M(1-b_{\phi})+M(1-b_{\phi^{\prime}})},\;\forall\,e^{\prime}\prec
e,$ (13)

where the binary variable $b_{ee^{\prime}}$ is set to 1 if sub-task
$e^{\prime}$ directly follows sub-task $e$. Furthermore, constraint (A-C) is
activated only when both $b_{\phi}$ and $b_{\phi^{\prime}}$ equal 1, leading
to $t_{e}+1\leq t_{e^{\prime}}$.

Constraint $\langle 18\rangle$ states that the sub-task $e^{\prime}$, if
following right after sub-task $e$, must be activated no more than one time
step after the completion of $e$, which becomes

$\displaystyle t_{e^{\prime}p}^{-}\leq t_{e}$
$\displaystyle+1+M(1-b_{ee^{\prime}})$
$\displaystyle+\boxed{M(1-b_{\phi})+M(1-b_{\phi^{\prime}})}.$ (14)

When $b_{ee^{\prime}}=1$, indicating that sub-task $e^{\prime}$ immediately
follows sub-task $e$, and additionally, when $b_{\phi}=b_{\phi^{\prime}}=1$,
the condition $t_{e^{\prime}p}^{-}\leq t_{e}+1$ is established.

Constraint $\langle 19\rangle$ implies that two sub-tasks cannot be completed
simultaneously, which is now expressed as:

$\displaystyle b_{e}^{e^{\prime}}+b_{e^{\prime}}^{e}$ $\displaystyle=1,$ (15a)
$\displaystyle M(b_{e}^{e^{\prime}}-1)$ $\displaystyle\leq
t_{e}-t_{e^{\prime}}+\boxed{M(1-b_{\phi})+M(1-b_{\phi^{\prime}})},$ (15b)
$\displaystyle t_{e}-t_{e^{\prime}}\leq$ $\displaystyle
Mb_{e}^{e^{\prime}}-1+\boxed{M(1-b_{\phi})+M(1-b_{\phi^{\prime}})},$ (15c)

where $b_{e}^{e^{\prime}}=1$ indicates that sub-task $e$ is completed after
sub-task $e^{\prime}$. When $b_{\phi}=b_{\phi^{\prime}}=1$, and if
$b_{e}^{e^{\prime}}=1$, it follows that $t_{e}\geq t_{e^{\prime}}$. Meanwhile,
if $b_{e^{\prime}}^{e}=0$, the condition $t_{e^{\prime}}-t_{e}\leq-1$ applies.
Consequently, this leads to $t_{e}\geq t_{e^{\prime}}+1$.

###  A-D Temporal constraints associated with the activation of the first sub-
task

Constraint $\langle 23\rangle$ specifies that if $e$ is the first one to be
completed and there is no preceding sub-task whose completion triggers $e$,
then $e$ must be activated at the beginning:

$\displaystyle t_{ep}^{-}\leq M(1-b_{e})+M(1-b_{p})+\boxed{M(1-b_{\phi})},$
(16)

where the binary variable $b_{e}=1$ indicates that sub-task $e$ is the first
to be completed. When $b_{\phi}=b_{e}=b_{p}=1$, it follows that
$t_{ep}^{-}=0$, meaning that $e$ is activated at the beginning with the $p$-th
clause in the vertex label being true.

Constraint $\langle 25\rangle$ specifies the specific categories of states
from which robots should initiate, which becomes:

$\displaystyle b_{pq}^{\text{init}}$ $\displaystyle\leq b_{p},$ (17a)
$\displaystyle b_{pq}^{\text{init}}$ $\displaystyle\leq
Mb_{e}+\boxed{M(1-b_{\phi})},$ (17b) $\displaystyle b_{pq}^{\text{prior}}$
$\displaystyle\leq b_{p},$ (17c) $\displaystyle b_{pq}^{\text{prior}}$
$\displaystyle\leq M(1-b_{e})+\boxed{M(1-b_{\phi})}.$ (17d)

For the robots engaged in the $q$-th positive literal of the $p$-th clause in
the starting vertex label of sub-task $e$, the binary variable
$b_{pq}^{\text{init}}$ indicates that the robots begin from their initial
states. Conversely, $b_{pq}^{\text{prior}}$ indicates that the robots start
from their positions following the completion of preceding sub-tasks of $e$.
If $b_{p}=0$, it implies no robot is involved in the $p$-th clause, leading to
$b_{pq}^{\text{init}}=b_{pq}^{\text{prior}}=0$. When $b_{\phi}=b_{e}=1$ and
$b_{p}=1$, it results in $b_{pq}^{\text{prior}}=0$. This means that if sub-
task $e$ is the first to be completed, the involved robots should begin from
their initial states. Conversely, when $b_{\phi}=1$, $b_{e}=0$, and $b_{p}=1$,
it leads to $b_{pq}^{\text{init}}=0$, indicating that if sub-task $e$ is not
the first to be completed, the involved robots should start from their
locations after finishing prior sub-tasks of $e$.

##  Appendix B Flat specifications for MRPD tasks

####  B-1 Task 1

$\displaystyle\phi=$
$\displaystyle\,\Diamond(\pi_{\text{furn}}^{1,1}\wedge\bigcirc(\pi_{\text{furn}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{3,3}))$
$\displaystyle\wedge\Diamond(\pi_{\text{pack}}^{3,3}\wedge\Diamond\pi_{\text{dock}}^{3,3})\wedge\neg\pi_{\text{pack}}^{3,3}\,\mathcal{U}\,\pi_{\text{furn}}^{3,3}$
$\displaystyle\wedge\Diamond\pi_{\text{outd}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}\wedge\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$
$\displaystyle\wedge\neg\pi_{\text{outd}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{1,1}\wedge\neg\pi_{\text{outd}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{3,3}$
(18)
$\displaystyle\wedge\neg\pi_{\text{pet}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{1,1}\wedge\neg\pi_{\text{pet}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{3,3}$
$\displaystyle\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{outd}}^{1,1}\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{pet}}^{1,1}$
$\displaystyle\wedge\Diamond\pi_{\text{heal}}^{2,2}\wedge\Diamond\pi_{\text{groc}}^{2,2}\wedge\Diamond(\pi_{\text{pack}}^{2,2}\wedge\Diamond\pi_{\text{dock}}^{2,2})$
$\displaystyle\wedge\neg\pi_{\text{groc}}^{2,2}\,\mathcal{U}\,\pi_{\text{heal}}^{2,2}\wedge\neg\pi_{\text{pack}}^{2,2}\,\mathcal{U}\,\pi_{\text{groc}}^{2,2}$

####  B-2 Task 2

$\displaystyle\phi=$
$\displaystyle\,\Diamond\pi_{\text{furn}}^{1,1}\wedge\Diamond\pi_{\text{outd}}^{1,1}\wedge\Diamond\pi_{\text{heal}}^{1,1}\wedge\Diamond\pi_{\text{groc}}^{1,1}$
$\displaystyle\wedge\Diamond\pi_{\text{elec}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}\wedge\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$
$\displaystyle\wedge\neg\pi_{\text{heal}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{1,1}\wedge\neg\pi_{\text{heal}}^{1,1}\,\mathcal{U}\,\pi_{\text{outd}}^{1,1}$
$\displaystyle\wedge\neg\pi_{\text{groc}}^{1,1}\,\mathcal{U}\,\pi_{\text{furn}}^{1,1}\wedge\neg\pi_{\text{groc}}^{1,1}\,\mathcal{U}\,\pi_{\text{outd}}^{1,1}$
(19)
$\displaystyle\wedge\neg\pi_{\text{elec}}^{1,1}\,\mathcal{U}\,\pi_{\text{heal}}^{1,1}\wedge\neg\pi_{\text{elec}}^{1,1}\,\mathcal{U}\,\pi_{\text{groc}}^{1,1}$
$\displaystyle\wedge\neg\pi_{\text{pet}}^{1,1}\,\mathcal{U}\,\pi_{\text{heal}}^{1,1}\wedge\neg\pi_{\text{pet}}^{1,1}\,\mathcal{U}\,\pi_{\text{groc}}^{1,1}$
$\displaystyle\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{elec}}^{1,1}\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{pet}}^{1,1}$

####  B-3 Task 3

$\displaystyle\phi=$
$\displaystyle\,\Diamond\pi_{\text{heal}}^{1,1}\wedge\Diamond\pi_{\text{groc}}^{1,1}\wedge\Diamond\pi_{\text{elec}}^{1,1}\wedge\Diamond\pi_{\text{pet}}^{1,1}$
$\displaystyle\wedge\Diamond(\pi_{\text{pack}}^{1,1}\wedge\Diamond\pi_{\text{dock}}^{1,1})$
$\displaystyle\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{heal}}^{1,1}\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{groc}}^{1,1}$
(20)
$\displaystyle\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{elec}}^{1,1}\wedge\neg\pi_{\text{pack}}^{1,1}\,\mathcal{U}\,\pi_{\text{pet}}^{1,1}$
$\displaystyle\wedge\left(\Diamond\left(\pi_{\text{outd}}^{2,2}\wedge\Diamond\left(\pi_{\text{pack}}^{2,2}\wedge\Diamond\pi_{\text{dock}}^{2,2}\right)\right)\right.$
$\displaystyle\vee\left.\Diamond\left(\pi_{\text{outd}}^{3,3}\wedge\Diamond\left(\pi_{\text{pack}}^{3,3}\wedge\Diamond\pi_{\text{dock}}^{3,3}\right)\right)\right)$