Temporal logic motion planning in unknown environments

In this paper, we consider a robot motion planning problem from a specification given as a syntactically co-safe linear temporal logic formula over a set of properties known to be satisfied at the regions of an unknown environment. The robot is assumed to be equipped with deterministic motion and accurate sensing capabilities. The environment is assumed to be partitioned into a finite number of identical square cells. By bringing together tools from formal verification, graph theory, and grid-based exploration, we develop an incremental algorithm that makes progress towards satisfying the specification while the robot discovers the environment using its local sensors. We show that the algorithm is sound and complete. We illustrate the feasibility and effectiveness of our approach through a simulated case study.