Going Far, Logically

1 Introduction

All of us fly in airplanes. We know that flight plans are almost never 100% accurate. We all have a vested interest in ensuring that planes we fly in are sufficiently far from other planes that are flying in the sky at the same time. The goal of this paper is to develop a hybrid logical and constraint based framework to ensure that moving objects with positional uncertainty (where will the object be at a given time) remain sufficiently far apart.

Our work builds on [Yaman et al., 2004] who developed the concept of a "go-theory". A go-theory is a finite set of "go-atoms." A go-atom can express statements such as 'Plane p1 leaves location L1 some time between 10 and 12 and arrives at location L2 at some time between 30 and 40 and during the flight the speed of the plane is between 5 and 6". They provide algorithms to check if a given plane is within a given region at a given time point. They also introduce ground atoms of the form near(o1, o2, d, t1, t2) - intuitively, this means that at all times during the interval t1, t2, o1 and o2 are guaranteed to be within d units of each other.

In this paper, we introduce a predicate symbol called far(o1, o2, d, t1, t2) - intuitively, this means that at all times during the interval t1, t2, o1 and o2 are guaranteed to be at least d units apart.

One may think that near() and far() are complements of each other. Unfortunately, this is not true. Yaman et. al.[Yaman et al., 2004] define interpretations and a notion of satisfaction. For near(o1, o2, d, t1, t2) atom to be a logical consequence of a go-theory G, for every interpretation I that satisfies G, it must be the case that for all times t1 ≤ t ≤ t2, the distance between the locations of o1 and o2 at time t is less than or equal to d. Thus, ¬near(()o1, o2, d, t1, t2) is a logical consequence of G if for every interpretation I which satisfies G there exists a time t1 ≤ t ≤ t2, the distance between the locations of o1 and o2 at time t (according to the interpretation I) is greater than d. In contrast, for far(o1, o2, d, t1, t2) to be entailed by S, it must be the case that for every interpretation I which satisfies G and for every time point t1 ≤ t ≤ t2, the distance between the locations of o1 and o2 at time t is greater than d. Thus, entailment of far() atoms is not the same as entailment of either near() atoms or ¬near() literals.

In this paper, we define the semantics of far() and develop an algorithm called CheckFar to check entailment of ground far() atoms by a go-theory G. We have conducted extensive experiments on the computational feasibility of CheckFar - our experiments show in a compelling way that in real world situations 1 , CheckFar will work very well indeed. In our experiments we answered far queries in less than 0.6 seconds for go theories up to 1000 atoms per object.

2 Background On go-Theories

We now provide a quick overview of go-theories from[Yaman et al., 2004]. We assume the existence of several sets of constant symbols: R is the set of all real numbers, O is the set of names of objects, P = R×R is the set of all points in two-dimensional cartesian space. We assume the existence of three disjoint sets of variable symbols, VR, VO, and VP, ranging over R, O and P, respectively. A real term t is any member of R ∪VR. Object terms and point terms are defined similarly. Ground terms are defined in the usual way. We now define atoms as follows.

• If o1, o2 are object terms, and d, t1, t2 are positive real terms, then near(o1, o2, d, t1, t2) is an atom. Intuitively, this atom says that o1, o2 are within distance d of each other during the time interval [t1, t2].
• If o is an object term, P1, P2 are point terms, and t1, t2 are positive real terms, then in(o, P1, P2, t1, t2) is an

1 We built an application to manage separation between ships in port shipping lanes.

atom. Intuitively, this atom says that object o is in the rectangle whose lower left (resp. upper right) corner is P1 (resp. P2) at some point in the time interval [t1, t2].

• If o is an object term, P1, P2 are point terms, and t-1 , t+1 , t-2 , t+2 , v-, v+ are positive real terms, then go(o, P1, P2, t-1 , t+1 , t-2 , t+2 , v-, v+) is an atom called a go atom. Intuitively, this atom says that object o leaves point P1 at some time in [t-1 , t+1 ] and arrives at point P2 during [t-2 , t+2 ], traveling in a straight line with a minimum speed v- and maximum speed v+.

Ground atoms are defined in the usual way. A go theory is a finite set of ground go-atoms. Note that go-theories do not contain near() or in() atoms.

