Task and motion planning subject to Linear Temporal Logic (LTL) specifications in complex, dynamic environments requires efficient exploration of many possible future worlds. Model-free reinforcement learning has proven successful in a number of challenging tasks, but shows poor performance on tasks that require long-term planning. In this work, we integrate Monte Carlo Tree Search with hierarchical neural net policies trained on expressive LTL specifications. We use reinforcement learning to find deep neural networks representing both low-level control policies and task-level “option policies” that achieve high-level goals. Our combined architecture generates safe and responsive motion plans that respect the LTL constraints. We demonstrate our approach in a simulated autonomous driving setting, where a vehicle must drive down a road in traffic, avoid collisions, and navigate an intersection, all while obeying rules of the road.

Sampling-based methods have advanced the state of the art in robotic motion planning and control across complex, high-dimensional domains. With few exceptions, such approaches only admit simple constraints and objectives, such as collision-avoidance and reaching a goal state. In this work we leverage the best of two worlds: the scalability of sampling-based motion planning and the precise formal guarantees of temporal logic. We present an incremental sampling-based algorithm that synthesizes a motion control policy satisfying a bounded Signal Temporal Logic formula over properties of a given environment. Our key insight is that we can bias the selection of samples using a quantitative measure of how well the best path in the current tree of samples satisfies the specification. This allows us both to converge to a path that satisfies the specification, and to improve upon an existing path, i.e. to satisfy the specification with maximum robustness. We illustrate the performance of our method in several case studies.

In formal synthesis, the goal is to find a composition of components from a finite library such that the composition satisfies a given logical specification. In this paper, we consider the problem of synthesizing magic card tricks from component actions, where some of the actions depend on non-deterministic choices made by the audience. This problem can be naturally represented as a quantified logical formula of the form: Exists a composition, Forall nondeterministic choices, Uniquely-Exists intermediate and final outputs satisfying a logical specification, that is, an (∃∀∃!) satisfiability problem. We present a novel approach to solve this problem that exploits the unique-existence of intermediate and final outputs for any given composition and choice values. We illustrate how several popular magic card tricks can be recovered using this approach. These tricks evolved through human ingenuity over decades, but we demonstrate that formal synthesis can generate a number of novel variants of these tricks within minutes. In contrast, a direct encoding to quantified SMT problem fails to find a solution in hours.

We address the problem of diagnosing and repairing specifications for hybrid systems, formalized in signal temporal logic (STL). Our focus is on automatic synthesis of controllers from specifications using model predictive control. We build on recent approaches that reduce the controller synthesis problem to solving one or more mixed integer linear programs (MILPs), where infeasibility of an MILP usually indicates unrealizability of the controller synthesis problem. Given an infeasible STL synthesis problem, we present algorithms that provide feedback on the reasons for unrealizability, and suggestions for making it realizable. Our algorithms are sound and complete relative to the synthesis algorithm, i.e., they provide a diagnosis that makes the synthesis problem infeasible, and always terminate with a non-trivial specification that is feasible using the chosen synthesis method, when such a solution exists. We demonstrate the effectiveness of our approach on controller synthesis for various cyber-physical systems, including an autonomous driving application and an aircraft electric power system.

We present a counterexample-guided inductive synthesis approach to controller synthesis for cyber-physical systems subject to signal temporal logic (STL) specifications, operating in potentially adversarial nondeterministic environments. We encode STL specifications as mixed integer-linear constraints on the variables of a discrete-time model of the system and environment dynamics, and solve a series of optimization problems to yield a satisfying control sequence. We demonstrate how the scheme can be used in a receding horizon fashion to fulfill properties over unbounded horizons, and present experimental results for reactive controller synthesis for case studies in building climate control and autonomous driving.

We present a new framework for reactive synthesis that considers the dynamics of the robot when synthesizing correct-by-construction controllers for nonlinear systems. Many high-level synthesis approaches employ discrete abstractions to reason about the dynamics of the continuous system in a simplified manner. Often, these abstractions are expensive to compute. We circumvent the need to have detailed abstractions for nonlinear systems by proposing a framework for adapting abstractions based on partial solutions to the low-level controller synthesis problem. The contribution of this paper is a reactive synthesis algorithm that makes use of our adaptation procedure to update the high-level strategy each time the non-deterministic discrete abstraction is modified. We combine this with a verified low-level controller synthesis scheme capable of automatically synthesizing controllers for a wide class of nonlinear systems. This novel synthesis framework is demonstrated on a dynamical robot executing an autonomous inspection task.

Temporal logics have proven effective for correct-by-construction synthesis of controllers for a wide range of robotic applications. Receding horizon frameworks mitigate the computational intractability of reactive synthesis for temporal logic, but have thus far been limited by pursuing a single sequence of short horizon problems to the goal. We propose a receding horizon algorithm for reactive synthesis that automatically determines a path to the currently pursued goal at runtime, responding as needed to nondeterministic environment behavior. This is achieved by allowing each short horizon to have multiple local goals, and determining which local goal to pursue based on the current global goal, the currently perceived environment and a pre-computed invariant dependent on the global goal. We demonstrate the utility of this additional flexibility in grant-response tasks, using a search-and-rescue example. Moreover, we show that these goal-dependent invariants mitigate the conservativeness of the receding horizon approach.

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.

