רונן ברפמן

Inspired by the success of the distributed computing community in applying logics of knowledge and time to reasoning about distributed protocols, we aim for a similarly powerful and high-level abstraction when reasoning about control problems involving uncertainty. This paper concentrates on robot motion planning with uncertainty in both control and sensing, a problem that has already been well studied within the robotics community. First, a new and natural problem in this domain is defined: Does there exists a sound and complete termination condition for a motion, given initial and goal locations? If yes, how to construct it? Then we define a high-level language, a logic of time and knowledge, which we use to reason about termination conditions and to state general conditions for the existence of sound and complete termination conditions in a broad domain. Finally, we show that sound termination conditions that are optimal in a precise sense provide a natural example of knowledge-based programs with multiple implementations.