If G is a go-theory and o is an object id, the restriction of G to o, denoted Go is the set {g ∈ G | obj(g) = o}.

An interpretation is a continuous function I : O×R+ → P. Intuitively, I(o, t) is o's location at time t.

Definition 1 Let g = go(o, P1, P2, t-1 , t+1 , t-2 , t+2 , v-, v+) be a ground atom and I be an interpretation. I satisfies g w.r.t. a time interval T = [t1, t2] iff:

• t1 ∈ [t-1 , t+1 ] and I(o, t1) = P1
• t2 ∈ [t-2 , t+2 ] and I(o, t2) = P2
• ∀t ∈ [t1, t2], I(o, t) is on the line segment [P1, P2]
• ∀t, t′ ∈ [t1, t2], t < t′ implies dist(I(o, t), P1) < dist(I(o, t′ ), P1), where dist is the function that computes the Euclidean distance between two points.
• For all but finitely many times in [t1, t2], v = d(|I(o, t)|)/dt is defined and v-(g) ≤ v ≤ v+(g).

This intuitively says that I |= g w.r.t. a time interval T = [t1, t2] iff o starts moving at t1 and stops moving at t2 and furthermore, during [t1, t2], the object moves away from P1 towards P2 without either stopping or turning back or wandering away from the straight line connecting P1 and P2. We are now ready to define the full concept of satisfaction.

I satisfies a ground literal (denoted I |= A) in these cases:

1. I |= go(o, P1, P2, t-1 , t+1 , t-2 , t+2 , v-, v+) iff there exists an interval [t1, t2] such that I |= Aw.r.t. [t1, t2].
2. I |= near(o1, o2, d, t1, t2) iff dist(I(o1, t), I(o2, t)) ≤
3. d for all t1 ≤ t ≤ t2.
4. I |= in(o, P1, P2, t1, t2) iff there are numbers t ∈ [t1, t2], x ∈ [P1 x , P2 x ] and y ∈ [P1 y , P2 y ] such that I(o, t) = (x, y).
5. I |= ¬A iff I does not satisfy A.

The above definition can be extended in the obvious way to handle quantification - in this paper, we will only consider the ground case.

I satisfies (or is a model of) a set of ground atoms MT iff I satisfies every A ∈ MT. MT is consistent iff there is an interpretation I such that I |= MT. L is a logical consequence of MT, denoted MT |= L, iff every model of MT is also a model of L.

3 far() atoms

We are now ready to extend the logic in [Yaman et al., 2004] to include far() atoms. If o1, o2 are objects, and d, t1, t2 are real terms, then far(o1, o2, d, t1, t2) is a far() atom.

Definition 2 (satisfaction of far() atoms) Suppose f is a ground far atom and I is an interpretation. I |= f iff for all t1 ≤ t ≤ t2, dist(I(o1, t), I(o2, t)) > d.

We say a go theory G entails f iff whenever I |= G, it is also the case that I |= f. The far()-entailment problem is that of checking whether a given go-theory entails a ground far()-atom. The entailment of a negated near literal does not imply entailment of the associated far atom. Similarly entailment of a negated far literal does not imply entailment of the associated near atom. However, the following results hold:

Lemma 1 Suppose G is a go theory and suppose far(o1, o2, d, t1, t2) and near(o1, o2, d, t1, t2) are ground. If G |= far(o1, o2, d, t1, t2), then G |= ¬near(o1, o2, d, t1, t2). If G |= near(o1, o2, d, t1, t2), then G |= ¬far(o1, o2, d, t1, t2).

The following result tells us that checking for entailment of a ground far()-atom is co-NP complete.

Theorem 1 Let G be a go theory and f = far(o, o′ , d, t1, t2) be a ground atom. Checking if G |= f is coNP-complete.

We will omit the proofs due to space constraints.

4 Far Algorithm

Finding an algorithm to solve the far()-entailment problem is a complex task. Our solution involves the following steps. First we partition a go-theory into clusters Go of go-atoms about the same object o. Next, for any given go-atom g, we define the temporal certainty interval which specifies a time interval when the object is guaranteed to be on the line segment [loc1(g), loc2(g)]. Third, we define the positional certainty interval that finds the smallest subsegment of the above line in which the vehicle is guaranteed to be at time t. Both temporal and positional certainty intervals are defined w.r.t. a given ordering of go-atoms. Our fourth step is to explain how to solve the far()-entailment problem when a go-theory has only two go-atoms (one for each object) and t1 = t2 in the far() atom whose entailment we are trying to check. Our fifth step generalizes this to the case when t1 ≤ t2. Finally, we show how to remove the assumption that G contains only two go-atoms.

