A Motion Closed World Asumption

1 Introduction

Reasoning about moving objects is becoming increasingly important. Air traffic controllers in both the US and Europe are facing a dramatically increasing workload as the number of flights increases. Cell phone companies are increasingly interested in knowing where cell phones on their network are located - this is useful for hand-off policies between cell phone towers. Vehicle security systems such as LOJACK and ONSTAR are increasingly being used to determine where vehicles are and where they are not.

[Yaman et al., 2004] proposed the concept of a "go theory" which can be used to make statements of the form "Object o is expected to leave location P1 at some time point in the interval [t-1 , t+1 ] and reach location P2 at some time point in the interval [t-2 , t+2 ] traveling at a velocity between v1 and v2. Go theories can be used, for example, to make statements such as "Plane p22 is expected to take off from Paris at some time between 10 and 12 and land at Boston at some time between 18 and 23 traveling at a speed between 10 to 20." Go theories are sets of such statements. Figure 1 shows the spatial layout of one such go-theory (the go theory is written in text at the top). [Yaman et al., 2004] provides a model theory for go theories, together with algorithms to check entailment of certain kinds of atoms: "in" atoms that check if a given moving object is within a given region at a given time, and "near" atoms which are used to check if two objects are within a given distance of each other at some time.

Though the semantics given by [Yaman et al., 2004] is adequate for positive atoms, it is inadequate for negative atoms. For example, suppose we consider the go-theory containing just the two statements above about plane p22. In this case, we would like to infer that plane p22 is not in Detroit at time 30, even though it may be theoretically possible for the plane to make it to Detroit. The goal of this paper is to ensure that intelligent negative inferences of this kind can be made from go-theories.

The contributions and organization of this paper are as follows: in Section 2, we recapitulate the syntax of go-theories from [Yaman et al., 2004]. In section 3, we introduce the concept of a coherent model of a go-theory, and describe the concept of coherent entailment. We also introduce the Motion Closed World Assumption (MCWA for short) and show how the MCWA can be used to reason about negative information. Also in Section 3, we show that the problem of checking if a go-theory has a coherent model is NP-complete. In Section 4, we provide algorithms to evaluate "in" literals w.r.t. the MCWA semantics. We are developing algorithms to process other kinds of queries such as the near literals described in [Yaman et al., 2004] - however, space reasons prevent us from presenting them. Section 5 describes a prototype implementation to answer positive and negative "in" queries - the implementation shows that our system is highly scalable. We compare our work with related work in Section 6.

2 Go-Theories: Syntax and Semantics

We first provide a quick overview of the main definitions of [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. When these terms are ground, 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 atom. When these terms are ground, 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. When all these terms are ground, 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.

If A is an atom, then A and ¬A are called literals. Due to space constraints, we only consider literals in this paper - [Yaman et al., 2004] provide a richer syntax including conjunction and disjunction.

An interpretation is a continuous function I : O×R+ → P. Intuitively, I(o, t) is o's location at time t. We first define satisfaction of a "go" atom w.r.t. a given time interval.

Definition 1 Let g = go(o, P1, P2, t-1 , t+1 , t-2 , t+2 , v-, v+) be an atom and I be an interpretation. I satisfies g over 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).

The above definition intuitively says that I |= g over a time interval T = [t1, t2] iff o starts moving at t1, stops moving at t2 and during this interval, 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 concept of satisfaction of arbitrary literals.

Definition 2 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 satisfies A over [t1, t2].
2. I |= near(o1, o2, d, t1, t2) iff dist(I(o1, t), I(o2, t)) ≤ d for all t1 ≤ t ≤ t2
3. 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).
4. I |= ¬A iff I does not satisfy A.

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.

Example 1 The Planes go-theory of Figure 1 is consistent as the interpretations I1, I2 below both satisfy it.

