Xu, Bingxin2013-09-052018-01-292013-01-28bibid: 8267018https://hdl.handle.net/1813/33823This thesis presents the development of high-level guaranteed robot control for reactive behaviours by relaxing two assumptions: 1) the workspace is well-known in advance; 2) the temporal logic based formalisms encode the specification by expressing the properties of future paths. This paper addresses the challenges of relaxing both of the assumptions by presenting an approach for automatically re-synthesizing a hybrid controller that guarantees user-defined high-level robot behaviour while exploring and updating a partially unknown workspace, and providing a concise grammar for specifying highlevel tasks that require memory of past events. In the first challenge, this thesis introduces an approach that includes dynamically adding new regions into the workspace during execution, automatically rewriting the specification, and re-synthesizing the controller while preserving the robot state and its history of task completion. The approach is implemented within the LTLMoP toolkit and is demonstrated in an experiment. For the second challenge, this thesis introduces an innovative structured English grammar for specifying high-level behaviour that automatically performs memory operations without requiring explicit definition from the specification designer. This grammar admits intuitive, unambiguous specifications for tasks that implicitly use memory for purposes including non-repeated goals, strictly ordered requirements, etc. The approach is also implemented within the LTLMoP toolkit.en-UShigh-level controlrobotformal methodsdissertation or thesis