arXiv subjects

Hadas Kress-Gazit

Publications and source records attributed to Hadas Kress-Gazit.

34 records · Page 2Linked to original sources

arXiv2022

Automated Task Updates of Temporal Logic Specifications for Heterogeneous Robots

Given a heterogeneous group of robots executing a complex task represented in Linear Temporal Logic, and a new set of tasks for the group, we define the task update problem and propose a framework for automatically updating individual robot tasks given their respective existing tasks and capabilities. Our heuristic, token-based, conflict resolution task allocation algorithm generates a near-optimal assignment for the new task. We demonstrate the scalability of our approach through simulations of multi-robot tasks.

cs.RO↗

arXiv2022

Automatic Encoding and Repair of Reactive High-Level Tasks with Learned Abstract Representations

We present a framework that, given a set of skills a robot can perform, abstracts sensor data into symbols that we use to automatically encode the robot's capabilities in Linear Temporal Logic. We specify reactive high-level tasks based on these capabilities, for which a strategy is automatically synthesized and executed on the robot, if the task is feasible. If a task is not feasible given the robot's capabilities, we present two methods, one enumeration-based and one synthesis-based, for automatically suggesting additional skills for the robot or modifications to existing skills that would make the task feasible. We demonstrate our framework on a Baxter robot manipulating blocks on a table, a Baxter robot manipulating plates on a table, and a Kinova arm manipulating vials, with multiple sensor modalities, including raw images.

cs.RO↗

arXiv2022

Elliptical Slice Sampling for Probabilistic Verification of Stochastic Systems with Signal Temporal Logic Specifications

Autonomous robots typically incorporate complex sensors in their decision-making and control loops. These sensors, such as cameras and Lidars, have imperfections in their sensing and are influenced by environmental conditions. In this paper, we present a method for probabilistic verification of linearizable systems with Gaussian and Gaussian mixture noise models (e.g. from perception modules, machine learning components). We compute the probabilities of task satisfaction under Signal Temporal Logic (STL) specifications, using its robustness semantics, with a Markov Chain Monte-Carlo slice sampler. As opposed to other techniques, our method avoids over-approximations and double-counting of failure events. Central to our approach is a method for efficient and rejection-free sampling of signals from a Gaussian distribution such that satisfy or violate a given STL formula. We show illustrative examples from applications in robot motion planning.

eess.SY↗

arXiv2021

Synthesizing Modular Manipulators For Tasks With Time, Obstacle, And Torque Constraints

Modular robots can be tailored to achieve specific tasks and rearranged to achieve previously infeasible ones. The challenge is choosing an appropriate design from a large search space. In this work, we describe a framework that automatically synthesizes the design and controls for a serial chain modular manipulator given a task description. The task includes points to be reached in the 3D space, time constraints, a load to be sustained at the end-effector, and obstacles to be avoided in the environment. These specifications are encoded as a constrained optimization in the robot's kinematics and dynamics and, if a solution is found, the formulation returns the specific design and controls to perform the task. Finally, we demonstrate our approach on a complex specification in which the robot navigates a constrained environment while holding an object.

cs.RO↗

arXiv2021

Counterexample-Guided Repair for Symbolic-Geometric Action Abstractions

Integrated Task and Motion Planning (TMP) provides a promising class of approaches for solving robot planning problems with intricate symbolic and geometric constraints. However, the practical usefulness of TMP planners is limited by their need for symbolic abstractions of robot actions, which are difficult to construct even for experts. We propose an approach to automatically construct and continuously improve a symbolic abstraction of a robot action via observations of the robot performing the action. This approach, called automatic abstraction repair, allows symbolic abstractions to be initially incorrect or incomplete and converge toward a correct model over time. Abstraction repair uses constrained polynomial zonotopes (CPZs), an efficient non-convex set representation, to model predicates over joint symbolic and geometric state, and performs an optimizing search over symbolic edit operations to predicate formulae to improve the correspondence of a symbolic abstraction to the behavior of a physical robot controller. In this work, we describe the aforementioned predicate model, introduce the symbolic-geometric abstraction repair problem, and present an anytime algorithm for automatic abstraction repair. We then demonstrate that abstraction repair can improve realistic action abstractions for common mobile manipulation actions from a handful of observations.

cs.RO↗

arXiv2021