• I1 : p22 leaves Paris at time 11, flies to Boston at a constant speed of 14.85 and arrives in Boston at 19. p22 waits in Boston until 32, then it departs for Paris with a constant speed of 13.2 arriving in Paris at 41. The other plane, p34 leaves London at time 25 and flies to Delhi at a constant speed of 18.52, arriving in Delhi at 38.
• I2 : p22 leaves Paris at time 10, flies to Boston at constant speed of 14.85 and reaches Boston at 18. It waits in Boston until 19, when it takes off for Detroit where it arrives at time 21. It immediately departs and reaches Boston at time 29. At time 30, p22 leaves Boston and flies to Paris at a constant speed of 11.88, arriving in Paris at time 40. The other plane, p34 leaves London at time 25 and flies to Delhi at a constant speed of 18.52, arriving in Delhi at 38.

It is important to note that even though I2 satisfies the Planes go theory, it is an interpretation that allows plane p22 to wander around in ways that were not explicitly stated in the Planes go theory. In particular, it lets the plane wander to Detroit which was never mentioned in the go-theory. We would like to exclude such "wandering" interpretations as they prevent us frommaking the intuitive (nonmonotonic) inference that Plane p22 was never in Detroit.

Throughout the rest of the paper we are going to use the notation G[o] to denote the set of all atoms about an object o in a go theory G.

Definition 3 Let G be a go theory, o be an object and G[o] = {g1, g2, . . . , gn}. Then for every gi, gj ∈ G[o] we define a partial order ⪯ such that gi ⪯ gj iff t+2 (gi) ≤ t-1 (gj). A total order ⊑ on G[o] is compatible with G[o] iff ⊑ is a topological sort of ⪯.

Definition 4 Suppose G is a go theory, o is an object and ⊑ is a total order compatible with G[o]. Then L(G[o], ⊑) is set of linear constraints such that

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

Intuitively Sg,Eg are variables that represent the times o starts and stops moving.

Definition 5 A go theory G is non-collinear iff for each object o there are no g, g′ ∈ G[o] such that

• The intersection of line segments [loc1(g), loc2(g)] and [loc1(g′ ), loc2(g′ )] is a line segment [P,Q],
• The direction of the movement in g and g′ is same, i.e., ∃k ∈ R+ such that ⃗v = k × ⃗u where ⃗v = loc2(g) - loc1(g) and ⃗u = loc2(g′ ) - loc1(g′ )
• t-1 (g) ≤ t+2 (g′ ) and t-1 (g′ ) ≤ t+2 (g), i.e. temporally overlapping.

The following theorem establishes necessary and sufficient conditions for non-collinear go theories to be consistent.

Theorem 1 A non-collinear go theory G is consistent iff for every object o there is a total order ⊑o compatible with G[o] such that L(G[o], ⊑o) has a solution.

3 Coherence

In this section, we define the concept of a coherent interpretation. We start by defining precedence of time intervals.

Definition 6 (Precedence) Let S = {T1, . . . Tn} be a set of time intervals, where Ti = [ti1, ti2] for each i. Ti immediately precedes Tj in S if ti2 ≤ tj1 and for every Tk ∈ S, either tk2 ≤ ti2 or tk1 ≥ tj1.

Intuitively, I is a coherent interpretation of a go theory G if for each object o, there is a time interval T such that for every time point t ∈ T, I(o, t) either satisfies a go-atom in G or keeps the object at the destination of the last satisfied go-atom in G .

Definition 7 (Coherent Model and Theory) Let I be a model of the go theory G. Let G[o] = {g1, g2, . . . , gn} be the set of all go-atoms in G about object o. I is coherent w.r.t. o and G iff

• (i) There are time intervals T1 = [t11, t12], T2 = [t21, t22], . . ., Tn = [tn1, tn2] such that for each i, I satisfies gi over Ti and
• (ii) For every pair of time intervals Ti, Tj such that Ti immediately precedes Tj in {T1, T2, . . . , Tn} the following holds:
• ∀t ∈ [ti2, tj1] I(o, t) = loc2(gi), i.e. destination of gi.

