Automating Geometric Proofs of Collision Avoidance with Active Corners

Consider the planar side-view of an airplane flying, initially descending at constant velocity and then ascending with constant velocity. For simplicity, assume the aircraft has infinite acceleration. In this example, we represent the bounds of the aircraft as an axis-aligned rectangle with width $2w$ and height $2h$ that moves in the $(x,y)$ plane. The airplane begins at the origin and moves in the plane with piecewise trajectory $\mathcal{T}$:

Suppose the rectangle translates with its center moving along this piecewise trajectory. Additionally, assume there is a point obstacle at $(x_{O},y_{O})$ to be avoided; that is, the rectangle never intersects the obstacle. Then we can state an quantified (or implicit) formulation of obstacle avoidance:

The implicit formulation of the safe region (3) straightforwardly represents a safety property of obstacle avoidance - if an object moving with its center fixed along the nominal trajectory $\mathcal{T}$ is far enough away (either width $w$ in the $x$-axis or height $h$ in the $y$-axis) from a point obstacle at $(x_{O},y_{O})$, it is safe. Here we use safe region to mean the set of all obstacle locations for which collision is avoided.

The need for a quantifier-free equivalent of Equation (3) motivates an explicit formulation of the safe region for the obstacle. The goal of this work is to automate the generation of such a formulation. We compute the reachable set of the object as it moves along a trajectory in order to compute the complement of the safe region: the unsafe region. We can express the unsafe region (the set of all locations for which an obstacle will collide with the object as it moves along a given trajectory) directly as a union of regions in the plane, each defined (in this case) by an intersection of linear inequalities bounding the region, plotted in Figure 1. The inequalities are presented in Appendix A.

In this work, we define the safe region as the set of obstacle locations where, given a polygon’s trajectory, a collision will not occur. Correspondingly, the unsafe region is called that because it will be unsafe if an obstacle invades that area. As such, the unsafe region corresponds to the reachable set of the polygon as it moves along a trajectory. We can define a quantified representation of the safe region: the implicit formulation from (1). We also use the term explicit formulation in this work; we use that to mean an equivalent to the implicit formulation, but without quantifiers like $\forall$ and $\exists$. Our method applies to convex polygons; concave polygons and circles are not within the scope of this work. In this paper, we discuss polygons with central symmetry for ease of exposition, though the method straightforwardly extends to irregular and asymmetric convex polygons (Appendix B).

We consider two-dimensional planar trajectories defined piecewise, with each piece a function $y=f(x)$ or $x=f(y)$ and $f$ a $C^{1}$ function (differentiable and having a continuous derivative). Trajectories must have a finite number of these $C^{1}$ pieces. The pieces themselves need not be continuous, though the applications we study do include continuous piecewise trajectories. The subdomains for the piecewise trajectory must be non-overlapping and exhaustive, meaning their union should cover the entire domain of the trajectory. Polygons move along the trajectory without rotating. Since the polygons translate along the trajectory, there is a constant vector offset $\begin{bmatrix}\Delta x_{i}\\ \Delta y_{i}\end{bmatrix}$ from the center to the $i$-th vertex, and there are $n$ vertices for an $n$-sided polygon. Thus, the trajectory for vertex $i$ is $y-\Delta y_{i}=f(x-\Delta x_{i})$ or $x-\Delta x_{i}=f(y-\Delta y_{i})$. We consider the trajectories of all vertices of the polygon in an attempt to bound its motion and compute the reachable set of the object as it moves along the trajectory.

Throughout this section we consider a trajectory of the form $y=f(x)$; the case for $x=f(y)$ is symmetric. The boundaries of the safe region are typically formed by the trajectories of a pair of opposite corners of the vehicle (Figure 2) – we call this pair of corners active corners. We choose the active corners to represent the outermost extent of the object along the trajectory; as such, their motion bounds the safe region. Which corners are active depends on the slope of the trajectory (which can be computed from the derivative of $f$) and the shape of the convex object. A corner $v_{i}$ is active when the slope $\theta$ of the trajectory is between the slopes of the sides adjacent to $v_{i}$; when a corner is active, its opposite corner is also active based on the symmetry of the polygon. More precisely, if we number the corners $v_{1}$ through $v_{n}$ counter-clockwise (with $v_{n+1}=v_{0}$ and $v_{-1}=v_{n}$), corner $v_{i}$ is active if and only if the slope $\theta$ of the trajectory is in the angle interval $[\angle\overrightarrow{v_{i-1}v_{i}},\angle\overrightarrow{v_{i}v_{i+1}}]$, or symmetrically in the angle interval $[\angle\overrightarrow{v_{i+1}v_{i}},\angle\overrightarrow{v_{i}v_{i-1}}]$. Because the direction of the trajectory is inconsequential for our purpose, $\theta$ is modulo $180{}^{\circ}$.

