The use of formal methods for synthesis has recently enabled the automated construction of verifiable high-level robot control. Most approaches use a discrete abstraction of the underlying continuous domain, and make assumptions about the physical execution of actions given a discrete implementation; examples include when actions will complete relative to each other, and possible changes in the robot's environment while it is performing various actions. Relaxing these assumptions give rise to a number of challenges during the continuous implementation of automatically synthesized hybrid controllers. This paper presents several distinct timing semantics for controller synthesis, and compares them with respect to the assumptions they make on the execution of actions. It includes a discussion of when each set of assumptions is reasonable, and the computational tradeoffs inherent in relaxing them at synthesis time.

Recent advances have enabled the automatic generation of correct-by-construction robot controllers from high-level mission specifications. However, most current approaches operate under the closed-world assumption, i.e., only elements of the world explicitly modeled a priori can be taken into account during execution. In this paper, we tackle the problem of specifying and automatically updating the missions of robots operating in worlds that are open with respect to new elements, such as new objects and regions of interest. We demonstrate our approach in a scenario featuring a robotic courier whose world is open with respect to letters addressed to new recipients.

This paper illustrates the Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit. LTLMoP is an open source software package that transforms high-level specifications for robot behavior, captured using a structured English grammar, into a robot controller that guarantees the robot will complete its task, if the task is feasible. If the task cannot be guaranteed, LTLMoP provides feedback to the user as to what the problem is. Due to its modular nature, users can control a variety of different robots using LTLMoP, both simulated and physical, with the same specification. It shows an example robot waiter scenario, with LTLMoP controlling both a PR2 in simulation (using Gazebo), showcasing the interface between LTLMoP and the Robot Operating System (ROS)2, as well as an Aldebaran Nao humanoid in the lab.

This video shows a demonstration of a fully autonomous robot, an iRobot ATRV-JR, which can be given commands using natural language. Users type commands to the robot on a tablet computer, which are then parsed and processed using semantic analysis. This information is used to build a plan representing the high level autonomous behaviors the robot should perform [2][1]. The robot can be given commands to be executed immediately (e.g., "Search the floor for hostages.") as well as standing orders for use over the entire run (e.g., "Let me know if you see any bombs.").

The Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit is a software package designed to generate a controller that guarantees a robot satisfies a task specification written by the user in structured English. The controller can be implemented on either a simulated or physical robot. This video illustrates the use of LTLMoP to generate a correct-by-construction robot controller. Here, an Aldebaran Nao humanoid robot carries out tasks as a worker in a simplified grocery store scenario.

This paper addresses the challenge of creating correct-by-construction controllers for robots whose actions are of varying execution durations. Recently, Linear Temporal Logic synthesis has been used to construct robot controllers for performing high-level tasks. During continuous execution of these controllers by a physical robot, one or more low-level controllers are invoked simultaneously. If these low-level behaviors take different lengths of time to complete, the system will pass through several potentially unsafe intermediate states. This paper presents an algorithm that either generates a hybrid controller such that every continuous behavior of the robot is safe, or determines at synthesis time that the behavior may be unsafe. The proposed approach is implemented within the LTLMoP toolkit for reactive mission planning.

The Linear Temporal Logic MissiOn Planning (LTLMoP) toolkit is a software package designed to assist in the rapid development, implementation, and testing of high-level robot controllers. In this toolkit, structured English and Linear Temporal Logic are used to write high-level reactive task specifications, which are then automatically transformed into correct robot controllers that can be used to drive either a simulated or a real robot. LTLMoP's modular design makes it ideal for research in areas such as controller synthesis, semantic parsing, motion planning, and human-robot interaction.