NASA/TP–2011–217067

State-Based Implicit Coordination

and Applications

Anthony J. Narkawicz and C ́esar A. Mu ̃noz

Langley Research Center, Hampton, Virginia

March 2011
NASA STI Program . . . in Profile

Since its founding, NASA has been dedicated

to the advancement of aeronautics and space

science. The NASA scientific and technical

information (STI) program plays a key part

in helping NASA maintain this important

role.

The NASA STI Program operates under the

auspices of the Agency Chief Information

Officer. It collects, organizes, provides for

archiving, and disseminates NASA’s STI.

The NASA STI Program provides access to

the NASA Aeronautics and Space Database

and its public interface, the NASA Technical

Report Server, thus providing one of the

largest collection of aeronautical and space

science STI in the world. Results are

published in both non-NASA channels and

by NASA in the NASA STI Report Series,

which includes the following report types:

• TECHNICAL PUBLICATION. Reports of

completed research or a major significant

phase of research that present the results

of NASA programs and include extensive

data or theoretical analysis. Includes

compilations of significant scientific and

technical data and information deemed to

be of continuing reference value. NASA

counterpart of peer-reviewed formal

professional papers, but having less

stringent limitations on manuscript length

and extent of graphic presentations.

• TECHNICAL MEMORANDUM.

Scientific and technical findings that are

preliminary or of specialized interest, e.g.,

quick release reports, working papers, and

bibliographies that contain minimal

annotation. Does not contain extensive

analysis.

• CONTRACTOR REPORT. Scientific and

technical findings by NASA-sponsored

contractors and grantees.

• CONFERENCE PUBLICATION.

Collected papers from scientific and

technical conferences, symposia, seminars,

or other meetings sponsored or

co-sponsored by NASA.

• SPECIAL PUBLICATION. Scientific,

technical, or historical information from

NASA programs, projects, and missions,

often concerned with subjects having

substantial public interest.

• TECHNICAL TRANSLATION. Englishlanguage translations of foreign scientific

and technical material pertinent to

NASA’s mission.

Specialized services also include creating

custom thesauri, building customized

databases, and organizing and publishing

research results.

For more information about the NASA STI

Program, see the following:

• Access the NASA STI program home page

at http://www.sti.nasa.gov

• E-mail your question via the Internet to

help@sti.nasa.gov

• Fax your question to the NASA STI Help

Desk at 443-757-5803

• Phone the NASA STI Help Desk at

443-757-5802

• Write to:

NASA STI Help Desk

NASA Center for AeroSpace Information

7115 Standard Drive

Hanover, MD 21076–1320
NASA/TP–2011–217067

State-Based Implicit Coordination

and Applications

Anthony J. Narkawicz and C ́esar A. Mu ̃noz

Langley Research Center, Hampton, Virginia

National Aeronautics and

Space Administration

Langley Research Center

Hampton, Virginia 23681-2199

March 2011
Acknowledgments

The authors would like to thank the members of the review committee presided by Ricky Butler

and formed by Natalia Alexandrov, Jeffrey Maddalon, and David Wing for their insightful

comments that helped to improve earlier versions of this paper.

The use of trademarks or names of manufacturers in this report is for accurate reporting and does not

constitute an offical endorsement, either expressed or implied, of such products or manufacturers by the

National Aeronautics and Space Administration.

Available from:

NASA Center for AeroSpace Information

7115 Standard Drive

Hanover, MD 21076-1320

443-757-5802
Abstract

In air traffic management, pairwise coordination is the ability to achieve separation

requirements when conflicting aircraft simultaneously maneuver to solve a conflict.

Resolution algorithms are implicitly coordinated if they provide coordinated resolution maneuvers to conflicting aircraft when only surveillance data, e.g., position

and velocity vectors, is periodically broadcast by the aircraft. This paper proposes

an abstract framework for reasoning about state-based implicit coordination. The

framework consists of a formalized mathematical development that enables and

simplifies the design and verification of implicitly coordinated state-based resolution algorithms. The use of the framework is illustrated with several examples of

algorithms and formal proofs of their coordination properties. The work presented

here supports the safety case for a distributed self-separation air traffic management

concept where different aircraft may use different conflict resolution algorithms and

be assured that separation will be maintained.

i
Contents

1 Introduction 1

2 Notation and Basic Definitions 3

2.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2.2 Assumptions and Basic Definitions . . . . . . . . . . . . . . . . . . . 4

3 A General Theory of Coordination 7

3.1 Independent and Coordinated Criteria . . . . . . . . . . . . . . . . . 8

3.2 A Theory of Criteria . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3.3 General Theorems . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3.4 Derived and Composed Criteria . . . . . . . . . . . . . . . . . . . . . 12

4 Safety Properties 14

4.1 Absence of Conflict . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4.2 Divergence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

4.3 Repulsion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

5 Criteria 17

5.1 Divergence, Horizontal, and Repulsion Criteria . . . . . . . . . . . . 17

5.2 Coordination Properties of D, Hε, and Rε. . . . . . . . . . . . . . . 21

5.3 Fundamental Properties of Horizontal Criterion . . . . . . . . . . . . 22

5.3.1 Tangential Resolutions Satisfy Horizontal Criterion . . . . . . 22

5.3.2 Maximality of Horizontal Criterion . . . . . . . . . . . . . . . 24

5.4 Three-Dimensional Criteria . . . . . . . . . . . . . . . . . . . . . . . 26

6 Conflict Resolution Algorithms 29

6.1 Modified Voltage Potential . . . . . . . . . . . . . . . . . . . . . . . . 29

6.2 ACCoRD’s Track Angle Resolution . . . . . . . . . . . . . . . . . . . 32

6.3 Geometric Optimization’s Track Angle Resolution . . . . . . . . . . 34

6.4 Numerical Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

7 Formal Properties of MVP, GOtrackε

f

, and ACCoRDtrackε 41

7.1 MVP is Coordinated for Repulsion . . . . . . . . . . . . . . . . . . . . 42

7.2 GOtrackε

1

and ACCoRDtrackε are ConflictFree-Coordinated . . . . . . 43

7.3 MVP is ConflictFree-Coordinated with GOtrackε

1

and ACCoRDtrackε. 43

7.4 MVP is Not ConflictFree-Coordinated . . . . . . . . . . . . . . . . . . 44

7.5 GOtrackε

1

2

is Not ConflictFree-Coordinated . . . . . . . . . . . . . . . 45

7.6 GOtrackε

1

2

and MVP are Not ConflictFree-Coordinated . . . . . . . . . 47

8 Conclusion 48

ii
1 Introduction

The next generation of air traffic management systems may enable a mode of operation where aircraft take a primary responsibility in the management of air traffic

separation. This mode of operation, which is called self-separation, is supported

by advances in hardware and software technologies. For example, global navigation

satellite systems, such as Global Positioning System (GPS), will provide accurate

surveillance information, which is then broadcast to traffic aircraft and ground elements by systems such as Automatic Dependent Surveillance-Broadcast (ADS-B).

This information is then used by separation assurance systems, such as conflict

detection and resolution algorithms (CD&R), to warn aircraft crew and air traffic

controllers about traffic conflicts and to advise pilots on possible resolution maneuvers.

The conflict management function of the self-separation concept is a safetycritical component of the system. The safety case for that concept must guarantee

that distributed separation assurance systems interact in a consistent way, i.e., aircraft do not fly into each other when they independently and simultaneously maneuver to solve a conflict using to their onboard CD&R logic. As discussed by Wing

et al. [20], the conflict management function in a self-separation concept may rely

on a multi-layered approach where one or more CD&R algorithms are used at different times by different aircraft. Providing a guarantee of safe interaction between

these different algorithms requires verification that the distributed resolution maneuvers provided by the onboard systems are complementary. The characterization

of complementary resolution maneuvers is not a trivial task. Different resolution

algorithms have different safety goals. One algorithm, for example, may try to

immediately recover separation, while another algorithm may try to iteratively improve the separation requirement. Even in the case where the safety goal is the

same, algorithms that safely interact with themselves in a distributed environment

do not necessarily interact with each other in a safe way.

In CD&R literature [10], the terms cooperation and coordination are often used

to describe aircraft interaction when solving a conflict. Several approaches have

been proposed to handle this interaction, for example by exchanging intent information [1,9,18,19], by a temporary delegation of responsibility for separation [7], or

by geometric methods [2,4,5,8]. This paper provides a mathematical framework for

understanding implicit coordination by geometric methods for state-based CD&R.

Geometric methods refers to decision making rules that only depend on the geometry

of the encounters, such as the rule in the Visual Flight Rules that states that when

aircraft are approaching head-on, each aircraft shall alter their course to the right.

State-based CD&R refers to the use of nominal aircraft trajectories that do not include intent information and are defined as linear projections of the current position

and velocity of the aircraft for a given lookahead time. Finally, implicit coordination

refers to the case where aircraft do not negotiate their resolution maneuvers but still

take complimentary actions.

The implicit coordination concept considered in this paper only relies on periodically broadcast surveillance from traffic aircraft, for example via ADS-B. This

concept is particularly suitable for distributed systems since it does not assume ex1
change of aircraft intention and does not rely on an explicit resolution negotiation

between the aircraft. Furthermore, state-based separation assurance systems use

simple models of the aircraft dynamics and the airspace geometry. These models yield analytical solutions that can be implemented very efficiently in software

systems. In air/ground distributed air traffic management concepts, such as the

self-separation concept, state-based CD&R often serves as backup for intent-based

systems. Therefore, the overall safety of these concepts is ultimately dependent on

state-based algorithms.

The proposed framework provides formal mathematical definitions of coordination and other fundamental concepts such as loss of separation, air traffic conflict,

and pairwise resolution algorithm. The notion of coordination proposed here is relative to an abstract concept of a safety property, which characterizes safety goals

that are intended to be maintained by a family of resolution algorithms. The framework also includes a set of theorems for reasoning about coordination for particular

algorithms and particular safety properties. These theorems do not only enable the

proof that a given algorithm is implicitly coordinated with itself, but more interestingly, they enable and simplify the proofs that the given algorithm is implicitly

coordinated with other conflict resolution algorithms.

The mathematical development presented here can be used by developers of

state-based separation assurance systems to design implicitly coordinated algorithms

that are correct by construction and whose formal properties can be derived from the

theorems provided by the framework. It could also be used by technical committees

working on certification standards for distributed separation assurance systems. In

the paper “A Criteria Standard for Conflict Resolution: A Vision for Guaranteeing

the Safety of Self-Separation in NextGen” [12], the framework presented here is used

to propose a standard for guaranteeing the safe interaction of state-based separation

assurance algorithms. The proposed standard does not rely on a single mandated

CD&R algorithm but rather it proposes a set of common criteria to be satisfied

by algorithms that operate under a self-separation concept. That paper provides

concrete examples of criteria for conflict resolution and loss of separation recovery

algorithms. The fact that those criteria guarantee implicit coordination has been

proved once and for all using the framework presented in this paper. Certifying

that a particular algorithm complies the standard entails the verification that the

algorithm satisfies the criteria, which is a relatively simple task that can also be

accomplished by using the results in this framework.

This paper is logically structured in two parts. The first part, composed of

sections 2 through 5, lays out the theoretical aspects of the framework. Section 2

concerns notation, basic definitions, and geometrical and physical assumptions. Section 3 presents the main theoretical contribution of this work: an abstract theory

of state-based coordination. It is in this section that theorems providing sufficient

and necessary conditions for proving coordination are stated and proved. Section 4

specifies safety properties for conflict-free, repulsive, and divergent resolution maneuvers. Section 5 provides a set of theorems for proving coordination of resolution

algorithms for the safety properties presented in Section 4. The second part of the

paper consists of sections 6 and 7. This part illustrates the theoretical concepts

with practical examples. Section 6 formally specifies well-known CD&R algorithms.

2
Several coordination properties of these algorithms are formally proved in Section 7.

Finally, the last section concludes this work.

2 Notation and Basic Definitions

This section presents the mathematical notation used in the paper and provides the

basic definitions required to understand the concepts developed in the rest of the

paper.

2.1 Notation

Vector variables are written in boldface and can be denoted by their components.

For example, if u is a 2-dimensional vector, then u denotes the pair (ux, uy). The

two-dimensional Euclidean norm of the vector u is denoted by1

kuk ≡ q

u

2

x + u

2

y

,

and the dot product of the 2-dimensional vectors u and w is denoted

u · w ≡ (uxwx + uywy).

Furthermore, 0 denotes the zero vector, i.e.,

0 ≡ (0, 0),

and u

⊥ denotes the right perpendicular vector to u, i.e.,

u

⊥ ≡ (uy, −ux).

From these definitions, it can be easily proved that u · u

⊥ = 0.

The function sign maps real numbers to unit values in {−1, 1} and is defined

as follows.

sign(x) ≡



1 if x ≥ 0,

−1 otherwise.

The expression ι = ±1 denotes the fact that an integer ι belongs to the set

{−1, 1}. Moreover, the symbols ¬, =⇒ , ⇐⇒ denote logical negation, implication,

and equivalence, respectively. In the context of this paper, a predicate is a Boolean

function. For example, a predicate on vectors is a function that maps vectors into

Boolean values.

The mathematical development presented in this paper has been specified and

formally verified in the Prototype Verification System (PVS) [15]. PVS is a proof

assistant that consists of a specification language, based on classical higher-order

logic, and a mechanical theorem prover for this logic. The PVS specification language allows for the precise definition of mathematical objects such as functions

and relations, and the precise statement of logical formulas such as lemmas and

theorems. Proofs of logical formulas can be mechanically checked using the PVS

1The symbol ≡ is used to introduce mathematical definitions.

3
theorem prover, which guarantees that every proof step is correct and that all possible cases of a proof are covered. All lemmas and theorems presented in this

paper have been mechanically checked in PVS. For the sake of simplicity, only

proof sketches of the main results are presented in the paper. The complete development, including all definitions and formal proofs, is available from http:

//shemesh.larc.nasa.gov/people/cam/ACCoRD.

The use of a formal language, e.g., in this case the specification language of

PVS, enforces rigorous definitions of mathematical objects, where all dependencies

are clearly specified. This level of rigor guarantees a very high confidence on the

correctness of the results presented in this paper. However, this also makes the notation heavy and difficult to read for the non-expert reader. For this reason, the work

presented here uses standard mathematical notation and does not assume that the

reader is familiar with the syntax or semantics of the PVS language. In particular,

some syntactical conventions are taken by the authors to make this development

more accessible to the casual reader:

• The PVS specification language is strongly typed, i.e., all declarations are explicitly typed [16]. This feature guarantees that all PVS functions are total

and well-defined. For instance, a mathematical formula that includes a division needs to make explicit the fact that the divisor is different from zero,

otherwise the expression would be undefined. In PVS, these conditions are

handled by a type system, which is enforced by the PVS type-checker. Since

