Formal Specification of Continuum Deformation Coordination

TL;DR

This paper formally defines continuum deformation coordination for multi-agent systems in obstacle-rich environments using linear temporal logic, ensuring safety and liveness through precise conditions.

Contribution

It introduces a formal specification framework for continuum deformation coordination incorporating safety and liveness in complex environments.

Findings

Safety conditions for collision avoidance and containment are established.

Liveness ensures the system reaches the desired formation.

Formal LTL specifications enable rigorous verification of multi-agent coordination.

Abstract

Continuum deformation is a leader-follower multiagent cooperative control approach. Previous work showed a desired continuum deformation can be uniquely defined based on trajectories of d +1 leaders in a d-dimensional motion space and acquired by followers through local inter-agent communication. This paper formally specifies continuum deformation coordination in an obstacle-laden environment. Using linear temporal logic (LTL), continuum deformation liveness and safety requirements are defined. Safety is prescribed by providing conditions on (i) agent deviation bound, (ii) inter-agent collision avoidance, (iii) agent containment, (iv) motion space containment, and (v) obstacle collision avoidance. Liveness specifies a reachability condition on the desired final formation.

Tables

Table 1. Table I: Communication weights w i , i 1 subscript 𝑤 𝑖 subscript 𝑖 1 w_{i,i_{1}} , w i , i 2 subscript 𝑤 𝑖 subscript 𝑖 2 w_{i,i_{2}} , and w i , i 3 subscript 𝑤 𝑖 subscript 𝑖 3 w_{i,i_{3}}

$i$	$i_1$	$i_2$	$i_3$	$w_{i,i_1}$	$w_{i,i_2}$	$w_{i,i_3}$
$4$	$1$	$7$	$10$	$0.60$	$0.20$	$0.20$
$5$	$2$	$8$	$9$	$0.60$	$0.20$	$0.20$
$6$	$3$	$9$	$10$	$0.60$	$0.20$	$0.20$
$7$	$4$	$8$	$10$	$0.40$	$0.36$	$0.24$
$8$	$5$	$7$	$9$	$\frac{1}{3}$	$\frac{1}{3}$	$\frac{1}{3}$
$9$	$5$	$6$	$8$	$0.31$	$0.42$	$0.27$
$10$	$4$	$6$	$7$	$0.35$	$0.29$	$0.36$

Equations

$$\mathbf{\Lambda }\left({\mathbf{a}}_1,\cdots ,{\mathbf{a}}_{d+1}\right)=\mathrm{rank}\left(\left[\begin{array}{ccc}{\mathbf{a}}_2-{\mathbf{a}}_1& \cdots & {\mathbf{a}}_{d+1}-{\mathbf{a}}_1\end{array}\right]\right)=d,$$

$$\mathbf{\Omega }\left({\mathbf{a}}_1,\cdots ,{\mathbf{a}}_{d+1},\mathbf{c}\right)={\left[\begin{array}{ccc}{\mathbf{a}}_1& \cdots & {\mathbf{a}}_{d+1}\\ 1& \cdots & 1\end{array}\right]}^{-1}\left[\begin{array}{c}\mathbf{c}\\ 1\end{array}\right].$$

$$\left[\begin{array}{c}{\alpha }_1\\ ⋮\\ {\alpha }_{d+1}\end{array}\right]=\mathbf{\Omega }\left({\mathbf{a}}_1,\cdots ,{\mathbf{a}}_{d+1},\mathbf{c}\right).$$

$${\mathbf{r}}_i^{\mathrm{HT}}\left(t\right)=\mathbf{Q}\left(t,t_0\right){\mathbf{r}}_i^0+\mathbf{d}\left(t,t_0\right),$$

$$\forall t,\mathbf{\Lambda }\left({\mathbf{r}}_1^{\mathrm{HT}},\cdots ,{\mathbf{r}}_{d+1}^{\mathrm{HT}}\right)=d.$$

