Jean-Baptiste Jeannin

Khalil Ghorbal

Yanni Kouskoulas

Aurora Schmidt

Ryan Gardner

Stefan Mitsch

André Platzer

A Formally Verified Hybrid System for Safe Advisories in the Next-Generation Airborne Collision Avoidance System

d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

With growing air traffic, the airspace becomes more crowded, and the risk of airborne collisions between aircraft increases. In the 1970s, after a series of mid-air collisions, the Federal Aviation Administration (FAA) decided to develop an onboard collision avoidance system: the Traffic Alert and Collision Avoidance System (TCAS). This program had great success, and prevented many mid-air collisions over the years. Some accidents still happened; for example, a collision over Überlingen in 2002 occurred due to conflicting advice between TCAS and air traffic control. Airspace management will evolve significantly over the next decade with the introduction of the next-generation air traffic management system; this will create new requirements for collision avoidance. To meet these new requirements, the FAA has decided to develop a new system: the Next-Generation Airborne Collision Avoidance System, known as ACAS X [START_REF][END_REF][START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF][START_REF] Kochenderfer | Next generation airborne collision avoidance system[END_REF].

Like TCAS, ACAS X avoids collisions by giving vertical guidance to an aircraft's pilot. A typical scenario involves two aircraft: the ownship where ACAS X is installed, and another aircraft called the intruder that is at risk of colliding with the ownship. ACAS X is designed to avoid Near Mid-Air Collisions (NMACs), situations where two aircraft come within r p = 500 ft horizontally and h p = 100 ft vertically [START_REF] Kochenderfer | Next generation airborne collision avoidance system[END_REF] of each other. The NMAC definition describes a volume centered around the ownship, shaped like a hockey puck of radius r p and half-height h p .

In order to be accepted by pilots, and thus operationally suitable, ACAS X needs to strike a balance between giving advice that helps pilots avoid collisions but also minimizing interruptions. These goals drive the design in opposite directions each other, and cannot both be perfectly met in the presence of unknown pilot behavior. As part of the ACAS X development process, this work focuses on precisely characterizing the circumstances in which ACAS X gives safe ad- vice, and where safety is traded off for operational suitability, helping to identify modifications that improve its safety and performance.

Airborne Collision Avoidance System ACAS X

In order to prevent an NMAC with other aircraft, ACAS X uses various sensors to determine the position of the ownship, as well as the positions of any intruders [START_REF]Algorithm design description for the surveillance and tracking module of ACAS X[END_REF]. It computes its estimate of the best pilot action by linearly interpolating a precomputed table of scores for actions, and, if appropriate, issuing an advisory to avoid potential collisions [START_REF]Algorithm design description for the threat resolution module of ACAS X[END_REF] through a visual display and a voice message.

An advisory is a request to the pilot of the ownship to alter or maintain her vertical speed. ACAS X advisories are strictly vertical, and never request any horizontal maneuvering. Table 1 shows the advisories ACAS X can issue. For example, Do-Not-Climb (DNC) requests that the pilot not climb, and Climb-1500 (CL1500) requests that the pilot climb at more than 1500 ft/min. The current version of ACAS X can issue a total of 16 different advisories plus Clear-of-Conflict (COC), which indicates that no action is necessary, and Multi-Threat-Level-Off (MTLO), which is used in the case of multiple intruders. To comply with an advisory, the pilot must adjust her vertical rate to fall within the advised vertical rate range. Based on previous research [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], the pilot is assumed to do so using a vertical acceleration of strength at least a lo starting after a delay of at most δ after the advisory has been announced by ACAS X.

At the heart of ACAS X is a table whose domain describes the instantaneous state of an encounter, and whose range is a set of scores for each possible action [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF][START_REF] Kochenderfer | Compression of optimal value functions for Markov decision processes[END_REF]. The table is obtained from a Markov Decision Process (MDP) approximating the dynamics of the system in a discretization of the state-space, and optimized using dynamic programming to maximize the expected value of events over all future paths for each action [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF]. Near Mid-Air Collision events, for example, are associated with large negative values and issuing an advisory is associated with a small negative value. The policy is to choose the action with the highest expected value from a multilinear interpolation of grid points in this table. ACAS X uses this table, along with some heuristics, to determine the best action to take for the geometry and dynamic conditions in which it finds itself.

Identifying Formally Verified Safe Regions

Since ACAS X involves both discrete advisories to the pilot and continuous dynamics of aircraft, it is natural to formally verify it using hybrid systems. However the complexity of ACAS X, which uses at its core a large lookup tabledefining 29,212,664 interpolation regions within a 5-dimensional state-space-makes the direct use of hybrid systems verification techniques intractable. Our approach is different. It identifies safe regions in the state space of the system where we prove formally that the current positions and velocities of the aircraft ensure that a particular advisory, if followed, prevents all possible NMACs. Then it compares these regions to the configurations where the ACAS X table returns this same advisory. Moreover our safe regions are symbolic in their parameters, and can thus be easily adapted to new parameters or new versions of ACAS X.

Going beyond the results of [START_REF] Jeannin | A formally verified hybrid system for the next-generation airborne collision avoidance system[END_REF], this paper devises and formally proves safety regions for advisories that can be cor-rected later on. In that context, an advisory need not be safe on its own to be considered acceptable, but the system needs to be able to correct it with a subsequent advisory. This is particularly useful to assess the safety of preventative advisories, and leads to the discovery of very relevant unexpected behaviors of the system.

Our results provide independent characterizations of the ACAS X behavior to provide a clear and complete picture of its performance. Our method can be used by the ACAS X development team in two ways. It provides a mathematical proof-with respect to a hybrid systems model-that ACAS X is absolutely safe for some configurations of the aircraft. Additionally, when ACAS X is not safe, it is able to identify unsafe or unexpected behaviors and suggests ways of correcting them.

Our approach of formally deriving safe regions then comparing them to the behavior of an industrial system is, as far as we are aware, the first of its kind in the formal verification of hybrid systems. The approach may be valuable for verifying or assessing properties of other systems with similar complexities, or also using large lookup tables, which is a common challenge in practice. Finally, the constraints we identified for safety are fairly general and could be used to analyze other collision avoidance systems.

The paper is organized as follows. After an overview of the method in Sect. 2, we start with a simple two-dimensional model assuming immediate reaction of the pilot in Sect. [START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF]. We extend the model to account for the reaction time of the pilot in Sect. 4, consider more liberal safe regions to tolerate advisories that are only safe if followed up by suitable subsequent advisories in Sect. 5, and extend the results to a three-dimensional model in Sect. 6. Relationships and extensions are discussed in Sect. 7. In Sect. 8, we compare the advisory recommended by a core component of ACAS X with our safe regions, identifying the circumstances where safety of those ACAS X advisories is guaranteed within our model.

Overview of the ACAS X Modelling Approach

To construct a safe region of an advisory for an aircraft, imagine following all allowable trajectories of the ownship relative to the intruder, accounting for every possible position of the ownship and its surrounding puck at every future moment in time. The union of all such positions of the puck describes a potentially unsafe region; for each point there exists a trajectory that results in an NMAC. Dually, if the intruder is outside this set, i.e., in the safe region, an NMAC cannot occur in the model.

Fig. 1 depicts an example of a head-on encounter and its associated safe region for the advisory CL1500, projected in a vertical plane with both aircraft. It is plotted in a coordinate system fixed to the intruder and centered at the initial 1. The green safe-region indicates starting points in the state space for which the aircraft will remain safe for the duration of the encounter when following the CL1500 advisory. Note that no safe region exists above the trajectory since the ownship could accelerate vertically at greater than g/4 or climb more than +1500 ft/min, in accordance with Table 1.

Model of Dynamics

Let us consider an encounter between two planes-ownship O and intruder I, as portrayed in Fig. 2. Following the notation of the ACAS X community [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], let r = r be the horizontal distance between the aircraft (called range) and h the height of the intruder relative to the ownship. We assume that the relative horizontal velocity r v of the intruder with respect to the ownship is constant throughout the encounter. I.e., from a top view, the planes follow straight-line trajectories. Let θ v be the non-directed angle between r v and the line segment r. In the vertical dimension, we assume that the ownship's vertical velocity v can vary at any moment, while the intruder's vertical velocity v I is fixed throughout the encounter. Moreover, we assume that the magnitude of the vertical acceleration of the ownship cannot exceed a d in absolute value.

Our analysis considers all these as symbolic parameters and is, thus, valid for any value they might have. For a typical encounter, r varies between 0 nmi and 7 nmi, 1 h between -4,000 ft and 4,000 ft, r v = r v between 0 kts Fig. 1 Nominal trajectory of the ownship (red) and safe region for the intruder (green), immediate response and 1,000 kts, and v and v I between -5,000 ft/min and +5,000 ft/min. The acceleration a d is usually g/2, where g is Earth's gravitational acceleration. The NMAC puck of ACAS X has radius r p = 500 ft and half-height h p = 100 ft.

Model of Advisories

Recall that ACAS X prevents NMACs by giving advisories to the ownship's pilot. Every advisory, except Clear-of-Conflict (COC), has a vertical rate range of the form (-∞, v lo ] or [v lo , +∞) for some vertical rate v lo (Table 1), which we call the target vertical velocity. We model any advisory by its corresponding target vertical velocity v lo , and a binary variable w for its orientation, whose value is -1 if the vertical rate range of the advisory is (-∞, v lo ] and +1 if it is [v lo , +∞). This symbolic encoding can represent many advisories and is robust to changes in the ACAS X advisory set. As a matter of fact, the only advisory that this symbolic encoding cannot handle is the recently-added Multi-Threat Level-Off (MTLO) advisory, only relevant in the presence of multiple intruders.

Following the ACAS X design [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], we assume that the ownship pilot complies with each advisory within δ seconds, and that she accelerates with acceleration at least a lo to reach the target vertical velocity.

Safe Region for an Immediate Pilot Response

We present in this section a simplified version of the dynamics from Sect. 2.1. We give a hybrid model for this simplified system and prove its safety. The new assumptions will be relaxed in later sections to achieve the safety verification of the full model of Sect. 2.1. cal miles nmi (1,852 metres), knots kts (nautical miles per hour), feet ft (0.3048 meter) and minutes min (60 seconds).

Model

In this section, we assume that the ownship and intruder are flying head-on (θ v = 180 • ). We also assume that the pilot reacts immediately to any advisory (δ = 0 s), and that the advisory COC is not allowed. These assumptions will be relaxed in Sect. 4 and Sect. 6. The model in this section permits updates to the resolution advisory but, unlike in Sect. 5, each advisory issued has to be safe, i.e., it has to prevent any NMAC at any future time, even if followed forever. We assume that r is a scalar: if r ≥ 0 then the ownship is flying towards the intruder, otherwise it is flying away from it. Both cases could require an advisory. Since the ownship and intruder are flying head-on with straight line trajectories, there exists a vertical plane containing both their trajectories. In this plane, the puck becomes a rectangle centered around the ownship, of width 2r p and height 2h p , and there is an NMAC if and only if the intruder is in this rectangle (in gray on Fig. 1).

Differential Dynamic Logic and KeYmaera X

We model our system using Differential Dynamic Logic dL [START_REF] Platzer | Differential dynamic logic for hybrid systems[END_REF][START_REF] Platzer | Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics[END_REF][START_REF] Platzer | Logics of dynamical systems[END_REF][START_REF] Platzer | A uniform substitution calculus for differential dynamic logic[END_REF], a logic for reasoning about hybrid programs, a programming language for hybrid systems. The logic dL allows discrete assignments, control structures, and execution of differential equations. It is implemented in the theorem prover KeYmaera X [START_REF] Fulton | KeYmaera X: An axiomatic tactical theorem prover for hybrid systems[END_REF], that we use to verify our safe regions with respect to our models. All the KeYmaera X models and proofs of this paper can be found at http: //www.ls.cs.cmu.edu/pub/AcasX-long.zip.