PVS type annotations tend to be verbose, formulas in this paper appear untyped. When necessary, the type domain of variables is made explicit in the

context where the formula appears.

• PVS is based on higher-order logic, so it supports the definition of functions

that return functions or that have functions as arguments. In this paper,

arguments of a higher-order function are called parameters. For example,

this paper uses the notions of parametric predicate and parametric set. A

parametric predicate P on vectors, with parameters s, v, is a higher-order

function that takes as arguments vectors s and v, and returns a predicate on

vectors. Similarly, a parametric set A of vectors, with parameters s, v, is a

higher-order function that takes as arguments vectors s and v, and returns

a set of vectors. Sub- and super-indices will be used to denote parameters,

e.g., Ps,v and As,v are, respectively, the predicate and set resulting from the

application of the parametric predicate P and parametric set A to s and v.

• The PVS notation is declarative, i.e., there is not a notion of memory state

as in a programming language. Algorithms are represented by functions. By

convention, names of functions that are intended to have a logical meaning

are written in italics. Functions that represent algorithms to be implemented

in a programming language are written in typewriter font.

2.2 Assumptions and Basic Definitions

This paper considers pairwise resolution algorithms that return guidance maneuvers

for aircraft. The terms ownship and intruder are used to distinguish between the

4
aircraft for which the resolution maneuver is computed, which corresponds to the

ownship, and the traffic aircraft, which corresponds to the intruder. These designations are relative. Each aircraft will be from its point of view the ownship and

the other aircraft will be the intruder. Without loss of generality, the development

presented here takes the point of view of one of the aircraft, and that aircraft will

be designated as the ownship.

The algorithms discussed here only use state-based information for the two aircraft, i.e., position and velocity vectors that are elements of a Euclidean space.

Aircraft dynamics are represented by a simple kinematic model where points move

at constant linear speed. For notational convenience, this paper mostly uses the

Euclidean 2-dimensional geometry instead of the 3-dimensional one, but as shown

in Section 5.4, all the results in this paper have been generalized to the Euclidean

3-dimensional airspace. The current state of the ownship and intruder aircraft are

denoted by the following vectors.

so Initial position of the ownship aircraft

vo Initial velocity of the ownship aircraft

si Initial position of the intruder aircraft

vi Initial velocity of the intruder aircraft

It is assumed that the ground speeds of the ownship and intruder aircraft are not

zero, i.e., kvok 6= 0 and kvik 6= 0. Therefore, vo 6= 0 and vi 6= 0.

In the airspace system, the separation requirement for two aircraft is specified

by a minimum horizontal separation D (typically, D is 5 nautical miles). A loss

of separation between two aircraft occurs when the distance between them is less

than D.

Definition 1. The ownship and intruder aircraft are in loss of separation if and

only if it holds that

kso − sik < D.

The separation requirement can be understood as an imaginary circle of diameter D around each aircraft, and a conflict between two aircraft as a future overlapping

of these circles. In this paper, an alternative but equivalent view is considered where

the intruder is surrounded by a circle, called the protected zone, of radius D. From

this perspective, a conflict between the ownship and intruder aircraft is defined as

the existence of a time t ≥ 0 at which the ownship is in the interior of the intruder’s

protected zone. In conflict detection algorithms, it is also required that t is within a

specified lookahead time. However, since this work concerns resolution algorithms,

a lookahead time is not considered.

Definition 2. The ownship and intruder aircraft are in conflict if and only if there

exists t ≥ 0 such that, at time t, separation is lost, i.e.,

k(so + t vo) − (si + t vi)k < D.

Since (so +t vo)−(si +t vi) = (so −si)+t(vo −vi), the mathematical expression

that characterizes conflict can be defined on s = so − si and v = vo − vi, i.e., the

5
relative position and velocity vectors, respectively, of the ownship with respect to

the intruder. Therefore, conflict can be viewed as a predicate of two vectors s and v

rather than a predicate of four vectors so, vo, si, and vi. This relative view simplifies

the mathematical development presented in this paper. Thus, the predicate Conflict

can be formally defined as follows.

Conflict(s, v) ≡ ∃ t ≥ 0 : ks + t vk < D. (1)

In this paper, the relative position and velocity vectors, s and v, will commonly be

used in place of so − si and vo − vi, respectively.

In a distributed airspace concept, a resolution algorithm can be defined as a

function that computes one resolution maneuver for the aircraft that executes the

algorithm, i.e., the ownship. In this paper, this definition is generalized such that

a resolution algorithm returns a set of vectors, each of which represents a distinct

resolution maneuver for the ownship. Since in PVS all functions are total, i.e., they

are defined for all the elements of the domain, the generalization used in this paper

has the advantage of encoding the case were no resolutions are available for the

ownship as the empty set. That is, if there are no resolutions available, then an

empty set is returned by the resolution algorithm.

Definition 3. A resolution algorithm is a function cr that takes as arguments the

current state of the ownship and intruder aircraft, e.g., so, vo, si, vi, and returns a

set of velocity vectors, where each of these vectors corresponds to a possible velocity

maneuver for the ownship.

The velocity maneuvers provided by a resolution algorithm are intended to maintain a safety objective between aircraft, which may be violated at the current state.

Usually, the safety objective is that the aircraft are not in conflict. This paper uses

an abstract concept of safety objectives, called safety properties. One characteristic

of safety properties is that the ownship and the intruder agree on whether the given

notion of safety is currently satisfied. That is, if from the perspective of one aircraft,

the current state appears safe, then it should appear safe to the other aircraft as

well. Section 4 will show that this restriction holds for typical safety objectives such

as conflict-free, repulsion, and divergence.

Definition 4. A safety property is a parametric predicate P on vectors, with parameters s, v, such that for all parameters s, v and for all v

0

,

Ps,v(v

0

) ⇐⇒ P−s,−v(−v

0

).

The vectors s, v, and v

0

in Definition 4 are intended to be relative vectors, where

s and v are the current relative position and velocity of the aircraft.

Given a safety property P and current relative vectors s and v, if Ps,v(v

0

) holds,

then it is said that v

0

satisfies P. If a safety property P is satisfied when one of the

aircraft maneuvers according to a resolution algorithm cr, while the other aircraft

maintains its current velocity, then resolution algorithm cr is said to be independent

for the safety property P or, more formally, P-independent.

6
Definition 5. The resolution algorithm cr is P-independent if for all s = so − si

and v = vo −vi such that Ps,v(v) does not hold, Ps,v(v

0

o −vi) holds for every vector

v

0

o ∈ cr(so, si

, vo, vi).

Definition 5 can be read as “the resolution algorithm cr is independent for a

safety property P if it computes velocity maneuvers for the ownship that restore P

when P is not satisfied at the current state.” Since vectors so, si, vo, vi, and v

0

o are

universally quantified in this definition, if an algorithm cr is P-independent from

the ownship’s point of view, it is also P-independent from the intruder’s point of

view.

Even when two resolution algorithms cro and cri are both P-independent, it

is still possible that the algorithms return maneuvers that do not satisfy the safety

property when both aircraft simultaneously maneuver. The coordination property

defined below ensures that the safety property is met when both aircraft simultaneously maneuver.

Definition 6. A resolution algorithm cro is P-coordinated with a resolution algorithm cri if for all s = so − si and v = vo − vi such that Ps,v(v) does not hold,

Ps,v(v

0

o − v

0

i

) holds for all vectors v

0

o ∈ cro(so, si

, vo, vi) and v

0

i ∈ cri(si

, so, vi, vo).

Definition 6 can be read as “the resolution algorithm cro is coordinated with

cri for a safety property P if they compute velocity maneuvers for the ownship and

the intruder aircraft that restore the safety property P when P is not satisfied at

the current state.” This definition involves two algorithms simultaneously executed

by two aircraft. From their own perspectives, each aircraft is the ownship while

the other aircraft is the intruder. Since vectors so, si, vo, vi, and v

0

o are quantified

universally, if an algorithm cro is P-coordinated with cri, then it is also true that

criis P-coordinated with cro.

It is noted that independence is a property held by one algorithm, while coordination is a property held by two algorithms. However, by abuse of notation, a

resolution algorithm cr is said to be P-coordinated if it is P-coordinated with itself.

This corresponds to the special case where the ownship and intruder aircraft are

using the same algorithm.

3 A General Theory of Coordination

It is usually difficult to prove that resolution algorithms are P-independent or Pcoordinated for a particular safety property P. Direct proofs of independence and

coordination involve exhaustive case analyses that spell out of the control flow of

the algorithms.

This section develops a mathematical theory that establishes sets of conditions,

called criteria, that guarantee independence and coordination of resolution maneuvers for an abstract safety property. Using this theory, the proof that two algorithms

cro and cri are independent and coordinated for a safety property P can be done

in two steps:

1. Find a criterion that guarantees P-independence and P-coordination.

7
2. Prove the all resolution vectors computed by cro and cri satisfy the criterion.

This proof approach would be as difficult as a direct proof if it had to be done from

scratch every time. However, the criterion constructed in the first step can often be

defined in a general way so that it can be applied to a family of resolution algorithms.

Section 5 gives several examples of criteria for different safety properties. The second

step, i.e., the proof that the maneuvers computed by a resolution algorithm satisfy

a criterion, still needs to be proved for every algorithm. But it can be argued that

this proof is simpler than direct proofs of independence and coordination. Section 7

illustrates this technique with concrete resolution algorithms.

3.1 Independent and Coordinated Criteria

Definition 7. A criterion is a parametric set of vectors A, with parameters s, v.

If A is a criterion, the set As,v consists of vectors in the relative coordinate

system, where the parameters s and v are, respectively, the current relative position

and velocity of the aircraft. If all vectors in the set As,v satisfy the safety property P,

the criterion A is said to be independent for P or, more formally, P-independent.

Definition 8. A criterion A is P-independent if for all for all parameters s, v and

for all v

0 ∈ As,v, Ps,v(v0

) holds.

A resolution algorithm satisfies a criterion when all the maneuvers computed by

the algorithm are included in the criterion.

Definition 9. A resolution algorithm cr satisfies the criterion A if for all s = so−si

and v = vo − vi, v

0

o ∈ cr(so, si

, vo, vi) implies (v

0

o − vi) ∈ As,v.

The following theorem states that to prove that a resolution algorithm is Pindependent, it is sufficient to prove that the algorithm satisfies a criterion that is

P-independent. It is easily proved from the definitions.

Theorem 1. If

1. the criterion A is P-independent and

2. the resolution algorithm cr satisfies A,

then cr is P-independent.

The concept of coordination for resolution algorithms can be generalized to a

concept of coordination between criteria.

Definition 10. A criterion A is P-coordinated with B if for all s = so − si, v =

vo−vi, and vectors v

0

o

, v

0

i

such that ¬Ps,v(v) holds, (v

0

o−vi) ∈ As,v and (v

0

i−vo) ∈

B−s,−v imply that Ps,v(v

0

o − v

0

i

) holds.

By abuse of notation, it is said that a criterion A is P-coordinated if it is Pcoordinated with itself.

The following theorem states that to prove that two resolution algorithms are

coordinated for a safety property P, it is sufficient to show that the algorithms

satisfy P-coordinated criteria.

8
Theorem 2. If

1. the criterion A is P-coordinated with B, and

2. the resolution algorithms cro and cri satisfy A and B, respectively,

then cro is P-coordinated with cri.

3.2 A Theory of Criteria

Theorems 1 and 2 provide a way to prove that resolution algorithms are independent

and coordinated for a safety property. At first glance, it seems that the problem

of proving P-independence and P-coordination for resolution algorithms has been

merely transformed into a problem of proving P-independence and P-coordination

for set of the vectors in a criterion. However, the power of this approach is that

criteria that satisfy P-independence and P-coordination can be defined in an abstract way, independently from specific safety properties or resolutions algorithms.

This section presents basic conditions for the construction of these criteria. These

conditions will be needed to prove the main theorems in Section 3.3, where the

first conditions of theorems 1 and 2 are reduced to verifying simpler, geometric

conditions.

Definition 11. A set of vectors S is closed under sum if for all vectors v, u ∈ S,

v + u ∈ S.

It is often useful to know that for a given safety property P, the complement of

P is closed under sum.

Definition 12. A criterion A is sum independent for a safety property P if for all

parameters s, v such that ¬Ps,v(v) holds, for all vectors u

0 ∈ As,v and v0 ∈ As,v,

Ps,v(u

0 + v0

) holds.

The relation between sum independence and coordination is the main focus of

Section 3.3.

There is a notion of a set of vectors being independent of length, and this has

slightly different definitions for criteria and safety properties.

Definition 13. A criterion A is independent of length if for all vectors s, v, v

0

, and

for all positive real numbers r, As,v = As,r v.

Definition 14. A safety property P is independent of length if for all vectors s, v, v

0

and all positive real numbers r and p, Ps,v(v

0

) ⇐⇒ Ps,r v(p v

0

).

The notion of an open set is fundamental to the mathematical field of real analysis [17] and it is presented here, in the context of vector analysis, for completeness.

Definition 15. A set S of vectors is open if for all v ∈ S, there exists a positive

real number δ > 0 such that for all vectors u with kuk < δ, v + u ∈ S.

9
For instance, if P is a safety property, then the set of vectors that do not satisfy

P, denoted by ¬P, is open if for all vectors s, v, v

0

such that ¬Ps,v(v

0

) holds, there

exists δ > 0 such that for all vectors u

0 with ku0k < δ, ¬Ps,v(v0 + u0

).

The two criteria A and B in Definition 10 are usually defined by the same

parametric set. In this case, the criterion is said to be symmetric if the two aircraft

see the same set of vectors from their own perspectives.

Definition 16. A criterion A is symmetric if for all parameters s, v and for all

vectors v

0

, v

0 ∈ As,v if and only if −v0 ∈ A−s,−v.

There is a dual concept to symmetry, called asymmetry, where the criteria A

and B are defined by the same parametric set and the two aircraft see the same set

of vectors except for a sign that encodes the perspective of the ownship. The formal

definition of asymmetry requires a notion of signed criterion that takes an additional

parameter ε = ±1. A signed criterion Aε defines two criteria: A−1 and A1. The

parameter ε refers to the side of the origin on which any trajectory from s along

a vector in Aε passes, from the perspective of the ownship. For example, in the

Euclidean 2-dimensional airspace, ε may refer to the horizontal directions left and

right. If a vertical dimension is considered, as in Section 5.4, the parameter ε may

also refer to the vertical directions up and down.

Definition 17. A signed criterion Aεis antisymmetric if for all parameters s, v, ε

and for all vectors v

0

, v

0 ∈ Aε

s,v

if and only if −v

0 ∈ A−ε

−s,−v

.

3.3 General Theorems

This section presents theorems that reduce the proof of criteria coordination to sum

independence, which is a simpler geometric property.

Let A be a criterion and P be an arbitrary safety property. The results in this

section use the following equality.

v

0

o − v