$$\forall t,\left[\begin{array}{c}\mathrm{vec}\left({\mathbf{Q}}^T\right)\\ \mathbf{d}\end{array}\right]=\left[\begin{array}{cc}{\mathbf{I}}_d\otimes \mathbf{P}(t_0)& {\mathbf{I}}_d\otimes 1_{d\times 1}\end{array}\right]\mathrm{vec}\left(\mathbf{P}(t)\right),$$

$$\mathbf{P}(t)=\left[\begin{array}{ccc}{r}_{1,1}^{\mathrm{HT}}& \cdots & r_{1,d}^{\mathrm{HT}}\\ ⋮& ⋮& ⋮\\ r_{d+1,d}^{\mathrm{HT}}& \cdots & r_{d+1,d}^{\mathrm{HT}}\end{array}\right]\in {\mathbb{R}}^{\left(d+1\right)\times d}.$$

$$\forall t\in [t_0,t_f],\forall i\in \mathcal{V},\mathbf{\Omega }\left({\mathbf{r}}_1^{\mathrm{HT}},\cdots ,{\mathbf{r}}_{d+1}^{\mathrm{HT}},{\mathbf{r}}_i^{\mathrm{HT}}\right)={\mathbf{\Omega }}_{i,0},$$

$$\forall i\in \mathcal{V},{\mathbf{\Omega }}_{i,0}=\mathbf{\Omega }\left({\mathbf{r}}_1^0,\cdots ,{\mathbf{r}}_{d+1}^0,{\mathbf{r}}_i^0\right)\in {\mathbb{R}}^{d+1}.$$

$$\forall i\in {\mathcal{V}}_F,{\mathbf{\Omega }}_{i,0}>0.$$

$${\left[\begin{array}{ccc}{w}_{i,i_1}& \cdots & w_{i,i_{d+1}}\end{array}\right]}^T=\mathbf{\Omega }\left({\mathbf{r}}_{i_1}^0,\cdots ,{\mathbf{r}}_{i_{d+1}}^0,{\mathbf{r}}_i^0\right).$$

$$\frac{{\mathrm{d}}^2{\mathbf{r}}_i}{\mathrm{d}{t}^2}={\mathbf{u}}_i,$$