Due to space constraints, we will proceed under the assumption that G is non-collinear as defined below. Extending our algorithm to remove this assumption is straightforward 2 Our implementations do not require this assumption.

2 [Yaman et al., 2004] provides a technique to merge multiple collinear go-atoms into "movements" that are non-collinear. The same technique can be used here.

Definition 3 A go theory G is non-collinear iff there are no go-atoms g, g′ ∈ G such that obj(g) = obj(g′ ) and the following two conditions both hold:

• The intersection of line segments [loc1(g), loc2(g)] and [loc1(g′ ), loc2(g′ )] is a line segment [P,Q] such that P is visited before Q in both g and g′ and
• t-1 (g) ≤ t+2 (g′ ) and t-1 (g′ ) ≤ t+2 (g).

4.1 Temporal and Positional Certainty Intervals

In this section, we define the notions of temporal and positional uncertainty.

Definition 4 (C(G, o,⊑)) Let G be a go theory and o be an object id. Let ⊑ be any total ordering on Go . The set C(G, o, ⊑) of linear constraints associated with G, o, ⊑ is defined as follows:

• ∀g = go(o, P1, P2, t-1 , t+1 , t-2 , t+2 , v-, v+) ∈ Go
• t-1 ≤ Sg ≤ t+1 and t-2 ≤ Eg ≤ t+2
• v- ×(Eg -Sg) ≤ dist(P1, P2) ≤ v+ ×(Eg -Sg)
• for every g, g′ ∈ Go such that g ⊑ g′ : Eg ≤ Sg′ .

Sg and Eg are variables associated with an atom g which intuitively denote the start time and end time of the movement described by g. When Go has only one atom g,we will use C(g) as a short hand notation.

Example 1 Let g = go(o, (40, 10), (70, 50), 12, 13, 21, 21, 4, 10) and g′ = go(o, (70, 50), (30, 80), 20, 21, 30, 31, 4, 10). Suppose G = {g, g′ } and g ⊑ g′ . Then C(G, o, ⊑) contains the following constraints:

• 12 ≤ Sg ≤ 13, 21 ≤ Eg ≤ 21 ,
• 4 × (Eg - Sg) ≤ 50 ≤ 10 × (Eg - Sg).
• 20 ≤ Sg′ ≤ 21, 30 ≤ Eg′ ≤ 31 ,
• 4 × (Eg′ - Sg′ ) ≤ 50 ≤ 10 × (Eg - Sg),
• Eg ≤ Sg′ .

We now use linear programming methods to define the temporal certainty interval of a go atom.

Definition 5 (TCI(G, o, ⊑, g)) Let G be a go theory, o be an object, and ⊑ be a total order on Go such that C(G, o, ⊑) has a solution. The temporal certainty interval, TCI(G, o, ⊑, g), of an atom g ∈ Go w.r.t. ⊑ is the time interval [T -, T +] where

• T - is the result of solving the linear program: "maximize Sg subject to C(G, o,⊑)",
• T + is the result of solving the linear program: "minimize Eg subject to C(G, o,⊑)".

When Go has only one atom g we will TCI(g) as a short hand notation. Intuitively, TCI(G, o,⊑, g) is the interval when we know for sure that object o is within the line specified in go-atom g.

Example 2 Let g and g′ be the two go atoms in Example 1. TCI(g) is [13, 21]. If G = {g, g′ } and g ⊑ g′ , then TCI(G, o, ⊑, g′ ) = [21, 30].

Conversely, given a time point t and a ground go-atom g, we wish to know the potential segment on the line connecting loc1(g) and loc2(g) where the object associated with g could possibly be. To find this, we need another linear program.