0

i = (v

0

o − vi) + (vo − v

0

i

) − (vo − vi).

Theorem 3. If

1. A is symmetric and sum independent for P, and

2. ¬P is closed under sum,

then A is P-coordinated.

Proof. Let s = so − si, v = vo − vi, and v

0

o

, v

0

i

be any vectors such that ¬Ps,v(v)

holds. Suppose that both (v

0

o − vi) ∈ As,v and (v

0

i − vo) ∈ A−s,−v. It suffices to

prove that Ps,v(v

0

o − v

0

i

) holds. Define v

0 = (v0

o − vi) and u

0 = (vo − v0

i

). The goal

is to prove that

Ps,v(v

0 + u0 − v).

Assume that this is false. Since ¬Ps,v(v

0 + u0 − v) and ¬Ps,v(v) both hold and ¬P

is closed under sum, it follows that ¬Ps,v(v

0 + u0

) holds.

However, since A is symmetric and −u

0 ∈ A−s,−v, it follows that u0 ∈ As,v. Since

A is sum independent for P, it follows that Ps,v(v

0 + u0

). This is a contradiction

and therefore completes the proof.

10
Theorem 4. If

1. A is symmetric, independent of length, and P-coordinated, and

2. ¬P is open and independent of length,

then A is sum independent for P.

Proof. Suppose that s, v, v

0

, and u

0 are vectors such that ¬Ps,v(v), v0 ∈ As,v, and

u

0 ∈ As,v. It suffices to prove that Ps,v(v0 +u0

) holds. Suppose that this is not true.

Then ¬Ps,v(v

0 + u0

). Since ¬P is open, there exists δ > 0 such that if kwk < δ,

then ¬Ps,v(v

0 + u0 + w). In particular, ¬Ps,v(v0 + u0 − c v), where c =

δ

2 kvk

. Since

¬P is independent of length, ¬Ps,c v(v

0 + u0 − c v) holds.

Define vectors vo, vi, v

0

o and v

0

i

as follows.

vo = 0,

vi = −c v,

v

0

o = v

0 − c v,

v

0

i = −u

0

.

The following equations can easily be proved from these definitions.

v

0

o − vi = v

0

,

vo − v

0

i = u

0

,

vo − vi = c v,

v

0

o − v

0

i = v

0 + u0 − c v.

Thus, ¬Ps,c v(v

0

o − v

0

i

) holds. Since A is P-coordinated, it suffices to prove the

following three properties.

1. ¬Pso−si,vo−vi

(vo − vi),

2. v

0

o − vi ∈ Aso−si,vo−vi

, and

3. v

0

i − vo ∈ Asi−so,vi−vo

.

The first of these properties is equivalent to ¬Ps,c v(c v), which follows from the

facts that ¬Ps,v(v) holds and that ¬P is independent of length. The statement that

v

0

o − vi ∈ Aso−si,vo−vi

is equivalent to v

0 ∈ As,c v, which follows from the facts that

v

0 ∈ As,v holds and that A is independent of length. Finally, the statement that

v

0

i − vo ∈ Asi−so,vi−vo

is equivalent to −u

0 ∈ A−s,−c v, which follows from the facts

that u

0 ∈ As,v holds, that A is independent of length, and that A is symmetric.

This completes the proof.

Corollary 5 follows directly from Theorems 3 and 4.

Corollary 5 (Equivalence of Coordination and Sum Independence). Suppose that

1. A is symmetric, sum independent, and independent of length, and

11
2. ¬P is open, closed under sum, and independent of length,

then A is P-coordinated if and only if it is sum independent for P.

There are analogues of theorems 3 and 4 in the case where Aεis antisymmetric.

These are stated below, and the proofs are identical in form.

Theorem 6. If

1. Aεis antisymmetric and sum independent for P, and

2. ¬P is closed under sum,

then Aεis P-coordinated with A−ε.

Theorem 7. If

1. Aε

is antisymmetric, independent of length, and Aεis P-coordinated with A−ε,

and

2. ¬P is open and independent of length,

then Aεis sum independent for P.

3.4 Derived and Composed Criteria

Criteria can be composed to form larger sets of vectors that preserve their coordination properties. This section presents two criteria combinators, called derivation

and composition, and states theorems that provide sufficient conditions under which

these combinators preserve coordination with respect to a safety property P.

Theorem 2 is used to prove that if cro and cri are resolution algorithms that

satisfy the criterion A, and if A is P-coordinated, then cro is P-coordinated with

cri. In some cases, the condition that cro satisfies A can be weakened in this

statement. That is, given a criterion A, it is often possible to construct a family

of criteria from A, called the derived criteria of A, such that if cro satisfies one

of the derived criteria and cri satisfies A, the resolution algorithms cro and cri

are still P-coordinated. The family of derived criteria of A is parameterized by a

nonnegative number p.

Definition 18. Let A be a criterion, the family of derived criteria of A, denoted

Deriv p(A), is defined as follows.

Deriv p(A)s,v ≡ {v

0

|(v

0 − p v) ∈ As,v}.

From this definition it is easy to see that Deriv 0(A)s,v = A. Theorem 8 gives

sufficient conditions under which the criterion Deriv p(A) is a weaker condition on

the algorithm cro than the criterion A.

Theorem 8. If the criterion A is closed under sum and −p v ∈ As,v, then A is a

subset of Deriv p(A), i.e.,

As,v ⊆ Deriv p(A)s,v.

12
The most important property of the derived criterion is coordination.

Theorem 9. If p + q = 1 and the criterion A is symmetric and sum independent

for a safety property P, then Deriv p(A) is P-coordinated with Deriv q(A).

Proof. Let s = so − si, v = vo − vi, and v

0

o

, v

0

i

be any vectors such that ¬Ps,v(v)

holds. Suppose that (v

0

o − vi) ∈ Deriv p

(A)s,v and (v

0

i − vo) ∈ Deriv q

(A)−s,−v.

It suffices to prove that Ps,v(v

0

o − v

0

i

) holds. By the definition of Deriv q(A), v

0

i −

vo + q v ∈ A−s,−v. Since A is symmetric, vo − v

0

i − q v ∈ As,v. By the definition

of Deriv p(A), v

0

o − vi − p v ∈ As,v. Since A is sum independent, it follows that

Ps,v(v

0

o−vi−p v+vo−v

0

i−q v) holds, and since v

0

o−vi−p v+vo−v

0

i−q v = v

0

o−v

0

i

,

the result follows.

Corollary 10. If the criterion A is symmetric and sum independent for P, then A

is P-coordinated with Deriv 1(A).

It is important to note that if the criterion As,v contains the vector 0, then the

derived criterion Deriv p(A)s,v contains the relative velocity vector p v. In particular,

if p = 1 and A is symmetric and sum independent for P, then, by Corollary 10, an

algorithm cro that always returns the current velocity vector is coordinated with

an algorithm cri that satisfies the criterion A.

Using the derivation combinator, a composition combinator is defined that takes

two criteria A and B and composes them into one criterion Comp(A, B), called the

composed criterion, that contains vectors from both criteria.

Definition 19. The composed criterion of A and B is defined as follows.

Comp(A, B) ≡ A ∪ (B ∩ Deriv 1(A)). (2)

The following theorem gives sufficient conditions under which the composed

criterion preserves coordination for a safety property P.

Theorem 11. Let A be sum independent for the safety property P and symmetric,

such that ¬P is closed under sum. If B is P-coordinated with B

0

, then Comp(A, B)

is P-coordinated with Comp(A, B

0

).

Proof. Theorem 3 in Section 3.3 implies that A is coordinated. Let s = so − si,

v = vo − vi, and v

0

o

, v

0

i

be any vectors such that ¬Ps,v(v) holds. Suppose that

(v

0

o − vi) ∈ Comp(A, B)s,v and (v

0

i − vo) ∈ Comp(A, B

0

)−s,−v. It suffices to prove

that Ps,v(v

0

o − v

0

i

) holds. There are four possibilities:

1. (v

0

o − vi) ∈ As,v and (v

0

i − vo) ∈ A−s,−v.

2. (v

0

o − vi) ∈ As,v and (v

0

i − vo) ∈ B0

−s,−v ∩ Deriv 1

(A)−s,−v.

3. (v

0

o − vi) ∈ Bs,v ∩ Deriv 1

(A)s,v and (v

0

i − vo) ∈ A−s,−v.

4. (v

0

o − vi) ∈ Bs,v ∩ Deriv 1

(A)s,v and (v

0

i − vo) ∈ B0

−s,−v ∩ Deriv 1

(A)−s,−v.

The result follows in the first case from the fact that A is coordinated for P, in the

second and third cases from the fact that A is coordinated with Deriv 1(A) for P

(Corollary 10), and in the final case from the fact that B and B

0 are coordinated

for P.

13
4 Safety Properties

As stated in Definition 4 in Section 2.2, a safety property is a predicate used by

the ownship and intruder aircraft to agree on whether a particular state is safe.

For example, if the ownship determines that a given relative resolution maneuver

is conflict-free, the same resolution maneuver must be conflict-free when considered

by the intruder aircraft.

The safety property of interest for conflict resolution algorithms is the absence

of conflict between the ownship and the intruder aircraft. However, in some circumstances, that safety property cannot be immediately recovered, for example when

the aircraft are already in loss of separation. In those cases, it may be useful to consider a stronger safety property such as divergence, i.e., the resolution maneuvers

guarantee that the distance between the aircraft immediately increases, or a weaker

safety property such as repulsion, i.e., the resolution maneuvers guarantee that the

distance at time of closest approach increases.

In an expressive logic like the one provided by the verification system PVS, safety

properties can be specified using universal or existential quantifiers. The statement

of these definitions follow their natural logical description. However, quantifiers

are not always implementable in an algorithmic way and, therefore, these natural

definitions of safety properties cannot be mechanically checked by a computer. This

section provides analytical definitions of safety properties that can be implemented

by algorithms and that are equivalent to their intuitive logical description based on

quantifiers.

4.1 Absence of Conflict

The safety property that determines whether a given state is conflict-free is defined

by the predicate

ConflictFrees,v(v

0

) ≡ ¬Conflict(s, v

0

). (3)

The parametric predicate ConflictFree is a safety property according to Definition 4 in Section 2.2, i.e., it satisfies the following condition.

ConflictFrees,v(v

0

) ⇐⇒ ConflictFree−s,−v(−v

0

).

Since Formula (3) involves a quantifier in the definition of Conflict, it is not practical

for checking whether a given relative vector v

0

is conflict-free. This section offers

an alternative, but equivalent, characterization of the safety property ConflictFree,

where the quantifier has been eliminated.

If Conflict(s, v) holds, then the half line s + t v, with t ≥ 0, must intersect the

circle of radius D at exactly two distinct times t. These times correspond to the

solutions of the quadratic equation

0 = ks + t vk

2 − D2

= kvk

2

t

2 + 2 (s · v)t + (ksk2 − D).

(4)

The discriminant of the polynomial on t in Formula (4) is given by 4 ∆(s, v), where

∆(s, v) ≡ ks · vk

2 − kvk2

(ksk

2 − D2

). (5)

14
Equation (4) has solutions when the discriminant is nonnegative and it has exactly

two distinct solutions when it is strictly positive, i.e., when ∆(s, v) > 0. The roots

of this quadratic equation are given by the following function, where ι = ±1.

ΘD(s, v, ι) ≡

−s · v + ι

p

ks · vk

2 − kvk2(ksk2 − D2)

kvk

2

. (6)

If Conflict(s, v) holds, ΘD(s, v, −1) is the time when the aircraft lose separation and

ΘD(s, v, 1) is the time when the aircraft recover separation. The following lemmas

are proved by algebraic manipulations.

Lemma 12. If ∆(s, v) ≥ 0, then ks + ΘD(s, v, ι) vk = D, for ι = ±1, and

ΘD(s, v, −1) ≤ ΘD(s, v, 1).

Furthermore, if ∆(s, v) > 0, then ΘD(s, v, −1) < ΘD(s, v, 1).

Lemma 13. If ksk ≥ D, then Conflict(s, v) holds if and only if s · v < 0 and

∆(s, v) > 0.

From Equation (3) and Lemma 13, the following equivalence holds.

ConflictFrees,v(v

0

) ⇐⇒ ksk ≥ D and (s · v

0 ≥ 0 or ∆(s, v0

) ≤ 0). (7)

Equation (7) provides and analytical way to check whether a relative vector v

0

results in a projected linear trajectory that is free of conflict.

4.2 Divergence

Another safety property that is useful, especially when the aircraft are already in

loss of separation, is divergence. It is stronger than the notion of conflict in the

case where the aircraft are currently horizontally separated. The ownship and the

intruder aircraft are (horizontally) divergent if the distance between the aircraft is

increasing, i.e.,

Divergences,v(v

0

) ≡ ∀ t > 0 : ks + t v

0

k > ksk. (8)

The parametric predicate Divergence is a safety property, i.e., it satisfies that for all

vectors v

0

,

Divergences,v(v

0

) ⇐⇒ Divergence−s,−v(−v

0

).

Equation (8) is not practical for checking divergence because of the universal quantification on t. However, it can be proved using basic algebra that divergence is

equivalent to the dot product s · v being nonnegative. Thus, the following equivalence holds.

Divergences,v(v

0

) ⇐⇒ s · v

0 ≥ 0. (9)

Equation (9) provides and analytical way to check whether a relative vector v

0

results in a projected linear trajectory that is divergent.

15
4.3 Repulsion

A resolution maneuver is repulsive if it increases the minimum future distance between the aircraft. Given the current relative velocity vector vo−vi

, for the ownship

aircraft with respect to the intruder, repulsion is a predicate on the relative velocity

vector v

0

o − vi

, where v

0

o

is a new velocity vector representing a maneuver for the

ownship. It implies that the minimum distance achieved by the aircraft for positive

time is greater if the new velocity vector v

0

o

is chosen by the ownship instead of the

current vector vo. This is formalized as follows.

The time tca(s, v), referred to as the time of closest approach for the vectors

s and v, is the time at which the aircraft achieve minimum horizontal separation.

If the relative velocity vector v is zero, the distance between the aircraft remains

constant at the value ksk. In this case, the time of closest approach is defined to be

0. In the general case, the time of closest approach is defined as follows.

tca(s, v) ≡

