The brief history of human-robot teams can be traced through the changing perspective of a robot's role within the team, which has evolved from being treated as a tool to a recent shift toward the desire to have the robot act as an equal partner. While researchers have made tremendous strides in recent years, "making robots into team players" [1] that can work with humans as peers still presents a multitude of challenges. One key characteristic of a synergistic team is the ability to intervene or backup each other as necessary (e.g., when the other is underperforming). Hence, in this article, we formulate distributed human-robot teamwork in the framework of mixed-initiative interaction, which is an interaction strategy that lets the best-suited member of the team to perform the work by allowing team members to interleave their contributions to the overall team performance through opportunistic seizure and relinquishment of task initiatives. Specifically, this paper aims to address the issue of initiative decision-making - that is, when should a robot take over (relinquish) control from (to) a human teammate.

A key challenge in the automatic verification of robot mission software, especially critical mission software, is to be able to effectively model the performance of a human operator and factor that into the formal performance guarantees for the mission. We present a novel approach to modelling the skill level of the operator and integrating it into automatic verification using a linear Gaussians model parameterized by experimental calibration. Our approach allows us to model different skill levels directly in terms of the behavior of the lumped, robot plus operator, system. Using MissionLab and VIPARS (a behavior-based robot mission verification module), we present a comparison of our predicted performance guarantees for two missions in which a teleoperated quadrotor identifies a target for an autonomous ground robot to intercept: one mission in which the operator flies the quadrotor by line of sight to locate the target and one where the operator flies the quadrotor using its video feed. We demonstrate the effectiveness of our approach by comparing predicated performance to experimentally measured performance.

Localization and mapping algorithms can allow a robot to navigate well in an unknown environment. However, whether such algorithms enhance any specific robot mission is currently a matter for empirical validation. In this paper we apply our MissionLab/VIPARS mission design and verification approach to an autonomous robot mission that uses probabilistic localization software. Two approaches to modeling probabilistic localization for verification are presented: a high-level approach, and a sample-based approach which allows run-time code to be embedded in verification. Verification and experimental validation results are presented for two different missions, each using each method, demonstrating the accuracy of verification, and both are compared with verification of an odometry-only mission, to show the mission-specific benefit of localization.

The effective use of autonomous robot teams in highly-critical missions depends on being able to establish performance guarantees. However, establishing a guarantee for the behavior of an autonomous robot operating in an uncertain environment with obstacles is a challenging problem. This paper addresses the challenges involved in building a software tool for verifying the behavior of a multi-robot waypoint mission that includes uncertain environment geometry as well as uncertainty in robot motion. One contribution of this paper is an approach to the problem of a-priori specification of uncertain environments for robot program verification. A second contribution is a novel method to extend the Bayesian Network formulation to reason about random variables with different subpopulations, introduced to address the challenge of representing the effects of multiple sensory histories when verifying a robot mission. The third contribution is experimental validation results presented to show the effectiveness of this approach on a two-robot, bounding overwatch mission.

The objectives of this article are: 1) to present a taxonomy for mixed-initiative human-robot interaction and 2) to survey its state of practice through the examination of past research along each taxonomical dimension. The paper starts with some definitions of mixed-initiative interaction (MII) from the perspective of human-computer interaction (HCI) to introduce the basic concepts of MII. We then synthesize these definitions to the robotic context for mixed-initiative human robot teams. A taxonomy for mixed-initiative in human-robot interaction is then presented. The goal of the taxonomy is to inform the design of mixed-initiative human-robot systems by identifying key elements of these systems. The state of practice of mixed-initiative human-robot interaction is then surveyed and examined along each taxonomical dimension.

Certain robot missions need to perform predictably in a physical environment that may have significant uncertainty. One approach is to leverage automatic software verification techniques to establish a performance guarantee. The addition of an environment model and uncertainty in both program and environment, however, means that the state space of a model-checking solution to the problem can be prohibitively large. An approach based on behavior-based controllers in a process-algebra framework that avoids state-space combinatorics is presented here. In this approach, verification of the robot program in the uncertain environment is reduced to a filtering problem for a Bayesian network. Validation results are presented for the verification of a multiple-waypoint and an autonomous exploration robot mission.

We have developed an approach that can be used by mission designers to determine whether or not a performance guarantee for their mission software, when carried out under the uncertain conditions of a real-world environment, will hold within a threshold probability. In this paper we demonstrate its utility for verifying multirobot missions, in particular a bounding overwatch mission.

Certain robot missions need to perform predictably in a physical environment that may only be poorly characterized in advance. We have previously developed an approach to establishing performance guarantees for behavior-based controllers in a process-algebra framework. We extend that work here to include random variables, and we show how our prior results can be used to generate a Dynamic Bayesian Network for the coupled system of program and environment model. Verification is reduced to a filtering problem for this network. Finally, we present validation results that demonstrate the effectiveness of the verification of a multiple waypoint robot mission using this approach.

This paper describes the need and methods required to construct an integrated software verification and mission specification system for use in robotic missions intended for counter-weapons of mass destruction (c-WMD) operations, as part of a 3-year effort for the Defense Threat Reduction Agency. The overall system architecture is described. The principal tool for verification is a process algebra, PARS, based on port automata theory. PARS is introduced, emphasizing its ability to represent probabilistic programs and uncertain and dynamic environments, followed by the analysis of mission properties for an example robotic mission.