29 accepted papers
Robots fail, potentially leading to a loss in the robot’s perceived reliability (PR), a measure correlated with trustworthiness. In this study we examine how various kinds of failures affect the PR of the robot differently, and how this measure recovers without explicit social repair actions by the …
Recent work has demonstrated how one can write high-level specifications for swarm behaviors and automatically create controllers for the individual robots to achieve the overall swarm task. In this paper, we address the question of how to modify, during execution, the desired behavior while maintai
Recent work has demonstrated how one can write high-level specifications for swarm behaviors and automatically create controllers for the individual robots to achieve the overall swarm task. In this paper, we address the question of how to modify, during execution, the desired behavior while maintai…
Given a collaborative high-level task and a team of heterogeneous robots with behaviors to satisfy it, this work focuses on the challenge of automatically adjusting the individual robot behaviors at runtime such that the task is still satisfied. We specifically address scenarios when robots encounte
We propose an integrated planning framework for quadrupedal locomotion over dynamically changing, unforeseen terrains. Existing approaches either rely on heuristics for instantaneous foothold selection–compromising safety and versatility–or solve expensive trajectory optimization problems with compl
In this paper we present a grammar and control synthesis framework for online modification of Event-based Signal Temporal Logic (STL) specifications, during execution. These modifications allow a user to change the robots' task in response to potential future violations, changes to the environment,
We present a method for calculating the probability that a robot successfully performs a task described using Signal Temporal Logic (STL). We focus on cases where the failure probability is very small, hence a traditional Monte-Carlo method becomes inefficient due to the large number of samples requ…
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 capabilitie…
We propose a decentralized control algorithm for a minimalistic robotic swarm with limited capabilities such that the desired global behavior emerges. We consider the problem of searching for and encapsulating various targets present in the environment while avoiding collisions with both static and…
In this work, we synthesize control for high-level, reactive robot tasks that include timing constraints and choices over goals and constraints. We enrich Event-based Signal Temporal Logic by adding disjunctions, and propose a framework for synthesizing controllers that satisfy such specifications.
We develop a method for synthesizing control policies for stochastic, linear, time-varying systems that must perform tasks specified in signal temporal logic. We build upon an efficient, sampling-based framework that computes the probability of the system satisfying its specification. By exploiting…
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 reacti
Robots deployed in airports, malls, and stadiums today require expert oversight, pre-provided maps, and infrastructure. These systems are engineered to their specific deployment spaces and rely heavily on geometric maps for motion planning. In this work we consider a robot with only local-sensing an…
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…
In this work, we describe an end-to-end system for automatically synthesizing correct-by-construction structure and controls for modular manipulators from high-level task specifications. We define specifications that include both continuous trajectories the end-effector must follow and constraints o…
In this paper, we propose an abstraction that captures high-level formation and location-based swarm behaviors, and an automated control synthesis framework to generate correct-by-construction behaviors. Our abstraction includes symbols representing both possible formations and physical locations in…
Recently, Linear Temporal Logic (LTL) has been used as a formalism for defining high-level robot tasks, and LTL synthesis has been used to automatically create correct-by-construction robot control. The underlying premise of this approach is that the robot has a set of actions, or skills, that can b…
Soft robots utilize compliant materials to perform motions and behaviors not typically achievable by rigid bodied systems. These materials and soft actuator fabrication methods have been leveraged to create multigait walking soft robots. However, soft materials are prone to failure, restricting the…
This paper combines techniques from Formal Methods and Human-Robot Interaction (HRI) to address the challenge of a robot walking with a human while maintaining a socially acceptable distance and avoiding collisions. We formulate a set of constraints on the robot motion using Satisfiability Modulo Th…
We present a controller for human-robot handovers that is automatically synthesized from high-level specifications in Signal Temporal Logic (STL). In contrast to existing controllers, this approach can provide formal guarantees on the timing of each of the handover phases. Using synthesis also allow…
The great promise of modular robots is the ability to create on demand robots; however, choosing the “right” design based on a task is still a challenging problem. In this paper, we present an approach to automatically synthesize both the design and control for modular robots from a task description…
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 s…
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 tradeoff reduc
Current methods of grounding natural language instructions do not include reactive or temporal components, making these methods unsuitable for instructions describing tasks as sets of conditional instructions. We introduce the Verifiable Distributed Correspondence Graph (V-DCG) model, which enables…
The advantage of modular robot systems lies in their flexibility, but this advantage can only be realized if there exists some reliable, effective way of generating configurations (shapes) and behaviors (controlling programs) appropriate for a given task. In this paper, we present an end-to-end syst…
We consider multiple robots operating in a shared workspace, each given a high-level task specification in the form of Linear Temporal Logic (LTL) formulas. The robots have no a priori knowledge about the tasks of the other robots and might run into conflicts during task execution. In this work, we…
In this work, we take a step towards bridging the gap between the theory of formal synthesis and its application to real-world, complex, robotic systems. In particular, we present an end-to-end approach for the automatic generation of code that implements high-level robot behaviors in a verifiably c
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 simplif…
We consider two robots operating in a common workspace where each can sense the location of the other. Each robot has its own high-level task, given as a temporal logic formula, which may include requirements regarding the other robot (e.g. the robot cannot enter a room that the other robot is curre…