Capability Augmentation for Heterogeneous Dynamic Teaming
with Temporal Logic Tasks

In this section, we formalize a model for the agent and environment. We consider a group of heterogeneous agents operating in a partitioned 2D shared environment. In each region, there can either be a service request that an agent can satisfy by visiting that region, an indication that the region should be avoided, or neither. Formally, we define the environment as a tuple $Env=(\mathcal{Q},E,\Pi,\mathcal{L})$, where $\mathcal{Q}$ is the set of nodes (vertices) corresponding to environment regions and $E\subseteq\mathcal{Q}\times\mathcal{Q}$ is the set of directed edges such that $(q,q^{\prime})\in E$ iff an agent can transition from node $q$ to node $q^{\prime}$(this includes self-transitions). The environment we consider is a grid such that all transitions that are not self-transition are the same distance. For $q\in\mathcal{Q}$, let $adj(q)\subset\mathcal{Q}$ be the set of nodes that are adjacent to node $q$, i.e., $q^{\prime}\in adj(q)\iff(q,q^{\prime})\in E$. Let $\Pi$ be a set of labels that report the the service requests and indications of danger of the environment, and $\mathcal{L}:\mathcal{Q}\mapsto 2^{\Pi}$ be a mapping that matches each node to a set of labels. Agents are asked to visit and avoid the features of the environment by referencing if it is in a node with a corresponding label.

We assume that the agents travel between nodes using existing edges. As they travel, they incur costs based on the number of transitions they take that are not self-transitions. The agents are synchronized using a central clock. At every time step the agents either transition to a new node or make a self-transition and stay in place. These transitions always take a single time step. Agents are indexed from a finite set $\{1,...,N_{A}\}$, where $N_{A}$ is the total number of agents in the environment.

We define an individual agent as a tuple $a_{j}=(\mathcal{C}_{j},q_{j}(0))$, where $\mathcal{C}_{j}$ is the set of capabilities of agent $j$, $j\in\{1,...,N_{A}\}$. The capabilities of each agent determine how they collaborate with other agents (detailed in Sec. II-B and Sec. II-C). Let $\mathcal{C}_{global}$ be the total set of capabilities held by all the agents in the system, i.e., $\mathcal{C}_{global}=\cup_{j\in\{1,\ldots,N_{A}\}}\mathcal{C}_{j}$. We define $I_{c}$ as the set of indices of agents with a specific capability $c$ where $c\in\mathcal{C}_{global}$, i.e. $j\in I_{c}\iff c\in\mathcal{C}_{j}$. Let $q_{j}(k)\in\mathcal{Q}$ be the node occupied by agent $j$ at time $k$, and $q_{j}(0)$ be the agent’s initial node. In this paper, we only consider the high-level motion plan, i.e., the transitions of robots between nodes. We assume any number of agents can be in the same node and take the same transitions simultaneously without worry of collision. The inter-agent collision can be avoided by using a lower-level controller tracking the high-level motion plan, which will be considered in future work. We define a group trajectory $\mathbf{Q}\in\mathcal{Q}^{T_{p}\times N_{A}}$ as the sequence of nodes every agent visits where $\mathbf{Q}[k]=[q_{1}(k),\ldots,q_{N_{A}}(k))]$ and $T_{p}$ is the planning horizon (defined in Sec. II-D).

Next, we define our language for specifying tasks for the agents. In this paper, we use MTL [14][15] to formally define an individual specification for each agent. We define the individual MTL specification for an agent $j$ over its trace. The trace of agent $j$ is defined as $\mathbf{O}_{j}=\mathbf{o}_{j}(0),\mathbf{o}_{j}(1),...,\mathbf{o}_{j}(T_{p})$, where $\mathbf{o}_{j}(k)$ is the observation of agent $j$ at time step $k$, defined as

Here, $n_{j}^{c}(k)$ is the number of agents with capability $c$ in the same node with agent $j$ at time step $k$ excluding agent $j$:

where $\beta$ is a binary indicator function that returns $1$ if a statement is true and $0$ otherwise. The reason we include $n_{j}^{c}(k)$ is so we can evaluate tasks using capability-augmenting collaboration. The syntax of the MTL we use in this paper is defined as follows:

Here, $k_{1},k_{2}\in\mathbb{Z}_{\geq 0}$ are time bounds with $k_{1}\leq k_{2}<\infty$. $\lozenge_{[k_{1},k_{2}]}$ is the temporal operator eventually, and $\lozenge_{[k_{1},k_{2}]}\phi$ requires that $\phi$ has to be true at some point in the time interval $[k_{1},k_{2}]$. $\square_{[k_{1},k_{2}]}$ is the temporal operator always, and $\square_{[k_{1},k_{2}]}\phi$ requires that $\phi$ must be true at all points in the time interval $[k_{1},k_{2}]$. $U_{[k_{1},k_{2}]}$ is the temporal operator until, and $\phi_{1}U_{[k_{1},k_{2}]}\phi_{2}$ requires that $\phi_{2}$ is true at some point in $[k_{1},k_{2}]$ and $\phi_{1}$ is always true before that. $\neg$, $\land$, and $\lor$ are the negation, conjunction, and disjunction Boolean operators, respectively. AP is an atomic proposition. We will formally encode capability-augmenting collaboration into the atomic propositions in Section II-C. We use $(\mathbf{O}_{j},k)\models\phi$ to denote that the trace of agent $j$ satisfies the MTL formula $\phi$ at time $k$. The time horizon of a formula $\phi$, denoted as $T_{\phi}$, is the smallest time point in the future for which the observation is required to determine the satisfaction of the formula. Formal definitions of the semantics, as well as the time horizon $T_{\phi}$ can be found in [14] and [15].

In this subsection, we define a specific kind of atomic proposition called CATs that we use to formalize and encode capability-augmenting collaboration into MTL.

Intuitively, an agent $j$ can satisfy the CAT (2) at time $k$ in two ways. The first is to reach a node labeled by a specified $\pi$, i.e., $\pi\in\mathcal{L}(q_{j}(k))$. In cases when agent $j$ cannot reach a node with label $\pi$, the second way that the agent may be able to satisfy the CAT is that there are at least $m_{aug}$ agents with a compatible capability $c_{aug}\in\mathcal{C}_{global}$ and less than $m_{al}$ agents with capability $c_{al}\in\mathcal{C}_{global}$ in the agent’s node $q_{j}(k)$ excluding itself. We refer to $c_{aug}$ as an augmenting capability and $c_{al}$ as an availability-limiting capability. In other words, if the required number of agents with an augmenting capability $c_{aug}$ are present and available in an agent’s node, then the agent can satisfy the CAT with their assistance without being in a node with the required label $\pi$. The agents with the augmenting capability are unavailable if and only if there are no less than $m_{al}$ agents with the availability-limiting capability $c_{al}$ in the agent’s node excluding itself because we assume that the agents with the augmenting capability $c_{aug}$ may be assisting other agents. We make this conservative assumption to ensure that generating trajectories based on CATs is tractable. We will address relaxing this assumption in future work. The second way to satisfy a CAT, i.e., satisfying it via collaboration, is referred to as capability-augmenting collaboration. The satisfaction of a CAT, referred to as the qualitative semantics, is formulated in the following definition.

There are two special cases for a CAT. First, if $m_{al}>|I_{c_{al}}|$, which means that agents with capability $c_{aug}$ are always available to collaborate, we remove $c_{al},m_{al}$ from the CAT for simplicity, i.e., the CAT is denoted as $\langle\pi,\{c_{aug},m_{aug}\},\{\}\rangle$. Second, if $m_{aug}>|I_{c_{aug}}|$, which means that agents with capability $c_{aug}$ can never collaborate with agent $j$, we remove $c_{aug},m_{aug}$ from the CAT and turn it into $\langle\pi,\{\},\{\}\rangle$ for simplicity. In both cases, the semantics (3) can be evaluated without the omitted components.