Definition 6 (PCI(G, o,⊑, g, t)) Let G be a go theory, o be an object, and ⊑ be a total order on atoms of Go such that C(G, o,⊑) has a solution. Let g be an atom in Go such that TCI(G, o,⊑, g) is defined and t be any time point in TCI(G, o,⊑, g). The positional certainty interval, PCI(G, o,⊑, g, t), of atom g at time t w.r.t. ordering ⊑ is defined as follows:

• Let C(g, t) be the set of constraints:
• dg,t v+(g) ≤ t -Sg ≤ dg,t v-(g)
• D-dg,t v+(g) ≤ Eg - t ≤ D-dg,t v-(g)

where D = dist(loc1(g), loc2(g)). Note that this is a linear program when g is fixed because many terms above (such as D, v-(g),v+(g) are constants).

• Let dmin g,t be the result of solving the linear program

• Let dmax g,t be obtained by maximizing the objective function in the above linear program (instead of minimizing).
• Let P -(G, o,⊑, g, t) be the point exactly dmin g,t units away from loc1(g) on the line connecting loc1(g), loc2(g) and likewise, let P +(G, o,⊑, g, t) be the point exactly dmax g,t units away from loc1(g) on the same line.

The positional certainty interval PCI(G, o,⊑, g, t) is the line segment from P -(G, o, ⊑, g, t) to P +(G, o, ⊑, g, t).

When Go has only one atom g we use the shorter notation PCI(g, t).

Lemma 2 Let g be a go atom such that TCI(g) is defined, I be an interpretation, and suppose t ∈ TCI(g). If I |= g, then I(o, t) is on the line segment PCI(g, t).

4.2 Binary go-theories about a single time point

A binary go-theory is one which contains two go-atoms G = {g, g′ } where obj(g) = o, obj(g′ ) = o′ . Consider a ground far() query far(o, o′ , t1, t2, d) where t1 = t2. We need to check if the distance between o and o′ is guaranteed to be greater than d at time t. The following lemma presents necessary and sufficient conditions for entailment of such queries under the above assumptions.

Lemma 3 Let G = {g, g′ } be a go-theory such that obj(g) = o and obj(g′ ) = o′ and let f = far(o, o′ , d, t, t) be a ground atom. G |= f iff

• t ∈ TCI(g) and t ∈ TCI(g′ ) and
• The minimum distance between line segments PCI(g, t) and PCI(g′ , t) is greater than d.

Example 3 Let g = go(o, (40, 10), (70, 50), 12, 13, 21, 21, 4, 10) and g′ = go(o′ , (55, 20), (45, 80), 17, 18, 32, 33, 2, 6) be two atoms. Let G = {g, g′ } and f = far(o, o′ , 5, 19, 19). TCI(g) = [13, 21] and TCI(g′ ) = [18, 32] both include the time point 19. At time 19, o is somewhere on the line segment PCI(g, 19) = [(58, 34), (65.2, 43.6)] and object o' is on the line segment PCI(g′ , 19) = [(54.67, 21.97), (53.08, 31.84)]. The minimum distance between these two lines is 33.73 which is greater than 5 so G |= f .

Consider the atom near(o, o′ , d, t, t) atom instead of far(o, o′ , d, t, t) then the second bullet of Lemma 3 becomes: "The maximum distance between line segments PCI(g, t) and PCI(g′ , t) is less than or equal to d". This maximum distance is achieved at the end points of PCI(g, t) and PCI(g′ , t), e.g. P -(g, t) and P +(g′ , t). However the minimum distance between PCI(g, t) and PCI(g′ , t) is not necessarily at the end points hence its computation is more complex.

4.3 Binary go-theories with temporal intervals

The complexity of computing far queries gets magnified even more when we consider the case t1 ≤ t2. For the near atom this is easy because it is enough to check the distance at the end points of PCI(g, t) and as shown in [Yaman et al., 2004] end points of PCI(g, t) are piecewise linear functions over a time interval. This is not enough for the far atom. For this reason answering far queries over time intervals requires a different approach then the one in [Yaman et al., 2004].

We first define the space envelope of a go-atom. Intuitively, the space envelope of a go-atom g is the set of all (x, y, t)-triples such that there exists a model I of g in which I(obj(g), t) = (x, y). In other words, it defines where and when it is possible for object o to be.

