Formal Specification of Continuum Deformation Coordination
Hossein Rastgoftar Jean-Baptiste Jeannin Ella Atkins
eess.SY cs.SY




Momentum-Net: Fast and convergent 
 
iterative neural network for inverse problems

    Il Yong Chun, Member, IEEE, Zhengyu Huang^∗, Hongki Lim^∗, Student Member, IEEE, 
 and Jeffrey A. Fessler, Fellow, IEEE





The authors indicated by asterisks (^∗) contributed equally to this work.
This work is supported in part by the Keck Foundation, NIH U01 EB018753, NIH R01 EB023618, NIH R01 EB022075, and NSF IIS 1838179.
Il Yong Chun was with the Department of Electrical Engineering and Computer Science, The University of Michigan, Ann Arbor, MI 48019 USA,
and is now with the Department of Electrical Engineering, the University of Hawai'i at Mānoa, Honolulu, HI 96822 USA (email: iychun@hawaii.edu).
Zhengyu Huang, Hongki Lim, and Jeffrey A. Fessler are with the Department of Electrical Engineering and Computer Science, The University of Michigan, Ann Arbor, MI 48019 USA (email: 
zyhuang@umich.edu; hongki@umich.edu; fessler@umich.edu).
This paper has appendices. The prefix “A” indicate the numbers in section, theorem, equation, figure, table, and footnote in the appendices.
This paper was presented in part at the Allerton Conference on Communication, Control, and Computing, Monticello, IL, USA, in Oct. 2018.


    
===============================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================================

empty
empty




Continuum deformation is a leader-follower multi-agent cooperative control approach. Previous work showed a desired continuum deformation can be uniquely defined based on trajectories of +1 leaders in a -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.






§ 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 <cit.>, and formally specify its safety and liveness requirements.


Multi-agent system coordination
applies methods such as consensus <cit.> 
with application to distributed motion control <cit.>, sensing <cit.>, medical systems <cit.>, and smart grids <cit.>.  
For containment control <cit.> multiple leaders guide the MAS toward a target shape using consensus to update positions <cit.>  under fixed and switching communication topologies  <cit.>. 
Directed communication topologies <cit.>, event-based containment control <cit.>, and finite-time containment control  <cit.> have been formulated.
Formal specification and verification of multi-agent systems have received considerable attention <cit.>, 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 <cit.>. 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. <ref>). 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 <ref>, 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  <ref> is followed by sufficient safety conditions in  Section <ref>.


Simulation results and conclusions are presented in Sections <ref> and <ref>, respectively.


§ PRELIMINARY NOTIONS





 §.§ 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 -dimensional polytope. Our approach creates a partition of the polytope into a number of -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 𝒯 is defined as the non-zero volume specified by points 𝐚_1,…,𝐚_d+1∈ℝ^d. Note that 𝐚_1,…,𝐚_d+1∈ℝ^d form a valid d-simplex if and only if the following rank condition is satisfied:


    Λ(𝐚_1,⋯,𝐚_+1)=rank([  𝐚_2-𝐚_1        ⋯ 𝐚_+1-𝐚_1 ])=d,
























If (<ref>) is satisfied, we can define vector operator Ω given an arbitrary vector 𝐜 and 𝐚_1,…,𝐚_d+1:


    Ω(𝐚_1,⋯,𝐚_+1,𝐜)=
        [  𝐚_1    ⋯ 𝐚_+1;    1    ⋯    1;      ]
        ^-1[ 𝐜; 1 ]
        .


Note that  Ω(𝐚_1,⋯,𝐚_+1,𝐜)∈ℝ^d+1, let

    [  α_1;    ⋮; α_+1 ]=
    Ω(𝐚_1,⋯,𝐚_+1,𝐜).




As shown in Fig. <ref>, a 2-dimension motion space (=2) can be divided into 10 regions based on the signs of α_1, α_2, and α_3.















Similarly, a 3-dimension motion space can be divided into 55 regions based on the signs of α_1, α_2, α_3 and α_4. In general, we can decide whether 𝐜 is inside or outside a simplex based on the signs of α_1,…,α_d+1:












The point 𝐜 is positioned inside the (open) simplex defined by 𝐚_1, ⋯, 𝐚_+1 if and only if  Ω(𝐚_1,⋯,𝐚_+1,𝐜)> 0. 





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







 §.§ Continuum Deformation Definition

Consider an MAS consisting of N agents identified by unique index numbers 𝒱={1,⋯,N}.   Agents 1 through +1 are leaders and the remaining agents are followers acquiring the desired coordination through local communication, e.g. 𝒱_L={1,⋯,+1} is the set of leaders and 𝒱_F={+2,⋯,N} is the set of followers. 
We denote by 𝐫_i(t) the actual position of agent i at time t, and by 𝐫_i(t) its desired position at time t.
The j-th coordinate of 𝐫_i is denoted as r_i,j, and the j-th coordinate of 𝐫_i is denoted as r_i,j.

Let 𝐫_i^0 and 𝐫_i^f denote initial and final positions of agent i∈𝒱, respectively.

The desired position of agent i  is defined by:

    𝐫_i(t)=𝐐(t,t_0)𝐫_i^0+𝐝(t,t_0),

where 𝐫_i^0=𝐫_i(t_0), 𝐫_i^f=𝐫_i(t_f) (i∈𝒱), t_0 and t_f denote initial and final time,
𝐐(t,t_0)∈ℝ^× is the Jacobian matrix, 𝐐(t_0,t_0)=𝐈_∈ℝ^× is the identity matrix,  𝐝(t,t_0)∈ℝ^× 1 is the rigid-body displacement vector, and 𝐝(t_0,t_0)=0∈ℝ^× 1. The affine transformation (<ref>) is called  homogeneous transformation in continuum mechanics <cit.>. 

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

    ∀ t,    Λ(𝐫_1,⋯,𝐫_+1)=.











Because homogeneous transformation is a linear mapping, 𝐐 and 𝐃 elements are uniquely related to leader position components by

    ∀ t,    [ vec(𝐐^T);        𝐝 ]
    =
    [ 𝐈_⊗𝐏(t_0)  𝐈_⊗1_× 1 ]vec(𝐏(t)),

where "⊗" is the Kronecker product, 1_∈ℝ^(+1)× 1 is the one-entry matrix, and

    𝐏(t)=
    [   r_1,1^HT          ⋯   r_1,d^HT;          ⋮          ⋮          ⋮; r_d+1,d^HT          ⋯ r_d+1,d^HT;            ]∈ℝ^(+1)×.



Ω(𝐫_1(t),⋯,𝐫_+1(t),𝐫_i(t))∈ℝ^(+1)× 1 remains time-invariant at any time t∈ [t_0,t_f]:

    ∀ t∈ [t_0,t_f],∀ i∈𝒱,    Ω(𝐫_1,⋯,𝐫_+1,𝐫_i)=Ω_i,0,

is time-invariant, where

    ∀ i∈𝒱,    Ω_i,0=Ω(𝐫_1^0,⋯,𝐫_+1^0,𝐫_i^0)∈ℝ^+1.



































Assumption: This paper assumes follower agents are positioned inside the leading simplex at initial time t_0: 

    ∀ i∈𝒱_F,    Ω_i,0>0.



 §.§ Continuum Deformation Acquisition


Assume directed graph 𝒢=𝒢(𝒱,ℰ) defines a fixed inter-agent communication topology, 𝒱 is the node set and ℰ⊂𝒱×𝒱 is the edge set. Follower i∈𝒱_F communicates with +1 in-neighbor agents defined by
set 𝒩_i={i_1,⋯,i_+1}⊂𝒱. 
It is assumed that Λ(𝐫_i_1,0,⋯,𝐫_i_+1,0)= (∀ i∈𝒱_F), so in-neighbor agents of follower i form an -dimensional simplex at initial time t_0. Follower inter-agent communications are weighted and obtained from

    [  w_i,i_1        ⋯ w_i,i_+1 ]
        ^T=Ω(𝐫_i_1^0,⋯,𝐫_i_+1^0,𝐫_i^0).