We assign an MTL specification $\phi_{j}$ defined over $\mathbf{O}_{j}$ to each agent $j$. We define $\rho(\mathbf{O}_{j},\phi_{j},k)$ to quantify the satisfaction of $\phi_{j}$, where $\rho$ maps a trace $\mathbf{O}_{j}$, an MTL formula $\phi_{j}$, and time step $k$ to either $1$ or $-1$ depending on satisfaction. It is defined formally as follows:

This metric does not report the degree of satisfaction as a robustness metric would. Rather, it numerically captures Boolean satisfaction for individual agents. We determine the planning horizon from the individual specifications as $T_{p}=\max_{j\in\{1,...,N_{A}\}}(T_{\phi_{j}})$. We evaluate the performance of agent $j$ using $\rho(\mathbf{O}_{j},\phi_{j},0)$ and an individual motion cost. The motion cost $J_{j}:\mathcal{Q}^{T_{p}\times N_{A}}\mapsto\mathbb{Z}_{\geq 0}$ is the number of transitions, excluding self-transitions, an agent takes and is formulated as:

We define individual agent performance $P_{j}:\mathcal{Q}^{T_{p}\times N_{A}}\times\phi_{j}\mapsto\mathbb{R}$ as:

where $M$ is a large enough positive number $M\in\mathbb{R}_{\geq 0}$ to prioritize the satisfaction of $\phi_{j}$. Note that we use the nodes that makeup $\mathbf{Q}$ to solve for the sequence of observations $\mathbf{O}_{j}$, meaning that $\mathbf{Q}$ and $\phi_{j}$ are enough to evaluate $P_{j}$. $M$ should be larger than the largest possible value of an individual cost $M\geq\sup_{\mathbf{Q}}J_{j}(\mathbf{Q})$. $P_{j}$ is an aggregate metric used to evaluate both task satisfaction and accumulated cost.

Our objective is to find an optimal group trajectory $\mathbf{Q}^{*}$, that utilizes the heterogeneous capabilities of the agents to maximize the agent performance and abide by all motion constraints. We solve for optimal trajectories as follows :

We maximize agent performance rather than constraining the system to satisfy all individual specifications. We do so to allow as many agents as possible to satisfy their specifications when not all specifications are feasible.

Example: Consider a system composed of three agents ($N_{A}=3$) with one aerial and two ground robots (see Fig. 1). The aerial robot must reach a node with the label “Scenic” to take a picture and upload it to a database at a node with the label “Upload”. The ground robots must reach a region with the label “Goal” at some point and never touch “Water”. The ground robot can enter the “Water” regions if it is carried by an aerial agent. The ground robots have a wireless connection to the database that the aerial agent can use to upload its picture when they are together, independently of whether they are in a node with the label “Upload”. The aerial robot can carry one ground robot at a time. Agents plan their trajectories using a central computer, but cannot use it to send or receive images.

We assume that if an agent is in a node where it can perform actions such as taking and uploading pictures, either on its own or in a collaborating way, it does so automatically. All actions happen instantaneously.