The dL formula for the model that we use in this section is given in Eq. [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF]. We use the notation L -1 impl for the safe region: the letter L stands for lower bound (for w = 1; it is an upper bound for w = -1); the subscript impl stands for implicit safe region, as described in Sect. 3.3; and the superscript -1 indicates that the region is safe for unbounded time; the rationale behind its use will become more clear in Sect. 5.2.

r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a lo > 0 ∧ (w = -1 ∨ w = 1) ∧ L -1 impl (r, h, v, w, v lo ) → [( ( ?true ∪ (w := -1 ∪ w := 1); v lo := * ; ?L -1
impl (r, h, v, w, v lo ); advisory := (w, v lo ) );

a := * ; {r = -r v , h = -v, v = a & wv ≥ wv lo ∨ wa ≥ a lo } ) * ] (|r| > r p ∨ |h| > h p ) (1)
This formula of the form p → [α]q says all executions of hybrid program α starting in a state satisfying logical formula p end up in a state satisfying q. It is akin to the Hoare triple {p}α{q} with precondition p and postcondition q. The precondition in Eq. ( 1) imposes constraints on several constants, as well as the formula L -1 impl (r, h, v, w, v lo ) (which we identify below) that forces the intruder to be in a safe region for an initial advisory (w, v lo ). We cannot guarantee safety if the intruder starts initially in an unsafe region. The postcondition encodes absence of NMAC. Lines 3-5 express the action of the ACAS X system. The nondeterministic choice operator ∪ in Line 3 expresses that the system can either continue with the same advisory by doing nothing-just testing the trivial condition ?true-this ensures it always has a valid choice and cannot get stuck. Otherwise it can choose a new advisory (w, v lo ) in Line 4 that passes the safety condition L -1 impl (r, h, v, w, v lo ) in Line 5advisory represents the next message to the pilot. Line 6 expresses the action of the ownship pilot, who can nondeterministically choose an arbitrary acceleration (a := * ). The ownship and intruder aircraft then follow the continuous dynamics in Line 7. The evolution of the variables r, h and v is expressed by a differential equation, and requires (using the operator &) that the ownship evolves towards its target vertical velocity v lo at acceleration a lo (condition wa ≥ a lo ), unless it has already reached vertical velocity v lo (condition wv ≥ wv lo ). Finally, the star * on Line 8 indicates that the program can be repeated any number of times, allowing the system to go through several advisories.

Implicit Formulation of the Safe Region

In this section, we identify what formula can be used as safe region L -1 impl (r, h, v, w, v lo ) to prove Eq. [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF]. As in Sect. 2, we use a coordinate system fixed to the intruder and with its origin at the initial position of the ownship (see Fig. 1).

First case: if w = +1 and v lo ≥ v. Fig. 1 shows, in red, a possible trajectory of an ownship following exactly the requirements of ACAS X. This nominal trajectory of the ownship is denoted by N and merely represents one possible scenario to consider. The pilot reacts immediately, and the ownship starts accelerating vertically with acceleration a lo until reaching the target vertical velocity v lo -describing a parabola-then climbs at vertical velocity v lo along a straight line. Horizontally, the relative velocity r v remains constant. Integrating the differential equations in Eq. (1) Line 7, the ownship position (r n , h n ) at time t along N is given by:

(r n , h n ) =      r v t , a lo 2 t 2 + vt if 0 ≤ t < v lo -v a lo (a) r v t , v lo t - (v lo -v) 2 2a r if v lo -v a lo ≤ t (b) (2)
Recall that in the ACAS X specification, the ownship moves vertically with acceleration of at least a lo , then continues with vertical velocity of at least v lo . Therefore all possible future positions of the ownship will turn out to be above the red nominal trajectory. An intruder is safe if its position is always either to the side of or under any puck centered on a point in N , that is:

∀t.∀r n .∀h n . (r n , h n ) ∈ N → |r-r n | > r p ∨h-h n < -h p (3)
We call this formulation the implicit formulation of the safe region. It does not give explicit equations for the safe region border, but expresses them instead implicitly by quantifiers with respect to the nominal trajectory from Eq. (2).

Generalization. The reasoning above is generalized to the case where the target vertical velocity is exceeded (v lo < v) -which happens after the parabola part of the nominal trajectory-and symmetrically to the case of descend-type advisories (w = -1).

Eq. (1) gives the pilot ample flexibility in how to respond to a resolution advisory and gives ACAS X full flexibility to choose any advisories respecting L -1 impl (r, h, v, w, v lo ). In particular, we cannot assume the pilot would follow the nominal trajectory N . We prove that, nevertheless, the safe regions identified like this respect safety property Eq. ( 1). The implicit formulation of the safe region is L -1 impl (r, h, v, w, v lo ) in Fig. 3, and verified to be safe in KeYmaera X:

Theorem 1 (Correctness of implicit safe regions) The dL formula given in Eq. (1) is valid. That is as long as the advisories followed obey formula L -1 impl there will be no NMAC.

Explicit Formulation of the Safe Region

The implicit formulation of the safe region gives an intuitive understanding of where it is safe for the intruder to be. However, because it still contains quantifiers, its use comes at the extra cost of eliminating the quantifiers, which is inefficient

Implicit formulation A(t, hn, v, w, v lo ) ≡ 0 ≤ t < max(0, w(v lo -v)) a lo ∧ hn = wa lo 2 t 2 + vt ∨ t ≥ max(0, w(v lo -v)) a lo ∧ hn = v lo t - w max(0, w(v lo -v)) 2 2a lo L -1 impl (r, h, v, w, v lo ) ≡ ∀t.∀rn.∀hn. rn = rvt ∧ A(t, hn, v, w, v lo ) → (|r -rn| > rp ∨ w(h -hn) < -hp) Explicit formulation case -1 1 (r, v, w, v lo ) ≡ -rp ≤ r < -rp - rv min(0, wv) a lo case -1 2 (r, v, w, v lo ) ≡ -rp - rv min(0, wv) a lo ≤ r ≤ rp - rv min(0, wv) a lo bound 1 (r, h, v, w, v lo ) ≡ wrv 2 h < a lo 2 (r + rp) 2 + wrvv(r + rp) -rv 2 hp bound 2 (r, h, v, w, v lo ) ≡ wh < - min(0, wv) 2 2a lo -hp case -1 3 (r, v, w, v lo ) ≡ rp - rv min(0, wv) a lo < r ≤ rp + rv max(0, w(v lo -v)) a lo case -1 4 (r, v, w, v lo ) ≡ rp + rv max(0, w(v lo -v)) a lo < r bound 3 (r, h, v, w, v lo ) ≡ wrv 2 h < a lo 2 (r -rp) 2 + wrvv(r -rp) -rv 2 hp bound 4 (r, h, v, w, v lo ) ≡ (rv = 0) ∨ wrvh < wv lo (r -rp) - rv max(0, w(v lo -v)) 2 2a lo -rvhp case -1 5 (r, v, w, v lo ) ≡ -rp ≤ r < -rp + rv max(0, w(v lo -v)) a lo case -1 6 (r, v, w, v lo ) ≡ -rp + rv max(0, w(v lo -v)) a lo ≤ r bound 5 (r, h, v, w, v lo ) ≡ wrv 2 h < a lo 2 (r + rp) 2 + wrvv(r + rp) -rv 2 hp bound 6 (r, h, v, w, v lo ) ≡ (rv = 0 ∧ r > rp) ∨ wrvh < wv lo (r + rp) - rv max(0, w(v lo -v)) 2 2a lo -rvhp L -1 expl (r, h, v, w, v lo ) ≡ wv lo ≥ 0 → 4 i=1 (case -1 i (r, v, w, v lo ) → bound i (r, h, v, w, v lo )) ∧ wv lo < 0 → 6 i=5 (case -1 i (r, v, w, v lo ) → bound i (r, h, v, w, v lo ))
Fig. 3 Implicit and explicit formulations of the safe region for an immediate response (lower bounds for w = 1, upper bound for w = -1)

and impractical to repeatedly compute during the comparison part of our analysis. An efficient comparison with the ACAS X table, as described in Sect. 8, can only be achieved with a quantifier-free, explicit formulation, that we present in this section. We show that both formulations are equivalent. As for the implicit formulation, we derive the equations for one representative case before generalizing them.

First case: if w = +1, r v > 0, v < 0 and v lo ≥ 0. We are in the case shown in Fig. 1 and described in detail in Sect. 3.3.

The nominal trajectory N is given by Eq. ( 2). The boundary of the (green) safe region in Fig. 1 is drawn by either the bottom left hand corner, the bottom side or the bottom right hand corner of the puck. For this case, this boundary can be characterized by a set of equations (where cases 1 to 4 follow cases 1 to 4 of Fig. 3): 0. positions left of the puck's initial position (r < -r p ) are in the safe region;

1. then the boundary follows the bottom left hand corner of the puck as it is going down the parabola of Eq. (2)(a); therefore for -r p ≤ r < -r p -rvv a lo , the position (r, h) is safe if and only if h < a lo 2rv 2 (r+r p ) 2 + v rv (r+r p )-h p ; 2. following this, the boundary is along the bottom side of the puck as it is at the bottom of the parabola of Eq. (2)(a); therefore for -r p -rvv a ≤ r ≤ r p -rvv a lo , the position (r, h) is in the safe region if and only if h < -v 2 2a lo -h p ; 3. then the boundary follows the bottom right hand corner of the puck as it is going up the parabola of Eq. (2)(a); therefore for

r p -rvv a lo < r ≤ r p + rv(v lo -v) a lo , the position (r, h) is safe if and only if h < a lo 2rv 2 (r -r p ) 2 + v rv (r - r p ) -h p ;
4. finally the boundary follows the bottom right-hand corner of the puck as it is going up the straight line of Eq. (2)(b); therefore for r p + rv(v lo -v)

a lo < r, the po- sition (r, h) is in the safe region if and only if h < v lo rv (r -r p ) -(v lo -v) 2 2ar -h p .
Generalization. The general case is given in the formula L -1 expl (r, h, v, w, v lo ) of Fig. 3. The cases 1-4 and their associated bounds are for the case wv lo ≥ 0, whereas cases 5 and 6 and associated bounds are for wv lo < 0; both cases 5 and 6 follow the bottom left-hand corner of the puck as it is going along the nominal trajectory. We use KeYmaera X to formally prove that this explicit safe region formulation is equivalent to its implicit counterpart:

Lemma 1 (Equivalence of explicit safe regions) If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0 and a lo > 0, then the conditions L -1 impl (r, h, v, w, v lo ) and L -1 expl (r, h, v, w, v lo ) are equivalent.
Since the assumptions of Lemma 1 are invariants of the model in Eq. ( 1), the explicit safe regions give a model that inherits safety from Theorem 1, which we formally prove in KeYmaera X by a combination of contextual equivalence reasoning and monotonicity reasoning [START_REF] Platzer | A uniform substitution calculus for differential dynamic logic[END_REF] to embed the conditional equivalence from Lemma 1 into the context of Theorem 1.

Corollary 1 (Correctness of explicit safe regions)