Learning and Planning for Temporally Extended Tasks in Unknown Environments

We propose a novel planning technique for satisfying tasks specified in temporal logic in partially revealed environments. We define high-level actions derived from the environment and the given task itself, and estimate how each action contributes to progress towards completing the task. As the map is revealed, we estimate the cost and probability of success of each action from images and an encoding of that action using a trained neural network. These estimates guide search for the minimum-expected-cost plan within our model. Our learned model is structured to generalize across environments and task specifications without requiring retraining. We demonstrate an improvement in total cost in both simulated and real-world experiments compared to a heuristic-driven baseline.

cs.RO↗

arXiv2021

Event-Based Signal Temporal Logic Synthesis for Single and Multi-Robot Tasks

We propose a new specification language and control synthesis technique for single and multi-robot high-level tasks; these tasks include timing constraints and reaction to environmental events. Specifically, we define Event-based Signal Temporal Logic (STL) and use it to encode tasks that are reactive to uncontrolled environment events. Our control synthesis approach to Event-based STL tasks combines automata and control barrier functions to produce robot behaviors that satisfy the specification when possible. Our method automatically provides feedback to the user if an Event-based STL task can not be achieved. We demonstrate the effectiveness of the framework through simulations and physical demonstrations of multi-robot tasks.

cs.RO↗

arXiv2020

Formalizing and Guaranteeing* Human-Robot Interaction

Robot capabilities are maturing across domains, from self-driving cars, to bipeds and drones. As a result, robots will soon no longer be confined to safety-controlled industrial settings; instead, they will directly interact with the general public. The growing field of Human-Robot Interaction (HRI) studies various aspects of this scenario - from social norms to joint action to human-robot teams and more. Researchers in HRI have made great strides in developing models, methods, and algorithms for robots acting with and around humans, but these "computational HRI" models and algorithms generally do not come with formal guarantees and constraints on their operation. To enable human-interactive robots to move from the lab to real-world deployments, we must address this gap. This article provides an overview of verification, validation and synthesis techniques used to create demonstrably trustworthy systems, describes several HRI domains that could benefit from such techniques, and provides a roadmap for the challenges and the research needed to create formalized and guaranteed human-robot interaction.

cs.RO↗

arXiv2019

The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems

In formal synthesis of reactive systems an implementation of a system is automatically constructed from its formal specification. The great advantage of synthesis is that the resulting implementation is correct by construction; therefore there is no need for manual programming and tedious debugging tasks. Developers remain, nevertheless, hesitant to using automatic synthesis tools and still favor manually writing code. A common argument against synthesis is that the resulting implementation does not always give a clear picture on what decisions were made during the synthesis process. The outcome of synthesis tools is mostly unreadable and hinders the developer from understanding the functionality of the resulting implementation. Many attempts have been made in the last years to make the synthesis process more transparent to users. Either by structuring the outcome of synthesis tools or by providing additional automated support to help users with the specification process. In this paper we discuss the challenges in writing specifications for reactive systems and give a survey on what tools have been developed to guide users in specifying reactive systems and understanding the outcome of synthesis tools.

cs.LO↗

arXiv2018

An Integrated System for Perception-Driven Autonomy with Modular Robots

The theoretical ability of modular robots to reconfigure in response to complex tasks in a priori unknown environments has frequently been cited as an advantage and remains a major motivator for work in the field. We present a modular robot system capable of autonomously completing high-level tasks by reactively reconfiguring to meet the needs of a perceived, a priori unknown environment. The system integrates perception, high-level planning, and modular hardware, and is validated in three hardware demonstrations. Given a high-level task specification, a modular robot autonomously explores an unknown environment, decides when and how to reconfigure, and manipulates objects to complete its task. The system architecture balances distributed mechanical elements with centralized perception, planning, and control. By providing an example of how a modular robot system can be designed to leverage reactive reconfigurability in unknown environments, we have begun to lay the groundwork for modular self-reconfigurable robots to address tasks in the real world.

cs.RO↗

arXiv2018

Accomplishing High-Level Tasks with Modular Robots