Note that w_i,i_k is the communication weight between follower i∈𝒱_F and in-neghbpor agent i_k∈𝒩_i (k=1,⋯,d+1).
































 §.§ MAS Collective Dynamics Model

 
Let 𝐫_i∈ℝ^× 1 denote actual position of agent i∈𝒱.

    d^2𝐫_idt^2=𝐮_i,

where


    𝐮_i=
        𝐫̈_i(given)   i∈𝒱_L
    β_v∑_j∈𝒩_iw_i,j(𝐫̇_j-𝐫̇_i)+β_r∑_j∈𝒩_iw_i,j(𝐫_j-𝐫_i)   i∈𝒱_F.


For continuum deformation communication weights are consistent with agents' positions at t_0 and assigned by Eq. (<ref>). 

































































 §.§ Temporal Logic

Temporal Logic (TL) can capture temporal behavior of a dynamical system.
In this paper we use a logic based on LTL_-X <cit.>. The logic LTL_-X is a flavour of Linear Temporal Logic without the Next operator X (sometimes written ∘), 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 ϕ. 
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_i,j, as well as a multiplication e_1× 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 ⊤, a comparison of two expressions e_1≤ e_2, or a disjunction ϕ_1ϕ_2, negation ¬ϕ or until ϕ_1𝒰ϕ_2 of two formulas.

    e     ::= c | r_i,j | r_i,j | e× e | e+e | e-e | e/e
    ϕ    ::= ⊤ | e≤ e | ϕϕ | ¬ϕ | ϕ𝒰ϕ

We call atomic formulas the formulas of the form e≤ e.
As is usual in LTL, we define the operators False , conjunction , 
always  and eventually  as:

    = ¬⊤   ϕ   = ⊤𝒰ϕ
    ϕ_1ϕ_2     = ¬(¬ϕ_1¬ϕ_2)     ϕ    =  ¬¬ϕ


For any time t≥ 0, the state 𝒮(t) of our system is a function giving the valuation of every state variable: 𝒮(t):{r_1,1,…,r_N,,r_1,1,…,r_N,}→ℝ