The dL formula given in Eq. (1) remains valid when replacing all occurrences of L -1 impl with L -1 expl . That is as long as the advisories followed obey formula L -1 expl there will be no NMAC.

Safe Region for a Delayed Pilot Response

Since the pilot will need some time to react to an advisory issued by ACAS X, we generalize the model of Sect. 3 to account for a non-deterministic, non-zero pilot delay, and for periods of time where the system does not issue an advisory (i.e., COC). In Fig. 4, for example, the pilot reacts to a CL1500 advisory only after a certain reaction delay during which she was still in the process of initiating a descent.

Model

In this section, we still assume that the ownship and intruder are flying head-on (θ v = 180 • ). We use the same conventions as in Sect. 3 for r and r v . The model includes an initial period where there is no compliance with any advisorythe ownship accelerates non-deterministically (within limits) in the vertical direction. As before, we derive the safe regions by considering all possible positions of the ownship's puck in all possible trajectories that might evolve in the encounter. To represent pilot delay for an advisory, the model assumes an immediate advisory, and period of noncompliance δ, representing the time it takes the pilot to respond. To represent COC, the model looks for a safe advisory it can issue ε in the future if necessary, where ε is the system delay-i.e., the time before the system can issue a new advisory-and shortest COC. Hence the period of noncompliance is ε + δ.

1 r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a lo > 0 ∧ a d ≥ 0 ∧ δ ≥ 0 2 ∧ ε ≥ 0 ∧ (w = -1 ∨ w = 1) ∧ D d impl (r, h, v, w, v lo ) → 3 [( ?true ∪ 4 (w := -1 ∪ w := 1); v lo := * ; 4 (d := δ; ?D d impl (r, h, v, w, v lo ); adv := (w, v lo ) ∪ 5 d := δ + ε; ?D d impl (r, h, v, w, v lo ); adv := COC) ; 6 a := * ; ?(wa ≥ -a d ); t := 0; 7 {r = -r v , h = -v, v = a, d = -1, t = 1 & 8 (t ≤ ε) ∧ (d ≤ 0 → wv ≥ wv lo ∨ wa ≥ a lo )} 9 ) * ] (|r| > r p ∨ |h| > h p ) (4)
We modify the model of Eq. ( 1) to capture these new ideas, and obtain the model of Eq. ( 4), highlighting the differences in bold. The structure, precondition (lines 1 and 2) and postcondition (line 9) are similar. The clock d, if positive, represents the amount of time until the ownship pilot must respond to the current advisory to remain safe. Lines 3 to 5 represent the actions of the ACAS X system. As before, the system can continue with the same advisory (?true). Otherwise it can select a safe advisory (w, v lo ) to be applied after at most delay δ; or it can safely remain silent, displaying COC, if it knows an advisory (w, v lo ) that is safe if it is followed after a combined pilot and system and pilot delay of δ + ε. In line 6, the pilot non-deterministically chooses an acceleration (a := * ), within some limit (wa ≥ -a d ). The set of differential equations in line 7 describes the system's dynamics, and the conditions in line 8 use the clock t to ensure that continuous time does not evolve longer than system delay ε without a system response (t ≤ ε). Those conditions also ensure that when d ≤ 0 the pilot starts complying with the advisory. The model is structured so that the pilot can safely delay responding to an advisory for up to δ, and the system can additionally delay issuing an advisory associated with COC for up to ε. Because of the loop in our model (line 9), the safety guarantees of this theorem apply to encounters whose advisories change as the encounter evolves, encounters with periods of no advisory, and encounters where the ownship pilot exhibits some nondeterministic behavior in the vertical dimension.

In the rest of the section we use the same approach as in Sect. 3: we first derive an implicit formulation, then an equivalent explicit formulation of the safe region, and prove that the safe region guarantees that the intruder cannot cause an NMAC.

Implicit Formulation of the Safe Region

As in Sect. 3.3, let us place ourselves in the coordinate system centered on the current position of the ownship and where the intruder is fixed, and let us first assume that the ownship receives an advisory (w, v lo ) such that w = +1, and that δ ≥ 0. Let us focus on the period of time before the pilot reacts, which we henceforth call delay. During the delay, the ownship can take any vertical acceleration less than a d in absolute value, therefore its most restrictive nominal trajectory N d is to accelerate the opposite way of the advisory, at acceleration -a d . Horizontally, its speed is constant at r v . It thus describes a delay parabola, in red on Fig. 4, and its position (r n , h n ) along the nominal trajectory for

0 ≤ t < δ is given by (r n , h n ) = r v t, -
∀t.∀r n .∀h n .(r n , h n ) ∈ N d → |r-r n | > r p ∨h-h n < -h p
Symmetrically, the reasoning of this section extends to the case where w = -1. Moreover, we can handle cases where d < 0, i.e., after the pilot has reacted, by replacing d by max(0, d). The generalized implicit formulation of the safe region is given as D d impl in Fig. 5. Note that it involves the expression Theorem 2 (Correctness of delayed safe regions) The dL formula given in Eq. (4) is valid. That is as long as the advisories obey formula D d impl there will be no NMAC.

A(t -max(0, d), h n -h d , v d , w, v lo ) from

Explicit Formulation of the Safe Region

Similarly as in Sect. 4, we determine an explicit formulation of the safe region, called D d expl in Fig. 5 based on Fig. 3, and prove it correct in KeYmaera.

Lemma 2 (Equivalence of delayed explicit safe regions)

If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0, a lo > 0, a d ≥ 0, δ ≥ 0 and ε ≥ 0 then the two conditions D d impl (r, h, v, w, v lo ) and D d expl (r, h, v, w, v lo ) are equivalent.

Safe Region for Subsequent Advisories

The safety analysis from Sect. 3 requires the system to only issue advisories that will never lead to a collision. After presenting our initial results to ACAS X designers and engineers, we received feedback that the safety advice for single advisories was too restrictive for their operational purposes.

Early in an encounter, there is often enough separation between aircraft and time in the encounter so that an initial advisory, which would not be safe on its own, can still be changed or corrected to keep the aircraft safe. The rationale is that while ACAS X is designed to avoid collisions, it is also designed to avoid bothering pilots as much as possible.

To balance these concerns, if an encounter is not immediately threatening, ACAS X will typically first issue COC, or a preventive advisory like DNC or DND, before issuing a more disruptive advisory to the pilot. In those cases, the first advisory is often not safe in the sense of Sect. 3 : it will tend to keep the planes from flying directly towards each other immediately and will only ensure safety for a few seconds, but not for the rest of the encounter.

As a consequence, running the safety analysis on the immediate advisory leads to counterexamples considered as false alarms by the ACAS X designers. Anything is safe if you are far enough away; many of the examples of unsafe behavior we found were uninteresting because if the pilots chose a course that brought them closer, the system would issue a more disruptive, but safer follow-on advisory. This section builds on the previous work to develop a more sophisticated safety analysis that evaluates the safety of the present advisory, and whether it is safe or could still be made safe in the future, if necessary, via subsequent advisories.

Implicit formulation

B d (t, hn, v) ≡ 0 ≤ t < max(0, d) ∧ hn = - wa d 2 t 2 + vt const ≡ h d = - wa d 2 max(0, d) 2 + v max(0, d) ∧ v d -v = -wa d max(0, d) D d impl (r, h, v, w, v lo ) ≡ ∀t.∀rn.∀hn.∀h d .∀v d . rn = rvt ∧ (B d (t, hn, v) ∨ const ∧ A(t -max(0, d), hn -h d , v, w, v lo )) → (|r -rn| > rp ∨ w(h -hn) < -hp)
Explicit formulation

r d = rv max(0, d) v d = v -wa d max(0, d) h d = - wa d 2 max(0, d) 2 + v max(0, d) case 7 (r) ≡ -rp ≤ r ≤ rp bound 7 (r, h) ≡ wh < -hp case 8 (r) ≡ rp < r ≤ r d + rp case 9 (r) ≡ -rp ≤ r < r d -rp bound 8 (r, h)≡ wrv 2 h < - a d 2 (r -rp) 2 + wrvv(r -rp) -rv 2 hp bound 9 (r, h)≡ wrv 2 h < - a d 2 (r + rp) 2 + wrvv(r + rp) -rv 2 hp D d expl (r, h, v, w, v lo ) ≡ 9 i=7 (case i (r) → bound i (r, h)) ∧ L -1 expl (r -r d , h -h d , v d , w, v lo )
Fig. 5 Implicit and explicit formulations of the safe region for a delayed response

We use the neologism safeable to describe this superset of the safe region. This section builds up safeable in three steps. We first present two-sided safe regions, providing both an upper and a lower bound to the trajectory. We then present bounded safe regions, which only ensure absence of collision for a limited amount of time ε; bounded safe regions provide no guarantee after time ε, and the corresponding model has no liveness. Based on these important building blocks, we finally present safeable regions, which model subsequent advisories, and have a corresponding model providing liveness. This section is new, and was not presented in the conference version of this paper [START_REF] Jeannin | A formally verified hybrid system for the next-generation airborne collision avoidance system[END_REF].

Throughout the section, we sill assume that the ownship and intruder are flying head-on (θ v = 180 • ), and we use the same conventions as in Sect. 3 for r and r v . We say that a subsequent advisory is a reversal if and only if it is a downsense advisory (w = -1) while the first advisory was upsense (w = 1)-or vice-versa. In the opposite case we usually call the subsequent advisory a strengthening or a weakening.

Two-Sided Safe Region with Immediate Pilot Response

A first step towards the treatment of subsequent advisories is to provide both a lower and an upper bound to the trajectory of the ownship while it follows an initial advisory. Indeed, if the initial advisory is upsense with a reversal as a subsequent advisory, then it is crucial to also have an upper bound on the height and vertical velocity of the aircraft when the pilot starts following the subsequent advisory. Safe regions described in Sect. 3 are not sufficient, as they only provide a lower bound when w = 1, and an upper bound when w = -1. To simplify the explanation, let us first consider the case of an initial upsense advisory, i.e., with w = 1; the case of the initial downsense advisory is symmetric. Lower bound and upper bound will refer to the case w = 1; lower and upper bound are switched in the case w = -1.

Model

Let us consider a pilot receiving an initial advisory (w, v lo ) with w = 1, for example CL1500 or DND. In Sect. 3 we argued that following the advisory (w, v lo ) meant that either the vertical speed of the ownship should be greater than v lo , or its acceleration should be greater than a lo , leading to the differential equation's domain wv ≥ wv lo ∨ wa ≥ a lo . Similarly, we fix upper bounds v up and a up on the vertical velocity and acceleration of the ownship while following advisory (w, v lo ). They are again symbolic parameters, with typical values a up = g/2 and v up = 10,000 ft/min. We modify the model of Eq. ( 1) to capture these new ideas, and obtain the model of Eq. ( 5), highlighting the differences in bold.