For example, on the hexagon of Figure 2, $v_{1}$ and $v_{4}$ are active when $\theta\in[0{}^{\circ},60{}^{\circ}]\cup[180{}^{\circ},240{}^{\circ}]$; $v_{2}$ and $v_{5}$ are active when $\theta\in[60{}^{\circ},120{}^{\circ}]\cup[240{}^{\circ},300{}^{\circ}]$; and $v_{3}$ and $v_{6}$ are active when $\theta\in[120{}^{\circ},180{}^{\circ}]\cup[300{}^{\circ},360{}^{\circ}]$. At transition points (where the active corners change), the boundary of the safe region may not follow an active corner. We detail what happens then in Section III-C.

Given an obstacle at point $(x_{O},y_{O})$, we can check if it is inside the unsafe region (or reachable set) in a computationally efficient fashion. If an obstacle lies outside the unsafe region, it would be either above both corner-trajectories or below both corner-trajectories for whichever corners are active. We can express the location of the obstacle with respect to a corner-trajectory in a single equation by considering the value of $y_{O}-f(x_{O}-\Delta x_{i})-\Delta y_{i}$ for active corner (vertex) $v_{i}$. This term will be positive for both vertices $v_{i},v_{j}$ if the obstacle is above both corner-trajectories, and similarly negative if the obstacle is below both. Therefore, any point $(x_{O},y_{O})$ in the safe region has a positive value for the product of the two expressions above, and any point in the unsafe region has a negative or zero value for this product. This yields the following test to check if an object lies in (part of) the unsafe region:

where $\Delta x_{i},\Delta y_{i},\Delta x_{j},\Delta y_{j}$ are the (constant) offsets from the center of the polygon to the active corners (vertices) $v_{i},v_{j}$.

When implementing this algorithm, the trajectories of all other vertices lie within the trajectories of the active corners, so to check whether an obstacle lies in the portion of the unsafe region defined by the active corners, it suffices to check over all pairs of vertices $(v_{i},v_{j})$ with $i,j\in\{1,2,...n\}$. If the test in (4) indicates that an object lies within the unsafe region, trajectory $y=f(x)$ or $x=f(y)$ is clearly unsafe.

It turns out that using only active corners would yield an underestimate of the reachable set, which would be unsound for verifying safety. Figure 3 illustrates why: the white area bounded by the trajectories of the corners does not contain the red “notch”, even though a collision would occur with an obstacle in this notch. Therefore, if the test in (4) yields a value $>0$, the advisory is not necessarily safe; we additionally check safety at all transition points $(x_{T},y_{T})$ to see whether the obstacle at $(x_{O},y_{O})$ lies within the polygon centered at $(x_{T},y_{T})$. Recall that transition points are defined as points on the trajectory where the active corners switch. In the full test for safety (Equation 6), this check is represented as in_polygon() and can leverage one of many point-in-polygon implementations, which generally run in linear time on the order of number of vertices. As the slope of the function may change at the boundary between piecewise subfunctions, we also add a notch check at each subdomain boundary.

In order to account for piecewise functions, we modify our method in two ways to avoid using a subfunction outside the subdomain over which it holds. The first is a modification to hold subfunctions constant outside of the subdomain over which they’re defined; and the second is an additional boolean clause to the safety test in (4) so it only applies over a valid subdomain. In this case, the subdomain is an interval $[x_{Ti},x_{T(i+1)}]$, where $x_{Ti},x_{T(i+1)}$ may be piecewise boundaries or transition points. Because of this, there may be many subdomains for a single piecewise case in which there happen to be many transition points.

First, we define a function $g(x)$ (or $g(y)$ symmetrically) that holds the value of each subfunction outside of its subdomain $[x_{Ti},x_{T(i+1)}]$. The function $g(\cdot)$ is used in place of $f(\cdot)$ in (4) above. Let $y_{Ti}=f(x_{Ti})$.

