The research described here is aimed at applying formal logic to problems that are usually approached using systems and control theory or geometric reasoning. The problem addressed is whether a mobile robot will be able to reach its destination, given that it can move as long as necessary but that its control and sensing are affected by uncertainty. In practical applications, often all the possible trajectories are computed from a map, and then the ones feasible for the controller are kept; when the robot moves, it gradually discards all the trajectories that cannot produce the obtained sensor values. The authors translate this problem into the search for a sound and complete termination condition for the motion, given initial and goal positions. The existence and optimality of such conditions are discussed.

In section 2, the problem is defined, and geometric reasoning is used to demonstrate the existence of termination conditions in some cases. In section 3, the logic of knowledge and time used is defined. The language contains temporal and epistemic modal operators, and is used in defining both the state of the environment and the state of the robot. In section 4, the properties of the termination condition (optimality, soundness, and completeness) are characterized and analyzed. Section 5 transforms the generation of the termination condition into the problem of generating the optimal implementation of a knowledge-based program. Proofs are given in an appendix.

The authors see this logic-based approach to motion planning as an important step in dealing with multi-robot systems, where the usual geometric reasoning will be too complex. Because knowledge-based systems in robotics are at an early stage and still give poor results in comparison to other approaches, this paper offers interesting results and new perspectives for development in this area.