I is a coherent model of G iff I is coherent w.r.t. o and G for all objects o.

G is a coherent go-theory iff G has a coherent model.

Example 2 Let G be the go theory in Figure 1. Let I1 and I2 be the two interpretations in Example 1. I1 is coherent with respect to G and p22 because it satisfies g1 over [11, 19], g2 over [32, 40] and in between [19, 32] plane p22 is in Boston. I2 is not coherent with respect to G and p22 because although it satisfies g1 over [10, 18], g2 over [30, 41] during [18, 30], p22 does not stay in Boston which is the destination of g1.

The following lemma and definition are useful in checking whether a non-collinear go-theory has a coherent model or not.

Definition 8 Suppose G is a non-collinear go theory, o is an object and ⊑ is a total order compatible with G[o]. Let g1 ⊑ g2 · · · ⊑ gn be the atoms of G[o]. ⊑ is spatially continuous w.r.t. G[o] iff for every i, 1 ≤ i < n, loc2(gi) = loc1(gi+1), i.e., gi's destination is gi+1's origin;

Lemma 1 Suppose G is a non-collinear go theory. G is coherent if for every object o there is a total order ⊑o compatible with G[o] such that L(G[o], ⊑o) has a solution and ⊑o is spatially continuous w.r.t. G[o].

The following theorem shows that checking coherence of a go-theory is NP-complete.

Theorem 2 (i) Checking coherence of a non-collinear go theory is NP-complete. (ii) Checking coherence of a go theory is NP-complete.

The proof is omitted due to lack of space. We now define the concept of coherent entailment.

Definition 9 (MCWA entailment) Let L be a ground literal and G be a go theory. G entails L via MCWA, denoted G|=mcwaL, iff every coherent model of G also satisfies L.

The MCWA is inspired by Minker's generalized closed world assumption [Minker, 1982] where a class of models is used to check if a given literal is true. We do the same here. The following example shows that the MCWA can handle examples such as the Planes example.

Example 3 Let G be the go theory in Figure 1. Let I1 and I2 be the interpretations in Example 1. Suppose a = in(p22, (75, 200), (85, 210), 23, 30). G|=mcwaa since in all coherent models of G, during [23, 30] plane p22 is in Boston which is inside the rectangle of the atom a.

Suppose b = in(p22, (55, 185), (80, 200), 23, 30). Then G|=mcwa¬b since in all coherent models of G, during [23, 30] plane p22 stays in Boston which is not in the rectangle of the atom b.

Also note that G ̸|= a and G ̸|= ¬b because according to the semantics in [Yaman et al., 2004] plane p22 can be anywhere during [23, 30].

Theorem 3 Let L be a ground in() literal and G be a go theory. Checking if G|=mcwaL is co-NP complete.

Since incoherent theories entail everything the following section describes algorithms for coherent go theories.

4 MCWA-Entailment Algorithms

This section provides algorithms to check for MCWAentailment of both positive and negative ground literals. Due to space limitations we assume all theories are non-collinear go theories. Extending our algorithm to remove this assumption is straightforward using the methods defined in [Yaman et al., 2004] that combine collinear go atoms into "movements"- our implementation applies to all go theories.

We first introduce some notations. If g is a go atom, then LS(g) is the line segment between the source and destination of g. Let G be a go-theory, o be an object and ⊑ be a total ordering compatible with G[o]. Let P be a point on LS(g) where g ∈ G. Then T -(G[o],⊑, g, P) and T +(G[o],⊑, g, P) are the earliest and latest possible times for o to be at P, subject to G,o, ⊑ and g. 1

4.1 Coherent in()

In this section, we show how to check whether a ground atom of the form a = in(o, q1, q2, t1, t2) is MCWA-entailed by a go-theory G. Let Rec(a) denote the set of points P such that qx 1 ≤ P x ≤ qx 2 and qy 1 ≤ P y ≤ qy 2 .