(

0, if v = 0,

−

s·v

kvk

2 , otherwise.

(10)

The following theorem, which is proved using elementary algebraic methods,

states that tca indeed computes the time of closest approach between the aircraft.

Theorem 14. For all real numbers t,

ks + tca(s, v) vk ≤ ks + t vk.

A stronger result can be proved when v is nonzero.

Theorem 15. If v 6= 0, then for all real numbers t 6= tca(s, v),

ks + tca(s, v) vk < ks + t vk.

Using the function tca, repulsive resolution maneuvers are formally defined by

the following predicate.

Repulsions,v(v

0

) ≡ tca(s, v) > 0 and

(tca(s, v

0

) ≤ 0 or

ks + tca(s, v) vk < ks + tca(s, v

0

) v

0

k).

(11)

Equation (11) provides an analytical way to check whether a relative vector v

0

results in a projected linear trajectory that is repulsive with respect to the original

vector v. The parametric predicate Repulsion is a safety property, i.e., it satisfies

that for all vectors v

0

,

Repulsions,v(v

0

) ⇐⇒ Repulsion−s,−v(−v

0

).

16
5 Criteria

As stated in Definition 7 in Section 3.1, a criterion is a parametric set of vectors

with parameters s and v. This section presents concrete examples of criteria that

are useful when proving coordination and independence for the safety properties

Divergence, ConflictFree, and Repulsion. Theorems about these criteria are presented, including whether they are closed under sum, sum independent, independent

of length, symmetric, and antisymmetric. One criterion that is particularly helpful

when proving results about conflict resolution algorithms is the horizontal criterion,

given by Definition 13 in Section 5.1. In Section 5.3, proofs of some fundamental

properties of this criterion are presented, including a proof that it is maximal among

signed, symmetric criteria that are independent of length and coordinated for ConflictFree. Finally, in Section 5.4, the notions of criteria, coordination, independence,

and resolution algorithms are all extended to a three dimensional airspace. In that

section, an antisymmetric criterion is defined for vertical maneuvers, and it is proved

that this criterion is coordinated for the 3D version of the ConflictFree safety property. This new criterion is combined with the horizontal criterion using tools from

Section 3.4 to form a new criterion that is coordinated and allows both vertical and

horizontal resolution maneuvers.

5.1 Divergence, Horizontal, and Repulsion Criteria

Figure 1 illustrates the criterion D, called divergence criterion, which is defined as

follows.

Ds,v ≡ {v

0

| s · v

0 ≥ 0}. (12)

The following lemma states that the criterion D is independent for the safety property Divergence (Section 4.2) and, if ksk

2 ≥ D, it is also independent for the safety

property ConflictFree (Section 4.1).

Lemma 16.

• For all v

0 ∈ Ds,v, Divergences,v

(v

0

) holds.

• If ksk

2 ≥ D, then for all v0 ∈ Ds,v, ConflictFrees,v

(v

0

) holds.

Proof. By Formula (9) in Section 4.2, D consists of all vectors that satisfy the

predicate Divergence. The second part is a direct consequence of the definition of

the predicate Divergence.

Figure 2 illustrates the signed criterion Hε, called horizontal criterion, which is

defined as follows.

Hε

s,v ≡ {v

0

| ksk ≥ D and s · v

0 ≥

ε

D

(s · v

0⊥)

p

ksk

2 − D2}. (13)

The signed criterion Hε

s,v defines two criteria: H1s,v

, which is shown in blue, and

H−1

s,v

, which is shown in green. The sets H1

s,v and H−1s,v are not disjoint. Indeed,

vectors in the gray area are in both sets. The following lemmas state that the signed

criterion Hεis ConflictFree -independent.

17
Ds,v

0

v

s

Figure 1. Divergence Criterion D

H−1

s,v

v

s

0

D

H1

s,v

Figure 2. Horizontal Criterion Hε

18
v

D

s

0

Deriv p(H−1)

Figure 3. Derived Horizontal Criterion Deriv p(H−1)

Lemma 17. For all v

0 ∈ Hε

s,v

, ConflictFrees,v(v

0

) holds.

Figure 3 illustrates the derived horizontal criterion Deriv p(H−1), when p ≤ 1.

That criterion is a superset of H−1. However, in contrast to H−1, the derived

criterion Deriv p(H−1) is not independent for the safety property ConflictFree when

p > 0. As shown by Figure 3, some vectors in Deriv p(H−1) intersect the protected

area around the intruder aircraft.

Figure 4 illustrates the signed criterion Rε, called repulsion criterion, which is

defined as follows.

Rε

s,v ≡ {v

0

| ε s · v

⊥ ≤ 0 and s · v < 0 and s · v0 ≤ 0 and ε v0

· v

⊥ < 0}. (14)

The set Rε

s,v

is always empty when ε = sign(s · v

⊥). The following lemma gives

sufficient conditions under which the signed criterion Rεis Repulsion-independent

(Section 4.3).

Lemma 18. If Conflict(s, v) holds, then for all v

0 ∈ Rε

s,v

, Repulsions,v(v

0

) holds.

Proof. Suppose Conflict(s, v) holds and v

0 ∈ Rε

s,v

, but that Repulsions,v(v

0

) does

not hold. By the definition of the predicate Repulsion, tca(s, v) and tca(s, v

0

) are

both positive. It suffices to prove that

ks + tca(s, v) vk < ks + tca(s, v

0

) v

0

k.

It is a basic property of linear algebra that if e1 and e2 are any two nonzero

orthogonal vectors, then any vector w can be written as a linear combination of e1

19
s

0

v

R−1

s,v

Figure 4. Repulsion Criterion Rε

and e2 as follows.

w =

w · e1

ke1k

2

e1 +

w · e2

ke2k

2

e2.

Further, with such a decomposition, the squared norm kwk

2

can be computed by

the following equation.

kwk

2 =

(w · e1)

2

ke1k

2

+

(w · e2)

2

ke2k

2

.

Let stca = s + tca(s, v) v. It is easy to see from the definition of the function tca

that stca and v are orthogonal. Thus, the following equation is satisfied.

v

0 =

v

0

· stca

kstcak

2

stca +

v

0

· v

kvk

2

v.

Similarly, s + tca(s, v) v can be written as a linear combination of v and v

⊥, and

since it is perpendicular to v and −ε s · v

⊥ is nonnegative, it follows that

ks + tca(s, v) vk =

−1

kvk

ε s · v

⊥.

If it can be proved that

ks + tca(s, v

0

) v

0

k ≥ −1

kvk

(ε s · v

⊥ + ε tca(s, v0

) v

0

· v

⊥), (15)

then the result will follow, because tca(s, v

0

) > 0, and by hypothesis, −ε v

0

·v

⊥ > 0.

Thus, it suffices to prove Equation (15). It follows from definitions that

−ε s · v

⊥ − ε tca(s, v0

) v

0

· v

⊥ = (s + tca(s, v0

) v

0

) · (−ε v

⊥)

≤ ks + tca(s, v

0

) v

0

k k − ε v

⊥k

= ks + tca(s, v

0

) v

0

k kvk,

20
where the inequality is given by the Cauchy-Schwartz inequality. The result follows

from there.

5.2 Coordination Properties of D, Hε, and Rε

Proven facts about these criteria are presented below, including whether they are

closed under sum, sum independent, independent of length, symmetric, and antisymmetric. These results are used to deduce that the criteria D, Hε

, and Rε, defined

in Section 5.1, are coordinated with themselves for the safety properties Divergence,

ConflictFree, and Repulsion, respectively.

Lemma 19. The criteria D, Hε, and Rε, for ε = ±1, are all closed under sum.

Lemma 20. The complement of the predicates ConflictFree and Divergence are

closed under sum.

Lemma 21. All of the following propositions hold.

1. The Criterion D is sum independent for Divergence.

2. The Signed criterion Hεis sum independent for ConflictFree.

3. The Signed criterion Rεis sum independent for Repulsion.

Lemma 22. The criteria D, Hε, and Rε, for ε = ±1, are all independent of length.

Lemma 23. The safety properties Divergence, ConflictFree, Repulsion, and their

complements, are all independent of length.

Lemma 24. The criteria D, Hε, and Rε, for ε = ±1, are all symmetric.

The results in Section 3.3, which relate coordination between criteria to these

simpler geometric properties, are used to deduce coordination for the criteria defined

in Section 5.1.

Theorem 25. The criteria D, Hε, and Rε are coordinated with themselves for the

safety properties Divergence, ConflictFree, and Repulsion, respectively.

Proof. This follows from Corollary 5 in Section 3.3 and from lemmas 19 to 24.

The horizontal criterion Hεsatisfies all the hypotheses of Theorem 9. Hence,

even although in general the derived criterion Deriv p(Hε) is not independent or

coordinated with itself for the safety property ConflictFree, it is always coordinated

with Hεfor the safety property ConflictFree.

Lemma 26. For ε = ±1 and p ≥ 0, the derived criterion Deriv p(Hε) is ConflictFreecoordinated with Hε

.

The following theorem is a consequence of Lemma 26. Its usefulness is illustrated

in Section 7.3 to prove that two distinct resolution algorithms are ConflictFreecoordinated.

21
Theorem 27. Suppose that cro and cri are resolution algorithms for the ownship

and the intruder aircraft, respectively, such that cro satisfies Hε and that for all

vectors so, si, vo, vi, v

0

i

, v

0

i ∈ cri(si

, so, vi, vo) implies v

0

i − vi ∈ Hε

si−so,vi−vo

. Then

cro and cri are coordinated for the safety property ConflictFree.

Proof. By lemma 26, it suffices to prove that the algorithm cri satisfies the criterion

Deriv 1(Hε). That is, it suffices to prove that if v

0

i ∈ cri(si

, so, vi, vo), then v

0

i−vo ∈

Deriv 1(Hε)si−so,vi−vo, or equivalently (v

0

i − vo) − (vi − vo) ∈ Hε

si−so,vi−vo

. Since

(v

0

i − vo) − (vi − vo) = v

0

i − vi

, the result follows.

5.3 Fundamental Properties of Horizontal Criterion

According to Lemma 17, the horizontal criterion Hεis ConflictFree-independent

and, according to Theorem 25, Hεis also ConflictFree-coordinated. Since ConflictFree is the intended safety property of conflict resolution algorithms, the horizontal

criterion is particularly important for designing CD&R algorithms and for verifying

their coordination properties.

This section provides some fundamental results on the horizontal criterion. First,

it is proved that any conflict resolution algorithm that computes relative velocity

vectors that are tangent to the protected zone satisfies the horizontal criterion and,

therefore, it is independent and coordinated for the safety property ConflictFree.

Second, it is shown that the horizontal criterion is maximal among signed criteria

that are symmetric, independent of length, and coordinated for ConflictFree.

5.3.1 Tangential Resolutions Satisfy Horizontal Criterion

A common approach to developing algorithms that resolve conflicts between the

ownship and the intruder is to find a new velocity vector v

0

o

for the ownship such

that the new relative velocity vector v

0 = v0

o−vi has the property that the trajectory

from s along v

0

is tangent to the circle of radius D around the origin. If the intruder

does not maneuver, then the minimum separation between the aircraft is precisely

D. Here, these kinds of resolutions are called line solutions.

In Figure 5, the vector v

0

is tangent to the right side of the circle. From this

diagram, it is clear that s · v

0⊥ = D kv0⊥k = D kv0k. Similarly, in the case where

the trajectory from s along v

0

is tangent to the left side of the circle, the equation

−s · v

0⊥ = D kv0k holds. In addition, since the trajectory from s along v0

reaches

the tangent point at a nonnegative time, and since this time is equal to tca(s, v

0

),

it follows from the definition of the function tca that s · v

0 ≤ 0.

This motivates the following definition of the predicate LineSolution, which determines whether a given trajectory, in the relative coordinate system, is tangent

to the circle of radius D around the origin. The predicate depends on a unit value

ε = ±1, with ε = −1 corresponding to a right tangent and ε = 1 to a left tangent.

LineSolution(s, v

0

, ε) ≡ −ε s · v

0⊥ = Dkv0

k and s · v

0 ≤ 0. (16)

This predicate holds for vectors s and v

0 precisely when the half line s + t v0

,

with t ≥ 0, is tangent to the circle of radius D around the intruder in the relative

coordinate system.

22
0

v

0⊥

v

0

s

D

Figure 5. Relative Vector v

0 Tangent to the Circle

Lemma 28. If LineSolution(s, v

0

, ε) holds, then

ks + tca(s, v

0

) v

0

k = D.

Since line solutions characterize tangent trajectories to the circle of radius D,

they yield conflict free resolutions. This fact is a direct consequence of Theorem 14

and Lemma 28.

Theorem 29. If LineSolution(s, v

0

, ε) holds, then ¬Conflict(s, v

0

).

The function tangent line, defined below, is used to compute vectors that

satisfy the predicate LineSolution. It takes as arguments a relative position vector

s such that ksk ≥ D and a unit value ε = ±1. It returns a vector that is tangent to

the protected zone.

tangent line(s, ε) ≡

if ksk = D then

ε s

⊥

else

let d = ksk

2

in

(

D2

d

− 1) s +

ε D√

d − D2

d

s

⊥

endif

(17)

The proofs of the following lemmas rely on standard vector algebra.

Lemma 30. If ksk ≥ D and ε = ±1, then LineSolution(s, tangent line(s, ε), ε)

holds.

23
Lemma 31. If ksk ≥ D, then LineSolution(s, v

0

, ε) holds if and only if there exists

k ≥ 0 such that

v

0 = k tangent line(s, ε).

Lemma 32 gives an alternative characterization of the horizontal criterion that

uses the function tangent line.

Lemma 32. For all vectors s and v, and ε = ±1,

Hε

s,v = {v

0

| ksk ≥ D and εtangent line(s, ε) · v

0⊥ ≥ 0}.

The following lemma states that vectors that satisfy the predicate LineSolution

also satisfy the horizontal criterion. Therefore, since by Theorem 25, the horizontal

criterion Hεis ConflictFree-coordinated, resolution algorithms that compute line

solutions are also ConflictFree-coordinated. This result is stated by Theorem 34.

Lemma 33. If ksk ≥ D and LineSolution(s, u, ε) holds, then u ∈ Hε

s,v

.

Proof. By Lemma 31, if LineSolution(s, u, ε) holds, then there exists k ≥ 0 such

that u = k tangent line(s, ε). Thus, ε tangent line(s, ε) · u

⊥ = 0, and the result

follows directly from Lemma 32.

Theorem 34. Suppose that cro and cri are resolution algorithms for the ownship

and the intruder, respectively, and that for all vectors so, si, vo, vi, v

0

o

, v

0

i

,

1. v

0

o ∈ cro(so, si

, vo, vi) implies that LineSolution(s, v

0

o − vi

, ε) holds, and

2. v

0

i ∈ cri(si

, so, vi, vo) implies that LineSolution(−s, v

0

i − vo, ε) holds.

Then cro and cri are coordinated for the safety property ConflictFree.

Proof. By Theorem 2 in Section 3.1 and Theorem 25, it suffices to prove that cro

and cri each satisfy the criterion Hε. This follows immediately from Lemma 33.

5.3.2 Maximality of Horizontal Criterion

Theorem 35 (Maximality of Hε). Suppose that Aεis a symmetric signed criterion

that is independent of length and contains the horizontal criterion Hε. If Aεis

coordinated for ConflictFree and ¬ConflictFrees,v(v) holds, then Aε

s,v = Hεs,v

.

Proof. Note that Theorem 4 implies that Aεis sum independent. By contradiction,

suppose that there are vectors s, v, and v

0

such that v

0 ∈ Aε

s,v

, v

0 ∈ H /ε

s,v

, and

¬ConflictFrees,v(v) holds. By Lemma 32,

ε tangent line(s, v) · v

0⊥ < 0.

By using the Cauchy-Schwartz inequality, it is shown that there exists δ > 0 such

that for every vector w with kwk < δ, ε tangent line(s, v) · (v

0 + w)⊥ < 0. For

any such vector w, v

0 + w ∈ H/ε

s,v

.

Choose any positive real number c such that kc sk < δ. Therefore, v

0+c s ∈ H/ε

s,v

.

By Lemma 32, if u is any vector that is not an element of the set Hε

s,v

, then the

24
Kε

D

s

0

v

Figure 6. Criterion Kε

negative vector −u is an element of this set. Applying this to the vector v

0 + c s, it

follows that −v

0 −c s is an element of Hε

s,v and therefore an element of Aεs,v as well.

Since −v

0−c s and v0 are both elements of Aε

s,v

, and since A is sum independent,

it follows that their sum, which is equal to −c s, satisfies ConflictFrees,v(−c s). This

is a contradiction since s +

1

c

(−c s) = 0.

The theorem above states that the horizontal criterion is maximal among symmetric, coordinated, signed criteria that are independent of length. This result is

false if the hypothesis of length-independence is removed, even among criteria that

are ConflictFree-independent. In particular, the derived criterion Deriv

1

2 (Hε

) contains the horizontal criterion Hε

. This derived criterion is coordinated with itself

by Theorem 9 in Section 3.4. Define a new signed criterion Kε as follows.

K

ε

s,v ≡ Deriv

1

2 (Hε

)s,v ∩ (Hε

s,v ∪ H−ε

s,v

). (18)

This criterion is shown graphically in Figure 6.

It follows from definitions that the criterion Kεis symmetric. By Lemma 17 , Hε

and H−ε are ConflictFree-independent. Since Kεis contained in the union of these

two sets, Kεis ConflictFree-independent as well. However, since Deriv

1

2 (Hε

) is not

independent of length, neither is the signed criterion Kε. If ¬ConflictFrees,v(v

0

)

holds, then Hε

s,v ⊂ Kεs,v and this inclusion is proper. Thus, the horizontal criterion

Hεis not maximal among symmetric, ConflictFree-coordinated, signed criteria.

25
5.4 Three-Dimensional Criteria

For notational convenience, the mathematical framework presented in this paper is

illustrated in the Euclidean 2-dimensional airspace. However, all definitions such

as those of safety property, conflict resolution algorithm, independence, coordination, criterion, etc., and their properties, naturally extend to the Euclidean 3-

dimensional geometry. The formal development in PVS discussed in this paper is

both 2-dimensional and 3-dimensional.

As opposed to the rest of this paper, all vectors in this section, e.g., the position

and velocity vectors of the aircraft so, si, vo, vi, are assumed to be 3-dimensional.

Furthermore, u(x,y) and uz denote the 2-dimensional and vertical projections of u,

respectively. When r is a real number, the notation u with [z ← r] denotes the

3-dimensional vector (ux, uy, r).

In the Euclidean 3-dimensional airspace, the separation requirement for two

aircraft is specified by a minimum horizontal separation D and a minimum vertical

separation H, which is typically 1000 feet. In the relative 3-dimensional coordinate

system, the separation requirement is represented by a cylinder of radius D and

half-height H around the intruder aircraft. A loss of separation between two aircraft

occurs when the ownship enters this cylinder, i.e., when the following inequalities

hold

k(so − si)(x,y)k < D,

|(so − si)z| < H.

A conflict in the 3-dimensional airspace is defined as a projected loss of separation

and is formally defined by the predicate 3DConflict.

3DConflict(s, v) ≡ ∃ t ≥ 0 : k(s + t v)(x,y)k < D and |(s + t v)z| < H,

where s = so − si and v = vo − vi. Therefore, the 3-dimensional predicate

3DConflictFree is defined as follows.

3DConflictFrees,v(v

0

) ≡ ¬3DConflict(s, v

0

). (19)

The following lemma relates two-dimensional and three-dimensional conflicts.

Lemma 36. A 3-dimensional conflict implies a 2-dimensional one, i.e.,

3DConflict(s, v) =⇒ Conflict(s(x,y), v(x,y)).

Moreover, 3-dimensional ConflictFree is implied by the 2-dimensional one, i.e.,

ConflictFrees(x,y)

,v(x,y)

(v

0

(x,y)

) =⇒ 3DConflictFrees,v(v

0

).

The parametric predicate 3DConflictFree is a safety property, i.e., it satisfies

that for all 3-dimensional vectors v

0

,

3DConflictFrees,v(v

0

) ⇐⇒ 3DConflictFree−s,−v(−v

0

).

26
Furthermore, the complement of 3DConflictFree, i.e., the set of vectors that satisfy

¬3DConflictFree, is closed under sum.

The natural 3-dimensional extension of the horizontal criterion Hε, called 3DHε,

is defined as follows.

3DHε

s,v ≡ {v

0

| v

0

(x,y) ∈ Hε

s(x,y),v(x,y)

}

As stated by the following theorem, the criterion 3DHεsatisfies all the properties

of its 2-dimensional counterpart Hε.

Theorem 37. The three-dimensional signed criterion 3DHε

s,v

is independent for the

safety property 3DConflictFree. Furthermore, it is symmetric and sum independent

for 3DConflictFree.

The following theorem follows from Theorem 3 in Section 3.3, Theorem 37, and

properties of the predicate 3DConflictFree.

Theorem 38. The signed criterion 3DConflictFree is coordinated with itself for

3DConflictFree.

A more interesting example of a 3-dimensional signed criterion is the vertical

criterion V

ε

, which is defined as follows.

V

ε

s,v ≡ {v

0

| (kv(x,y)k = 0 and ε v

0

z ≥ 0 and ε sz ≥ H)

or

(let ι = if |sz| ≥ H then ε sign(sz) else −1 endif in

∆(s(x,y), v(x,y)) > 0 and ΘD(s(x,y), v(x,y), ι) > 0 and

let p = (s + ΘD(s(x,y), v(x,y), ι) v) with [z ← ε H] in

IntersectsHalfPlane(s, v

0

, p, ε))},

where

IntersectsHalfPlane(s, v

0

, p, ε) ≡ v

0

· p 6= 0 and

let t =

D2 − s · p

v0· p

in

t ≥ 0 and

ε (sz + t v

0

z

) ≥ ε pz,

Intuitively, the set V

ε

s,v

consists of vectors v

0

that solve a predicted conflict by

maintaining vertical separation when the aircraft are not horizontally separated. In

the vertical criterion V

ε

, the unit value ε represents the two possible regions for

vertical resolution: up, when ε = 1, and down, when ε = −1. Figure 7 illustrates

V

ε when ε = 1. Reference [12] provides a detailed description of this criterion.

Lemma 39. The signed criterion V

ε

is independent for 3DConflictFree, i.e., for

all v

0 ∈ Vε

s,v

, 3DConflictFrees,v(v

0

) holds.

27
V

1

s,v

v s 0

v

p

s + ΘD(s(x,y), v(x,y), −1) v

Figure 7. Vertical Criterion V

1

The vertical criterion V

ε

is an example of an antisymmetric criterion. Furthermore, it is sum independent for the safety property 3DConflictFree. Therefore, by

Theorem 6 in Section 3.3, the following coordination property holds.

Theorem 40. The vertical criterion V

ε

is coordinated with V

−ε

for the safety property 3DConflictFree.

In contrast to the horizontal criterion where both aircraft have to use the same

horizontal direction, i.e., both left or both right, to solve a predicted conflict, the vertical criterion requires that the aircraft use opposite vertical directions, i.e., up/down

or down/up, to solve the conflict.

Theorems 38 and 40 guarantee that the horizontal and vertical criteria are each

coordinated with themselves for 3DConflictFree. However, those theorems do not

guarantee that the criteria are coordinated with each other. In general, it does

not hold that two algorithms cro and cri that satisfy, respectively, the horizontal criterion 3DHε and the vertical criterion V

ε are coordinated for 3DConflictFree.

Theorem 11 in Section 3.4 provides a simple way to combine different criteria, which

are coordinated with themselves for a safety property P. The composed criterion

contains vectors in both criteria and is coordinated for P. The following theorem

provides a criterion C

εh,εv

, parametric by two unit values εh and εv, that is coordinated for 3DConflictFree.

Theorem 41. Let C

εh,εv be the criterion defined as the following set of 3-dimensional

vectors.

C

εh,εv

s,v ≡ Comp(3DHε

, V

ε

)s,v.

The criterion C

εh,εv

is coordinated with C

εh,−εv

for the safety property 3DConflictFree.

Proof. The results follows directly from theorems 11 (Section 3.4), 37, 40, and the

fact that the complement of the predicate 3DConflictFree is closed under sum.

28
Finally, Theorem 41 gives sufficient conditions to show that two, possibly different, 3-dimensional conflict resolution algorithms are coordinated.

Theorem 42. Let cro and cri be 3-dimensional conflict resolution algorithms. If

cro satisfies C

εh,εv and cri satisfies Cεh,−εv

, then cro and cri are coordinated for

3DConflictFree.

Proof. The result follows from Theorem 2 in Section 3.1 and Theorem 41.

The criterion C

εh,εv

illustrates the usefulness of composing two criteria using

Comp. The composed criteria is coordinated for 3DConflictFree. Since it is 3-

dimensional, it allows for both horizontal and vertical maneuvers. This criterion is

at the basis of a standard for guaranteeing implicit coordination of 3-dimensional

conflict resolution algorithms [12] in a distributed self-separation airspace concept.

6 Conflict Resolution Algorithms

As defined in Section 2, an algorithm that returns guidance maneuvers that attempt to restore a safety property is called a resolution algorithm. When the safety

property is ConflictFree, the algorithm is called a conflict resolution algorithm.

This section provides several examples of conflict resolution algorithms and states

some basic properties of these algorithms. In particular, the following algorithms

are described: the Modified Voltage Potential algorithm [8] developed at the National Aerospace Laboratory (NLR) in the Netherlands, an algorithm for track angle

maneuvers developed at NASA Langley Research Center as part of the Airborne

Coordinated Conflict Resolution and Detection (ACCoRD) framework [13], and the

Geometric Optimization algorithm [2] for track angle maneuvers developed at NASA

Ames Research Center. The main results in this section are that the Modified Voltage Potential algorithm is not ConflictFree-independent and that the track-angle

algorithms of ACCoRD and Geometric Optimization are ConflictFree-independent.

6.1 Modified Voltage Potential

The Modified Voltage Potential [8] algorithm MVP is a conflict resolution algorithm

developed by NLR in the Netherlands. It takes as inputs the current state vectors

of the aircraft, i.e., so, si, vo, vi, and returns either an empty set if a resolution is

not found or a singleton set {v

0

o}, where v

0

o

is a new velocity vector for the ownship.

The algorithm relies on the function tca, defined in Section 4.3, which gives the

time of closest approach between the aircraft. The first step of the MVP algorithm is

to compute the time tca(s, v), where v = vo − vi. Then, the algorithm computes

the relative position of the two aircraft at the time tca(s, v), when the aircraft

achieve minimum separation. The relative position at this time is s + tca(s, v) v,

which is denoted stca and graphically shown in Figure 8. Here, it is assumed that

the aircraft are currently in conflict, although this is not required for the definition

of the algorithm MVP.

In Figure 8, the point stca is shown at the end of the dotted line. It is perpendicular to the vector v , i.e., stca · v = 0. If stca 6= 0, then the algorithm MVP returns a

29
0

stca

s

p

v

D

Figure 8. Relative Position stca at Time of Closest Approach

velocity vector v

0

o

for the ownship such that the relative vector v

0 = v0

o −vi satisfies

s + tca(s, v) v

0 = p,

where p denotes D

kstcak

stca. This is illustrated in Figure 9.

Thus, if tca(s, v) > 0, then v

0

o

can be calculated as follows.

v

0

o =

1

tca(s, v)

(p − s) + vi

=

1

tca(s, v)

(

D

kstcak

stca − s) + vi

=

1

tca(s, v)

(

D

kstcak

stca − (stca − tca(s, v) v)) + vi

=



D − kstcak

tca(s, v) kstcak



stca + v + vi

=



D − kstcak

tca(s, v) kstcak



stca + vo.

(20)

Equation (20) motivates the following definition of the algorithm MVP, which

returns the empty set if the time tca(s, v) is not positive or the vector stca is equal

to 0.

30
0

D

stca

s

p

v

0 v

Figure 9. MVP’s Relative Vector v

0 = v0

o − vi

MVP(so, si, vo, vi) ≡

let

s = so − si,

v = vo − vi,

stca = s + tca(s, v) v

in

if tca(s, v) > 0 and stca 6= 0 then

let v

0

o =



D − kstcak

tca(s, v) kstcak



stca + vo in

{v

0

o}

else

∅

endif

(21)

The next lemma follows directly from Equation (20) and states that the resolution maneuver provided by MVP achieves a distance D at the original time of closest

approach tca(s, v). Unfortunately, as shown by Theorem 44, this result does not imply that MVP achieves a distance D at the time of closest approach for the resolution

maneuver, i.e., tca(s, v

0

o − vi).

31
Lemma 43. For all s = so − si and v = vo − vi, if v

0

o ∈ MVP(so, si

, vo, vi) then

s + tca(s, v) (v

0

o − vi) = D

kstcak

stca,

where stca = s + tca(s, v) v.

The Modified Voltage Potential algorithm MVP is not independent for ConflictFree. In fact, a stronger result can be shown: if MVP returns a vector, then this

vector is always in conflict.

Theorem 44. Let s be the relative vector so − si. If ksk > D, Conflict(s, vo − vi)

holds, and v

0

o ∈ MVP(so, si

, vo, vi), then Conflict(s, v

0

o − vi) holds.

Proof. The formal proof is based on algebraic reasoning. A geometric, intuitive

proof of this result is given here. To understand the reasoning behind this theorem,

consider the diagram in Figure 9, which shows the geometric interpretation of the

vector v

0

o

computed by MVP(so, si, vo, vi). The triangle formed by the segments

s, stca, stca, p, and p, s is a right triangle. Since the sum of the interior angles of

any triangle is π, it follows that the interior angle formed by the segments stca, p

and p, s is strictly less than π

2

. Thus, the trajectory from s along the relative vector

v

0

o − vi

is not tangent to the circle. By Lemma 43, this trajectory does touch the

circle at the point p. It follows that this trajectory must touch the circle at two

distinct places, and it therefore passes through the interior of the circle.

6.2 ACCoRD’s Track Angle Resolution

ACCoRD is a mathematical framework for the design and formal verification of

state-based separation assurance algorithms [13]. The framework is written in PVS

and includes conflict resolution algorithms for track angle, ground speed, combined

track angle and ground speed, and vertical speed maneuvers. This paper only considers the algorithm for track angle maneuvers, which will be denoted ACCoRDtrackε

,

where ε is a unit value ±1. The main theorem in this section states that for ε = ±1,

ACCoRDtrackεis ConflictFree-independent.

The algorithm ACCoRDtrackε, where ε = ±1, has as arguments the vectors so,

si, vo, and vi. It returns a set of at most two vectors where each one of these

vectors, say v

0

o

, is a new velocity vector for the ownship such that kv

0

ok = kvok, i.e.,

v

0

o

represents a track angle maneuver for the ownship. Furthermore, the relative

velocity vector v

0 = v0

o − vi

is tangent to the circle on the side corresponding to the

unit value ε, i.e., it satisfies LineSolution(s, v

0

, ε) as defined in Section 5.3.1.

If v

0

o

is a track angle maneuver for the ownship and LineSolution(s, v

0

o − vi

, ε)

holds, then it follows from Lemma 31 that there is some k ≥ 0 such that

kvok

2 = kk tangent line(s, ε) + vik

2

. (22)

Equation (22) has the form kvok

2 = kk u + vik2

, for a given vector u. It is possible

to define a function that solves equations of this form for real numbers k. It follows

from the equation kvok

2 = kk u + vik2

that

0 = kk u + vik

2 − kvok2

= kuk

2

k

2 + (2 vi

· u)k + (kvik

2 − kvok2

).

(23)

32
This is a quadratic equation in k, which has at most two distinct solutions. Each

one of these solutions yields a resolution vector v

0

o

for the ownship. The solutions

to Equation (23) are given by −b+ι

√

b

2−4ac

2a

, where ι = ±1, and

a = kuk

2

,

b = 2 vi· u,

c = kvik

2 − kvok2

.

Thus, if b

2 − 4 a c ≥ 0 and k =

−b+ι

√

b

2−4 a c

2a > 0, then the vector v

0

o defined by

v

0

o = k +vi satisfies both kv

0

ok = kvok and LineSolution(s, v

0

o−vi

, ε). This motivates

the definition of the function track only line, which returns a real number.

track only line(u, vo, vi

, ι) ≡

let

a = kuk

2

,

b = 2 vi· u,

c = kvik

2 − kvok2

in

if b

2 − 4ac ≥ 0 then

−b + ι

√

b

2 − 4ac

2a

else

0

endif

(24)

The next lemma states that the algorithm track only line computes solutions

for k to the equation v

0

o = k u + vi

, where kv

0

ok = kvok.

Lemma 45. If u 6= 0, then kv

0

ok = kvok and k u = v

0

o − vi if and only if

k = track only line(u, vo, vi, ι),

for some ι = ±1.

Using track only line, the algorithm ACCoRDtrackε

, which computes track

angle maneuvers v

0

o

for the ownship that satisfy LineSolution(s, v

0

o − vi

, ε), for ε =

33
±1, can be defined as follows.

ACCoRDtrackε(so, si, vo, vi) ≡

let

s = so − si,

u = tangent line(s, ε),

k1 = track only line(u, vo, vi

, 1),

k2 = track only line(u, vo, vi, −1),

in

if k1 ≥ 0 then {k1 u + vi} else ∅ endif

∪

if k2 ≥ 0 then {k2 u + vi} else ∅ endif

(25)

Lemma 46 states that ACCoRDtrackεresolutions are correct and complete for

line solutions that are track angle maneuvers.

Lemma 46. Let s = so − si such that ksk ≥ D. For all ε = ±1, kv

0

ok = kvok and

LineSolution(s, v

0

o − vi

, ε) holds if and only if

v

0

o ∈ ACCoRDtrackε

(so, si, vo, vi).

The next theorem states that ACCoRDtrackεis ConflictFree-independent.

Theorem 47 (ACCoRDtrackεIndependence). For all vectors so, si, vo, vi, v

0

o and

ε = ±1, if

v

0

o ∈ ACCoRDtrackε

(so, si, vo, vi)

and Conflict(so − si, vo − vi) holds, then it holds that

ConflictFreeso−si,vo−vi

(v

0

o − vi).

Proof. By Theorem 29 and Lemma 46.

6.3 Geometric Optimization’s Track Angle Resolution

The geometric optimization approach to state-based conflict resolution [2] consists

of algorithms for track angle, ground speed, and combined track angle and ground

speed maneuvers. This paper only considers the track angle algorithm, which will

be denoted GOtrackε

f

, where ε is a unit value ±1 and f ≤ 1 is a nonnegative real

number. In the case where f = 1, the algorithm returns a maneuver vector for the

ownship such that if the intruder does not maneuver, then the resulting relative

velocity vector is tangent to the circle of radius D around the origin. The unit value

ε corresponds to the side of the circle, from the perspective of the ownship, on which

this relative vector is tangent, with ε = −1 corresponding to a right tangent and

ε = 1 to a left tangent.

The algorithm takes as inputs the current state vectors of the aircraft, i.e.,

vectors so, si, vo, vi. It returns a set of at most two vectors where each one of these

34
vectors, say v

0

o

, is a new velocity vector for the ownship such that kv

0

ok = kvok, i.e.,

v

0

o

represents a track angle maneuver for the ownship.

In the construction that follows, it will be implicit that the aircraft are currently

in conflict. If this is not the case, then the algorithm returns the empty set. The

main theorem in this section states that GOtrackε

f

is ConflictFree-independent when

the parameter f is equal to 1.

In order to specify the algorithm, some basic notation and trigonometric functions are needed. The first of these is the function track, which computes the track

angle of a vector, relative to true North. It is defined for u 6= 0 as follows.

track(u) ≡ atan2(uy, ux). (26)

Here, atan2(uy, ux) is the angle α that satisfies the equation u = (sin(α), cos(α)).

By convention, track(0) = 0.

The second function that is needed in the definition of the algorithm takes an

angle α, which is any real number, and returns another angle, trigonometrically

equivalent to α, which lies in the interval [0, 2π). It is defined by the following

equation.

to2pi(α) ≡ α − 2π · floor  α

2π



. (27)

It is easy to see that if α ∈ [0, 2π), then to2pi(α) = α.

Next, the algorithm GOtrackε

f

relies on the function angleto, which returns the

angle from one angle to another. The angle returned by this function lies in the

interval [−π, π). This function is defined as follows.

angleto(α, β) ≡ to2pi((β − α) + π) − π. (28)

Here, α and β are any real numbers.

Lemma 48. The angle α + angleto(α, β) is trigonometrically equivalent to β in

the sense that (α + angleto(α, β)) − β is an integer multiple of 2π.

There are various ways to define the function angleto so that it has the desired

properties. One such property, which has been proved for the definition of angleto

given in Equation (28), is given by the following lemma.

Lemma 49. If |α − β| < π, then angleto(α, β) = β − α.

The first step in the algorithm GOtrackε

f

is to compute the angle change α needed

in the relative velocity vector v = vo − viin order to achieve a tangent to the circle

of radius D around the origin. The side of the circle on which the tangent occurs

is determined by ε. The angle α is illustrated in Figure 10 for ε = −1 (a right

tangent), and its value is given in Formula (29).

If f ≤ 1, then any velocity vector v

0

o

returned by the algorithm results in a new

relative velocity vector v

0 = v0

o − vi that lies between the current velocity vector v

and a tangent vector to the circle on the side corresponding to ε. That is, the angle

from v to the vector v

0

is equal to f α. The function χ

∗

rel, defined below, computes

the track angle β of v

0

. This is illustrated in Figure 11.

35
0

s

v α

D

Figure 10. Angle Change α Needed for a Tangent

0

s

v

v

0

β

f α

α

D

Figure 11. Track Angle β of GOtrack’s v

0 = v0

o − vi

36
χ

∗

rel(s, v, f, ε) ≡ to2pi(track(v) + f α), (29)

where α denotes the angle angleto(track(v), track(−s) − ε asin( D

ksk

)).

The next lemma shows that if f = 1, then χ

∗

rel computes the track angle of a

vector that is tangent to the circle, on the side corresponding to the unit value ε.

Lemma 50. If k > 0, β = χ

∗

rel(s, v, 1, ε), and u = k · (sin(β), cos(β)), then

LineSolution(s, u, ε) holds.

The algorithm GOtrackε

f

is defined using the function χ

∗

rel. Any vector v

0

o

returned by the algorithm is a track angle maneuver for the ownship, i.e., kv

0

ok = kvok.

Furthermore, if f ≤ 1, then the relative velocity vector v

0

o − vi satisfies

track(v

0

o − vi) = χ

∗

rel(s, vo − vi

, f, ε).

The algorithm GOtrackε

f

is defined as follows.

GOtrackε

f

(so, si, vo, vi) ≡

let

s = so − si,

v = vo − vi,

β = χ

∗

rel(s, v, f, ε)

in

if v = 0 or

kvik

kvok

|sin(β − track(vi))| > 1 then

∅

else

let

e =

kvik

kvok

|sin(β − track(vi))|,

θ1 = β − asin(e),

v

0

o1 = kvok (sin(θ1), cos(θ2)),

θ2 = β − sign(asin(e))π + asin(e),

v

0

o2 = kvok (sin(θ2), cos(θ2))

in

if s · (v

0

o1 − vi) ≥ 0 then {v

0

o1

} else ∅ endif

∪

if s · (v

0

o2 − vi) ≥ 0 then {v

0

o2

} else ∅ endif

endif

(30)

The following lemma states that GOtrackε

f

returns the ownship’s current velocity

vector when f = 0.

Lemma 51. If s · (vo − vi) < 0 and v

0

o ∈ GOtrackε

0

(so, si, vo, vi), then v

0

o = vo.

37
An important property of the algorithm GOtrackε

f

is given by Theorem 53. The

proof of that theorem relies on the following lemma.

Lemma 52. If v

0

o ∈ GOtrackε

f

(so, si, vo, vi) and β = χ

∗

rel(s, vo − vi

, f, ε), then

kvik sin(β − track(vi)) = kvok sin(β − track(v

0

o

)).

Proof. By hypothesis, the algorithm returns a nonempty set. Therefore, v 6= 0,

0 ≤ e ≤ 1, and s · (v

0

o − vi) < 0, where

e =

kvik

kvok

|sin(β − track(vi))|,

θ = β − sign(asin(e))π

2

(1 + ι) + ι asin(e),

v

0

o = kvok (sin(θ), cos(θ)),

for some ι = ±1.

Since θ is trigonometrically equivalent to track(v

0

o

), it suffices to prove that

e = sin(χ

∗

rel(s, vo − vi

, f, ε) − θ). Expanding the definition of θ and cancelling equal

terms reduces the proof to the verification of the following equality.

e = sin(sign(asin(e))π

2

(1 + ι) − ι asin(e)).

If ι = −1, then this equation becomes e = sin(asin(e)), which is trivial. Alternatively, if ι = 1, then sign(asin(e))π

2

(1 +ι) is equal to sign(asin(e))π, which is either

−π or π. Thus, it suffices to prove that

e = sin(±π − asin(e)),

which is also trivial.

Theorem 53. If s · (vo − vi) < 0 and v

0

o ∈ GOtrackε

f

(so, si, vo, vi), then

1. kv

0

ok = kvok, and

2. track(v

0

o − vi) = χ

∗

rel(s, vo − vi

, f, ε).

Proof. The proof is sketched here, with the special cases and minor details are

omitted for brevity. As in the proof of Lemma 52, v 6= 0, 0 ≤ e ≤ 1, and s·(v

0

o−vi) <

0, where

β = χ

∗

rel(s, v, f, ε),

e =

kvik

kvok

|sin(β − track(vi))|,

θ = β − sign(asin(e))π

2

(1 + ι) + ι asin(e),

v

0

o = kvok (sin(θ), cos(θ)),

for some ι = ±1. The first part of the theorem is proved by simple algebraic and

trigonometric manipulations:

kv

0

ok = kvokk(sin(θ), cos(θ))k = kvok

q

(sin2(θ) + cos2(θ) = kvok.

38
The second part of the theorem follows from Lemma 52:

kvik sin(β − track(vi)) = |vok sin(β − track(v

0

o

)).

Since θ is trigonometrically equivalent to track(v

0

o

), by the subtraction property of

the sine function,

kvik (sin(β) cos(track(vi)) − sin(track(vi)) cos(β)) =

kvok (sin(β) cos(θ) − sin(θ) cos(β)).

Therefore,

tan(β) = kvok sin(θ) − kvik sin(track(vi))

kvok cos(θ) − kvik cos(track(vi))

=

v

0

ox − vix

v

0

oy − viy

= tan(track(v

0

o − vi)).

It is easy to prove that if w and u are any nonzero vectors where wy 6= 0, uy 6= 0,

wx/wy = ux/uy, s · w < 0, and s · u < 0, then track(w) = track(u). Applying

this to the vectors (sin(β), cos(β)) and v

0

o − vi gives the desired result.

The lemma below follows directly from Lemma 50 and Theorem 53.

Lemma 54. If Conflict(s, vo − vi) holds and v

0

o ∈ GOtrackε

1

(so, si, vo, vi), then

kvok = kv

0

ok and LineSolution(s, v

0

o − vi

, ε) holds.

The next theorem states that GOtrackε

1

is ConflictFree-independent.

Theorem 55 (GOtrackε

1

Independence). For all vectors s = so − si, v = vo − vi,

and v

0

o

, and for all ε = ±1, if

v

0

o ∈ GOtrackε1

(so, si, vo, vi)

and Conflict(s, v) holds, then it holds that

ConflictFrees,v(v

0

o − vi).

Proof. By Theorem 29 and Lemma 54.

6.4 Numerical Example

This section compares the resolution maneuvers computed by the algorithms presented before for a concrete scenario. The algorithms MVP and GOtrackε

f

are implemented in Python. Java and C++ implementations of ACCoRD’s CD&R algorithms

are available from http://shemesh.larc.nasa.gov/people/cam/ACCoRD. All the

implementations use the floating point arithmetic provided by their respective languages.

39
cr v

0

o ∈ cr(so, si

, vo, vi) v

0

i ∈ cr(si

, so, vi, vo)

MVP (484.50, −127.47) (265.49, 77.47)

ACCoRDtrackε(483.99, −135.10) (225.13, 108.69)

GOtrackε

1

(483.99, −135.10) (225.13, 108.69)

GOtrackε

1

2

(494.00, −91.98) (−154.34, 196.67)

Table 1. Maneuvers From Different Resolution Algorithms

Assume that D, so, si, vo, and vi are given as follows, where distances are in

nautical miles (nmi) and speeds are in knots, i.e., nautical miles per hour.

D = 5,

so = (0, 0),

si = (10, 0),

vo = (500, −50),

vi = (250, 0).

Let s = so − si and v = vo − vi be the relative position and velocity vectors,

respectively. In this case,

s = (−10, 0),

v = (250, −50).

The time of closest approach between the aircraft is given by tca(s, v) = 1

26 hours,

which is about 138.5 seconds, and the distance at time of closest approach is about

1.96 miles. Since the minimum safe separation D is 5 nautical miles, the aircraft

are in conflict.

Table 1 shows resolution vectors computed by the conflict resolution algorithms

MVP, ACCoRDtrackε, and GOtrackε

f

, where ε = −1, for the given values from the

ownship’s and intruders’ perspectives. In the case of GOtrackε

f

, the values f = 1

and f =

1

2

are considered. The results have been rounded to 2 decimal places.

According to Lemma 46 and Lemma 54, all maneuvers computed by GOtrackε

1

are

also computed by ACCoRDtrackε. This property is illustrated in the example by

the fact that ACCoRDtrackε and GOtrackε

1

compute the same track angle resolution

maneuvers.

Tables 2 and 3 show the time of closest approach and distance of closest approach

for the resolutions in Table 1 for the independent and coordinated cases, respectively.

The results have been rounded to 2 decimal places. In the independent case, the

distance at time of closest approach is the same from the ownship’s and intruder’s

perspective. Table 2 shows that in the given scenario, MVP and GOtrackε

1

2

do not

achieve separation when only one of the aircraft maneuvers. The fact that MVP

does not achieve separation is a numerical illustration of Theorem 44, which states

that resolution maneuvers computed MVP are always in conflict. Table 2 also shows

that in the independent case, for this scenario, both ACCoRDtrackε and GOtrackε

1

40
cr tca(s, v

0

o − vi) tca(−s, v

0

i − vo) Distance at tca

MVP 118.50 s 118.50 4.77 nmi

ACCoRDtrackε 115.39 s 98.23 s 5.00 nmi

GOtrackε

1

115.39 s 98.23 s 5.00 nmi

GOtrackε

1

2

129.18 s 48.17 s 3.53 nmi

Table 2. Time and Distance of Closest Approach (Independent Case)

cr τ = tca(s, v

0

o − v

0

i

) Distance at τ

MVP 87.63 s 6.83 nmi

ACCoRDtrackε 73.70 s 6.85 nmi

GOtrackε

1

73.70 s 6.85 nmi

GOtrackε

1

2

46.34 s 4.07 nmi

Table 3. Time and Distance of Closest Approach (Coordinated Case)

achieve a minimum separation of 5 nautical miles. The fact that ACCoRDtrackε

and GOtrackε

1

achieve exactly the required minimum separation is a numerical illustration of Lemma 46 and Lemma 54, which state, respectively, that ACCoRDtrackε

and GOtrackε

1

compute solutions that are tangent to the relative protected zone.

Table 3 shows that in this particular scenario the resolutions computed by MVP,

ACCoRDtrackε, and GOtrackε

1

are coordinated. However, the minimum separation

achieved when both aircraft simultaneously maneuver according to GOtrackε

1

2

is less

than the required minimum separation of 5 nautical miles.

This example suggests that GOtrackε

1

2

is neither ConflictFree-independent nor

ConflictFree-coordinated. These apparent counterexamples to independence and

coordination need to be formally verified. It may be that the figures in the tables

are imprecise due to the effect of rounding errors in the floating point arithmetic

used by the programming languages where the algorithms were implemented. The

scenario also suggests that the conflict resolution algorithms MVP, ACCoRDtrackε,

and GOtrackε

1

are ConflictFree-coordinated with themselves. However, this numerical example cannot be considered a proof of coordination. In addition to possible

floating point error imprecisions, the existence of one scenario where coordination

holds cannot be generalized to all possible scenarios. The next section provides

formal, incontrovertible proofs of the coordination properties of MVP, GOtrackε

f

, and

ACCoRDtrackε.

7 Formal Properties of MVP, GOtrackε

f

, and ACCoRDtrackε

This section presents formal proofs of several results regarding coordination of MVP,

GOtrackε

f

, and ACCoRDtrackε. In particular, it is shown that MVP is coordinated

for Repulsion and that GOtrackε

1

and ACCoRDtrackε are ConflictFree-coordinated

41
with themselves, with each other, and with MVP. Formal proofs of the facts that MVP

and GOtrackε

1

2

are not ConflictFree-coordinated with themselves are also presented.

Furthermore, numerical evidence is provided to support the claim that they are not

ConflictFree-coordinated with each other.

7.1 MVP is Coordinated for Repulsion

The proof that the Modified Voltage Potential algorithm MVP is coordinated for

Repulsion illustrates the use of the repulsion criterion Rε defined in Section 5. The

coordination result for MVP follows from the fact that it satisfies Rε.

Lemma 56. Let v = vo−vi and suppose that Conflict(s, v) holds, s+tca(s, v) v 6=

0, and v

0

o ∈ MVP(so, si

, vo, vi). Then

v

0

o − vi ∈ Rε

s,v

,

where ε = −sign(s · v

⊥).

Proof. It can be proved from the definition of MVP that

v

0

o − vi =

1

tca(s, v)

(

D

kstcak

stca − s),

where stca = s+tca(s, v) v. It is easy to see that tca(s, v) must be positive. Thus,

by the definition of Rε, it suffices to prove the following four conditions.

1. ε s · v

⊥ ≤ 0.

2. s · v < 0.

3. s · (

D

kstcak

stca − s) ≤ 0.

4. ε (

D

kstcak

stca − s) · v

⊥ ≤ 0.

The first condition follows directly from the fact that ε = −sign(s · v

⊥), and the

second follows from Conflict(s, v). The third condition follows from the CauchySchwartz inequality:

D

kstcak

(s · stca) ≤

D

kstcak

ksk kstcak

= Dksk

≤ s · s.

The fourth condition follows from the facts that stca · v

⊥ = s · v⊥ and ε s · v⊥ ≤ 0:

ε (

D

kstcak

stca − s) · v

⊥ = ε (

D

kstcak

− 1)(s · v

⊥)

≤ 0.

(31)

The final inequality here uses the fact that D ≥ kstcak, which in turn follows directly

from Conflict(s, v).

42
Theorem 57. The algorithm MVP is coordinated for Repulsion.

Proof. Lemma 56 implies that when the aircraft are in conflict, the algorithm MVP

satisfies the criterion Rε, where ε = −sign(s · v

⊥). The result follows from Theorem 25 (Section 3.3) and Theorem 2 (Section 3.1).

7.2 GOtrackε

1 and ACCoRDtrackε are ConflictFree-Coordinated

This section proves that the algorithms GOtrackε

1

, and ACCoRDtrackε are ConflictFree-coordinated with themselves and with each. The proof follows from the fact

that each of these algorithms satisfies the horizontal criterion Hε, defined in Section 5.1.

Lemma 58. The algorithms GOtrackε

1

and ACCoRDtrackεeach satisfy the horizontal

criterion Hε.

Proof. If v

0

o ∈ GOtrackε

1 ∪ ACCoRDtrackε

, then by Lemma 54 (Section 6.3) and

Lemma 46 (Section 6.2), it follows that LineSolution(s, v

0

o − vi

, ε) holds. The result

follows directly from Lemma 33 (Section 5.3.1).

Theorem 59. The resolution algorithms GOtrackε

1

and ACCoRDtrackε are coordinated with themselves and with each other for ConflictFree.

Proof. This follows directly from Lemma 58 and Theorem 34 (Section 5.3.1).

7.3 MVP is ConflictFree-Coordinated with GOtrackε

1 and ACCoRDtrackε

This section proves that the resolution algorithm MVP is ConflictFree-coordinated

with the algorithms GOtrackε

1

, and ACCoRDtrackε. This proof requires that the

value ε is chosen such that ε s · (vo − vi)

⊥ ≤ 0. The result relies on Theorem 27

(Section 5.2).

Lemma 60. If s = so − si, v = vo − vi, and v

0

o are vectors such that Conflict(s, v)

holds, s + tca(s, v) v 6= 0, v

0

o ∈ MVP(so, si

, vo, vi), and ε s · v

⊥ ≤ 0, then v0

o − vo ∈

Hε

s,v

.

Proof. Since Conflict(s, v) holds, it is clear from the definition of the function tca

that tca(s, v) is positive. As noted in the proof of Lemma 56 (Section 7.1), it can

be proved from the definition of MVP that

v

0

o − vi =

1

tca(s, v)

(

D

kstcak

stca − s),

where stca = s + tca(s, v) v. Thus,

v

0

o − vo = (v

0

o − vi) − v

=

1

tca(s, v)

(

D

kstcak

stca − s) − v

=

1

tca(s, v)

(

D

kstcak

stca − s) −

1

tca(s, v)

(stca − s)

=

D − kstcak

tca(s, v)kstcak

stca.

(32)

43
Since stca · v

⊥ = s · v⊥, it can be proved using techniques from linear algebra that

stca =

−ε stca · v

⊥

kvk

2

(−ε v

⊥)

=

−ε s · v

⊥

kvk

2

(−ε v

⊥).

Further, by hypothesis, the coefficient of the vector −ε v

⊥ in this equation is nonnegative. Hence, it follows from Equation (32) that there is a nonnegative real

number r ≥ 0 such that

v

0

o − vo = r (−ε v

⊥).

By Lemma 32 (Section 5), it is easy to see that Hεis closed under multiplication by

a nonnegative scalar, so it suffices to prove that −ε v

⊥ ∈ Hε

s,v

. This always holds

and can be proved from definitions using linear algebraic manipulations.

Theorem 61. Let cr be a resolution algorithm such that for all v

0

o ∈ cr(so, si

, vo, vi),

v

0

o ∈ LineSolution(so − si

, v

0

o − vi

, ε), where ε s · v

⊥ ≤ 0. The resolution algorithm

MVP is ConflictFree-coordinated with cr.

Proof. By Lemma 33 (Section 5.3.1) and Theorem 27 (Section 5.2), it suffices to

prove that for all s = so − si,v = vo − vi, v

0

i ∈ MVP(si

, so, vi, vo), if Conflict(s, v)

holds, then (v

0

i − vi) ∈ Hε

s,v

. This follows directly from Lemma 60.

Theorem 62. The resolution algorithm MVP is ConflictFree-coordinated with both

GOtrackε

1

and ACCoRDtrackε, if ε is chosen such that ε s · v

⊥ ≤ 0.

Proof. By Lemma 54 (Section 6.3) and Lemma 46 (Section 6.2), both GOtrackε

1

and

ACCoRDtrackεcompute line solutions. The result follows from Theorem 61.

7.4 MVP is Not ConflictFree-Coordinated

Theorems 57 and 61 state, respectively, that the Modified Voltage Potential algorithm MVP is Repulsion-coordinated and, furthermore, ConflictFree-coordinated

with any algorithm that computes tangent trajectories to the protected zone. The

numerical example in Section 6.4 suggest that MVP is also ConflictFree-Coordinated.

However, as the following theorem shows, MVP is not ConflictFree-coordinated with

itself. In other words, there exist scenarios where MVP does not achieve separation

when both aircraft simultaneously maneuver according to the resolutions computed

by the algorithm.

Theorem 63. The algorithm MVP is not ConflictFree-coordinated.

Proof. To prove this theorem, it suffices to show that there exists D, so, si, vo,

vi, v

0

o

, and v

0

i

such that Conflict(so − si, vo − vi), v

0

o ∈ MVP(so, si

, vo, vi), and

v

0

i ∈ MVP(si

, so, vi, vo), where Conflict(so − si, v

0

o − v

0

i

) holds.

44
Let D, so, si

, vo, and vi be defined as follows, where distances are in nautical

miles and speeds are in knots.

D = 5,

so = (0, 0.1),

si = (√

30.24, 0),

vo = (500, 0),

vi = (250, 0).

(33)

Simple algebraic manipulations can be used to show that vectors returned by the

evaluations of MVP(so, si, vo, vi) and MVP(si, so, vi, vo) are given by

v

0

o = (500,

1225

√

30.24

), (34)

v

0

i = (250, −

1225

√

30.24

), (35)

respectively.

The time at which the two aircraft achieve minimum separation when both

aircraft simultaneously maneuver is computed by the function tca (Section 4.3),

and is given by the following quotient.

tca(s, v

0

o − v

0

i

) = −

(−

√

30.24, 0.1) · (250, 2450/

√

30.24)

k(250, 2450/

√

30.24)k

2

= −

245/

√

30.24 − 250 √30.24

2502 + 24502/30.24

.

It can be proved that the distance between the aircraft at this time is strictly less

than 4.85 nautical miles, i.e., that the following inequality holds.

ks + tca(s, v

0

o − v

0

i

) (v

0

o − v

0

i

)k < 4.85.

In contrast to the numerical example presented in Section 6.4, the arithmetic used

in this proof is exact. Hence, this inequality formally proves that MVP is not ConflictFree-coordinated.

7.5 GOtrackε

1

2

is Not ConflictFree-Coordinated

In [2], it is claimed that if GOtrackε

fo

is ConflictFree-coordinated with GOtrackε

fi

,

then fo + fi ≥ 1. This section shows that the converse claim does not hold, i.e, the

fact that fo+fi ≥ 1 does not imply that the algorithms are ConflictFree-coordinated.

Although it holds for particular values of fo and fi, e.g., when fo = 1 and fi = 0, it

does not hold when fo = fi =

1

2

.

Theorem 64. The algorithm GOtrackε

1

2

is not ConflictFree-coordinated.

45
Proof. To prove this theorem, it suffices to show that there exists D, so, si

, vo, vi,

ε, v

0

o

, and v

0

i

such that Conflict(so − si, vo − vi), v

0

o ∈ GOtrackε

1

2

(so, si, vo, vi), and

v

0

i ∈ GOtrackε

1

2

(si, so, vi, vo), where Conflict(so − si, v

0

o − v

0

i

) holds.

Let D, so, si, vo, vi, and ε be defined as follows, where distances are in nautical

miles and speeds are in knots.

D = 5,

so = (0, 0),

si = ( 10

√

3

, 0),

vo = (500, 0),

vi = (250, 0),

ε = −1.

The following equalities follow directly from definitions.

track(vo) = π

2

,

track(vi) = π

2

,

track(vo − vi) = π

2

,

χ

∗

rel(s, vo − vi

, 0, −1) = π

2

,

χ

∗

rel(s, vo − vi

,

1

2

, −1) = 2π

3

,

χ

∗

rel(s, vo − vi

, 1, −1) = 5π

6

.

Vectors v

0

o ∈ GOtrackε

1

2

(so, si, vo, vi) and v

0

i ∈ GOtrackε

1

2

(si, so, vi, vo) can be computed as follows.

v

0

o = (125

2

(1 + 3√5),

125

2

√

3 (1 −

√

5)),

v

0

i = (125, 125√

3).

Thus,

v

0

o − v

0

i = (125

2

(3√

5 − 1), −

125

2

√

3 (1 + √5)).

The relative velocity vector v

0

o −v

0

i

therefore has a norm equal to 500 knots. Hence,

the time when the aircraft achieve minimum separation is given by

tca(s, v

0

o − v

0

i

) = −1

5002

(s · (v

0

o − v

0

i

))

=

1

5002

625 (√15 −

1

√

3

).

The distance between the aircraft at this time satisfies the following inequality.

ks + tca(s, v

0

o − v

0

i

) (v

0

o − v

0

i

)k < 4.1.

46
In contrast to the numerical example presented in Section 6.4, the arithmetic used

in this proof is exact. Hence, this inequality formally proves that GOtrackε

1

2

is not

ConflictFree-coordinated.

7.6 GOtrackε

1

2

and MVP are Not ConflictFree-Coordinated

This section presents numerical evidence that the resolution algorithm GOtrackε

1

2

is not ConflictFree-coordinated with MVP, not even when ε represents the opposite

direction to the resolution returned by MVP. The result that follows uses values

returned by an implementation of the algorithm GOtrackε

1

2

and, therefore, may be

inaccurate. Since those values have not been formally checked in PVS, the following

result does not qualify as a formal proof. To distinguish this result from all the

other results presented in this paper, it is stated as a conjecture instead of a lemma

or theorem.

The algorithm GOtrackε

1

2

has as a parameter ε = ±1, which refers to direction

(left or right). The algorithm MVP does not have such a parameter, because it returns

a vector for the ownship that yields a relative velocity vector that passes on the same

side of the origin as the original relative velocity vector. Thus, when coordination

is considered between the algorithms GOtrackε

1

2

and MVP, there is only one choice of

the unit ε that could possibly provide coordination. This is the unit that satisfies

ε s · v

⊥ ≤ 0, where s and v are the current relative position and velocity vectors,

respectively.

Conjecture 1. The algorithms GOtrackε

1

2

and MVP are not ConflictFree-coordinated,

not even when the parameter ε is chosen so that ε s · v

⊥ ≤ 0.

To prove this conjecture, it suffices to show that there exists D, so, si, vo, vi,

ε, v

0

o

, and v

0

i

such that Conflict(so − si, vo − vi), v

0

o ∈ GOtrackε

1

2

(so, si, vo, vi), and

v

0

i ∈ MVP(si

, so, vi, vo), where Conflict(so − si, v

0

o − v

0

i

) holds.

An example is now given that numerically justifies that such a scenario does

indeed exist. Let D, so, si, vo, and vi be given as in Formula (33) and let ε be

−1. It is easy to see that ε s · v

⊥ ≤ 0. The vector v0

i ∈ MVP(si

, so, vi, vo) is exactly

defined by Formula (35). A vector v

0

o ∈ GOtrackε

1

2

(so, si, vo, vi) can be computed

numerically and is approximately given by

v

0

o ≈ (478.835, 143.993).

In this case, the time of closest approach if both aircraft maneuver, i.e., tca(s, v

0

o −

v

0

i

), is approximately 0.00654 hours or about 23.544 seconds. At this time, the

separation between the aircraft is approximately given by

ks + tca(s, v

0

o − v

0

i

) (v

0

o − v

0

i

)k ≈ 4.718.

Thus, the aircraft are in conflict, and this completes the argument for Conjecture 1.

The formal development of this argument is tedious although not necessarily difficult. The family of Geometric Optimization algorithms use analytical equations

involving trigonometric functions. Trigonometric reasoning is not currently wellhandled by state-of-the-art theorems provers.

47
GOtrackε

1

2

MVP GOtrackε

1

ACCoRDtrackε

GOtrackε

1

2

% %∗

MVP %∗ % ! !

GOtrackε

1 ! ! !

ACCoRDtrackε ! ! !

Table 4. Coordination of GOtrackε

1

2

, MVP, GOtrackε

1

, and ACCoRDtrackε.

8 Conclusion

This paper proposed a general mathematical framework for studying implicit coordination in the context of state-based separation assurance systems. Implicit coordination has been formally defined before [3,4,6,11]. In those papers, the concept of

coordination applies to a particular strategy for computing coordinated resolution

maneuvers or to a specific conflict resolution algorithm. The work presented in this

paper applies to any state-based separation assurance algorithm and to any type of

safety property for which coordination needs to proved.

The framework is illustrated by formally studying coordination properties of

well-known conflict resolution algorithms such as the Modified Voltage Potential

algorithm (MVP), the Geometric Optimization algorithm for track angle maneuvers

(GOtrackε

f

), and ACCoRD’s conflict resolution algorithm for track angle maneuvers (ACCoRDtrackε

). Table 4 summarizes the main results where the intersection

between a column and a row refers to ConflictFree-coordination for the given resolution algorithms. The symbol ! stands for cases where coordination has been

formally proved in PVS. The symbol % stands for cases where coordination has

been formally disproved in PVS, i.e., a counterexample for coordination has been

found and the claim that the counterexample does not satisfy coordination has been

formally proved in PVS. The symbol %∗stands for cases where a counterexample

for coordination has been found and the claim that coordination does not hold has

been numerically checked, but the formal proof of this claim is not provided. The

remaining cases have not been studied, but they could be analyzed in the same way

as the other cases presented in this paper.

The framework presented here relies on some physical and operational assumptions. For instance, the airspace is represented by a Euclidean geometry, where

aircraft fly linear trajectories and maneuver instantaneously. These assumptions

are common to state-based approaches. They allow for analytical solutions that

yield efficient implementations. Despite its limitations, state-based CD&R is used

in the self-separation concept [20] as a backup for more sophisticated separation

assurance systems. Therefore, state-based CD&R is a critical component of this

concept. The framework also assumes that resolution maneuvers are computed in

a pairwise fashion. Although multiple simultaneous conflicts may be rare, they will

exist and the safety case for a distributed air traffic concept of operations has to

guarantee that they are correctly handled. Future work in this area will look at this

48
problem. In particular, it will be studied how the criteria concept can be integrated

into prevention bands [14], a concept that naturally fuses conflict information for

multiple aircraft.

In summary, the framework presented here is believed to be a fundamental step

towards the understanding of how different state-based separation assurance algorithms can be deployed in the future airspace in a way that they safely interact

with each other. This framework provides the mathematical basis for an approach

to self-separation in NextGen that does not rely on a specifically mandated CD&R

algorithm but on a criteria-based standard for conflict resolution [12].

The results presented in this paper have been mechanically checked using an

interactive theorem prover, which provides strong guarantees that the mathematical

development is correct. The use of a mechanical theorem prover requires a detailed

description of the problem and a meticulous proof process. This level of rigor is

justified by the critical role that aircraft separation plays in the overall safety of the

next generation of air traffic management systems.

References

1. Antonio Bicchi and Lucia Pallottino. On optimal cooperative conflict resolution

for air traffic management systems. IEEE Transactions on Intelligent Transportation Systems, 1(4):221–232, December 2000.

2. Karl Bilimoria. A geometric optimization approach to aircraft conflict resolution. In Guidance, Navigation, and Control Conference, volume AIAA 2000-

4265, Denver, CO, August 2000.

3. Gilles Dowek and C ́esar Mu ̃noz. Conflict detection and resolution for 1,2,. . . N

aircraft. In 6th AIAA Aviation Technology, Integration and Operations Conference (ATIO), Belfast, Northern Ireland, September 2007.

4. Gilles Dowek, C ́esar Mu ̃noz, and V ́ıctor Carre ̃no. Provably safe coordinated

strategy for distributed conflict resolution. In Proceedings of the AIAA Guidance

Navigation, and Control Conference and Exhibit 2005, AIAA-2005-6047, San

Francisco, California, 2005.

5. Martin Eby. A self-organizational approach for resolving air traffic conflicts.

Lincoln Laboratory Journal, 7(2):239–254, 1994.

6. Andr ́e Galdino, C ́esar Mu ̃noz, and Mauricio Ayala. Formal verification of an

optimal air traffic conflict resolution and recovery algorithm. In D. Leivant and

R. de Queiroz, editors, Proceedings of the 14th Workshop on Logic, Language,

Information and Computation, volume 4576 of Lecture Notes in Computer Science, pages 177–188, Rio de Janeiro, Brazil, July 2007. Springer-Verlag.

7. G ́eraud Granger, Nicolas Durand, and Jean-Marc Alliot. Token allocation for

free-flight conflict solving. In Haym Hirsch and Steve Chien, editors, Proceedings

of the Thirteenth Innovative Applications of Artificial Intelligence Conference

49
(IAAI-01), pages 59–64, Menlo Park, CA, August 7–9 2001. American Association for Artificial Intelligence.

8. Jacco Hoekstra. Designing for safety: The free flight air traffic management concept. Technical Report 90-806343-2-8, Technische Universiteir Delft, November

2001.

9. Jana Kosecka, Claire Tomlin, George Pappas, and Shankar Sastry. Generation

of conflict resolution maneuvers for air traffic management. In International

Conference on Intelligent Robots and Systems, Grenoble, 1997.

10. James Kuchar and Lee Yang. A review of conflict detection and resolution

modeling methods. IEEE Transactions on Intelligent Transportation Systems,

1(4):179–189, December 2000.

11. Jeffrey Maddalon, Ricky Butler, Alfons Geser, and C ́esar Mu ̃noz. Formal verification of a conflict resolution and recovery algorithm. Technical Report NASA/TP-2004-213015, NASA Langley Research Center, NASA

LaRC,Hampton VA 23681-2199, USA, April 2004.

12. C ́esar Mu ̃noz, Ricky Butler, Anthony Narkawicz, Jeffrey Maddalon, and George

Hagen. A criteria standard for conflict resolution: A vision for guaranteeing

the safety of self-separation in NextGen. Technical Memorandum NASA/TM2010-216862, NASA, Langley Research Center, Hampton VA 23681-2199, USA,

October 2010.

13. C ́esar Mu ̃noz, Anthony Narkawicz, Ricky Butler, and Gilles Dowek. Mathematical framework for the design and verification of state-based separation assurance

algorithms. Manuscript, 2010.

14. Anthony Narkawicz, C ́esar Mu ̃noz, and Gilles Dowek. Formal verification of air

traffic prevention bands algorithms. Technical Memorandum NASA/TM-2010-

216706, NASA, Langley Research Center, Hampton VA 23681-2199, USA, June

2010.

15. Sam Owre, John Rushby, and Natarajan Shankar. PVS: A prototype verification

system. In Deepak Kapur, editor, Proceeding of the 11th International Conference on Automated Deductioncade, volume 607 of Lecture Notes in Artificial

Intelligence, pages 748–752. Springer, June 1992.

16. Sam Owre and Natarajan Shankar. The formal semantics of PVS. Technical

Report SRI-CSL-97-2, Computer Science Laboratory, SRI International, Menlo

Park, CA, August 1997.

17. Walter Rudin. Principles of Mathematical Analysis. McGraw-Hill, third edition,

1976.

18. Tom Schouwenaars, Jonathan How, and Eric Feron. Decentralized cooperative

trajectory planning of multiple aircraft with hard safety guarantees. In AIAA

Guidance, Navigation, and Control Conference and Exhibit, Providence, Rhode

Island, August 2004.

50
19. Claire Tomlin, George Pappas, and Shankar Sastry. Noncooperative conflict

resolution. In IEEE International Conference on Decision and Control, San

Diego, CA, December 1997.

20. David J. Wing, Robert A. Vivona, and David A. Roscoe. Airborne tactical

intent-based conflict resolution capability. In 9th AIAA Aviation Technology,

Integration, and Operations Conference (ATIO), Hilton Head, South Carolina,

USA, September 2009.

51
REPORT DOCUMENTATION PAGE Form Approved

OMB No. 0704–0188

The public reporting burden for this collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources,

gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection

of information, including suggestions for reducing this burden, to Department of Defense, Washington Headquarters Services, Directorate for Information Operations and Reports

(0704-0188), 1215 Jefferson Davis Highway, Suite 1204, Arlington, VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be

subject to any penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number.

PLEASE DO NOT RETURN YOUR FORM TO THE ABOVE ADDRESS.

Standard Form 298 (Rev. 8/98)

Prescribed by ANSI Std. Z39.18

1. REPORT DATE (DD-MM-YYYY)

01-03-2011

2. REPORT TYPE

Technical Publication

3. DATES COVERED (From - To)

4. TITLE AND SUBTITLE

State-Based Implicit Coordination and Applications

5a. CONTRACT NUMBER

5b. GRANT NUMBER

5c. PROGRAM ELEMENT NUMBER

5d. PROJECT NUMBER

5e. TASK NUMBER

5f. WORK UNIT NUMBER

411931-02-51-07-01, 457280.02.07.07.07

6. AUTHOR(S)

Anthony J. Narkawicz and C ́esar A. Mu ̃noz

7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES)

NASA Langley Research Center

Hampton, Virginia 23681-2199

8. PERFORMING ORGANIZATION

REPORT NUMBER

L–19959

9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES)