Additionally, we add a clause to ensure the modified subfunction $g(\cdot)$ is only used over the correct subdomain. First, we check $x_{Ti}-w<x_{O}<x_{T(i+1)}+w$, where $w$ is the half-width of the object. We also construct a line between the two active corners of the object in each of the two piecewise boundary locations $\big{(}x_{Ti},y_{Ti}\big{)}$ and $\big{(}x_{T(i+1)},y_{T(i+1)}\big{)}$ and check $(x_{O},y_{O})$ is between the two lines. This way, we ensure the test for being unsafe holds only for the region on which each subfunction applies. Figure 4 illustrates the function $g(\cdot)$ and the additional subdomain-related clauses.

This leads to a generic quantifier-free explicit formulation to test whether an obstacle is in the safe region, where $\{(x_{T},y_{T})_{i}\}$ represents the set of all transition and boundary points on the trajectory between piecewise subdomains. Our algorithm yields a test for whether an obstacle is unsafe; negating the boolean formula or its result allows testing whether an obstacle lies in the safe region.

Equation (6) is color-coded in correspondence with Figure 5. The first, third, and fourth lines ensure the test applies only over the correct piecewise domain and are in green; the second line checks the obstacle is between the active corners and is in blue; the fifth line is in orange and checks for the notch at transition points and piecewise subdomain boundaries. For ease of presentation, we have focused on convex, centrally-symmetric objects and point-mass obstacles. However, our method extends to obstacles with area, to asymmetric, irregular polygons, and even non-convex objects, as detailed in Appendix B.

Consider a segment of the motion along trajectory $y=f(x)$ or $x=f(y)$ in which no active corner switches or piecewise trajectory segment switches occur. We can arbitrarily rotate this segment of motion and the proof will hold, since the object translates along the trajectory without rotation. Assume, then, that a rotation is made by an angle $\theta$ such that the active corners are oriented along a vertical line. This rotation is an invertible transformation, so the logic of this proof holds through the entire trajectory. Because of this coordinate rotation, we consider only trajectories $y=f(x)$ for the proof; any trajectory $x=f(y)$ can be rotated into the form $y=f(x)$ invertibly, so our results hold for these forms as well. Let $v_{i},v_{j}$ denote the active corners for this segment, with corresponding offsets $\Delta x_{i},\Delta y_{i},\Delta x_{j},\Delta y_{j}$ in the rotated coordinate system.

Since no active corner switch occurs, then we know the slope of function $y=f(x)$ is limited by the shape of the polygon itself – let these bounds be $\pm m$, with $m$ representing the slope of the relevant sides of the polygon. Because the polygon is symmetric, the lower bound on slope is the negative of the upper bound (Figure 7). This proof is presented considering regular, symmetric polygons for simplicity, but extends to asymmetric polygons as discussed in Appendix B. To prove the soundness of our method, we must prove that all obstacles shown safe using our method ($\text{safe}_{\text{expl}}$) are also safe using the input implicit formulation ($\text{safe}_{\text{impl}}$). To prove $\text{safe}_{\text{expl}}\implies\text{safe}_{\text{impl}}$, we prove the contrapositive $\text{unsafe}_{\text{impl}}\implies\text{unsafe}_{\text{expl}}$.

Specifically, $\text{unsafe}_{\text{impl}}$ means that an obstacle at $(x_{O},y_{O})$ is inside a polygon centered at some coordinates $(x,y)$; $\text{unsafe}_{\text{expl}}$ means that the below holds from (4):

This proof has three sections: one holds for the majority of the trajectory segment, one for the beginning of the segment, and one of the end of the segment. The beginning- and end-of-segment proofs follow the form of the main proof but consider fixed polygons at the trajectory segment endpoints and are included in Appendix C for space reasons.

Consider a (symmetric) polygon $P$, with half-height $h$ and half-width $w$, centered at $(x_{C},y_{C})$, where $y_{C}=f(x_{C})$. Let $(x_{\text{int}},y_{\text{int}})$ be a point inside or on the edges of $P$. We prove that interior point $(x_{\text{int}},y_{\text{int}})$ lies between the active corners of an identical polygon $\mkern 1.5mu\overline{\mkern-1.5muP\mkern-1.5mu}\mkern 1.5mu$ located at $(x_{\text{int}},f(x_{\text{int}}))$. We do this by bounding three terms: 1) $f(x_{\text{int}})$, 2) $y_{\text{int}}$, and 3) the active corners of $\mkern 1.5mu\overline{\mkern-1.5muP\mkern-1.5mu}\mkern 1.5mu$ to prove that $y_{\text{int}}$ lies between them.