We first consider a non-collinear go theory G={g1, g2} about an object o, and an atom a = in(o, q1, q2, t1, t2). Assume Figure 2 depicts Rec(a) and the two line segments [P1, P3], [P3, P5] representing movements defined by g1 and g2. In any coherent model of G, g1 will be satisfied before g2. Hence the object enters Rec(a) at P2 and leaves Rec(a) at P4. If o always arrives at P2 before t2 and always leaves P4 after t1 subject to the constraints in G, then we can say that G|=mcwaa.

For an arbitrary go theory, any object might enter and leave Rec(a) multiple times. We need to identify these entrance and exit points as well as the atoms that contain them.

Definition 10 Let L be a sequence of line segments ℓ1 = [P11P12], ℓ2 = [P21P22],. . ., ℓn = [Pn1Pn2] such that for

1T -(G[o],⊑, g, P) is the solution to linear programming problem: minimize XP,g subject to L(G[o],⊑) ∪ L(P, g), where L(P, g) contains the following linear constraints:

• dist(loc1(g),P) v+(g) ≤XP,g -Sg ≤ dist(loc1(g),P) v-(g)
• dist(loc2(g),P) v+(g) ≤ Eg -XP,g ≤ dist(loc2(g),P) v-(g)

where XP,g is the variable that represents the time the object will arrive P while satisfying g. Sg and Eg are the variables associated with g in L(G[o],⊑). T +(G[o],⊑, g, P) can be computed in the same way, using maximization instead of minimization.

1 ≤ i < n, Pi2 = P(i+1)1. Let R be a rectangular region. An entry-exit of L for R is (i, j) iff

• ℓi ∩R ̸= ∅ and i > 1 =⇒ Pi1 ̸∈ R
• ℓj ∩R ̸= ∅ and j < n =⇒ Pj2 ̸∈ R
• ∀k ∈ [i, j) Pk2 ∈ R

The following lemma gives necessary conditions for G|=mcwaa when the atoms in G are satisfied in a specific order and the object enters and exits Rec(a) multiple times.

Lemma 2 Let G be a coherent go theory, o be an object and ⊑ be a total order compatible with G[o] such that L(G[o], ⊑) has a solution and ⊑ is spatially continuous w.r.t G[o]. Let g1 ⊑ g2 · · · ⊑ gn be the atoms of G[o]. Let a = in(o, q1, q2, t1, t2) be an atom. If G|=mcwaa then there is an entry-exit (i, j) of LS(g1) . . . LS(gn) for Rec(a) such that

The following algorithm uses this lemma to check for MCWA-entailment w.r.t. a specific total ordering.

Algorithm CheckCoherentIn(G, ⊑, a) Suppose a = in(o, q1, q2, t1, t2); Let g1 ⊑ g2 · · · ⊑ gn be atoms of G[o] if ⊑ is not spatially continuous w.r.t G[o] then return true if L(G[o], ⊑) has no solution then return true for each entry-exit (i, j) of LS(g1) . . . LS(gn) for Rec(a) Let [Pi, Qi] = LS(gi) ∩ Rec(a) Let [Pj,Qj] = LS(gj) ∩Rec(a) if T +(G[o], ⊑, gi, Pi) ≤ t2 and t1 ≤ T -(G[o], ⊑, gj , Qj ) then return true end for return false

Theorem 4 Suppose G is a coherent go-theory and a = in(o, q1, q2, t1, t2) is a ground atom. Then: a is entailed by G via MCWA iff for every total order ⊑ compatible with G[o], the algorithm CheckCoherentIn(G, ⊑, a) returns "true".

4.2 Coherent ¬in()

We now address the problem of checking whether a literal of the form ¬in(o,Q1,Q2, t1, t2) is MCWA-entailed by a gotheory G.