1 r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a lo > 0 ∧ a up ≥ a lo , 2 ∧ (w = -1 ∨ w = 1) ∧ C -1 impl (r, h, v, w, v lo , v up ) → 3 [( ( ?true ∪ 4 (w := -1 ∪ w := 1); v lo := * ; v up := * ; 5 ?C -1 impl (r, h, v, w, v lo , v up ); advisory := (w, v lo , v up ) ); 6 a := * ; 7 {r = -r v , h = -v, v = a 8 & (wv ≥ wv lo ∨ wa ≥ a lo ) 9 ∧((wv ≤ wv up ∧ wa ≤ a up ) ∨ wa ≤ 0)} 10 ) * ] (|r| > r p ∨ |h| > h p ) (5)
Beyond replacing the lower safe region L -1 impl by a twosided safe region C -1 impl , we impose a up ≥ a lo to ensure that More interestingly, we update the evolution domain of the differential equation (lines 8 and 9). To understand what it means for the ownship to respect the new upper bounds v up and a up , let us first consider an advisory for which w = 1, and let us distinguish two cases. If initially v ≤ v up , then both upper bounds on vertical velocity and acceleration need to be respected simultaneously, leading to condition v ≤ v up ∧ a ≤ a up . Otherwise, v > v up and the initial vertical speed of the aircraft v is initially already strictly greater than v up . Given that the pilot receives an upsense advisory, it would be unrealistic to assume that the aircraft would typically follow a negative acceleration to get its vertical speed to go back to v up . Instead, we assume that the pilot does not accelerate up further, leading to the condition a ≤ 0. Incorporating the symmetric case w = -1 leads to the general evolution domain for the upper bound (wv lo ≤ wv up ∧ wa ≤ a up ) ∨ wa ≤ 0.

This analysis leads to an important realization for the upper safe region: in the case where the initial vertical velocity overcomplies (i.e., when wv ≥ wv up ), the upper target vertical velocity is not v up anymore, but rather it is the initial value of v; in full generality the upper target vertical velocity becomes the modified upper target vertical velocity w max(wv up , wv). Throughout the implicit and explicit formulations of the safe region, this modified target vertical velocity will play the role simply played by v lo in Sect. 3; we usually highlight it in bold.

Implicit formulation of the safe region

The safe region C -1 impl for two-sided safety consists of L -1 impl from Fig. 3 and an additional upper bound U -1 impl . The implicit formulation of the upper bound U -1 impl is similar to the implicit formulation of the lower bound described in Sect. 3.3. As in Sect. 3.3, we use a coordinate system fixed to the intruder and with its origin at the initial position of the ownship.

First case: if w = +1 and v up ≥ v. We again consider a (different) upper nominal trajectory N up , represented in red on Fig. 6. This nominal trajectory accelerates vertically with acceleration a up until reaching the modified target vertical velocity (which, here, is v up = max(wv up , wv)), describing a parabola; it then continues at the vertical velocity v up along a straight line. As before, the horizontal velocity remains constant at r v . The ownship position (r n , h n ) at time t along

-rn| > rp ∨ w(h -hn) > hp) C -1 impl (r, h, v, w, v lo , vup) ≡ L -1 impl (r, h, v, w, v lo ) ∨ U -1 impl (r, h, v, w, vup) Explicit formulation case -1 10 (r, v, w, vup) ≡ -rp ≤ r ≤ rp bound 10 (r, h, v, w, vup) ≡ wh > hp case -1 11 (r, v, w, vup) ≡ rp < r ≤ rp + rvmax(0, w(vup -v)) aup case -1 12 (r, v, w, vup) ≡ -rp ≤ r < -rp + rvmax(0, w(vup -v)) aup bound 11 (r, h, v, w, vup) ≡ wrv 2 h > aup 2 (r -rp) 2 + wrvv(r -rp) + rv 2 hp bound 12 (r, h, v, w, vup) ≡ wrv 2 h > aup 2 (r + rp) 2 + wrvv(r + rp) + rv 2 hp case -1 13 (r, v, w, vup) ≡ -rp + rvmax(0, w(vup -v)) aup ≤ r case -1 14 (r, v, w, vup) ≡ rp + rvmax(0, w(vup -v)) aup < r bound 13 (r, h, v, w, vup) ≡ (rv = 0 ∧ r > rp)∨ wrvh > max(wvup, wv)(r + rp) - rvmax(0, w(vup -v)) 2 2aup + rvhp bound 14 (r, h, v, w, vup) ≡ (rv = 0)∨ wrvh > max(wvup, wv)(r -rp) - rvmax(0, w(vup -v)) 2 2aup + rvhp U -1 expl (r, h, v, w, vup) ≡ max(wvup, wv) > 0 → 13 i=10 (case -1 i (r, v, w, vup) → bound i (r, h, v)) ∧ max(wvup, wv) ≤ 0 → i∈{10,11,14} (case -1 i (r, v, w, vup) → bound i (r, h, v)) C -1 expl (r, h, v, w, v lo , vup) ≡ L -1 expl (r, h, v, w, v lo ) ∨ U -1 expl (r, h, v, w, vup)
Fig. 8 Implicit and explicit formulations of the safe region for an immediate response (upper bounds for w = 1, lower bound for w = -1)

this nominal trajectory is, thus, given by:

(r n , h n ) =              r v t , a up 2 t 2 + vt if 0 ≤ t < v up -v a up (a) r v t , v up t - (v up -v) 2 2a up if v up -v a up ≤ t (b) (6)
Recall that our specification is that the ownship moves vertically with acceleration of at most a up , then continues with vertical velocity of at most max(v up , v). Therefore all possible future positions of the ownship will turn out to be below the red upper nominal trajectory. Therefore, an intruder is now safe if its position (r, h) is always either to the side of or above any puck centered on a point in N up , that is:

∀t.∀r n .∀h n .(r n , h n ) ∈ N up → |r -r n | > r p ∨ h -h n > h p (7)
We call this formulation the implicit formulation of the upper safe region.

Generalization. The reasoning above is generalized to the case w = -1, leading to fully general equations for the implicit formulation of the upper safe region presented in Fig. 8. Finally, the condition for the two-sided advisory C -1 impl is built as a disjunction of the lower safety advisory L -1 impl and upper safety advisory U -1 impl . Although we cannot assume that the ownship will follow either nominal trajectory, we show that an ownship following the model of Eq. ( 5), thus respecting the two-sided condition C -1 impl , stays between both nominal trajectories, keeping it safe. The proof of safety is verified in KeYmaera X: Theorem 3 (Correctness of two-sided safe regions) The dL formula given in Eq. (5) is valid. That is as long as the advisories obey formula C -1 impl there will be no NMAC. First case: if w = +1, r v > 0, v ≤ 0 and v up > 0. In particular v up > v, therefore the modified upper target vertical velocity is max(v up , v) = v up . This is the case described in Fig. 6, and the nominal trajectory N up is given by Eq. ( 7).

Explicit formulation of the safe region

The boundary of the (green) safe region in Fig. 6

(r -r p ) - (vup-v) 2 2aup + h p .
Generalization The general case is given in the formula U -1 expl of Fig. 8. The cases 10-13, described above in a specific case, are for the case max(wv up , wv) > 0, whereas cases 10, 11 and 14 are used for the case max(wv up , wv) ≤ 0; case 14 follows the top left-hand corner of the puck. Finally, the explicit condition for the two-sided advisory C -1 expl is built as a disjunction of the lower and upper safety advisories, as shown in Fig. 8. A graphic representation of C -1 expl (in green) along with its associated nominal trajectories is shown in Fig. 7. We again use KeYmaera X to formally prove that this explicit two-sided safe region formulation is equivalent to its implicit counterpart: Lemma 3 (Equivalence of two-sided explicit safe regions) If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0, a lo > 0, a up ≥ a lo then the two conditions C -1 impl (r, h, v, w, v lo ) and C -1 expl (r, h, v, w, v lo ) are equivalent.

The assumptions of Lemma 3 are invariants of the model in Eq. ( 5) . As a consequence, a model of explicit safe regions inherits safety from Theorem 3, which we formally prove in KeYmaera X (again by conditional congruence reasoning).

Corollary 2 (Correctness of two-sided explicit safe regions) The dL formula given in Eq. (5) remains valid when replacing all occurrences of C -1 impl (r, h, v, w, v lo , v up ) with C -1 expl (r, h, v, w, v lo , v up ). That is, as long as the advisories followed obey formula C -1 expl (r, h, v, w, v lo , v up ) there will be no NMAC.

Bounded-Time Safe Regions

We build on the two-sided safe region to build a model and safe regions for bounded-time safety, i.e., regions only guaranteeing safety of the ownship up to some time ε. Flying aircraft in ways that are merely safe for a bounded time ε is inherently unsafe. It is, nevertheless, a critical building block toward constructing safeable regions, since those feature advisories that are acceptable for some time ε and can be followed up with safe subsequent advisories. This section studies only the former aspect of safety for bounded time. An intuitive understanding of bounded-time safe regions can be gathered from Fig. 9: the nominal trajectories stop at time ε, beyond which the safe region provides no guarantee. The corresponding safe regions are truncated vertically at r = r v ε + r p .

We call the corresponding conditions L ε impl and L ε expl for lower bounded-time safety, U ε impl and U ε expl for upper bounded-time safety, and C ε impl and C ε expl for two-sided boundedtime safety. By convention, a negative ε < 0 signifies an unbounded region, which fits to the notations L -1 impl and L -1 expl , U -1 impl and U -1 expl , C -1 impl and C -1 expl used in Sect. 3 and 5.1.

Model

We modify the model of Eq. ( 5) to reflect the ideas of safety for up to time ε and obtain the model of Eq. ( 8):

1 r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a lo > 0 ∧ a up ≥ a lo 2 ∧ (w = -1 ∨ w = 1) ∧ C ε impl (r, h, v, w, v lo , v up ) →
7 {r = -r v , h = -v, v = a, t = 1 8 & (t ≤ ε ∨ ε < 0) 9 ∧ (wv ≥ wv lo ∨ wa ≥ a lo ) 10 ∧ ((wv ≤ wv up ∧ wa ≤ a up ) ∨ wa ≤ 0) 11 } ) * 12 ) * ] (|r| > r p ∨ |h| > h p )
Fig. 9 Nominal trajectories of the ownship (red) and bounded-time safe region for the intruder (green), immediate response [START_REF] Fulton | KeYmaera X: An axiomatic tactical theorem prover for hybrid systems[END_REF] Beyond replacing the condition C -1 impl by C ε impl at lines 2 and 4, the most notable difference is the disappearance of the ?true case in the system decision (line 3 of Eq. ( 5)): since an advisory can only be followed during at most time ε, we disallow the model to loop and continue following the same advisory. However, we need to still allow the pilot to use several accelerations while she is following a given advisory; to model this we add a loop ( * ) around the pilot decisions on lines 6 to 11; in Eq. ( 5) this second loop was not necessary thanks to the ?true case. Finally, we add an explicit clock variable t to model time since the last advisory was issued. The variable t is initialized to 0 at each initial advisory (line 5), evolves with derivative 1 and enforces that the differential equation does not execute for longer than time bound ε (t ≤ ε in line 7) unless time is unbounded (encoded by ε < 0). Note that t is only reset on line 5 before the pilot's loop lines 6-10, so beyond time t = ε, only repetitions of the outer loop lines 3-11 in Eq. ( 8) make any progress, which will first issue an updated ACAS X advisory in lines 3-4 for the pilot to comply with from then on.

Implicit formulation of the bounded-time safe region

The implicit and explicit formulations of the boundedtime safe regions modify the different cases presented in Sect. 5.1 to take into account the time bound ε. The general philosophy is to have the bounded-time equations be an extension of the equations presented in Sect. 5.1: to achieve that all supplemental restrictions are of the form (ε < 0 ∨ restriction), which trivially evaluates to true when considering an unbounded time condition (represented by ε < 0). Full equations are presented in Fig. 10.

The implicit formulations L ε impl and U ε impl are very similar to the one presented in Sect. 5.1: when considering a bounded nominal lower or upper trajectory, we only add a condition t n ≤ ε whenever ε ≥ 0, to truncate the nominal trajectory at time t n = ε. As usual, the two-sided implicit formulation C ε impl is the disjunction of L ε impl and U ε impl .