Given such a state 𝒮(t) for the valuation of state variables, an expression e can be evaluated in the usual way to a real number that we write 𝒮(t)(e). The satisfaction of formula ϕ in state 𝒮(t) (i.e., at time t) is then given by:

    S(t)   ⊤ is always satisfied;
    
        S(t)    e_1≤ e_2  if and only if 𝒮(t)(e_1)≤𝒮(t)(e_2);
    
        S(t)   ¬ϕ if and only if S(t)ϕ;
    
        S(t)   ϕ_1ϕ_2  if and only ifS(t)ϕ_1 or S(t)ϕ_2;
    
        S(t)   ϕ_1𝒰ϕ_2  if and only if there exists t'≥ t such that
       S(t')ϕ_2 and for all t≤ t”< t' we have S(t”)ϕ_1.


For convenience, we write e^2 for the expression e× e; 𝐫_i-𝐫_i_2^2 for the expression 
(r_i,1-r_i,1)^2+⋯+(r_i,-r_i,)^2;
and Ω(𝐫_1,⋯,𝐫_+1,𝐫_i) as in Equation <ref> (Section <ref>).



































§ 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 𝐁⊂ℝ^, is finite and convex. Let 𝐁 enclose m_B simplexes 𝐁_1, ⋯, 𝐁_m_B, e.g. ⋃_i=1^m_B𝐁_i⊂𝐁. 𝐁_i is a -dimensional simplex with vertices at 𝐛_i,1∈ℝ^× 1, ⋯ 𝐛_i,+1∈ℝ^× 1.

Definition 2 (Obstacle): Let 𝒪⊂ℝ^ be a finite set defining motion space obstacles. Let 𝒪 encompass m_O simplex es 𝐎_1, ⋯, 𝐎_m_O, e.g. 𝒪⊂⋃_i=1^m_O𝐎_i. 𝐎_i is an -dimensional simplex with vertices 𝐨_i,1∈ℝ^× 1, ⋯ 𝐨_i,+1∈ℝ^× 1.









  
Safety Condition 1: Bounded Vehicle Deviation
Deviation of every agent from continuum deformation must not exceed δ, i.e., the actual position 𝐫_i (i∈𝒱) of every agent must stay within δ of its desired position 𝐫^HT_i.  This requirement can be expressed as:

    ⋀_i∈𝒱(𝐫_i-𝐫_i_2^2≤δ^2),ψ_1

where δ is constant and ·_2 is the 2-norm symbol. 



  
Safety Condition 2: Follower Containment Condition
Follower i∈𝒱_F must be inside the leading simplex at any time t. This condition can be expressed as:

    ∀ i∈𝒱_F,∀ t≥ t_0    𝐫_i∈𝒯(𝐫_1,⋯,𝐫_+1)

which can be expressed in our logic using the function Ω as:

    ⋀_i∈𝒱_F(Ω(𝐫_1,⋯,𝐫_+1,𝐫_i)≥ 0).ψ_2




  
Safety Condition 3: Inter-Agent Collision Avoidance

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

    ⋀_i,j∈𝒱, 
        i≠ j(𝐫_i-𝐫_j_2^2≥ (2ϵ)^2).ψ_3




  
Safety Condition 4: Motion Space Containment
Motion space containment is satisfied, if

    ∀ i∈𝒱,∀ t≥ t_0    𝐫_i∈𝐁

which can be expressed in our logic using the function Ω as:

    ⋀_i∈𝒱⋁_k=1^m_B(Ω(𝐛_k,1,⋯,𝐛_k,+1,𝐫_i)≥ 0).
    
        
    ψ_4

Eq. (<ref>) ensures existence of a simplex 𝐁_i⊂𝐁 enclosing leader i∈𝒱_L at any time t.




  
Safety Condition 5: Obstacle Collision Avoidance
Obstacle collision avoidance is satisfied if

    ∀ i∈𝒱,∀ t≥ t_0,    (𝐫_i∉𝒪).

which can be expressed in our logic using the function Ω as: 


    ⋀_i∈𝒱(⋀_k=1^m_O(Ω(𝐨_k,1,⋯,𝐨_k,m_B,𝐫_i)≥ 0)).ψ_5






Eq. (<ref>) ensures every agent i∈𝒱 is outside the obstacle zone defined by simplexes 𝐎_1, ⋯, 𝐎_m_O. 





  
Liveness Condition 6: Final Formation Rechability
Given agent desired final positions 𝐫_1^f, ⋯, 𝐫_N^f, the liveness condition is defined by:

    ⋀_i∈𝒱(𝐫_i- 𝐫_i^f_2^2≤ε^2)ψ_6.


























 

§ SUFFICIENT CONDITIONS

 

 §.§ Inter-Agent Collision Avoidance and Agent Containment

 It is computationally expensive to ensure inter-agent collision avoidance and follower containment using Eqs. (<ref>) and (<ref>). We can instead use the sufficient conditions provided in Theorem <ref> to guarantee these two MAS safety constraints at less computational cost.   




























<cit.>
 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

    δ_max=min{1 2(D_B-2ϵ),(D_S-ϵ)}

and

    λ_min=δ+ϵδ_max+ϵ.

Inter-agent collision avoidance and agent containment are guaranteed, if the
eigenvalues of pure deformation matrix 𝐔_D=(𝐐^T𝐐)^1 2, denoted λ_1, λ_2, and λ_3, satisfy 

    ∀ t≥0,    ⋀_i=1^3 (λ_min≤|λ_i(t)|),

and no agent deviation exceeds δ at any time t. 





<cit.>
Let m_1 and m_2 denote two points of the leading simplex that has the minimum separation distance at t_0. If δ_max=1 2(D_B-ϵ) then m_1, m_2∈𝒱 are two agents (Fig. <ref>(c)). Otherwise, m_1∈𝒱_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. <ref>(b)):

    𝐫_m_1^0-𝐫_m_2^0_2=μ(δ_max+ϵ),