Definition 7 Let g be a ground go-atom such that TCI(g) is defined and let T = [t1, t2] be any time interval such that T ⊆ TCI(g). The space envelope, SE(g, T) of g during interval T is {(x, y, t) | t ∈ T and (x, y) ∈ PCI(g, t)}.

Theorem 2 SE(g, T) is a convex set.

Example 4 Let g′ = go(o′ , (55, 20), (45, 80), 17, 18, 32, 33, 2, 6) be a go atom. The space envelope of g′ over time interval [19, 21], is shown in Figure 1 on the left side. It is easy to see that SE(g′ , [19, 21]) is convex.

We now define the set of points that are closer than a given distance d to any possible location of an object at a given time.

Definition 8 (d-neighbourhood) Let g be a ground go-atom such that TCI(g) is defined. Let d be a real number and let T = [t1, t2] be a time interval such that T ⊆ TCI(g). The d-neighbourhood of g during T , denoted Nbr(g, T, d) = {(x, y, t) | t1 ≤ t ≤ t2 and (x, y) ∈ NearPts(g, t, d)} where NearPts(g, t, d) = {(x, y) | ∃(x′ , y′ ) ∈ PCI(g, t) and dist((x, y), (x′ y′ )) ≤ d}.

Intuitively NearP ts(g, t, d) is the set of all points p such that all points on the line segment PCI(g, t) which are d units or less in distance from p at time t. Similarly Nbr(g, T, d) is the set of all points (x, y, t) such that it is possible for obj(g) to be within d units of (x, y) at some time t in interval T .

Theorem 3 (i) Nbr(g, T, d) is a convex set. (ii) If d = 0, then Nbr(g, T, d) = SE(g, T ).

Example 5 Let g = go(o, (40, 10), (70, 50), 12, 13, 19, 21, 4, 10) be a go atom. The 5-neighborhood of g over time interval [19, 21] is shown on the far right hand side of Figure 1. It is easy to see that it is a convex set.

The following theorem states necessary and sufficient conditions under which {g, g′ } |= f .

Theorem 4 Let f = far(o, o′ , d, t1, t2) and G = {g, g′ } be a go theory where obj(g) = o and obj(g′ ) = o′ . G |= f iff

• [t1, t2] ⊆ TCI(g) and [t1, t2] ⊆ TCI(g′ )
• Nbr(g, [t1, t2], d) ∩ SE(g′ , [t1, t2]) = ∅

Thus, an algorithm to solve the far()-entailment problem only needs to check both these conditions. [Mantyla, 1988] provides polynomial algorithms to check for the intersection of two convex sets - these can be used directly to check the second condition above.

Example 6 Let g = go(o, (40, 10), (70, 50), 12, 13, 21, 21, 4, 10) and g′ = go(o′ , (55, 20), (45, 80), 17, 18, 32, 33, 2, 6) be two go atoms. Let G = {g, g′ } and f = far(o, o′ , 5, 19, 21). Then TCI(g) = [13, 21] and TCI(g′ ) = [18, 32]. Both include the time interval [19, 21]. Figure 1 shows Nbr(g, [19, 21], 5) and SE(g′ , [19, 21]). It is apparent from the figure that the two do not intersect: hence G |= f.

4.4 Arbitrary Go-theories with temporal intervals

We now remove the restriction that G is a binary go-theory. Doing so introduces several complications. For any single o, there may be many possible total orderings associated with Go . Furthermore, for some theories we can predict the possible locations of an object not only in the certainty interval of an atom, but also during a time interval that spans over several atoms. The following lemma gives the necessary and sufficient conditions when this can be done.

Lemma 4 Let G be a go-theory, o be an object, and ⊑ be a total order on Go such that C(G, o,⊑) has a solution. Suppose g1 ⊑ g2 . . . ⊑ gn are the atoms of Go . TCI(G, o,⊑ , gi) ∪ TCI(G, o ⊑, gi+1) . . . ∪ TCI(G, o,⊑, gj) is a single time interval iff for every 1 ≤ i ≤ k < j ≤ n with TCI(G, o, ⊑, gk) = [T - k , T + k ] the following are true

• T + k = T - k+1
• loc2(gk) = loc1(gk+1)

Definition 9 Let G be a go-theory, o be an object, and ⊑ be a total order on Go such that C(G, o,⊑) has a solution. Suppose S ⊆ Go . S is temporally relevant to time interval [t1, t2] is iff