As usual, the proof of safety is verified in KeYmaera X:

Theorem 4 (Correctness of bounded-time implicit safe regions) The dL formula given in Eq. ( 8) is valid. That is as long as the advisories obey formula C ε impl there will be no NMAC for time up to ε if ε ≥ 0, and forever if ε < 0. There are no guarantees beyond time ε if ε ≥ 0.

The loop invariant used to prove Eq. ( 5) has a subtle difference compared to the previous theorems. Unlike in all previous theorems, C ε impl is not an invariant of the corresponding model Eq. ( 5) (but almost). To turn the implicit conditions of Fig. 10 into an invariant, we capture the remaining time that we must follow an advisory by simply turning ε into (ε -t) (i.e., when already having followed an advisory for duration t we have to follow it for the remaining duration ε -t). The condition ε < 0 encodes advisories that must be followed forever, and remains unchanged in the invariant. So ε < 0 ∨ t n ≤ ε turns into ε < 0 ∨ t n ≤ ε -t in both L ε impl and U ε impl to obtain the invariant.

Explicit formulation of the bounded-time safe region

The explicit formulation of the bounded-time safe region also builds on its unbounded-time counterpart from Sect. 5.1. In cases 1 to 6 and 10 to 14, and whenever ε ≥ 0, only the following cases need to be modified:

for a case that follows the bottom or top left-hand corner of the puck, the corresponding boundary of the safe region should now stop when the puck reaches time ε, i.e., when the corner reaches -r p + r v ε. Therefore we add the condition r ≤ -r p + r v ε. This is the case of case ε 1 , case ε 5 , case ε 6 , case ε 12 and case ε 13 ; for a case that follows the bottom or top right-hand corner of the puck, the corresponding boundary of the safe region should now stop when the puck reaches time ε, i.e., when the corner reaches r p + r v ε. Therefore we add the condition r ≤ r p + r v ε. This is the case of case ε 3 , case ε 4 , case ε 11 , and case ε 14 ; -case ε 10 models the boundary above the puck at time 0 and is unaffected by bounded time;

case ε 13 (r, v, w, vup) ≡ case -1 13 (r, v, w, vup) ∧ (ε < 0 ∨ r ≤ -rp + rvε) case ε 14 (r, v, w, vup) ≡ case -1 14 (r, v, w, vup) ∧ (ε < 0 ∨ r ≤ rp + rvε) L ε expl (r, h, v, w, v lo ) ≡ wv lo ≥ 0 → 4 i=1 (case ε i (r, v, w, v lo ) → bound i (r, h, v, w, v lo )) ∧ wv lo < 0 → 6 i=5 (case ε i (r, v, w, vup) → bound i (r, h, v, w, vup)) U ε expl (r, h, v, w, vup) ≡ max(wvup, wv) > 0 → 13 i=10 (case ε i (r, v, w, vup) → bound i (r, h, v, w, vup)) ∧ max(wvup, wv) ≤ 0 → i∈{10,11,14} (case ε i (r, v, w, vup) → bound i (r, h, v, w, vup)) C ε expl (r, h, v, w, v lo , vup) ≡ L ε expl (r, h, v, w, v lo ) ∨ U ε expl (r, h, v, w, vup)
Special cases of the bounded-time explicit formulation

case ε 15 (r, v, w, v lo ) ≡ case ε 16 (r, v, w, v lo ) ≡ ε ≥ 0 ∧ -rp + rvε ≤ r ≤ rp + rvε bound ε 15 (r, h, v, w, v lo ) ≡ ε ≤ max(0, w(v lo -v)) a lo → wh < a lo 2 ε 2 + wvε -hp ∧ ε > max(0, w(v lo -v)) a lo → wh < wvε - max(0, w(v lo -v)) 2 2a lo -hp bound ε 16 (r, h, v, w, vup) ≡ ε ≤ max(0, w(vup -v)) aup → wh > aup 2 ε 2 + wvε + hp ∧ ε > max(0, w(vup -v)) aup → wh > max(wvup, wv)ε - max(0, w(vup -v)) 2 2aup + hp Lε expl (r, h, v, w, v lo ) ≡ L ε expl (r, h, v, w, v lo ) ∧ (wv lo < 0 → case ε 15 (r, v, w, v lo ) → bound 15 (r, h, v, w, v lo )) Û ε expl (r, h, v, w, vup) ≡ U ε expl (r, h, v, w, vup) ∧ (max(wvup, wv) ≤ 0 → case ε 16 (r, v, w, vup) → bound 16 (r, h, v, w, vup)) Ĉε expl (r, h, v, w, v lo , vup) ≡ Lε expl (r, h, v, w, v lo ) ∨ Û ε expl (r, h, v, w, vup)
Fig. 10 Implicit and explicit formulations of the safe region for bounded time -case ε 2 should only appear if the puck ever reaches the bottom of the parabola Eq. ( 6)(a), that is, only in the case where -min(0,wv) a lo ≤ ε, which is exactly the condition we added.

The formulas for L ε expl , U ε expl and C ε expl are constructed from these cases as before.

However, those changes alone are not enough. In the expression of L ε expl and when wv lo ≥ 0, there is a missing explicit boundary along the bottom side of the puck at time ε; we add it explicitly as case 15 → bound 15 to form Lε expl . Similarly, in the expression of U ε expl and when we have max(wv up , wv) ≤ 0, there is a missing explicit boundary along the top side of the puck at time ε; we add it explicitly as case 16 → bound 16 to form Û ε expl . We still define Ĉε expl as the disjunction Lε expl ∨ Û ε expl . These extra cases 15 and 16 are inconsequential for the safeable result and are, thus, kept in the separate expression Ĉε expl .

Lemma 4 (Equivalence of bounded-time explicit safe regions)

If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0, a lo > 0, a up ≥ a lo then the two conditions C ε impl (r, h, v, w, v lo , v up ) and Ĉε expl (r, h, v, w, v lo , v up ) are equivalent.
To prove this lemma we first prove that L ε impl (r, h, v, w, v lo ) and Lε expl (r, h, v, w, v lo ) are equivalent, then that conditions U ε impl (r, h, v, w, v up ) and Û ε expl (r, h, v, w, v up ) are equivalent. The safety of explicit safe regions follows from Theorem 4 and Lemma 4 by conditional congruence reasoning.

Corollary 3 (Correctness of bounded-time explicit safe regions)

The dL formula in Eq. (8) remains valid when replacing all occurrences of C ε impl (r, h, v, w, v lo , v up ) with the formula Ĉε expl (r, h, v, w, v lo , v up ). That is, as long as the advisories followed obey formula Ĉε expl (r, h, v, w, v lo , v up ) there will be no NMAC.

Safeable region

Putting together the building blocks we have presented, we finally present safeable regions, implicit C safeable(ε) impl and explicit C safeable(ε) expl . The intuition behind safeable is captured in Fig. 11: we consider all the positions and speeds at which the ownship can end up at time ε, and in particular the lowest such position and speed (position lower 1), and the highest such position and speed (position upper 1). At the lowest position, we look at the most extreme strengthening available; and at the highest position, we look at the most extreme reversal available. The disjunction of the two safe regions of this strengthening and of this reversal corresponds to intruder positions that can be avoided by an appropriate action at time ε: this is the safeable region. Another way of seeing safeable is that it is a subset of bounded-time safe that also provides liveness of the model: it ensures that the ownship does not get stuck at time ε.

The safeable formulation is presented in Fig. 12, and a graphic representation in Fig. 11. Throughout this section we suppose that ε ≥ 0, i.e., all the safe regions not explicitly labelled as non-bounded-time (with superscript -1) have a finite time bound.

Model

The model is presented in Eq. ( 9), and builds on the bounded-time model Eq. ( 8), with very few changes.