where 

    μ=
    
    2    m_1,m_2∈𝒱
    
    1   m_1∈𝒱_F, m_2 is at the leading polytope boundary.

Considering Eq. (<ref>),

    (𝐫_m_2-𝐫_m_1)^T(𝐫_m_2-𝐫_m_1)=   (𝐫_m_2^0-𝐫_m_1^0)^T𝐔_D^2(𝐫_m_2^0-𝐫_m_1^0).

Assume 

    ∀ i,j∈𝒱,i≠ j,    ((δ+ϵ)≤min𝐫_i-𝐫_j_2),

then, inter-agent collision avoidance is ensured if inequality (<ref>) is satisfied. This implies that

    μ^2(δ+ϵ)^2≤   min{λ_1^2,λ_2^2,λ_3^2}μ^2(δ_max+ϵ)^2
    ≤   (𝐫_m_2,0-𝐫_m_1,0)^T𝐔_D^2(𝐫_m_2,0-𝐫_m_1,0).

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

    ∀ t, i=1,2,3,    ((δ+ϵδ_max+ϵ)^2≤λ_i^2(t)).

Consequently,  inter-agent collision is avoided if inequality (<ref>) is satisfied. Because 𝐐 is nonsingular at any time t and 𝐐(t_0,t_0)=𝐈_d, 𝐔_D eigenvalues are always positive. Therefore, Eq. (<ref>) is satisfied.



























































































































 §.§ Motion Space Containment

If safety condition ψ_2 is satisfied, then motion space containment is guaranteed by ensuring leaders remain inside the motion space 𝐁. Formally, given the formula:

    ⋀_i∈𝒱_L⋁_k=1^m_B(Ω(𝐛_k,1,⋯,𝐛_k,+1,𝐫_i)≥ 0),ψ_7

we have:

 If ψ_2ψ_7 is satisfied, then ψ_4 is satisfied.



 §.§ Obstacle Collision Avoidance

If safety condition ψ_2 is satisfied, then obstacle collision avoidance is guaranteed by ensuring leaders  do not collide with obstacles. Formally, given the formula:

    ⋀_i∈𝒱_L(⋀_k=1^m_O(Ω(𝐨_k,1,⋯,𝐨_k,m_B,𝐫_i)≥ 0)),ψ_8

we have:

 If ψ_2ψ_8 is satisfied, then ψ_5 is satisfied. 

Proofs of Theorems 2 and 3 are adapted from <cit.>.


§ SIMULATION RESULTS


Consider an MAS with N=10 agents evolving in 2 dimensions (=2). Agents 1, 2, and 3 are leaders; the remaining agents are followers. Inter-agent communication is defined by the Fig. <ref> graph, and follower communication weights are listed in Table <ref>. Follower communication weights are consistent with the initial formation and assigned by Eq. (<ref>).
  Fig. <ref> also shows MAS initial and final formations.  𝐁=𝐁_1⋃𝐁_2⋃𝐁_3 defines the motion space, and 𝒪=⋃_k=1^4𝐎_4 defines obstacles in 𝐁.


































 The paper assumes all agents are identical with β_r=2 and β_v=4. Agent positions are plotted versus time in Figs. <ref> (a) and  <ref> (b) with t∈ [0,227.5], t_0=0s, t_f=227.5s.




























 


 


Satisfaction of Safety Condition 1: Fig. <ref>(c) plots deviation of every follower versus time confirming that no follower exceeds δ=0.2286m at any time t∈[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 ϵ=0.25m, thus, δ_max δ_ma= 1.1174m. Given δ=0.2286, ϵ=0.25m, and δ_ma= 1.1174m,  λ_min=0.35 is computed by Eq. (<ref>). As shown in Fig. <ref>,  𝐔_D eigenvalues are greater than λ_min at any time t, hence, safety condition 2 is satisfied.

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



Satisfaction of Necessary Condition 6: 

As shown in Fig. <ref>, 𝐫_i-𝐫_i^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.






§ CONCLUSION



In this paper we formally specified continuum deformation coordination in a -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.










IEEEtran



