KB3D
----

Contact: C. Munoz (http://research.nianet.org/~munoz)
         National Institute of Aerospace (2007)

KB3D is a geometric optimization approach to Conflict Detection and Resolution
in a 3-D airspace.

To run all the proofs in PVS4.0 or higher type, assuming that ProofLite 
(http://research.nianet.org/~munoz/ProofLite) is installed:

$ proveit -a top

                           I. Full KB3D
                           ------------

Full KB3D is composed of three functions:
- vertical_speed_circle 
- ground_speed_line     
- heading_line
These functions provide, respectively, vertical speed only, ground
speed only, and heading only resolutions to the ownship. Circle and
line refer to the part of the protected zone that is tangent to the
resolution maneuver.  Note: ground_speed_circle and heading_circle
solutions were available in the original KB3D, but they have not been
upgraded to this current version.

Naming Conventions
------------------
vo,vi: Ownship and Traffic *absolute* velocity vectors, respectively.
s    : Relative position of ownship with respect to traffic.
v    : Relative velocity of ownship with respect to traffic, i.e., vo-vi
eps  : +/- 1 

Precondition(s,v)
-----------------

- Aircraft are not in conflict:
  sq(x(s))+sq(y(s)) >= sq(D) OR sq(z(s)) >= sq(H) 

- Aircraft are in predicted conflict:
  EXISTS t > 0. sq(x(s)+t*x(v))+sq(y(s)+t*y(v)) < sq(D) AND
                sq(z(s)+t*z(v)) < sq(H)

Vertical Speed Circle Solutions
-------------------------------
File          : vertical_speed_circle.pvs
Function      : vertical_speed_circle(s,vo,vi,eps):Vect3
Specification :
Let nvo = vertical_speed_circle(s,vo,vi,eps) in
  precondition(s,vo-vi) AND 
  sq(x(s)) + sq(y(s)) /= sq(D) OR sq(z(s)) >= sq(H) AND
  nvo /= (0,0,0) IMPLIES
  nvo is a resolution velocity for the ownship where
    x(nvo) = x(vo)
    y(nvo) = y(vo)

Ground Speed Line Solutions
---------------------------
File          : ground_speed_line.pvs
Function      : ground_speed_line(s,vo,vi,eps):Vect3
Specification :
Let nvo = ground_speed_line(s,vo,vi,eps) in
  sq(x(s))+sq(y(s)) > sq(D) AND 
  sq(x(nvo))+sq(y(nvo)) /= 0 IMPLIES  
  nvo is a resolution velocity for the ownship where
  nvo = (k*x(vo),k*y(vo),z(vo)) for k > 0.

Heading Line Solutions
----------------------
File          : heading_line.pvs
Function      : heading_line(s,vo,vi,eps):Vect3
Specification :
Let nvo = heading_line(s,vo,vi,eps) in
  sq(x(s))+sq(y(s)) > sq(D) AND 
  sq(x(nvo))+sq(y(nvo)) /= 0 IMPLIES  
  nvo is a resolution velocity for the ownship where
  sq(x(nvo))+sq(y(nvo)) = sq(x(vo))+sq(y(vo)) AND
  z(nvo) = z(vo)

                         II. Cooperative KB3D
                         --------------------
Cooperative KB3D is a subset of KB3D that provides cooperative maneuvers 
for the ownship. 
It consists of three functions:
- kb3d_vertical_speed (vertical speed only maneuver)
- kb3d_ground_speed   (ground speed only maneuver)
- kb3d_heading        (heading only maneuver)

Each function yields one cooperative resolution maneuver, in the form of
a new velocity vector, for the ownship.  

Naming Conventions
------------------
a,b  : Ownship and Traffic aircraft state information. 
       A state is a record with fields 
       s  = Absolute 3-D position.
       v  = Absolute velocity vector.

Vertical Speed Circle Solutions
-------------------------------
File          : kb3d_vertical.pvs
Function      : kb3d_vertical_speed(a,b):Vect3
Specification :
Let nva = kb3d_vertical_speed(a,b) in
Let nvb = kb3d_vertical_speed(b,a) in
  precondition(s(a)-s(b),v(a)-v(b)) AND 
  sq(x(s(a)-s(b))) + sq(y(s(a)-s(b))) /= sq(D) OR sq(z(s(a)-s(b))) >= sq(H) AND
  sq(x(v(a))) + sq(x(v(a))) /= 0 AND
  sq(x(v(b))) + sq(x(v(b))) /= 0 IMPLIES
    nva is a resolution velocity for ownship where
      x(nva) = x(va)
      y(nva) = y(va)
  AND 
    nvb is a resolution velocity for traffic where
      x(nvb) = x(vb)
      y(nvb) = y(vb)
  AND
    nva and nvb are cooperative 

Heading Line Solutions
----------------------
File          : kb3d_horizontal.pvs
Function      : kb3d_heading(a,b):Vect3
Specification :
Let nva = kb3d_heading(a,b) in
Let nvb = kb3d_heading(b,a) in
  precondition(s(a)-s(b),v(a)-v(b)) AND 
  sq(x(s(a)-s(b)))+sq(y(s(a)-s(b))) > sq(D) AND
  sq(x(v(a))) + sq(x(v(a))) /= 0 AND
  sq(x(v(b))) + sq(x(v(b))) /= 0 IMPLIES
    nva is a resolution velocity for ownship where
    sq(x(nva))+sq(y(nva)) = sq(x(v(a)))+sq(y(v(a))) AND
    z(nva) = z(v(a))
  AND 
    nvb is a resolution velocity for traffic where
    sq(x(nvb))+sq(y(nvb)) = sq(x(v(b)))+sq(y(v(b))) AND
    z(nvb) = z(v(b))

  AND
    nva and nvb are cooperative 

Ground Speed Line Solutions
---------------------------
File          : kb3d_horizontal.pvs
Function      : kb3d_ground_speed(a,b):Vect3
Specification :
Let nva = kb3d_ground_speed(a,b) in
Let nvb = kb3d_ground_speed(b,a) in
  precondition(s(a)-s(b),v(a)-v(b)) AND 
  sq(x(s(a)-s(b)))+sq(y(s(a)-s(b))) > sq(D) AND
  sq(x(v(a))) + sq(x(v(a))) /= 0 AND
  sq(x(v(b))) + sq(x(v(b))) /= 0 IMPLIES
    nva is a resolution velocity for ownship where
    nva = (ka*x(v(a)),ka*y(v(a)),z(v(a))), ka > 0
  AND 
    nvb is a resolution velocity for traffic where
    nvb = (kb*x(v(b)),ka*y(v(b)),z(v(b))), kb > 0
  AND
    nva and nvb are cooperative