This paper addresses the problem of designing control schemes for teams of robots engaged in complex highlevel tasks. It presents a method for automatically creating hybrid controllers that ensure that a team of possibly heterogeneous robots satisfies a user-defined high-level task. The proposed approach relaxes constraints on the simultaneous and interleaved motion of the robots, while maintaining constraints on their relative location to guarantee collision-avoidance and prevent deadlock. The approach is demonstrated in the context of a team of robots engaged in sorting objects for recycling.

This paper considers a team of cooperative, homogeneous robots operating in a nondeterministic environment, performing complex high-level tasks. We concurrently solve the problems of dynamic task assignment and reactive planning in a centralized fashion, allowing goal reassignment as needed in response to changes in the environment. To this end, we model the team of robots as a switched system whose various modes must be activated to satisfy high-level specifications, and describe a formal framework for synthesizing switching protocols for this system. The robots' continuous dynamics under a specific task allocation, as well as their operating environment, are encoded as formulas on a discrete abstraction, in the GR(1) fragment of linear temporal logic. The synthesized protocols ensure that the multi-robot task is fulfilled even in adversarial environments, and the presented abstraction provides a significant computational improvement over previous approaches. We illustrate these ideas in simulation, with applications to intrusion detection and surveillance.

Formal methods have recently been successfully applied to construct verifiable high-level robot control. Most approaches use a discrete abstraction of the underlying continuous domain, and make simplifying assumptions about the physical execution of actions given a discrete implementation. Relaxing these assumptions unearths a number of challenges in the continuous implementation of automatically-synthesized hybrid controllers. This paper describes a controller-synthesis framework that ensures correct continuous behaviors by explicitly modeling the activation and completion of continuous low-level controllers. The synthesized controllers exhibit desired properties like immediate reactiveness to sensor events and guaranteed safety of physical executions. The approach extends to any number of robot actions with arbitrary relative timings.

High-level robot control has recently seen the application of formal methods to the automatic synthesis of correct-by-construction controllers from user-defined specifications. When a specification fails to yield a corresponding controller, existing techniques provide feedback on portions of the specification that cause the failure, but at a coarse granularity. This work provides techniques for extracting minimal explanations of such failures. The approach is shown to provide refinement of the feedback on several example specifications.

A key challenge in robotics is the generation of controllers for autonomous, high-level robot behaviors comprising nontrivial sequences of actions, including reactive and repeated tasks. When constructing controllers to fulfill such tasks, it is often not known a priori whether the intended behavior is even feasible; plans are modified on the fly to deal with failures that occur during execution, often still without guaranteeing correct behavior. Recently, formal methods have emerged as a powerful tool to automatically generate autonomous robot controllers that guarantee desired behaviors expressed by a class of temporal logic specifications. However, when the specification cannot be fulfilled, these approaches do not provide the user with a source of failure, making the troubleshooting of specifications an unstructured and time-consuming process. This paper describes an algorithm to automatically analyze an unsynthesizable specification in order to identify causes of failure. It also introduces an interactive game to explore possible causes of unsynthesizability, in which the user attempts to fulfill the robot specification against an adversarial environment. The proposed algorithm and game are implemented as features within the LTLMoP toolkit for robot mission planning.

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.

One of the main challenges in robotics is the generation of controllers for autonomous, high-level robot behaviors comprising a non-trivial sequence of actions. Recently, formal methods have emerged as a powerful tool for automatically generating autonomous robot controllers that guarantee desired behaviors expressed by a class of temporal logic specifications. However, when there is no controller that fulfills the specification, these approaches do not provide the user with a source of failure, making the troubleshooting of specifications an unstructured and time-consuming process. In this paper, we describe a procedure for analyzing an unsynthesizable specification to identify causes of failure. We also provide an interactive game for exploring possible causes of failure, in which the user attempts to fulfill the robot specification against an adversarial environment. Our approach is implemented within the LTLMoP toolkit for robot mission planning.

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.

This paper addresses the challenge of incorporating event memory into the automatic synthesis of hybrid controllers for high-level reactive robot behavior. The goal is to provide a natural, concise grammar for specifying high-level tasks that require remembering past events, and to ensure that the required memory is correctly updated during controller execution. To this end, a structured English grammar for specifying high level behavior is provided 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 action sequences, etc. The proposed framework also guarantees the correctness of memory operations during continuous execution. The approach is implemented within the LTLMoP toolkit for reactive mission planning.

Halpern, Moses and Tuttle presented a definition of interactive proofs using a notion they called practical knowledge, but left open the question of finding an epistemic formula that completely characterizes zero knowledge; that is, a formula that holds iff a proof is zero knowledge. We present such a formula, and show that it does characterize zero knowledge. Moreover, we show that variants of the formula characterize variants of zero knowledge such as concurrent zero knowledge [Dwork, Naor, and Sahai 2004] and proofs of knowledge [Feige, Fiat, and Shamir 1987; Tompa and Woll 1987].