• The atoms in S satisfy the conditions in lemma 4 and
• There are atoms g, g' in S such that t1 ∈ TCI(G, o,⊑ , g) and t2 ∈ TCI(G, o, ⊑, g′ )

Example 7 Let g1 = go(o, (40, 10), (70, 50), 12, 13, 21, 21, 4, 10) and g2 = go(o, (70, 50), (30, 80), 20, 21, 30, 31, 4, 10) be go atoms. If G = {g1, g2} and g1 ⊑ g2 then C(G, o,⊑) has a solution. Moreover TCI(G, o,⊑, g1) = [13, 21], TCI(G, o,⊑, g2) = [21, 30] and TCI(G, o,⊑ , g1) ∪ TCI(G, o,⊑, g2) is a single interval. Suppose T = [19, 30] then {g1, g2} is temporally relevant to T .

We now generalize definitions 7 and 8 to accommodate nonbinary go-theories.

Definition 10 (SE(G, o,⊑, T)) Let G be a go-theory, o be an object, and ⊑ be a total order on Go such that C(G, o, ⊑) has a solution. If T = [t1, t2] is a time interval, then SE(G, o, ⊑, T) is the set of all points (x, y, t) such that

• t ∈ T and t ∈ TCI(G, o,⊑, g) for some g ∈ Go ,
• (x, y) is on PCI(G, o,⊑, g, t).

SE(G, o,⊑, T) is not defined if there is a time point t ∈ T such that for all g ∈ Go , t ̸∈ TCI(G,⊑, g).

Note that SE(G, o,⊑, T) is not necessarily convex when T spans over multiple go atoms. We can generalize Nbr to Nbr(G, o, ⊑, T, d) in a similar manner - these are omitted due to space constraints. Nbr(G,⊑, T, d) also may not be convex. We now state a theorem describing the conditions under which a go theory G entails a far() atom.

Theorem 5 Suppose G is a go-theory and o, o′ are objects. The ground atom f = far(o, o′ , d, t1, t2) is a logical consequence of G iff for every pair of total orders ⊑ and ⊑′ on Go and Go′ such that C(G, o, ⊑) and C(G, o′ , ⊑′ ) are solvable:

• ∃S ⊆ Go such that S is temporally relevant to [t1, t2]
• ∃S′ ⊆ Go′ such that S′ is temporally relevant to [t1, t2]
• Nbr(G, o, ⊑, [t1, t2], d) ∩ SE(G, o′ , ⊑′ , [t1, t2]) = ∅.

Example 8 Let g1 and g2 be go atoms in Example 7 and g′ = go(o′ , (55, 20), (45, 80), 17, 18, 32, 33, 2, 6). Let G = {g1, g2, g′ } and f = far(o, o′ , 5, 19, 30). If g1 ⊑ g2 and ⊑′= ∅ then Figure 2 shows Nbr(G, o,⊑, [19, 30], 5) and SE(G, o′ ,⊑′ , [19, 30]). The figure also shows that the sets intersect - hence G ̸|= f .

As Nbr(G, o, ⊑, T, d) and SE(G, o′ , ⊑, T ) are not always convex, computing their intersection is tricky. We partition T into subintervals T1, T2, . . . , Tn (we call this a convex partition of T) such that for all i < n, the end point of Ti is the end point of the temporal certainty interval of some g ∈ Go ∪ Go′ . It is easy to verify that n ≤ |Go | + |Go′ |. For each Ti, Nbr(G, o,⊑, Ti, d) and SE(G, o′ ,⊑, Ti) are convex and we leverage this in the CheckFar algorithm below.

Algorithm CheckFar(G, ⊑, ⊑′ , f )

Suppose f = far(o, o′ , d, t1, t2);

if C(G, o, ⊑) or C(G, o′ , ⊑′ ) has no solution then return true

Let So ⊆ Go such that So is temporally relevant to [t1t2]

Let So′ ⊆ Go′ such that So′ is temporally relevant to [t1t2]

if no such So or So′ exists then return false

Let T1, T2 . . . Tn be the convex partition of [t1, t2]

for each i < n do

if Nbr(G, o, ⊑, Ti, d) ∩ SE(G, o′ , ⊑′ , Ti]) ̸= ∅