The aerial robot has capability $\mathcal{C}_{1}=\{\text{``carry"}\}$. The ground agents have capabilities $\mathcal{C}_{2}=\mathcal{C}_{3}=\{\text{``WiFi"},\text{``wheels"}\}$. As shown in Fig. 1, the environment has labels $\Pi=\{\text{``Upload"},\text{``Scenic"},\text{``Water"},\text{``Goal"}\}$.

We encode that aerial agent can carry the ground agent over water with a CAT $\langle\neg\text{``Water''},\{\text{``carry''},1\},\{\text{``wheels''},1\}\rangle$ defined over the ground robot. Here, with a slight abuse of notation, we use $\neg\pi$ to denote a label that is assigned to all nodes that are not labeled by $\pi$, i.e., $(\neg\pi)\in\mathcal{L}(q)\iff\pi\not\in\mathcal{L}(q)$. This CAT allows the aerial agent to assist the ground robot over water if there are no other ground robots in the same node. The CAT defined over the aerial robot that encodes the aerial agent’s ability to upload pictures using a ground robot is $\langle\text{``Upload''},\{\text{``WiFi''},1\},\{\}\rangle$. These CATs provide a succinct encoding that captures capability-augmenting collaboration.

The aerial agent’s specification is to take a picture at “Scenic” in the first 6 time-steps and then upload it within 4 time-steps. The ground agents’ specification is to visit “Goal” in the first 10 time-steps and always avoid “Water” unless carried by an aerial agent. These specifications are encoded as follows:

In this section, we defined capability-augmenting collaboration as a method for agents to utilize each other’s capabilities to satisfy individual specifications. In the next section, we synthesize a Mixed Integer Program to find optimal group trajectories for the agents.

In the previous section, we formulated the problem of synthesizing a group trajectory that satisfies individual MTL specifications using capability-augmenting collaboration as an optimization problem (9). In this section, we detail our approach for solving (9) using a Mixed Integer Program (MIP). To do this, we first need to encode the group trajectories as decision variables and ensure that their motion is constrained as seen in (9). Next, we need to generate variables that allow us to determine the satisfaction of the CATs. Finally, we need to use these variables to solve (9).

In this subsection, we define a Mixed Integer Program (MIP) that finds a group trajectory for the agents. The discrete environment and binary and integer elements of the CAT encoding make using an MIP necessary for generating optimal group trajectories.

To begin with, we formulate MIP motion constraints for the individual agents. We define binary decision variables for motion as $z_{j,(q,q^{\prime}),k^{\prime}}\in\{0,1\},\;\forall j\in\{1,...,N_{A}\},\;(q,q^{\prime})\in E,k^{\prime}\in[0,...,T_{p}]$. If $z_{j,(q,q^{\prime}),k^{\prime}}=1$ then, agent $j$ moves from node $q$ to node $q^{\prime}$ at time $k^{\prime}$. Otherwise, a different transition is taken. This means that if $z_{j,(q,q^{\prime}),k}=1$, then $q_{j}(k)=q^{\prime}$ and $q^{\prime}$ is and element of the group trajectory $\mathbf{Q}$. The motion constraints for the trajectory generated at time-step $0$ are as follows:

Constraint (12) encodes an initial node for the agent using the MIP variables. Constraint (13) enforces that an agent may only take one transition at a time. Constraint (14) enforces that agents must either stay in place or move to an adjacent node. These three constraints combined are equivalent to the motion constraint in (9).

We determine $q_{j}(k)$ for each agent $j$ at each time step $k$, i.e. which nodes are included in $\mathbf{Q}$, as follows where $ind(q)$ retrieves the index of a node $q$:

To evaluate (9), we need to evaluate $\rho$ and $J_{j}$ in terms of our MIP variables. Evaluating these allows us to solve (9) through solving (8). To find $\rho$, we start by encoding the evaluation of CATs into MIP variables. For an individual CAT, we need to retrieve the agents in $I_{c_{aug}}$ and $I_{c_{al}}$ that are in the same node as agent $j$ using (16). We assign each node a unique index $ind(q)\in\{1,...,N_{Q}\}$ where $N_{Q}$ is the total number of nodes, i.e. $N_{Q}=|\mathcal{Q}|$. Let $\alpha^{j}_{j^{\prime},k}$ represent a binary variable that indicates if agent $j^{\prime}$ is in the same node as agent $j$ at time step $k$. We determine $\alpha^{j}_{j^{\prime},k}$ for agents $j^{\prime}$ with capabilities $c_{aug}$ and $c_{al}$ as follows:

Finally, we retrieve the number of agents with capability $c_{aug}$ and $c_{na}$ in the same node as agent $j$ as follows:

Next, we define binary variables for the components of the CAT. Let $z_{j,aug,k}\in\{0,1\}$ be a binary variable that is $1$ if there are at least $m_{aug}$ agents with capability $c_{aug}$in the same node as agent $j$ at time $k$ otherwise it is $0$. Let $z_{j,al,k}\in\{0,1\}$ be a binary variable that is $1$ if less than $m_{al}$ agents with capability $c_{al}$ are in the same node as agent $j$ at time $k$ otherwise it is $0$. We determine the value of these variables as follows:

Let $z_{j,\pi,k}\in\{0,1\}$ be a binary variable that is $1$ if agent $j$ is in a region with label $\pi$ and $0$ otherwise. Let $\mathcal{L}^{-1}(\pi)$ be the set of nodes with label $\pi$, i.e. $q\in\mathcal{L}^{-1}(\pi)\iff\pi\in\mathcal{L}(q)$. We determine the value of $z_{j,\pi,k}$ as follows:

To quantify the satisfaction of tasks $\phi_{j}$, we use $\rho(\mathbf{O}_{j},\phi_{j},k)$. We find $\rho(\mathbf{O}_{j},\phi_{j},k)$ as a function of our decision variables as follows:

We can calculate the individual costs, $J_{j}$, using the binary variables as follows:

Note that this returns the same value as (7). The constraints in (III-B)-(17) provide us with infrastructure to determine the satisfaction of individual CATs. We use (III-B)-(19) to evaluate the satisfaction of tasks. Using (20) and (21) we can evaluate agent performance as defined in (8). Finally, (12)-(14) provide the motion constraints found in (9). This accounts for all the pieces required to solve for an optimal group trajectory $\mathbf{Q}^{*}$ as defined in (9).

The algorithm that formalizes a procedure for generating group trajectories for a team of heterogeneous agents is given in Algorithm 1

In our case study, we focus on the system with one aerial and two ground agents that we used as an example in the Problem Statement.We use this case study to demonstrate the benefit of using our encoding for capability-augmenting collaboration. Each agent starts in the same node near the environment’s center. The aerial agent has an index of $1$ and the ground robots have indices of $2$ and $3$.

In this case study, we use an $M$ value of $M=50$ when solving (9). The initial node for each agent is the third row and third column of the environment shown in Figure 1. For the three-agent case, we found a solution to this problem in an average of $5.43s$ for thirty trials. Each agent completed its task in every trial The average movement for all agents across all trials was $3.33$ transitions. This means that the average individual agent performance was $46.67$. An example solution is shown in Figure 3. A solver not using CATs, i.e. task satisfaction is solely determined by the labels of the agents’ nodes, could only find solutions for two of the three agents. The motion cost of $2$ meaning the average individual agent performance was $14.67$. The average runtime for the solver not using CATs was $0.41s$. This shows a clear improvement in agent performance when using CATs in this case. However, the runtime using CATs was higher.

Additionally, we increased the number of agents to 5 with 2 aerial agents and 3 ground agents. For this case, we experienced an average runtime of $67.81s$ over thirty trials. Once again each agent finished its task in every trial when using CATs. We experience an average motion of $3.2$ transitions for each agent across all trials. This means that the average agent performance was $46.80$. For the solver not using CATs, only three of the five agents satisfied their tasks and the average motion cost was $1.8$. This means the average individual agent performance was $8.20$. We experienced improvements in agent performance with the increased number of agents when using CATs.

To further investigate the performance of our formulation, we use the tasks given in (10) and (11) and randomize our environment. We generate increasingly large environments to show the effects of CATs as the environment increases in size. We compare this to a system that does not use capability-augmenting collaboration when solving for a trajectory. The results for agent performance are shown in Figure 4. This figure shows the individual agent performance metric defined in (8). These results demonstrate that the use of CATs consistently results in improved individual agent performance. As the environment becomes larger, the desirable nodes (“Scenic”, “Upload”, and “Goal”) become more spread out, making tasks more difficult to satisfy. The use of capability-augmenting collaboration improved the ability of agents to satisfy their tasks in these trials by allowing them to use each other’s capabilities when the desirable nodes are harder to reach.