$$\begin{array}{rl}& {\mathbf{u}}_i=\{\begin{array}{ll}{\ddot{\mathbf{r}}}_i^{\mathrm{HT}}\left(\mathrm{given}\right)& i\in {\mathcal{V}}_L\\ {\beta }_v{\sum }_{j\in {\mathcal{N}}_i}{w}_{i,j}\left({\dot{\mathbf{r}}}_j-{\dot{\mathbf{r}}}_i\right)+{\beta }_r{\sum }_{j\in {\mathcal{N}}_i}{w}_{i,j}\left({\mathbf{r}}_j-{\mathbf{r}}_i\right)& i\in {\mathcal{V}}_F.\end{array}\end{array}$$

$$e$$

$$\varphi$$

$$\perp$$

$${\varphi }_1\wedge {\varphi }_2$$

$$S(t)$$

$$S(t^{\prime })\models {\varphi }_2$$

$$\framebox{$\displaystyle\bigwedge_{i\in\mathcal{V}}\Box\left(\|\mathbf{r}_{i}-\mathbf{r}^{\rm HT}_{i}\|_{2}^{2}\leq\delta^{2}\right),$}$$

$$\forall i\in {\mathcal{V}}_F,\forall t\ge t_0{\mathbf{r}}_i\in \mathcal{T}({\mathbf{r}}_1^{\mathrm{HT}},\cdots ,{\mathbf{r}}_{d+1}^{\mathrm{HT}})$$

$$\framebox{$\displaystyle\bigwedge_{i\in\mathcal{V}_{F}}\Box\left(\mathbf{\Omega}\left(\mathbf{r}^{\rm HT}_{1},\cdots,\mathbf{r}^{\rm HT}_{{d}+1},\mathbf{r}_{i}\right)\geq 0\right).$}$$

$$\framebox{$\displaystyle\bigwedge_{i,j\in\mathcal{V},\leavevmode\nobreak\ i\neq j}\Box\left(\|\mathbf{r}_{i}-\mathbf{r}_{j}\|_{2}^{2}\geq(2\epsilon)^{2}\right).$}$$

$$\forall i\in \mathcal{V},\forall t\ge t_0{\mathbf{r}}_i\in \mathbf{B}$$

$$\begin{split}\framebox{$\displaystyle\bigwedge_{i\in\mathcal{V}}\Box\bigvee_{k=1}^{m_{B}}\left(\mathbf{\Omega}\left(\mathbf{b}_{k,1},\cdots,\mathbf{b}_{k,{d}+1},\mathbf{r}_{i}\right)\geq 0\right).$}\\ \end{split}$$

$$\forall i\in \mathcal{V},\forall t\ge t_0,\square ({\mathbf{r}}_i\notin \mathcal{O}).$$

$$\begin{split}\framebox{$\displaystyle\bigwedge_{i\in\mathcal{V}}\Box\left(\bigwedge_{k=1}^{m_{O}}\neg\left(\mathbf{\Omega}\left(\mathbf{o}_{k,1},\cdots,\mathbf{o}_{k,m_{B}},\mathbf{r}_{i}\right)\geq 0\right)\right).$}\end{split}$$

$$\framebox{$\displaystyle\Diamond\Box\bigwedge_{i\in\mathcal{V}}\left(\|\mathbf{r}_{i}-\mathbf{r}_{i}^{f}\|_{2}^{2}\leq\varepsilon^{2}\right).$}$$

$${\delta }_{\max }=\min \left\{\frac{1}{2}\left(D_B-2ϵ\right),\left(D_S-ϵ\right)\right\}$$

$${\lambda }_{\min }=\frac{\delta +ϵ}{{\delta }_{\max }+ϵ}.$$

Full text

I Introduction

From package delivery and autonomous taxis to military applications, Unmanned Aerial Vehicles (UAV) are changing our daily lives. Some applications however cannot be achieved by a single UAV, but need a swarm of cooperating UAVs forming a Multi-Agent System (MAS). Examples of such applications are surveillance, formation flight, and traffic control. MAS perform critical tasks, and it is becoming increasingly important to formally specify and verify the correctness of their behavior, in terms of both safety and liveness requirements. In this paper we are primarily interested in formation flying. We treat MAS evolution as a continuum deformation [1], and formally specify its safety and liveness requirements.

Multi-agent system coordination applies methods such as consensus [2, 3] with application to distributed motion control [4, 5], sensing [6, 7], medical systems [8], and smart grids [9, 10]. For containment control [11, 12] multiple leaders guide the MAS toward a target shape using consensus to update positions [13, 11] under fixed and switching communication topologies [14, 15]. Directed communication topologies [16, 17], event-based containment control [18, 14], and finite-time containment control [19] have been formulated. Formal specification and verification of multi-agent systems have received considerable attention [20, 21, 22, 23], and our aim is to extend that work to the context of continuum deformation. Containment control assures asymptotic convergence to a desired configuration inside the convex region prescribed by leaders but has two limitations: (i) followers are not assured to remain inside the moving convex region defined by leader positions during transition; and (ii) inter-agent collision avoidance cannot be guaranteed for an arbitrary initial agent distribution. Continuum deformation extends containment control theory by prescribing a homogeneous mapping that guarantees inter-agent collision avoidance and that followers remain within the leader-defined boundary [1, 24]. In a continuum deformation coordination, inter-agent distances can aggressively change while no two particles collide. This property can advance swarm coordination maneuverability and agility, and allows a large-scale MAS to safely negotiate narrow channels in obstacle-laden environments.

As its main contribution, this paper formally specifies safety and liveness for the coordination of continuum deformation of an MAS with a large number of agents (Fig. 1). Using triangulation and tetrahedralization, safety conditions are defined to assure obstacle collision avoidance, inter-agent collision avoidance, and motion space containment in 2-dimensional and 3-dimensional continuum deformations. This paper also formally specifies a liveness condition that assures continuum deformation is possible given an initial MAS configuration and a motion space obstacle geometry.

This paper is organized as follows: In Section II, preliminaries in triangulation and tetrahedralization, continuum deformation coordination, graph theory, linear temporal logic, and MAS collective dynamics are reviewed. Continuum deformation formal specification in Section III is followed by sufficient safety conditions in Section IV. Simulation results and conclusions are presented in Sections V and VI, respectively.

II Preliminary Notions

II-A Triangulation and Tetrahedralization

To determine whether an agent stays in its designated motion space and does not collide with any obstacle, we need to compute whether this agent is inside or outside a given ${d}$-dimensional polytope. Our approach creates a partition of the polytope into a number of ${d}$-simplexes (i.e., a triangle for $d=2$ or a tetrahedron for $d=3$), thereby reducing the problem to checking whether our agent stays in one of the simplexes. A $d$-simplex $\mathcal{T}$ is defined as the non-zero volume specified by points $\mathbf{a}_{1},\ldots,\mathbf{a}_{d+1}\in\mathbb{R}^{d}$. Note that $\mathbf{a}_{1},\ldots,\mathbf{a}_{d+1}\in\mathbb{R}^{d}$ form a valid $d$-simplex if and only if the following rank condition is satisfied:

[TABLE]

If (1) is satisfied, we can define vector operator $\Omega$ given an arbitrary vector $\mathbf{c}$ and $\mathbf{a}_{1},\ldots,\mathbf{a}_{d+1}$:

[TABLE]

Note that $\Omega\left(\mathbf{a}_{1},\cdots,\mathbf{a}_{{d}+1},\mathbf{c}\right)\in\mathbb{R}^{d+1}$, let

[TABLE]

As shown in Fig. 2, a 2-dimension motion space (${d}=2$) can be divided into $10$ regions based on the signs of $\alpha_{1}$, $\alpha_{2}$, and $\alpha_{3}$. Similarly, a 3-dimension motion space can be divided into $55$ regions based on the signs of $\alpha_{1}$, $\alpha_{2}$, $\alpha_{3}$ and $\alpha_{4}$. In general, we can decide whether $\mathbf{c}$ is inside or outside a simplex based on the signs of $\alpha_{1},\ldots,\alpha_{d+1}$:

Proposition 1

*The point $\mathbf{c}$ is positioned inside the (open) simplex defined by $\mathbf{a}_{1}$, $\cdots$, $\mathbf{a}_{{d}+1}$ if and only if $\mathbf{\Omega}\left(\mathbf{a}_{1},\cdots,\mathbf{a}_{{d}+1},\mathbf{c}\right)>\mathbf{0}$. *

We use the term “containment” when a point $\mathbf{c}$ is inside a $d$-polytope, which typically represents a simplex of leaders, the motion space or an obstacle.

II-B Continuum Deformation Definition

Consider an MAS consisting of $N$ agents identified by unique index numbers $\mathcal{V}=\{1,\cdots,N\}$. Agents $1$ through ${d}+1$ are leaders and the remaining agents are followers acquiring the desired coordination through local communication, e.g. $\mathcal{V}_{L}=\{1,\cdots,{d}+1\}$ is the set of leaders and $\mathcal{V}_{F}=\{{d}+2,\cdots,N\}$ is the set of followers. We denote by ${\mathbf{r}}_{i}\left(t\right)$ the actual position of agent $i$ at time $t$, and by $\mathbf{r}^{\rm HT}_{i}\left(t\right)$ its desired position at time $t$. The $j$-th coordinate of ${\mathbf{r}}_{i}$ is denoted as $r_{i,j}$, and the $j$-th coordinate of $\mathbf{r}^{\rm HT}_{i}$ is denoted as $r^{\rm HT}_{i,j}$. Let $\mathbf{r}_{i}^{0}$ and $\mathbf{r}_{i}^{f}$ denote initial and final positions of agent $i\in\mathcal{V}$, respectively. The desired position of agent $i$ is defined by:

[TABLE]

where $\mathbf{r}_{i}^{0}=\mathbf{r}^{\rm HT}_{i}\left(t_{0}\right)$, ${\mathbf{r}^{\rm HT}_{i}}^{f}=\mathbf{r}^{\rm HT}_{i}\left(t_{f}\right)$ ($i\in\mathcal{V}$), $t_{0}$ and $t_{f}$ denote initial and final time, $\mathbf{Q}\left(t,t_{0}\right)\in\mathbb{R}^{{d}\times{d}}$ is the Jacobian matrix, $\mathbf{Q}\left(t_{0},t_{0}\right)=\mathbf{I}_{d}\in\mathbb{R}^{{d}\times{d}}$ is the identity matrix, $\mathbf{d}\left(t,t_{0}\right)\in\mathbb{R}^{{d}\times 1}$ is the rigid-body displacement vector, and $\mathbf{d}\left(t_{0},t_{0}\right)=\mathbf{0}\in\mathbb{R}^{{d}\times 1}$. The affine transformation (3) is called homogeneous transformation in continuum mechanics [25].

In a homogeneous transformation coordination, leaders form a ${d}$-dimensional leading polytope at any time $t$, therefore

[TABLE]

Because homogeneous transformation is a linear mapping, $\mathbf{Q}$ and $\mathbf{D}$ elements are uniquely related to leader position components by

[TABLE]

where ”$\otimes$” is the Kronecker product, $\mathbf{1}_{d}\in\mathbb{R}^{\left({d}+1\right)\times 1}$ is the one-entry matrix, and

[TABLE]

$\mathbf{\Omega}\left(\mathbf{r}^{\rm HT}_{1}\left(t\right),\cdots,\mathbf{r}^{\rm HT}_{{d}+1}\left(t\right),\mathbf{r}^{\rm HT}_{i}\left(t\right)\right)\in\mathbb{R}^{\left({d}+1\right)\times 1}$ remains time-invariant at any time $t\in[t_{0},t_{f}]$:

[TABLE]

is time-invariant, where

[TABLE]

Assumption: This paper assumes follower agents are positioned inside the leading simplex at initial time $t_{0}$:

[TABLE]

II-C Continuum Deformation Acquisition

Assume directed graph $\mathcal{G}=\mathcal{G}\left(\mathcal{V},\mathcal{E}\right)$ defines a fixed inter-agent communication topology, $\mathcal{V}$ is the node set and $\mathcal{E}\subset\mathcal{V}\times\mathcal{V}$ is the edge set. Follower $i\in\mathcal{V}_{F}$ communicates with ${d}+1$ in-neighbor agents defined by set $\mathcal{N}_{i}=\{i_{1},\cdots,i_{{d}+1}\}\subset\mathcal{V}$. It is assumed that $\mathbf{\Lambda}\left(\mathbf{r}_{i_{1},0},\cdots,\mathbf{r}_{i_{{d}+1},0}\right)={d}$ ($\forall i\in\mathcal{V}_{F}$), so in-neighbor agents of follower $i$ form an ${d}$-dimensional simplex at initial time $t_{0}$. Follower inter-agent communications are weighted and obtained from

[TABLE]

Note that $w_{i,i_{k}}$ is the communication weight between follower $i\in\mathcal{V}_{F}$ and in-neghbpor agent $i_{k}\in\mathcal{N}_{i}$ ($k=1,\cdots,d+1$).

II-D MAS Collective Dynamics Model

Let $\mathbf{r}_{i}\in\mathbb{R}^{{d}\times 1}$ denote actual position of agent $i\in\mathcal{V}$.

[TABLE]

where

[TABLE]

For continuum deformation communication weights are consistent with agents’ positions at $t_{0}$ and assigned by Eq. (7).

II-E Temporal Logic

Temporal Logic (TL) can capture temporal behavior of a dynamical system. In this paper we use a logic based on LTL*-X* [26]. The logic LTL*-X* is a flavour of Linear Temporal Logic without the Next operator X (sometimes written $\circ$), which makes it more adapted to reasoning about continuous-time systems. Since we are reasoning about an explicit system, we make our atomic formulas concrete, as comparisons of expressions. Our logic uses two syntactic categories: expressions $e$ and propositions $\phi$. An expression $e$ can be a constant $c$, a state variable representing the $j$-th coordinate of the actual position of agent $j$, ${r}_{i,j}$, a state variable representing the $j$-th coordinate of the desired position of agent $j$, ${r}^{\rm HT}_{i,j}$, as well as a multiplication $e_{1}\times e_{2}$, addition $e_{1}+e_{2}$, subtraction $e_{1}-e_{2}$, or division $e_{1}/e_{2}$ of two expressions. A formula can be True $\top$, a comparison of two expressions $e_{1}\leq e_{2}$, or a disjunction $\phi_{1}\lor\phi_{2}$, negation $\lnot\phi$ or until $\phi_{1}\mathcal{U}\phi_{2}$ of two formulas.

[TABLE]

We call atomic formulas the formulas of the form $e\leq e$. As is usual in LTL, we define the operators False $\bot$, conjunction $\land$, always $\Box$ and eventually $\Diamond$ as:

[TABLE]

For any time $t\geq 0$, the state $\mathcal{S}(t)$ of our system is a function giving the valuation of every state variable: $\mathcal{S}(t):\{{r}_{1,1},\ldots,{{r}}_{N,{d}},{r}^{\rm HT}_{1,1},\ldots,{r}^{\rm HT}_{N,{d}}\}\rightarrow\mathbb{R}$ Given such a state $\mathcal{S}(t)$ for the valuation of state variables, an expression $e$ can be evaluated in the usual way to a real number that we write $\mathcal{S}(t)(e)$. The satisfaction of formula $\phi$ in state $\mathcal{S}(t)$ (i.e., at time $t$) is then given by:

[TABLE]

For convenience, we write $e^{2}$ for the expression $e\times e$; $\|\mathbf{r}_{i}-\mathbf{r}^{\rm HT}_{i}\|_{2}^{2}$ for the expression $({r}_{i,1}-{r}_{i,1})^{2}+\cdots+({r}_{i,{d}}-{r}^{\rm HT}_{i,{d}})^{2}$; and $\mathbf{\Omega}\left(\mathbf{r}^{\rm HT}_{1},\cdots,\mathbf{r}^{\rm HT}_{{d}+1},\mathbf{r}_{i}\right)$ as in Equation 2 (Section II-A).

III Formal Specification

This paper’s first objective is to formally specify safety requirements for continuum deformation. MAS continuum deformation is considered safe if the following requirements are satisfied: (1) Bounded deviation, (2) Follower containment guarantee, (3) Inter-agent collision avoidance, (4) Motion-space containment, and (5) Obstacle collision avoidance.

The paper’s second objective is to formally specify a liveness condition: agent desired final position reachability.

Definition 1 (Motion Space): The motion space, denoted by $\mathbf{B}\subset\mathbb{R}^{d}$, is finite and convex. Let $\mathbf{B}$ enclose $m_{B}$ simplexes $\mathbf{B}_{1}$, $\cdots$, $\mathbf{B}_{m_{B}}$, e.g. $\bigcup_{i=1}^{m_{B}}\mathbf{B}_{i}\subset\mathbf{B}$. $\mathbf{B}_{i}$ is a ${d}$-dimensional simplex with vertices at $\mathbf{b}_{i,1}\in\mathbb{R}^{{d}\times 1}$, $\cdots$ $\mathbf{b}_{i,{d}+1}\in\mathbb{R}^{{d}\times 1}$.

Definition 2 (Obstacle): Let $\mathcal{O}\subset\mathbb{R}^{d}$ be a finite set defining motion space obstacles. Let $\mathcal{O}$ encompass $m_{O}$ simplex es $\mathbf{O}_{1}$, $\cdots$, $\mathbf{O}_{m_{O}}$, e.g. $\mathcal{O}\subset\bigcup_{i=1}^{m_{O}}\mathbf{O}_{i}$. $\mathbf{O}_{i}$ is an ${d}$-dimensional simplex with vertices $\mathbf{o}_{i,1}\in\mathbb{R}^{{d}\times 1}$, $\cdots$ $\mathbf{o}_{i,{d}+1}\in\mathbb{R}^{{d}\times 1}$.

III-0a Safety Condition 1: Bounded Vehicle Deviation

Deviation of every agent from continuum deformation must not exceed $\delta$, i.e., the actual position $\mathbf{r}_{i}$ ($i\in\mathcal{V}$) of every agent must stay within $\delta$ of its desired position $\mathbf{r}^{HT}_{i}$. This requirement can be expressed as:

[TABLE]

where $\delta$ is constant and $\|\cdot\|_{2}$ is the 2-norm symbol.

III-0b Safety Condition 2: Follower Containment Condition

Follower $i\in\mathcal{V}_{F}$ must be inside the leading simplex at any time $t$. This condition can be expressed as:

[TABLE]

which can be expressed in our logic using the function $\mathbf{\Omega}$ as:

[TABLE]

III-0c Safety Condition 3: Inter-Agent Collision Avoidance

Assume every agent is enclosed by a ball of radius $\epsilon$. Collision avoidance between any two different agents $i$ and $j$ is satisfied, if and only if:

[TABLE]

III-0d Safety Condition 4: Motion Space Containment

Motion space containment is satisfied, if

[TABLE]

which can be expressed in our logic using the function $\mathbf{\Omega}$ as:

[TABLE]

Eq. ($\psi_{4}$) ensures existence of a simplex $\mathbf{B}_{i}\subset\mathbf{B}$ enclosing leader $i\in\mathcal{V}_{L}$ at any time $t$.

III-0e Safety Condition 5: Obstacle Collision Avoidance

Obstacle collision avoidance is satisfied if

[TABLE]

which can be expressed in our logic using the function $\mathbf{\Omega}$ as:

[TABLE]

Eq. ($\psi_{5}$) ensures every agent $i\in\mathcal{V}$ is outside the obstacle zone defined by simplexes $\mathbf{O}_{1}$, $\cdots$, $\mathbf{O}_{m_{O}}$.

III-0f Liveness Condition 6: Final Formation Rechability

Given agent desired final positions $\mathbf{r}_{1}^{f}$, $\cdots$, $\mathbf{r}_{N}^{f}$, the liveness condition is defined by:

[TABLE]

IV Sufficient Conditions

IV-A Inter-Agent Collision Avoidance and Agent Containment

It is computationally expensive to ensure inter-agent collision avoidance and follower containment using Eqs. ($\psi_{3}$) and ($\psi_{2}$). We can instead use the sufficient conditions provided in Theorem 1 to guarantee these two MAS safety constraints at less computational cost.

Theorem 1

[1]** Let $D_{B}$ denote minimum separation distance between two agents at initial time $t_{0}$, and let $D_{S}$ denote the minimum boundary distance at initial time $t_{0}$. Define

[TABLE]

and

[TABLE]

Inter-agent collision avoidance and agent containment are guaranteed, if the eigenvalues of pure deformation matrix $\mathbf{U}_{D}=\left(\mathbf{Q}^{T}\mathbf{Q}\right)^{1\over 2}$, denoted $\lambda_{1}$, $\lambda_{2}$, and $\lambda_{3}$, satisfy

[TABLE]

*and no agent deviation exceeds $\delta$ at any time $t$. *

Proof:

[1] Let $m_{1}$ and $m_{2}$ denote two points of the leading simplex that has the minimum separation distance at $t_{0}$. If $\delta_{\mathrm{max}}={1\over 2}\left(D_{B}-\epsilon\right)$ then $m_{1},m_{2}\in\mathcal{V}$ are two agents (Fig. 3(c)). Otherwise, $m_{1}\in\mathcal{V}_{F}$ is the index number of a follower and $m_{2}$ denotes a point on the boundary of the leading simplex having minimum distance from $m_{1}$ (Fig. 3(b)):

[TABLE]

where

[TABLE]

Considering Eq. (3),

[TABLE]

Assume

[TABLE]

then, inter-agent collision avoidance is ensured if inequality ($\psi_{1}$) is satisfied. This implies that

[TABLE]

In other words, inter-agent collision avoidance is avoided if

[TABLE]

Consequently, inter-agent collision is avoided if inequality (12) is satisfied. Because $\mathbf{Q}$ is nonsingular at any time $t$ and $\mathbf{Q}(t_{0},t_{0})=\mathbf{I}_{d}$, $\mathbf{U}_{D}$ eigenvalues are always positive. Therefore, Eq. (12) is satisfied.

∎

IV-B Motion Space Containment

If safety condition $\psi_{2}$ is satisfied, then motion space containment is guaranteed by ensuring leaders remain inside the motion space $\mathbf{B}$. Formally, given the formula:

[TABLE]

we have:

Theorem 2

If $\psi_{2}\land\psi_{7}$ is satisfied, then $\psi_{4}$ is satisfied.

IV-C Obstacle Collision Avoidance

If safety condition $\psi_{2}$ is satisfied, then obstacle collision avoidance is guaranteed by ensuring leaders do not collide with obstacles. Formally, given the formula:

[TABLE]

we have:

Theorem 3

If $\psi_{2}\land\psi_{8}$ is satisfied, then $\psi_{5}$ is satisfied.

Proofs of Theorems 2 and 3 are adapted from [1].

V Simulation Results

Consider an MAS with $N=10$ agents evolving in 2 dimensions (${d}=2$). Agents $1$, $2$, and $3$ are leaders; the remaining agents are followers. Inter-agent communication is defined by the Fig. 4 graph, and follower communication weights are listed in Table I. Follower communication weights are consistent with the initial formation and assigned by Eq. (7). Fig. 4 also shows MAS initial and final formations. $\mathbf{B}=\mathbf{B}_{1}\bigcup\mathbf{B}_{2}\bigcup\mathbf{B}_{3}$ defines the motion space, and $\mathcal{O}=\bigcup_{k=1}^{4}\mathbf{O}_{4}$ defines obstacles in $\mathbf{B}$.

The paper assumes all agents are identical with $\beta_{r}=2$ and $\beta_{v}=4$. Agent positions are plotted versus time in Figs. 5 (a) and 5 (b) with $t\in[0,227.5],\leavevmode\nobreak\ t_{0}=0s,\leavevmode\nobreak\ t_{f}=227.5s$.

Satisfaction of Safety Condition 1: Fig. 5(c) plots deviation of every follower versus time confirming that no follower exceeds $\delta=0.2286m$ at any time $t\in[t_{0},t_{f}]s$.

Satisfaction of Safety Conditions 2 and 3: Given MAS initial formation, $D_{B}=2.7348m$ and $D_{S}=1.5996m$ are the minimum separation and boundary distances. The paper assumes that each agent is enclosed by a ball with radius $\epsilon=0.25m$, thus, $\delta_{\mathrm{max}}$ $\delta_{\mathrm{ma}}=1.1174m$. Given $\delta=0.2286$, $\epsilon=0.25m$, and $\delta_{\mathrm{ma}}=1.1174m$, $\lambda_{\mathrm{min}}=0.35$ is computed by Eq. (11). As shown in Fig. 6, $\mathbf{U}_{D}$ eigenvalues are greater than $\lambda_{\mathrm{min}}$ at any time $t$, hence, safety condition 2 is satisfied.

Satisfaction of Safety Conditions 4 and 5: Leader paths are plotted in Figs. 7 (a-c). As shown, motion containment and obstacle collision avoidance conditions are satisfied.

Satisfaction of Necessary Condition 6: As shown in Fig. 6, $\|\mathbf{r}_{i}-\mathbf{r}_{i}^{\mathrm{HT}}\|$ tends to zero at final time $t_{f}$, therefore, the liveness condition 6 is satisfied.

Acknowledgements

This work was supported in part by National Science Foundation Grant CNS 1739525.

VI Conclusion

In this paper we formally specified continuum deformation coordination in a ${d}$-dimensional motion space. Using triangulation and tetrahedralization, we developed safety and liveness conditions for continuum deformation. We constructed Linear Temporal Logic (LTL) formulae to check the validity of inter-agent and obstacle collision avoidance as well as agent and motion-space containment. We demonstrated validity of the method with simulation results. The paper shows how a large-scale continuum deformation satisfies the liveness and safety conditions we developed. This formal definition supports efficient specification and computational overhead when designing and deploying a large-scale MAS.