Declarative Reasoning about Moving Objects

Abstract

There are numerous applications where there is a critical need to reason about moving object plans under uncertainty. Previous work on spatio-temporal logics is limited to qualitative approaches and the work on spatio-temporal databases focus on the observations ignoring the intended movements of the objects. This thesis presents a Logic of Motion (LOM), a novel theory and algorithms that combine logic, constraint satisfaction and geometric reasoning. LOM provides a declarative syntax and model theory and formalizes how to reason about planned movements of objects, when there is uncertainty. LOM is the first quantitative logical treatment of moving objects that can account for the fact that we are not always sure when an object will leave or arrive a given location, and what its velocity will be. The thesis includes the following contributions:

LOM, the first quantitative logic to reason about flexible plans for moving objects.

An analysis of the computational complexity of reasoning with flexible plans for moving objects. This analysis includes an important theoretical result showing that complexity of consistency checking for LOM theories is at least NP-hard. I also provide algorithms to check consistency of a fraction of LOM theories called go-theories.

A class of motion theories, called Simple Go-Theories that are tractable.

Efficient algorithms to answer ground and non-ground queries in LOM concerning the possible location of the object and its proximity to other objects.

A study of default reasoning for motion-theories. It presents a motion closed world assumption for LOM that restrict the reasoning within a class of preferred models of the theory. Motion closed world assumption allows us to make more intelligent and customized inferences.

An investigation of deconfliction of motion-theories with respect to some integrity constraints. A deconfliction of a theory is a modification to the theory such that any model of the modified theory will entail the integrity constraints. I present an algorithm for efficiently computing a deconfliction of a theory.

Extensive empirical evaluation to demonstrate the efficiency of consistency checking, query answering and deconfliction algorithms.