1 r p ≥ 0 ∧ h p > 0 ∧ r v ≥ 0 ∧ a lo > 0 ∧ a up ≥ a lo 2 ∧ ε ≥ 0 ∧ (w = -1 ∨ w = 1) 3 ∧ C safeable(ε) impl (r, h, v, w, v lo , v ex lo , v up , v ex up ) → 4 [( ( (w := -1 ∪ w := 1); v lo := * ; v up := * ; 5 ?C safeable(ε) impl (r, h, v, w, v lo , v ex lo , v up , v ex up );
9 {r = -r v , h = -v, v = a, t = 1 & t ≤ ε 10 ∧ (wv ≥ wv lo ∨ wa ≥ a lo ) 11 ∧ ((wv ≤ wv up ∧ wa ≤ a up ) ∨ wa ≤ 0) 12 } ) * 13 ) * ] (|r| > r p ∨ |h| > h p ) (9)
In fact, we are only changing the conditions to C safeable(ε) impl on lines 2 and 4. But that makes a big difference: informally, instead of having a model that gets stuck at time ε, we now have a model that can always find a safeable advisory (although we don't formally prove that last fact yet).

Implicit and explicit formulations of the safeable regions

The formulations presented in Fig. 12 use the formulations of the bounded-time safe regions as building blocks.

The implicit and explicit formulations are built in very similar ways.

As shown in Fig. 11, the nominal lower bound trajectory consists of a bounded-time lower bound trajectory starting at time 0, followed by an unbounded-time lower bound trajectory starting at time ε; this nominal trajectory is at height h ex and vertical velocity v ex at time ε. Therefore the safeable lower bound consists of one bounded-time lower bound up to time ε, followed by an unbounded-time lower bound starting at time ε, height h ex L and vertical velocity v ex L . The nominal upper bound trajectory consists, however, of a bounded-time upper bound trajectory starting at time 0, followed by an unbounded time reversed (i.e., taking -w) lower bound trajectory starting at time ε; this nominal trajectory is at height h ex and vertical velocity v ex at time ε. Therefore the safeable upper bound consists of one bounded-time lower bound up to time ε, followed by an unbounded-time lower bound starting at time ε, height h ex U and vertical velocity v ex U .

Fig. 11 Nominal trajectories of the ownship (red) and safeable region for the intruder (green), immediate response

As usual, the proof of safety is verified in KeYmaera X:

Theorem 5 (Correctness of implicit safeable regions) The dL formula given in Eq. ( 9) is valid. That is as long as the advisories followed obey formula C safeable(ε) impl there will be no NMAC.

Before proving the equivalence of C safeable(ε) impl and C safeable(ε) expl , we first prove a lemma allowing us to simplify cases 15 and 16 presented in Sect. 5.2.

Lemma 5 (Simplification of cases 15 and 16) If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0, a lo > 0, a up ≥ a lo and ε ≥ 0:

given h ex L and v ex L as defined in the definition of L safeable(ε) expl in Fig. 12, then:

L -1 expl (r -r v ε, h -h ex , v ex , w, v ex lo ) → case ε 15 (r, v, w, v lo ) → bound ε 15 (r, h, v, w, v lo ); -given h ex
U and v ex U as defined in the definition of U safeable(ε) expl in Fig. 12, then:

L -1 expl (r -r v ε, h -h ex , v ex , -w, v ex lo ) → case ε 16 (r, v, w, v up ) → bound ε 16 (r, h, v, w, v up ).
Lemma 6 (Equivalence of explicit safeable regions) If w = ±1, r p ≥ 0, h p > 0, r v ≥ 0, a lo > 0, a up ≥ a lo and ε ≥ 0, then the two conditions C safeable(ε) impl and C safeable(ε) expl are equivalent.

6 Reduction from 3D Dynamics to 2D Dynamics

In this section, we show that, with respect to our assumptions, any 3-dimensional encounter (Sect. 2) can be reduced to a 2-dimensional encounter (Sect. 3) without loss of generality. This could be done using a change of reference frame and a dimension reduction.

For the sake of clarity, let us put ourselves in a reference frame (O, i, j, k) fixed to the ownship (O). In this reference frame, the position of an intruder I is represented by the tuple (x, y, h), and the differential equation system that governs its motion is given by x = r x , y = r y , (h ) = a, where r x , r y and a remain constant as time evolves. The motion of the encounter can be decoupled into a 2-dimensional In what follows, we reduce the horizontal encounter from a 2-dimensional motion to a 1-dimensional motion, thereby simplifying the problem conceptually and computationally by reducing its number of variables.

Fig. 13 depicts a top view of a generic encounter. We denote by r the position, and r v the velocity, of the intruder relative to the ownship, and by r v ≥ 0 the norm of r v .

First suppose r v > 0. The idea is to choose a reference frame (P, k, ) in which one axis k is aligned with r v , such that no relative motion happens in the other direction . Its fixed center P is defined as the orthogonal projection of point O on the direction of r v . The unit vector k is defined as rv rv , and is a unit such that (P, k, ) is positively oriented.

Let v |O (resp. v |P ) denote the coordinates of a vector v relative to the reference frame (O, i, j) (resp. (P, k, )). Then, the coordinates for r and r v are: r |O = (x, y), r v |O = (r x , r y ), r |P = (s, n) and r v |P = (-r v , 0). The scalar product r • r v and the cross product r × r v are independent of the horizontal reference frame, therefore:

xr x + yr y = -sr v xr y -yr x = nr v (10)
Given r x and r y , Eqns. [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF] imply that the coordinates (x, y) are uniquely determined by the choice of (s, n), as long as r v = 0 (using r v 2 = r 2 x + r 2 y ). For any 2-dimensional configuration, the encounter can thus be considered a head-on

Implicit formulation L safeable(ε) impl (r, h, v, w, v lo , v ex lo ) ≡ L ε impl (r, h, v, w, v lo ) ∧ ∀h ex L .∀v ex L . 0 ≤ ε < max(0, w(v lo -v)) a lo ∧ h ex L = wa lo 2 ε 2 + v lo ε ∧ v ex L = wa lo ε + v ∨ ε ≥ max(0, w(v lo -v)) a lo ∧ h ex L = v lo ε - w max(0, w(v lo -v)) 2 2a lo ∧ v ex L = v lo → L -1 impl (r -rvε, h -h ex L , v ex L , w, v ex lo ) U safeable(ε) impl (r, h, v, w, vup, v ex up ) ≡ U ε impl (r, h, v, w, vup) ∧ ∀h ex U .∀v ex U . 0 ≤ ε < max(0, w(vup -v)) aup ∧ h ex U = waup 2 ε 2 + vupε ∧ v ex U = waupε + v ∨ ε ≥ max(0, w(vup -v)) aup ∧ h ex U = w max(wvup, wv)ε - wmax(0, w(vup -v)) 2 2aup ∧ v ex U = w max(wvup, wv) → L -1 impl (r -rvε, h -h ex U , v ex U , -w, v ex up ) C safeable(ε) impl (r, h, v, w, v lo , v ex lo , vup, v ex up ) ≡ L safeable(ε) impl (r, h, v, w, v lo , v ex lo ) ∨ U safeable(ε) impl (r, h, v, w, vup, v ex up ) Explicit formulation L safeable(ε) expl (r, h, v, w, v lo , v ex lo ) ≡ L ε expl (r, h, v, w, v lo ) ∧ L -1 expl (r -rvε, h -h ex L , v ex L , w, v ex lo )
where

     h ex L = wa lo 2 ε 2 + v lo ε and v ex L = wa lo ε + v if 0 ≤ ε < max(0, w(v lo -v)) a lo h ex L = v lo ε - w max(0, w(v lo -v)) 2 2a lo and v ex L = v lo if ε ≥ max(0, w(v lo -v)) a lo U safeable(ε) expl (r, h, v, w, vup, v ex up ) ≡ U ε expl (r, h, v, w, vup) ∧ L -1 expl (r -rvε, h -h ex U , v ex U , -w, v ex up )
where

       h ex U = waup 2 ε 2 + vupε and v ex U = waupε + v if 0 ≤ ε < max(0, w(vup -v)) aup h ex U = w max(wvup, wv)ε - wmax(0, w(vup -v)) 2 2aup and v ex U = w max(wvup, wv) if ε ≥ max(0, w(vup -v)) aup C safeable(ε) expl (r, h, v, w, v lo , v ex lo , vup, v ex up ) ≡ L safeable(ε) expl (r, h, v, w, v lo , v ex lo ) ∨ U safeable(ε) expl (r, h, v, w, vup, v ex up )
Fig. 12 Implicit and explicit formulations of the safeable region encounter where s plays the role of r and where a new puck radius, denoted s p , plays the role of r p .

Let us now determine the radius s p of the dimensionreduced encounter, and prove that the absence of NMAC in (O, i, j)-characterized by r 2 > r 2 p -is equivalent to the absence of NMAC in (P, k, )-characterized by s 2 > s 2 p . Using [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF]:

r v 2 r 2 = r v 2 (x 2 + y 2 ) = (xr x + yr y ) 2 + (xr y -yr x ) 2 = r v 2 (s 2 + n 2 ) . Since r v = 0, this implies r 2 = s 2 + n 2 . Therefore, r 2 > r 2 p if and only if s 2 + n 2 > r 2 p or equivalently s 2 > r 2 p - n 2 . If r 2
p -n 2 < 0, the direction of the vector r v does not intersect the puck, the inequality s 2 > r 2 p -n 2 is trivially true, and the encounter is safe. If r 2 p -n 2 ≥ 0, we choose the new puck radius s p for the dimension-reduced encounter as s p = r p 2 -n 2 ≥ 0, and the safety condition in (P, k, ) becomes s 2 ≥ s 2 p . When θ v = 180 • , one has s = r, n = 0 and s p = r p as in Sect. 3-4.

As the encounter evolves in (O, i, j) along x = r x , y = r y , its dimension-reduced version evolves in (P, k, ) along the differential equations s = -r v , n = 0, obtained by differentiating Eqns. [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF] and canceling r v . The following proposition, proved in KeYmaera, combines both dynamics and shows that the absence of an NMAC of radius r p in (O, i, j) is equivalent to the absence of an NMAC of radius s p in (P, k, ).

Proposition 1 (Horizontal Reduction)

The following dL formula is valid

xr x + yr y = -sr v ∧ xr y -yr x = nr v ∧ x 2 + y 2 = n 2 + s 2 ∧ r v 2 = r 2 x + r 2 y → [x = r x , y = r y , s = -r v , n = 0] x 2 + y 2 > r 2 p ↔ s 2 > r 2 p -n 2 (11)
Observe that the horizontal NMAC condition in (P, k, ) only depends on the change of one variable rather than two. The proposition also applies to the special case r v = 0. In this case the origin P is no longer defined, and Eqns. [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF] are trivially true. The variables s and n are constants (s = 0, n = 0), their initial values are only restricted by the condition n 2 + s 2 = x 2 + y 2 in the assumption of the proposition, but they are not unique. When the relative position between the two aircraft does not evolve over time, if the intruder is at a safe distance initially, the encounter is still safe for all time.

Tightness of Conditions

The conditions L -1 impl and L -1 expl in Fig. 3, D d impl and D d expl in Fig. 5, andC safeable(ε) impl and C safeable(ε) expl in Fig. 12 specify conditions we have derived for safety under varying assumptions. While we have formally proved that each of these conditions is sufficient to guarantee safety within the relevant models (Theorem 1, Corollary 1, Theorem 2, Lemma 2, Theorem 5, and Lemma 6), we have not proved that these conditions are necessary for safety or tight. I.e., if an advisory and aircraft geometry meet the safety conditions, then the aircraft are guaranteed to be safe under the relevant assumptions. However, we have not proved that advisories are not safe when that advisory and the associated geometry do not meet the conditions.

In some cases, our conditions are overapproximations. For the conditions that do not account for subsequent advisories (safe conditions), L -1 impl /L -1 expl and D d impl /D d expl , consider the following physically unreliable geometry. The aircraft are diverging horizontally (e.g., θ v = 0 and r v > 0), the intruder is sufficiently above the ownship in altitude, i.e., more than h p above the ownship (h > h p ), and the aircraft are horizontally separated by exactly the radius of the puck, i.e., r = r p . Intuitively, the intruder is directly above the left edge of the gray box in Fig. 4. If considering an up-sense advisory, this geometry does not pass L -1 expl or D d expl because the conditions have no exception for intruders over the exact edge of the puck. However, NMAC would require the ownship to accelerate upward at an infinite rate, so NMAC is not possible.

There are cases where advisories fail to meet the conditions for subsequent advisories (safeable conditions), but are safe under the relevant assumptions as well. Conditions C safeable(ε) impl /C safeable(ε) expl are built from a lower-bound trajectory and an upper-bound trajectory where, e.g., the lowerbound trajectory ends with an unbounded-time trajectory corresponding to the strongest possible upward subsequent advisory (vertical velocity v ex ). Such construction forms a reasonable overapproximation under the intuition that if the strongest upward subsequent advisory makes the lower-bound initial-trajectory safe, that subsequent advisory would also make any other initial-trajectory safe. Analogous reasoning supports the construction of the upper-bound trajectory. The limitation of this approach, with respect to complete-ness, is that it implicitly assumes that the subsequent advisory is fixed, or determined at the time of the first advisory. I.e., it asks if there exists one subsequent advisory now (at least either the most extreme upward or downward advisory) that can guarantee safety in the future. In reality, ACAS X chooses the subsequent advisory later in time, with some knowledge of the initial portion of the trajectory. In some cases, it is advantageous, for example, to choose the most extreme downward advisory for lower initial trajectories and to choose the most extreme upward advisory for upper initial trajectories. The result of this overapproximation is that ACAS X could always choose a safe subsequent advisory for some geometries that cannot be concluded safeable by

C safeable(ε) impl /C safeable(ε) expl .

Comparison of Safety Theorems to ACAS X

The preceding theorems about safety are independent of the tested system. To characterize the safety of ACAS X itself, we check whether advisories indicated by the core component of ACAS X, consisting of the timing and logic tables, meet the conditions of the theorems. The timing and logic tables of ACAS X contain scores for each advisory for a set of discrete sample states. Each score quantifies the desirability of issuing the corresponding advisory when in the corresponding state and is the result of optimizing a Markov decision process (MDP). In practice, ACAS X multilinearly interpolates advisory scores from the values stored in the tables, given estimates of aircraft states. Although these estimates model uncertainty in practice, we check behavior for the sample points themselves, assuming perfect knowledge of state, to compare system behavior under bestcase circumstances. Table 2 shows the range of sample state points, called cut-points, for each of the 7 dimensions of the logic tables. These non-uniformly sampled cut-points were chosen by the ACAS X designers to maximize system performance for realistic encounters while keeping the size of the tables modest. The previous advisory state includes the previously-issued advisory and information about whether the pilot was acting to comply with the advisory at the previous time step. This information is used in the MDP state for the multi-step optimization. Together these samples make up over 648 billion state combinations for which scores are explicitly stored in the ACAS X logic tables.

Corollary 1 and Lemma 6 along with Theorem 5 reduce the safety of all future trajectories to a static condition on the current state: L -1 expl or C safeable(ε) expl

, respectively. We examine the advisory specified by the logic tables at each of the 648 billion state combinations for which scores are explicitly stored and check the advisory against the respective safe or safeable condition for that advisory. given in Fig. 12) and for which there exists an alternative advisory that does satisfy the respective safety conditions.