Consider a coherent go theory G={g1, g2} about an object o, and an in-atom a = in(o, q1, q2, t1, t2). As before Figure 2 depicts Rec(a) and two line segments [P1, P3], [P3, P5] representing the movements defined by g1 and g2. Note that in any coherent model of G, g1 is satisfied before g2. Hence the object enters Rec(a) at point P2 and leaves Rec(a) at point P4. G|=mcwa¬a iff

• t1 is greater than or equal to the start time of g1 in any coherent model of G.
• t2 is smaller than or equal to the end time of g2 in any coherent model of G.
• Let T1 be the earliest arrival time to P2 and T2 be the latest arrival time to P4 in any coherent model of G then T1 > t2 or T2 < t1.

The following lemma gives necessary conditions for G|=mcwa¬a to hold w.r.t. a specific total ordering ⊑ even if the object enters and exits Rec(a) multiple times.

Lemma 3 Let G be a coherent go theory, o be an object and ⊑ be a total order compatible with G[o] such that L(G[o], ⊑) has a solution and ⊑ is spatially continuous w.r.t. G[o]. Let g1 ⊑ g2 · · · ⊑ gn be the atoms of G[o]. Let a = in(o, q1, q2, t1, t2) be a ground atom. If G|=mcwa¬a then the following hold

• T +(G[o],⊑, g1, loc1(g1)) ≤ t1
• T -(G[o],⊑, gn, loc2(gn)) ≥ t2
• ∀ entry-exit (i, j) of LS(g1) . . .LS(gn) for Rec(a), T -(G[o],⊑, gi, Pi) > t2 or T +(G[o],⊑, gj,Qj) < t1 where [Pk, Qk] = LS(gk) ∩ Rec(a).

The following algorithm checks if G|=mcwa¬in() w.r.t. a specific total ordering.

Algorithm CheckCoherentNotIn(G, ⊑, ¬a) Suppose a = in(o, p1, p2, t1, t2); Let g1 ⊑ g2 · · · ⊑ gn the atoms of G[o]. if ⊑ is not spatially continuous w.r.t G[o] then return true if L(G[o], ⊑) has no solution then return true if t1 < T +(G[o], ⊑, g1, loc1(g1)) return false if t2 > T -(G[o], ⊑, gn, loc2(gn)) return false for each entry-exit (i, j) of LS(g1) . . . LS(gn) for Rec(a) Let [Pi, Qi] = LS(gi) ∩ Rec(a) Let [Pj,Qj] = LS(gj) ∩Rec(a) if T -(G[o], ⊑, gi, Pi) ≤ t2 and t1 ≤ T +(G[o], ⊑, gj , Qj ) then return false end for return true

Theorem 5 Suppose G is a coherent go-theory and L = ¬in(o, q1, q2, t1, t2) is a ground literal. Then L is entailed by G via MCWA iff for every total order ⊑ compatible with G[o], the algorithm CheckCoherentNotIn(G,⊑, a) returns "true".

5 Implementation

Determining MCWA-entailment is co-NP complete because the number of orderings spatially continuous w.r.t. G[o] can be exponential. However, in the real world, we expect a gotheory to allow only a small number of orderings compatible with G[o]. In other words, the respective order of movements an object is going to perform is mostly known. For example we might not know exactly when the plane p22 will land but we usually know where it is going to fly next. Thus, in practice there is a bound on the number of compatible total orderings per object.

For our experiments we generated random go theories with at most 256 spatially continuous orderings. This is not a hardcoded limit of our implementation. Generating random gotheories such that more than one spatially continuous ordering exists is a little bit tricky. Here is one method to generate a go theory G = {g1, g2, g3, g4, g5} with two spatially continuous orderings.

• Randomly pick points P1, P2, P3 and P4
• Set loc1(g1) = P1 and loc2(g1) = P2,
• Set loc1(g2) = P2, loc2(g2) = P3 and loc1(g3) = P3, loc2(g3) = P2,
• Set loc1(g4) = P2, loc2(g4) = P4 and loc1(g5) = P4, loc2(g5) = P2,
• Set temporal and speed intervals of every gi so that g1 is always first and the rest can be done in any order.