then return false

end for

return true

Theorem 6 Suppose G is a go-theory and f = far(o, o′ , d, t1, t2) is a ground atom. Then: f is entailed by G iff for every total order ⊑ and ⊑′ on Go and Go′ , the algorithm CheckFar(G, ⊑, ⊑′ , f ) returns "true".

5 Implementation

We have implemented the CheckFar algorithm in Matlab. Our test results show that CheckFar(G,⊑,⊑′ , f) runs in linear time. Note that a single run of CheckFar does not check if G |= f. In fact CheckFar(G,⊑,⊑′ , f) should be executed for every possible ⊑,⊑′ pair that produce a solvable set of constraints. Although in theory this number is exponential which leads to coNP-hardness, in practice we expect this number to be bounded by a manageable constant k. In general individual movements can have some uncertainty however the order in which they are going to be accomplished is usually well known. Figure 3 shows the running time of 3 far queries as we vary the number of atoms per object when k = 256. Each data point is an average of 300 runs. For these experiments we created go theories G with at most 16 total orderings and all atoms are in a rectangle of size 300 by 400. We queried those theories using three query templates Q1 = far(o, o′ , 1, t1, t2), Q2 = far(o, o′ , 50, t1, t2) and Q3 = far(o, o′ , 10000, t1, t2) where [t1, t2] is a random time interval with length 10. The reader will notice that as the distance increases, the time to compute the query decreases. In the case of Q3 which is trivially false it takes almost no time to return the answer. Queries Q1 and Q2 take at most 0.6 seconds for go theories with 1000 atoms per object.

6 RelatedWork

To our knowledge, there is no work on a logical foundation for checking separation between moving objects in the presence of temporal and spatial uncertainty. However, almost all models of moving entities like cars, airplanes, ships, humans and animals are subject to uncertainty about where they are at a given point in time.

[Gabelaia et al., 2003; Merz et al., 2003; Wolter and Zakharyaschev, ; Cohn et al., 2003] study spatio-temporal logics where time is a discrete sequence rather than being continuous. [Muller, ] describes a formal theory for reasoning about motion in a qualitative framework that supports complex motion classes. The work is purely symbolic. [Shanahan, 1995] discusses the frame problem, when constructing a logic-based calculus for reasoning about the movement of objects in a real-valued co-ordinate system. [Rajagopalan and Kuipers, 1994] focuses on relative position and orientation of objects with existing methods for qualitative reasoning in a Newtonian framework. The focus of these works is qualitative - in contrast our work is heavily continuous and rooted in a mix of geometry and logic rather in just logic alone. far() queries are not studied in any of these papers.

There is also some peripherally related work in computer graphics [Lin and Gottschalk, 1998] and in "moving object databases" [Erwig et al., 1999] - they provide no model theory or algorithms for far() queries nor allow any uncertainty.

7 Conclusions

The ability to query a large number of objects moving uncertainly in time and space so that separation constraints between objects are maintained is critical to many applications (e.g. air traffic control, shipping port lane management). In this paper, we have extended the "logic of motion" proposed by Yaman et. al. [Yaman et al., 2004] via a far() predicate. We develop a model theory for far()-entailment. We show that the far()-entailment problem is coNP-complete. We develop an efficient algorithm called CheckFar that effectively checks if a given total ordering of atoms in a go-theory preserve separation constraints. To check whether two objects are guaranteed to be at least d units of distance away from each other during an interval of time, we must apply CheckFar to different possible orderings of the atoms in the gotheory. In real-world applications such as air traffic control and a shipping port lane management we have built, we expect such orderings to be relatively small in number even if the number of objects is very large. The reason for this is that usually the flight plan for each airplane consists of a sequence of steps which only yields 1 ordering of the atoms per airplane (whereas our experiments have used 16). Our experiments show that CheckFar performs very well in practice.

Acknowledgements

This work was supported in part by ARO grant DAAD190310202, ARL grants DAAD190320026 and DAAL0197K0135, the ARL CTAs on Telecommunications and Advanced Decision Architectures, NSF grants IIS0329851 and IIS0412812 and 0205489 and UC Berkeley contract number SA451832441 (subcontract from DARPA's REAL program).