We say a state is non-safe, or non-safeable if it is a counterexample for the safe or safeable conditions respectively.

We selected a set of parameters for acceleration and delay ranges, shown in Table 3. The delays are parameterized by two values δ and ε. The first, δ, is the delay from time 0 to the time at which the pilot begins adjusting vertical acceleration to follow the first advisory. The second delay parameter, ε, is the delay from time 0 to the time at which the second issued advisory begins to be followed. Thus the first advisory is followed for ε -δ seconds and we require that ε > δ. The selections of delay parameters in Table 3 have ε values that are at least 1 second greater than δ to allow a period of 1 second or more of compliance with a first advisory. The right side of Table 3 gives the parameters governing the limits of ownship acceleration. The free acceleration, a d , as previously defined, is the maximum absolute acceleration of the pilot during delay or COC; it is swept between almost zero acceleration and g/2. (We used g/10 6 for almost zero to avoid divisions by zero in our conditions.) The second parameter, ∆a, the overcompliance acceleration, is the difference between the upper limit of acceleration under the advisory, a up , and the lower compliance limit, a lo . It is tied in each case to one half of the free acceleration a d . The delay parameter pairs are also tied together during each query, meaning that during the first query (δ, ε) = (0, 1) and for the second query (δ, ε) = (0, 2), and so on. All 16 combinations of delay pairs and acceleration pairs are tested against the total 648 billion cut-point combinations summarized in Table 2.

Counterexamples. Tables 4 and5 summarize the number of counterexamples (Def. 1) we found. The lower portions of the tables show the number of initial states tested that were not resolvable with any of the available safe or safeable actions. That is, for those unresolvable states, there are no available advisories that pass the conditions we formally proved. For the safe comparison, the checks we perform are limited to states in the ACAS X tables where COC is the previous advisory (about 196 billion states). In addition, the parameters ε and ∆a are not used in the safe conditions: ε is fixed to -1 as we assume that the pilot will follow the issued advisory forever; ∆a is not used as we assume that the vertical acceleration has only to respect a minimal rate (a lo ) to satisfy the advisory. Thus, only δ and a d vary. One can notice that taking into account the pilot delay in the formal We also observe, on the contrary, that increasing the free acceleration a d results in more counterexamples and more unresolvable encounters. This is a straightforward effect of our worst case analysis: if we allow g/2, say, as worst case vertical acceleration, then we have to consider that the pilot will actually accelerate at g/2 during the delay, which may be unrealistic. Overall, as shown in Table 4, we found billions of counterexamples to Corollary 1 (safe regions). Many were used to create test encounters and tested in the full system as a means of targeted stress testing. As alluded to earlier, the ACAS X system was able to resolve many of those by issuing subsequent advisories, which actually motivated the safeable extension we developed in this paper. Indeed, safeable counterexamples represent states where the advice given by ACAS X may not be correctable by subsequent advisories, although an alternative guaranteed safe sequence exists for our assumptions according to Lemma 6.

We can see from Table 5 that there are considerably fewer safeable counterexamples than safe ones, hundreds of millions instead of tens of billions. Theorem 5 (safeable regions) is designed to detect points of no return. As with safe regions, we see that the number of counterexamples tend to have an inverse relationship with pilot response delay although an exception to this trend occurs when delay is ex-actly 0. We believe this exception is caused by the fact that many states are resolvable when there is no pilot response delay, i.e., when the pilot responds immediately to the issued advice. Once a moderate response delay is assumed, there are many fewer resolvable initial states, resulting in fewer total counterexamples, albeit still a few hundred million. These safeable counterexamples are also being used to generate stressing short-time encounters that may be used for robustness testing.

Safety Analysis. The comparison of the system to safe condition D -1 expl (valid by Theorem 2) gave insight into possible improvements for ACAS X. Our analysis led to the identification of unexpected behavior in the ACAS X run 13 (i.e., version 13) lookup tables. In some cases, the ACAS X advisory seems to induce an NMAC, i.e., if the initial advisory is followed and not strengthened or reverted later, an NMAC will occur when it would not have occurred if the aircraft continued flying straight. A typical example, found during checking against Corollary 1 (safe regions) with δ = 0 and a d = g/2, is shown in Fig. 14. The ownship is flying from the left and the intruder from the right. The time 0 corresponds to the time of closest horizontal approach. As time progresses, the intruder flies towards the ownship and an NMAC happens near the time t = 0. The original path of the ownship does not lead to an NMAC. However, ACAS X issues a Do-Not-Climb advisory. If the pilot follows this advisory immediately and stops climbing, and if the initial advisory is not subsequently strengthened or reversed, an NMAC will occur.

In other cases of counterexamples to Corollary 1 (safe regions), the advisory does not seem to have any benefit. In those cases, flying at the vertical rates disallowed by the advisory would actually avoid NMAC, while not all allowed vertical rates of the advisory are safe. Some safe counterexamples are tolerated, as ACAS X tries to minimize alerting the pilot unless it has to do so; for these cases, ACAS X will issue or strengthen an advisory later to avoid issuing a disruptive alert immediately. Additionally, the assumption of straight vertical flight is not always valid. E.g., aircraft may actually be more likely to level-off than continue at high vertical rates in some cases. The particular unexpected behavior shown in Fig. 14 was independently identified by the ACAS X team using simulationbased testing, and is being addressed in a subsequent revision of the system. Safeable Analysis. In Fig. 15, we see an automatically discovered safeable counterexample. The pilot is assumed to start complying with the initially issued advisory at 5 seconds and will only begin complying with a potential subsequent advisory after 7 seconds from the initial time (the first advisory will thus be followed for 2 seconds). For this state, the ACAS X tables issue the advisory MDES, maintain descent. The upper panel shows the most extreme upper and lower paths that a subsequent advisory can restrict the ownship's motion to. Neither of these can avoid NMAC with the intruder. This is a relatively close range, slow closing encounter, as the initial horizontal separation is 1,500 feet and horizontal relative closing speed is only 90 feet/second. Both aircraft begin descending at moderate rates, offset vertically by 300 feet. The problem occurs because the most extreme descend advisory available has a rate of only 2500 feet/minute and with the ownship already descending at 2000 feet/minute the increase in descent rate cannot avoid the intruder. In this slow closing geometry, the two aircraft will be in horizontal conflict range for an extended period, which at this geometry lasts for 7 seconds starting at t = -3.5 to t = 3.5 seconds. In this case, Lemma 6 tells us that safeable actions include Do-Not-Descend and Climb-1500. The lower panel of Fig. 15 shows that if the ownship were, instead, told to climb at the maximum rates allowed by a sequence of upsense advisories, this situation would have been resolved, and so is indeed a counterexample.

The smaller number of safeable counterexamples are of special interest to system verification, as they are situations that cannot even be corrected by subsequent advisories. To aid in robustness testing and tuning of the actual system, we have created a set of short-time encounters based on the counterexamples found using the safeable analysis and are sharing these encounters with the ACAS X designers.

Overall, we have begun analyzing ACAS X using our theorem and are identifying numerous valuable outcomes. These results either help us characterize tradeoffs being made or help us identify undesirable behaviors in the system. As one of our next steps, we aim to prove that ACAS X gives safe advice for continuous regions of the state space. When comparisons are extended to check contiguous regions of the state space, our approach will have the potential for a complete analysis of the system over all potential encounter configurations, thereby reducing vulnerability to the sampling of encounter scenarios.

Related Work

Kochenderfer and Chryssanthacopoulos [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF] describe the design of the ACAS X lookup-tables. Their principled approach, based on optimizing an MDP, guarantees the selection of optimal advisories according to a cost model. The state space and dynamics are discretized. Their notion of optimality depends on costs assigned to various events.

Holland et al. [START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF] and Chludzinski [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF] simulate large numbers of encounters, including tracks from recorded flight data, to evaluate the performance of ACAS X. These simulations account for high-fidelity details of an encounter, but they only cover a finite set of the continuous state space with no formal guarantees.

Von Essen and Giannakopoulou [START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF] use probabilistic modelchecking to analyze an MDP based on [START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF]. They investigate the probability of several undesirable events occurring. Because they ostensibly analyze an MDP, their work inherits many of the assumptions of ACAS X, including errors due to discretized dynamics. Their analysis depends heavily on the MDP considered and thus needs to be redone on every version of ACAS X.

Lygeros and Lynch [START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF] use hybrid techniques to formally verify the TCAS conflict resolution algorithms. They assume-rather than prove-that TCAS ends up in a state where one aircraft has a climbing advisory and the other a descending advisory. They then prove (by hand) a lower bound on the vertical separation of both aircraft at the point of closest approach. In contrast, we do prove as opposed to assume that and when advisories are safe.

Tomlin et al. [START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF], Platzer and Clarke [START_REF] Platzer | Formal verification of curved flight collision avoidance maneuvers: A case study[END_REF], Loos et al. [START_REF] Loos | Formal verification of distributed aircraft controllers[END_REF] and Ghorbal et al. [START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF] use hybrid systems approaches to design safe horizontal maneuvers for collision avoidance. Dowek et al. [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF] and Galdino et al. [START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF] describe and verify in the PVS theorem prover a collision avoidance system of their design called KB3D.

Overall, our approach is different from previous complementary work in that:

unlike [START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF][START_REF] Kochenderfer | Robust airborne collision avoidance through dynamic programming[END_REF], we rely on an independent model from the one used to design ACAS X; unlike [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF][START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF][START_REF] Ghorbal | Hybrid theorem proving of aerospace systems: Applications and challenges[END_REF][START_REF] Loos | Formal verification of distributed aircraft controllers[END_REF][START_REF] Platzer | Formal verification of curved flight collision avoidance maneuvers: A case study[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF] we analyze an independent industrial system and not a safe-by-design system; unlike [START_REF] Dowek | Provably safe coordinated strategy for distributed conflict resolution[END_REF][START_REF] Von Essen | Analyzing the next generation airborne collision avoidance system[END_REF][START_REF] Galdino | Formal verification of an optimal air traffic conflict resolution and recovery algorithm[END_REF] our analysis uses realistic, continuous dynamics; unlike [START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF] we provide universal safe regions that can be reused for new versions of ACAS X or new systems; unlike [START_REF] Chludzinski | Evaluation of TCAS II version 7.1 using the FAA fast-time encounter generator model[END_REF][START_REF] Holland | Optimizing the next generation collision avoidance system for safe, suitable, and acceptable operational performance[END_REF][START_REF] Kochenderfer | Correlated encounter model for cooperative aircraft in the national airspace system version 1[END_REF][START_REF] Lygeros | On the formal verification of the TCAS conflict resolution algorithms[END_REF][START_REF] Tomlin | Conflict resolution for air traffic management: A study in multiagent hybrid systems[END_REF], we provide mechanized rigorous proofs of correctness of our model.

Conclusion and Future Work

We developed a general strategy for analyzing the safety of complicated, real-world aircraft collision avoidance systems, and applied it to ACAS X. Our strategy identifies safe regions where an advisory is proved to always keep the aircraft clear of NMAC, under some assumptions. We identified states where ACAS X is provably safe, and delivered others showing unexpected behaviors back to the ACAS X development team. The identified safe regions are independent from the version of ACAS X and can thus be reused for future versions. In future work, we plan to extend our hybrid model to account for curved trajectories of both aircraft as well as vertical acceleration of the intruder.