The advantage of modular self-reconfigurable robot systems is their flexibility, but this advantage can only be realized if appropriate configurations (shapes) and behaviors (controlling programs) can be selected for a given task. In this paper, we present an integrated system for addressing high-level tasks with modular robots, and demonstrate that it is capable of accomplishing challenging, multi-part tasks in hardware experiments. The system consists of four tightly integrated components: (1) A high-level mission planner, (2) A large design library spanning a wide set of functionality, (3) A design and simulation tool for populating the library with new configurations and behaviors, and (4) modular robot hardware. This paper builds on earlier work by the authors, extending the original system to include environmentally adaptive parametric behaviors, which integrate motion planners and feedback controllers with the system.

cs.RO↗

arXiv2018

Perception-Informed Autonomous Environment Augmentation With Modular Robots

We present a system enabling a modular robot to autonomously build structures in order to accomplish high-level tasks. Building structures allows the robot to surmount large obstacles, expanding the set of tasks it can perform. This addresses a common weakness of modular robot systems, which often struggle to traverse large obstacles. This paper presents the hardware, perception, and planning tools that comprise our system. An environment characterization algorithm identifies features in the environment that can be augmented to create a path between two disconnected regions of the environment. Specially-designed building blocks enable the robot to create structures that can augment the environment to make obstacles traversable. A high-level planner reasons about the task, robot locomotion capabilities, and environment to decide if and where to augment the environment in order to perform the desired task. We validate our system in hardware experiments

cs.RO↗

arXiv2017

Robot-Initiated Specification Repair through Grounded Language Interaction

Robots are required to execute increasingly complex instructions in dynamic environments, which can lead to a disconnect between the user's intent and the robot's representation of the instructions. In this paper we present a natural language instruction grounding framework which uses formal synthesis to enable the robot to identify necessary environment assumptions for the task to be successful. These assumptions are then expressed via natural language questions referencing objects in the environment. The user is prompted to confirm or reject the assumption. We demonstrate our approach on two tabletop pick-and-place tasks.

cs.RO↗

arXiv2017

Resource-Performance Trade-off Analysis for Mobile Robot Design

The design of mobile autonomous robots is challenging due to the limited on-board resources such as processing power and energy. A promising approach is to generate intelligent schedules that reduce the resource consumption while maintaining best performance, or more interestingly, to trade off reduced resource consumption for a slightly lower but still acceptable level of performance. In this paper, we provide a framework to aid designers in exploring such resource-performance trade-offs and finding schedules for mobile robots, guided by questions such as "what is the minimum resource budget required to achieve a given level of performance?" The framework is based on a quantitative multi-objective verification technique which, for a collection of possibly conflicting objectives, produces the Pareto front that contains all the optimal trade-offs that are achievable. The designer then selects a specific Pareto point based on the resource constraints and desired performance level, and a correct-by-construction schedule that meets those constraints is automatically generated. We demonstrate the efficacy of this framework on several robotic scenarios in both simulations and experiments with encouraging results.

cs.RO↗

arXiv2016

Dynamics-Based Reactive Synthesis and Automated Revisions for High-Level Robot Control

The aim of this work is to address issues where formal specifications cannot be realized on a given dynamical system subjected to a changing environment. Such failures occur whenever the dynamics of the system restrict the robot in such a way that the environment may prevent the robot from progressing safely to its goals. We provide a framework that automatically synthesizes revisions to such specifications that restrict the assumed behaviors of the environment and the behaviors of the system. We provide a means for explaining such modifications to the user in a concise, easy-to-understand manner. Integral to the framework is a new algorithm for synthesizing controllers for reactive specifications that include a discrete representation of the robot's dynamics. The new approach is demonstrated with a complex task implemented using a unicycle model.

cs.RO↗

arXiv2014

Unsynthesizable Cores - Minimal Explanations for Unsynthesizable High-Level Robot Behaviors

With the increasing ubiquity of multi-capable, general-purpose robots arises the need for enabling non-expert users to command these robots to perform complex high-level tasks. To this end, high-level robot control has seen the application of formal methods to automatically synthesize correct-by-construction controllers from user-defined specifications; synthesis fails if and only if there exists no controller that achieves the specified behavior. Recent work has also addressed the challenge of providing easy-to-understand feedback to users when a specification fails to yield a corresponding controller. Existing techniques provide feedback on portions of the specification that cause the failure, but do so at a coarse granularity. This work presents techniques for refining this feedback, extracting minimal explanations of unsynthesizability.

cs.RO↗