National Aeronautics and Space Administration

Washington, DC 20546-0001

10. SPONSOR/MONITOR’S ACRONYM(S)

NASA

11. SPONSOR/MONITOR’S REPORT

NUMBER(S)

NASA/TP–2011–217067

12. DISTRIBUTION/AVAILABILITY STATEMENT

Unclassified-Unlimited

Subject Category 03

Availability: NASA CASI (443) 757-5802

13. SUPPLEMENTARY NOTES

An electronic version can be found at http://ntrs.nasa.gov.

14. ABSTRACT

In air traffic management, pairwise coordination is the ability to achieve separation requirements when conflicting aircraft

simultaneously maneuver to solve a conflict. Resolution algorithms are implicitly coordinated if they provide coordinated

resolution maneuvers to conflicting aircraft when only surveillance data, e.g., position and velocity vectors, is periodically

broadcast by the aircraft. This paper proposes an abstract framework for reasoning about state-based implicit coordination.

The framework consists of a formalized mathematical development that enables and simplifies the design and verification of

implicitly coordinated state-based resolution algorithms. The use of the framework is illustrated with several examples of

algorithms and formal proofs of their coordination properties. The work presented here supports the safety case for a

distributed self-separation air traffic management concept where different aircraft may use different conflict resolution

algorithms and be assured that separation will be maintained.

15. SUBJECT TERMS

Air traffic, avoidance, conflict, detection, resolution, prevention, formal verification

16. SECURITY CLASSIFICATION OF:

a. REPORT

U

b. ABSTRACT

U

c. THIS PAGE

U

17. LIMITATION OF

ABSTRACT

UU

18. NUMBER

OF

PAGES

60

19a. NAME OF RESPONSIBLE PERSON

STI Help Desk (email: help@sti.nasa.gov)

19b. TELEPHONE NUMBER (Include area code)

(443) 757-5802