We have generalized the reasoning above to create random go theories with an arbitrary bound on the number of spatially continuous orderings.

We have implemented the two algorithms CheckCoherentIn and CheckCoherentNotIn in Matlab and conducted experiments on a mobile Athlon XP 1800 processor running under Windows XP and having 256MB of memory. Figure 3 shows the computation time of four types of queries for coherent go theories with at most 256 spatially continuous orderings and have the following properties: all points are selected randomly from the rectangle [(0, 0), (1000, 1200)] and the speeds allowed for any object less than 100. The four query templates we used are:

Q1: in(o, (500, 500), (550, 600), 0.5 ∗ h, 0.75 ∗ h) Q2: in(o, (100, 150), (350, 400), h-100, h-10) Q3: ¬Q1 Q4: ¬Q2

where h is the latest end time for any atom related to o in the given theory. The data points in Figure 3 are an average of 300 runs.

Our implementation performs very well, executing most queries in less than 0.3 seconds even when there are as many as 1,000 go-atoms per object. In the query Q1 where CheckCoherentIn returns true in almost every compatible orderings the algorithm runs in linear time with respect to number of atoms per object and takes up to 0.9 seconds when there are 1,000 go-atoms per object. Consequently Q3, the complement of Q1, takes almost no time because CheckCoherentNotIn returns false for any compatible ordering.

6 Related work

The Closed World Assumption (CWA) proposed by [Reiter, 1977] holds that anything that cannot be entailed by a theory is false. Minker [Minker, 1982] extended the CWA to a Generalized CWA (GCWA) that accounts for disjunction. GCWA states that a formula is false if it is false in all minimal models of the theory. The go-theories proposed by [Yaman et al., 2004] are disjunctive because the start and end times and object velocities are all known to be within a given range. The notion of a coherent model of a go-theory selects certain models (much like Minker selected minimal models in GCWA) and uses these to make closed world inferences.

[Intille, 1994; Intille et al., ] have used the CWA to track moving objects in football games using computer vision algorithms. They use CWA to adaptively select and weight image features used for correspondence. No motion reasoning of the type we perform in this paper is done.

Numerous spatio-temporal logics exist [Gabelaia et al., 2003; Merz et al., 2003; Wolter and Zakharyaschev, 2000;

Cohn et al., 2003] have proposed spatio-temporal logics. These logics extend temporal logics to handle space. By and large, these frameworks use discrete rather than the continuous representations we use. Moreover, these works focus on qualitative aspects of spatio-temporal reasoning, rather than deal quantitatively with the dynamics of motion. Our methods are rooted in a mix of geometry and logic, rather than in logic alone. Cohn [Anthony G. Cohn, 2001] provides an excellent survey of spatio-temporal logics but the survey sheds little light on reasoning above motion. A notable exception is the work of Muller [Muller, 1998a; 1998b] who describes a formal qualitative theory for reasoning about motion. The expressive power of the theory allows for the definition of complex motion classes. The work however is purely symbolic not quantitive.

7 Conclusions

Yaman et. al. [Yaman et al., 2004] introduce a logic based on "go theories" for reasoning about moving objects. In this paper, we show that this logic often does not allow us to infer that an object is not present at a given place or region, even though common sense would dictate that this is a reasonable inference to make. We define a class of models of go-theories called coherent models. We use this concept to define a motion closed world assumption (MCWA) and develop a notion of MCWA-entailment. We show that checking if a go-theory has a coherent model is NP-complete. An in atom checks if a given object is present in a given region during a given time interval. We provide sound and complete algorithms to check if an in literal (positive or negative in atom) can be inferred from a go-theory using the MCWA. In our experiments our algorithms executed queries in less than 1 second even when there are as many as 1,000 go-atoms per object.

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). The opinions expressed in this paper are those of authors and do not necessarily reflect the opinions of the funders.