Fig. 2

 2 Fig. 2 An encounter between ownship O and intruder I, with NMAC puck in gray of horizontal radius rp and vertical radius hp

Fig. 4

 4 Fig. 4 Nominal trajectory of the ownship (red) and safe region for the intruder (green), delayed response

a d 2 t 2

 2 + vt . After the delay, i.e., after time δ, the nominal trajectory N d is the same as a nominal trajectory N from Sect. 3, translated by time δ and by its position at time δ given by r d = r n (δ) and h d = h n (δ), and starting with vertical velocity v d = v -a d δ. As in Sect. 3.3, we can now express the implicit formulation of the safe region:

  Fig. 3 capturing the implicit safe region of Sect. 3.3 translated by time max(0, d), vertical height h d , and starting at vertical speed v d . It is proved correct in KeYmaera.

Fig. 6 Fig. 7

 67 Fig. 6 Nominal trajectory of the ownship (red) and upper safe region for the intruder (green), immediate response

  Constructing the explicit safety condition for the upper bound U -1 expl follows similar motivation and methods as in Sect. 3.4, but, instead of distinguishing cases upon the target vertical ve-locity v lo , it distinguishes them upon the modified upper target vertical velocity w max(wv up , wv).

5 t := 0; 6 (

 56 3 [( ( (w := -1 ∪ w := 1); v lo := * ; v up := * ; 4 ?C ε impl (r, h, v, w, v lo , v up ); advisory := (w, v lo , v up ) ); a := * ;

6 advisory 7 t := 0; 8 (

 678 := (w, v lo , v up ) ); a := * ;

Fig. 13

 13 Fig. 13 Top view of the two reference frames

Fig. 14

 14 Fig. 14 Safe Counterexample. Original ownship path (cyan) and intruder path (red) vs. ownship responding to a do-not-climb (DNC) advisory issued by the ACAS X tables in starting state: r = 4,000 ft, rv = 200 ft/s, θv = 180 • , h = 600 ft, v = 1,980 ft/min, v I = -1,500 ft/min.Time is shown counting from -20 s to time 0; the time of closest horizontal approach. The 2D projection of the NMAC cylinder is shown centered around the ownship as a dashed rectangle; the intruder intersecting with the NMAC region is shown by a red circle.

Fig. 15

 15 Fig. 15 Safeable counterexample, where "delay 1" (δ) = 5 s, "delay 2" (ε) = 7 s, a d = g/10 6 , and ∆a = 0. Action issued is "maintain" for the initial state r = 1, 500 ft, rv = 90 ft/s, θv = 2.88 rad, h = 300 ft, v = -33.33 ft/s, v I = -50 ft/s, previous advisory = None. Plots show absolute altitude of ownship vs. time and intruder vs. negative time; ownship travels left to right and the intruder right to left. Time is shown counting from -16 s to time 0; the time of closest horizontal approach. The delay times are shown in vertical dashed lines. The 2D projection of the NMAC cylinder is shown centered around the ownship as a dashed rectangle. When the intruder intersects with the NMAC region, it is shown by a red circle, and when the intruder misses the NMAC region it is shown as a red dot.

Table 1

 1 ACAS X advisories and their modeling variables

	ACAS X Specification [13]	Our model
	Vertical Rate Range	Strength Delay	Sign	Advisory

  impl (r, h, v, w, vup) ≡ ∀tn.∀rn.∀hn. rn = rvtn ∧ Aup(t, hn, v, w, vup) → (|r

	Implicit formulation
	Aup(t, hn, v, w, vup) ≡	0 ≤ tn <	max(0, w(vup -v)) aup	∧ hn =	waup 2	tn 2 + vtn
	∨	tn ≥	max(0, w(vup -v)) aup	∧ hn =	w max(wvup, wv) aup	tn -	wmax(0, w(vup -v)) 2 2aup
	U -1

  is drawn by either the top side, the top left hand corner or the top right hand corner of the puck. This explicit formulation is a little bit less intuitive than the formulation for the lower safe region of Sect. 3.4 because the different cases overlap. It can nonetheless be described by a set of equations (where cases 10 to 13 are similar to cases 10 to 13 of Fig.8): 0. positions left of the puck's initial position (r < -r p ) are in the safe region; 10. up to r = r p , the boundary is horizontal along the top side of the puck at its initial position; therefore for -r p ≤ r ≤ r p , the position (r, h) is in the safe region if and only if h > h p ; 11. then the boundary can follow the top right-hand corner of the puck as it is going down the parabola of Eq.

	(r, h) is safe if and only if h >	rv(vup-v) aup aup 2rv 2 (r + r p ) 2 + v , the position rv (r +
	r p ) + h p ; note that this case can overlap with case 10;
	13. finally the boundary follows the top left-hand corner of
	the puck as it is going up the straight line of Eq. (6)(a);
	therefore for -r p + is in the safe region if and only if h > rv(vup-v) ≤ r, the position (r, h) aup vup rv

[START_REF]Algorithm design description for the threat resolution module of ACAS X[END_REF]

(a); therefore for r p < r ≤ r p + rv(vup-v) aup

, the position (r, h) is safe if and only if h > aup 2rv 2 (r-r p ) 2 + v rv (r-r p )+h p ; 12. the boundary can also follow the top left-hand corner of the puck as it is going up the parabola of Eq. (

6

)(a); therefore for -r p ≤ r < -r p +

Table 2

 2 Discrete parameter ranges and number of cut-points specified by ACAS X run 13 and checked during comparison

	parameter		samples	range of values
	relative alt. h (ft)	45	[-8000, -4000, -3600, -3200, -2800, -2400, -2000, . . . , -100, -50, 0, 50, . . . , 4000, 8000]
	ownship alt. rate v (ft/s)	25	[-166.7, -83.3, -75.0, -66.7, -58.3, -50, . . . , -16.7, -8.3, -4.2, 0, 4.2, . . . , 83.3, 166.7]
	intruder alt. rate v I (ft/s)	25	[-166.7, -83.3, -75.0, -66.7, -58.3, -50, . . . , -16.7, -8.3, -4.2, 0, 4.2, . . . , 83.3, 166.7]
	previous advisory	33	{ NONE-NONE, DNC2000-NONE, DNC2000-DNC2000, . . . , SCL2500-NONE, SCL2500-SCL2500 }
	range r (ft)		101	[0, 50, 100, 150, 200, 250, 300, . . . , 1000, 1500, 2000, . . . , 39500, 40000, 100000, 200000]
	relative velocity rv (ft/s)	187	[0, 10, 20, 30, 40, 50, 60, 70, 80, 90 . . . , 1700, 1750, 1800, . . . , 2350, 2400, 2450, 2500]
	velocity angle θv (deg)	37	[0, 5, 10, 15, 20, 25, 30, 35, 40, 45, . . . , 145, 150, 155, 160, 165, 170, 175, 180]
	δ (seconds)	ε (seconds)	a d	∆a = aup -a lo
	0	1	g/10 6	0
	1	2	g/6	g/12
	3	5	g/3	g/6
	5	7	g/2	g/4

Table 3

 3 Delay and Acceleration Parameters Swept During Logic Comparison. Delay pairs (left) are tied together, while acceleration pairs (right) are tied. The 16 combinations of these pairs are tested.Approach. To perform the comparison we use a 10-node cluster, each with 48 cores and 128 GB RAM. Checks for the relevant conditions are implemented in Julia 2 and run on the 648 billion cut-point combinations in parallel, taking approximately 8 days. We first define what we mean by a counterexample.

	Definition 1 (Counterexample) We say that a state is a coun-
	terexample for the safe (resp. safeable) conditions if the ad-
	visory given by the ACAS X logic tables for that state vio-
	lates L -1 expl given in Fig. 3 (resp. C expl safeable(ε)

Table 4

 4 Number of Safe counterexamples (top) and number of unresolvable states (bottom) for each delay and acceleration parameter set

	Safe Counterexamples
	(in billions)	delay (δ, ε) in seconds
	acceleration (a d , ∆a)	(0, 1) (1, 2) (3, 5) (5, 7)
	(g/10 6 , 0)	15.38 15.05 14.85 14.79
	(g/6, g/12)	15.40 15.03 14.87 14.88
	(g/3, g/6)	15.43 15.02 14.95 15.14
	(g/2, g/4)	15.45 15.01 15.18 15.33
	Unresolvable States
	(in billions)	delay (δ, ε) in seconds
	acceleration (a d , ∆a)	(0, 1) (1, 2) (3, 5) (5, 7)
	(g/10 6 , 0)	10.42 10.64 10.84 10.96
	(g/6, g/12)	10.42 10.75 11.16 11.51
	(g/3, g/6)	10.42 10.88 11.59 12.36
	(g/2, g/4)	10.42 11.04 12.13 13.46

Table 5

 5 Number of Safeable counterexamples (top) and unresolvable states (bottom) for each delay and acceleration parameter set model reduces the number of counterexamples. This may seem at first counterintuitive as one expects less unsafe advisories if the pilot responds immediately. However, given that the previous advisory is a COC, the ACAS X tables are designed to not necessarily issue a disruptive advisory right away and will rather either issue a preventive advisory (such as DNC or DND) or simply a MAINTAIN before actually strengthening those advisories in the future if needed. Those first advisories may indeed violate the safe conditions although the system is able to resolve the potential encounters.

	Safeable
	Counterexamples
	(in millions)	delay (δ, ε) in seconds
	acceleration (a d , ∆a)	(0, 1) (1, 2) (3, 5) (5, 7)
	(g/10 6 , 0)	266.3	99.7	39.2	31.6
	(g/6, g/12)	310.0 117.2 101.4 164.9
	(g/3, g/6)	353.2 138.6 277.7 544.7
	(g/2, g/4)	398.9 163.6 668.8 898.7
	Unresolvable States
	(in billions)	delay (δ, ε) in seconds
	acceleration (a d , ∆a)	(0, 1) (1, 2) (3, 5) (5, 7)
	(g/10 6 , 0)	11.03 11.27 11.51 11.64
	(g/6, g/12)	11.03 11.40 11.85 12.23
	(g/3, g/6)	11.03 11.54 12.30 13.09
	(g/2, g/4)	11.03 11.71 12.86 14.23

We use units most common in the aerospace community, even though they are not part of the international system, including nauti-

http://julialang.org.

Acknowledgments. This research was conducted under the sponsorship of the Federal Aviation Administration Traffic Alert & Collision Avoidance System (TCAS) Program Office (PO) AJM-233 under contract number DTFAWA-11-C-00074. Additionally, support for the basic verification technology used as a foundation for this research was provided by the National Science Foundation under NSF CAREER Award CNS-1054246.

The authors would like to warmly thank Neal Suchy for his lead of the ACAS X project and support of this work, as well as Nathan Fulton, Ran Ji and Jan-David Quesel for their support of the KeYmaera tool. The authors would also like to thank Jeff Brush, Barbara Chludzinski, Dane Fichter, Jessica Holland, Robert Klaus, Barbara Kobzik-Juul, Mykel Kochenderfer, Ted Londner, Sarah Loos, Jessica Lopez, Ed Morehouse, Wes Olson, Michael Owen, Anshu Saksena, Joshua Silbermann, and the ACAS X development team for interesting discussions and remarks.

Implicit formulation

L ε impl (r, h, v, w, v lo ) ≡ ∀tn.∀rn.∀hn.

12 (r, v, w, vup) ≡ case -1 12 (r, v, w, vup) ∧ (ε < 0 ∨ r ≤ -rp + rvε)