Computer Engineering Commons^™

Using Taint Analysis And Reinforcement Learning (Tarl) To Repair Autonomous Robot Software, Damian Lyons, Saba Zahra

Faculty Publications

It is important to be able to establish formal performance bounds for autonomous systems. However, formal verification techniques require a model of the environment in which the system operates; a challenge for autonomous systems, especially those expected to operate over longer timescales. This paper describes work in progress to automate the monitor and repair of ROS-based autonomous robot software written for an a-priori partially known and possibly incorrect environment model. A taint analysis method is used to automatically extract the data-flow sequence from input topic to publish topic, and instrument that code. A unique reinforcement learning approximation of MDP utility …

Drone Proximity Detection Via Air Disturbance Analysis, Qian Zhao, Jason Hughes

Faculty Publications

The use of unmanned aerial vehicles (drones) is expanding to commercial, scientific, and agriculture applications, including surveillance, product deliveries and aerial photography. One challenge for applications of drones is detecting obstacles and avoiding collisions. A typical solution to this issue is the use of camera sensors or ultrasonic sensors for obstacle detection or sometimes just manual control (teleoperation). However, these solutions have costs in battery lifetime, payload, operator skill. We note that there will be an air disturbance in the vicinity of the drone when it’s moving close to obstacles or other drones. Our objective is to detect obstacles from …

An Approach To Fast Multi-Robot Exploration In Buildings With Inaccessible Spaces, Matt Mcneill, Damian Lyons

Faculty Publications

The rapid exploration of unknown environments is a common application of autonomous multi-robot teams. For some types of exploration missions, a mission designer may possess some rudimentary knowledge about the area to be explored. For example, the dimensions of a building may be known, but not its floor layout or the location of furniture and equipment inside. For this type of mission, the Space- Based Potential Field (SBPF) method is an approach to multirobot exploration which leverages a priori knowledge of area bounds to determine robot motion. Explored areas and obstacles exert a repulsive force, and unexplored areas exert an …

A Comparison Of Contextual Bandit Approaches To Human-In-The-Loop Robot Task Completion With Infrequent Feedback, Matt Mcneill, Damian Lyons

Faculty Publications

Artificially intelligent assistive agents are playing an increased role in our work and homes. In contrast with currently predominant conversational agents, whose intelligence derives from dialogue trees and external modules, a fully autonomous domestic or workplace robot must carry out more complex reasoning. Such a robot must make good decisions as soon as possible, learn from experience, respond to feedback, and rely on feedback only as much as necessary. In this research, we narrow the focus of a hypothetical robot assistant to a room tidying task in a simulated domestic environment. Given an item, the robot chooses where to put …

Evaluation Of Field Of View Width In Stereo-Vision-Based Visual Homing, Damian Lyons, Benjamin Barriage, Luca Del Signore

Faculty Publications

Visual homing is a local navigation technique used to direct a robot to a previously seen location by comparing the image of the original location with the current visual image. Prior work has shown that exploiting depth cues such as image scale or stereo-depth in homing leads to improved homing performance. While it is not unusual to use a panoramic field of view (FOV) camera in visual homing, it is unusual to have a panoramic FOV stereo-camera. So, while the availability of stereo-depth information may improve performance, the concomitant-restricted FOV may be a detriment to performance, unless specialized stereo hardware …

Formal Performance Guarantees For An Approach To Human In The Loop Robot Missions, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract— 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 …

An Approach To Robust Homing With Stereovision, Fuqiang Fu, Damian Lyons

Faculty Publications

Visual Homing is a bioinspired approach to robot navigation which can be fast and uses few assumptions. However, visual homing in a cluttered and unstructured outdoor environment offers several challenges to homing methods that have been developed for primarily indoor environments. One issue is that any current image during homing may be tilted with respect to the home image. The second is that moving through a cluttered scene during homing may cause obstacles to interfere between the home scene and location and the current scene and location. In this paper, we introduce a robust method to improve a previous developed …

Performance Verification For Robot Missions In Uncertain Environments, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract—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 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 …

Establishing A-Priori Performance Guarantees For Robot Missions That Include Localization Software, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

One approach to determining whether an automated system is performing correctly is to monitor its performance, signaling when the performance is not acceptable; another approach is to automatically analyze the possible behaviors of the system a-priori and determine performance guarantees. Thea authors have applied this second approach to automatically derive performance guarantees for behaviorbased, multi-robot critical mission software using an innovative approach to formal verification for robotic software. 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. Several …

Formal Performance Guarantees For Behavior-Based Localization Missions, Damian Lyons, Ron Arkin, Shu Jiang, Matt O'Brien, Feng Tang, Peng Tang

Faculty Publications

Abstract— 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 …

Establishing Performance Guarantees For Behavior-Based Robot Missions Using An Smt Solver, Feng Tang, Damian M. Lyons, Ronald Arkin

Faculty Publications

In prior work we developed an approach to formally representing behavior-based multi-robot programs, and the uncertain environments in which they operate, as process networks. We automatically extract a set of probabilistic equations governing program execution in that environment using a static analysis module called VIPARS, and solve these using a Dynamic Bayesian Network (DBN) to establish whether stated performance guarantees hold for the program in that environment. In this paper we address the challenge of expanding the range of performance guarantees that are possible by using an SMT-solver instead of a DBN. We translate flow functions, which are recursive probabilistic …

Performance Verification For Behavior-Based Robot Missions, Damian M. Lyons, Ron Arkin, Shu Jiang, Tsungming Liu, Paramesh Nirmal

Faculty Publications

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 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 …

Getting It Right The First Time: Robot Mission Guarantees In The Presence Of Uncertainty, Damian Lyons, Ron Arkin, Paramesh Nirmal, Shu Jiang, Tsung-Ming Liu, Julia Deeb

Faculty Publications

Abstract—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 …