Guaranteeing High-Level Behaviors while Exploring Partially Known Maps

This paper presents an approach for automatically synthesizing and re-synthesizing a hybrid controller that guarantees a robot will exhibit a user-defined high-level behavior while exploring a partially known workspace (map). The approach includes dynamically adjusting the discrete abstraction of the workspace as new regions are detected by the robot's sensors, automatically rewriting the specification (formally defined using Linear Temporal Logic) and re-synthesizing the control while preserving the robot state and its history of task completion. The approach is implemented within the LTLMoP toolkit and is demonstrated using a Pioneer 3-DX in the lab.