First, we bound $f(x_{\text{int}})$ (the center of $\mkern 1.5mu\overline{\mkern-1.5muP\mkern-1.5mu}\mkern 1.5mu$). Let $x_{\text{int}}=x_{C}+\Delta x$, for $\Delta x\in\left[-w,w\right]$. Let $f(x_{\text{int}})=f(x_{C}+\Delta x)=y_{C}+\Delta y$, for some $\Delta y$ which we will bound. The slope of the trajectory $\frac{dy}{dx}$ is bounded by $(-m,m)$, because this proof considers a segment of motion with no changes in active corner. Hence $\Delta y$ is bounded proportionally to $\Delta x$, with $\Delta y\in\left(-|m\Delta x|,|m\Delta x|\right)$. Therefore, $f(x_{\text{int}})\in\left(y_{C}-|m\Delta x|,y_{C}+|m\Delta x|\right)$. Our proof proceeds assuming $\Delta x\neq 0$, since if $\Delta x=0,x_{\text{int}}$ will lie on the vertical centerline of $P$. In that case, it is trivial to show $x_{\text{int}}$ lies between the active corners.

Now, we bound $y_{\text{int}}$. Recall $x_{\text{int}}=x_{C}+\Delta x$, for $\Delta x\in\left[-w,w\right]$. Given that the slopes of the sides on the top and bottom of $P$ are $\pm m$, we assert that any $(x_{\text{int}},y_{\text{int}})$ with $x_{\text{int}}=x_{C}+\Delta x$ has a corresponding $\Delta y_{\text{int}}\in\big{[}-h+|m\Delta x|,h-|m\Delta x|\big{]}$. This is illustrated in Figure 7 with a hexagon, but it generalizes to any symmetric convex polygon. Given this, we can bound the $x$ and $y$ interior coordinates as below:

Finally, we show interior point y-coordinate $y_{\text{int}}$ lies within the active corners of $\mkern 1.5mu\overline{\mkern-1.5muP\mkern-1.5mu}\mkern 1.5mu$. Because we consider a rotated coordinate frame such that the active corners are oriented along the vertical axis, the top and bottom active corners are located at $(\mkern 1.5mu\overline{\mkern-1.5mux_{\text{top}}\mkern-1.5mu}\mkern 1.5mu,\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu)=(x_{\text{int}},f(x_{\text{int}})+h)$ and $(\mkern 1.5mu\overline{\mkern-1.5mux_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu,\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu)=(x_{\text{int}},f(x_{\text{int}})-h)$, respectively. The bounds on $\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu$ and $\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu$ are given by the following:

Then $y_{\text{int}}\leq y_{C}-|m\Delta x|+h<\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu$ and $y_{\text{int}}\geq y_{C}+|m\Delta x|-h>\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu$.

The top active corner trajectory is given by $f_{\text{top}}(x)=f(x)+h$ and the bottom active corner trajectory is given by $f_{\text{bot}}(x)=f(x)-h$. By definition, $f_{\text{top}}(x_{\text{int}})=\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu$ and $f_{\text{bot}}(x_{\text{int}})=\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu$, or equivalently, $\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu-f_{\text{top}}(x_{\text{int}})=0$ and $\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu-f_{\text{bot}}(x_{\text{int}})=0$. Since $y_{\text{int}}<\mkern 1.5mu\overline{\mkern-1.5muy_{\text{top}}\mkern-1.5mu}\mkern 1.5mu$ and $y_{\text{int}}>\mkern 1.5mu\overline{\mkern-1.5muy_{\text{bot}}\mkern-1.5mu}\mkern 1.5mu$,

By multiplying the equations in (9), we get

This is equivalent test for whether an object lies in the unsafe region from (4). Therefore we have shown that for all $(x_{C},y_{C})$ points satisfying $y_{C}=f(x_{C})$, all points $(x_{\text{int}},y_{\text{int}})$ inside and on the boundary of a polygon centered at $(x_{C},y_{C})$ also have $(f_{\text{top}}(x_{\text{int}})-y_{\text{int}})\cdot(f_{\text{bot}}(x_{\text{int}})-y_{\text{int}})\leq 0$. These are exactly the definitions of $\text{unsafe}_{\text{impl}}$ and $\text{unsafe}_{\text{expl}}$ from IV-A earlier. Therefore, we have shown $\text{unsafe}_{\text{impl}}\implies\text{unsafe}_{\text{expl}}$ and the contrapositive $\text{safe}_{\text{expl}}\implies\text{safe}_{\text{impl}}$ holds as well.

A collision avoidance system intended to prevent near mid-air collisions, ACAS X, was verified in [21]. The KeYmaera X proof presented in [21] required a significant amount of human interaction (on the order of hundreds of hours), while the method presented in this paper generates an explicit formulation from the trajectory fully automatically. ACAS X prevents collisions between aircraft by issuing advisories (control commands) to one aircraft, the ownship. The bounds of aircraft in this work are shaped like hockey pucks (cylinders wider than they are tall) of a radius $r_{p}$ and half-height $h_{p}$. From a side perspective of an encounter between aircraft, the bounds are rectangular. In [21], verification was performed in a side-view perspective, assuming two aircraft approach each other in a vertically-oriented planar slice of three dimensions. A careful choice of reference frame can reduce a three-dimensional encounter between aircraft into a two-dimensional system, by modeling the encounter as a 1-dimensional vertical encounter and the distance of a horizontal encounter [21, Section 6].

To simplify calculations, [21] used the relative horizontal speed $r_{v}$ of the two aircraft and assumed it constant; the vertical velocity of the oncoming aircraft $\dot{h}$ is also assumed constant. Advisories consist of climb and descent speed advisories, yielding ownship trajectories that are piecewise combinations of parabolas and straight lines. One example trajectory is below in (11), which assumes the advisory issued is for the ownship to climb at a rate $\dot{h}_{f}$ greater than its current vertical velocity $\dot{h}_{0}$. $(r_{t},h_{t})$ are the $(x,y)$ coordinates for trajectory $\mathcal{T}$ in this example, and $a_{r}$ is the acceleration.

The implicit formulation of the safe region is below, for an oncoming aircraft at relative coordinates $r_{O},h_{O}$.

In [21], the authors eliminate the parametrization over $t$, which yields an initial parabolic section and then straight-line motion after. We use this $t$-free trajectory to compute the unsafe region, which is displayed in Figure 9. A boolean formulation of the unsafe region is in Appendix D-B.

Turning maneuvers for unmanned aerial vehicles (UAVs) have been verified as safe in [1], where the UAV was represented as a circular safety buffer around a point object fixed along the trajectory. The KeYmaera X proof presented in [1] required a significant amount of human interaction (on the order of hundreds of hours); in contrast, the method presented in this paper generates an explicit formulation from the trajectory fully automatically. This work represents motion in a two-dimension plane viewed top-down, with the buffer “puck” taking the form of a circle. The turning maneuver trajectory moves along a circular arc then in a straight line:

With a circular safety buffer of radius $r_{p}$, the implicit formulation ensures for all points along the trajectory, the obstacle $(x_{O},y_{O})$ is at least $r_{p}$ away.

Note that our method does not support circular objects, only polygons, so we overapproximate the circular safety buffer as a regular hexagon inscribing a circle. This approximation allows a valid overapproximation of the unsafe region, since the hexagon contains the original circle in [1]. Note that the approximation of a circle can be made arbitrarily precise by increasing the number of sides of a polygon used. A plot of the unsafe region is in Figure 10 and a boolean formulation of the unsafe region is in Appendix D-C.

This section presents a comparison of our method to quantifier elimination via cylindrical algebraic decomposition (CAD) in a variety of cases, from fully numeric to fully symbolic [12]. Results were generated using a 2017 iMac Pro workstation with 128  GB of RAM, with CAD results using Mathematica’s Resolve implementation. A table of results is shown in Table I. We use the examples from VI-A (ACAS X) and VI-B (UAV). The Dubins path example is inspired by common path planners and takes the form of two circular arcs connected by a straight line and ending with a line; its symbolic trajectory equation is included in Appendix D-A.

Our findings in Table I demonstrate the advantages and disadvantages of our method relative to quantifier elimination using CAD. For non-polynomial examples like a rectangle moving along the Dubins path described above or the UAV example from [1], the active corner method is able to compute fully symbolic formulations of the safe region when CAD fails to return an answer when run overnight (8+ hours). We do note that due to the complexity of a symbolic hexagon moving along the Dubins path, the number of transition points means our method cannot compute an answer, though neither can CAD. For a fully numeric example from [1], CAD took 2381 seconds to run but returned False incorrectly in place of a region. Additionally, memory is often a constraint for symbolic computation given the CAD algorithm’s doubly-exponential runtime [13]; many examples consumed 100+ GB of RAM and one case grew to consume 350 GB of RAM without returning an answer. In the worst case, however, our method consumes under 100MB of RAM. On the other hand, for strictly polynomial examples like that in [21], CAD runs quickly and efficiently, though our method remains competitive.