Popper

Sampling-based Verification and Falsification

Karl Popper and Falsifiability on wikipedia

People

Faculty: Vijay Kumar

Post Doc: Peng Cheng

Ph.D. Student: Jongwoo Kim

Staff: Gilad Buchman, Jim Keller

OpenGL-based 3D visualization of the trajectories of systems

Project description:

Popper is a toolbox that facilitates the verification of planners for a complex, dynamic system with uncertainties. Verification is achieved by modeling adversarial agents and all sources of uncertainties and disturbances and by attempting to find falsifying conditions. A plan is said to be verified for a finite time horizon if Popper cannot find a set of falsifying inputs for the plan that violates the specifications for the planner. Falsifying inputs, when found, serve as counter examples for the planner and as an aid to design better planning algorithms.

Popper has been applied to the verification of planners for multiple heterogeneous unmanned vehicles in the presence of uncertainties. See here for a case study describing the application to surveillance in the presence of adversarial agents.

A class of problems:

The problems include two Teams, called Player Team and Adversary Team, of vehicles. The vehicles could be man-controlled, such as Unmanned Aerial Vehicles, Unmanned Undersea Vehicles, and Unmanned Surface Vehicle. Several natural objects, such as severe weather, are also abstracted as the nature-controlled vehicle in this project.

A motion plan is given for Player Team to complete a task, which is described by spatial-temporal constraints on trajectories of two teams. Typical constraints include collision avoidance, fuel consumption, and maximal radar exposure. Adversary Team tries to fail the task of Player Team by violating the spatical-temporal constraints.

The objectives of this class of problems include:

1) Design falsification algorithms to find falsification controls for Adversary Team such that Player Team fails its task.

2) Design verification algorithms to prove that there are no falsification controls for Adversary Team.

Method Overview:

Because the search space, including the control space and state space, of the problems are continuous and a finite and exact representation is generally not available, sampled controls and states are used to approximate the search space.

Sampling-based falsification algorithms search for solutions by iteratively constructing search graphs with sampled controls and states. The search graph is initialized with a finite number of nodes, each of which is associated with an initial state. In each iteration, a node in the search graph is first chosen, a sample control is used to generate a trajectory segment from the state of the node, and the search graph is updated with the trajectory segment. If the current trajectories violate the task constraints, then a falsification control is returned. Otherwise, the algorithm will keep running until a given termination condition is satisfied.

Verification is achieved through resolution complete falsification algorithms, which will approximate every falsification controls in finite time. Reversely, if no solution control is returned from a falsification algorithm, then the given motion plan is verified.

System Overview

The system is designed to be independent of the actual implementation of the simulator or the planner. The Simulator, Planner and the Verification/Falsification Module are communicating through XML messages using a defined protocol.


Display of the projection of the search graph and solution paths

Example

Scenario: A reconnaissance task is given to a UAV. its task is to take pictures of an enemy facility while avoiding the severe weather, and excessive exposure to the radar mounted on a UGV. For more detailed explanation (ppt)

The UAV will fail in its task if it runs into the severe weather region, accumulates too much radar exposure, and takes too much time (fuel constraint).

click on diagram to play movie

In this sample movie Popper found trajectories for the UGV and Weather system that failed the UAV task. The task failed because the UAV flight time exceeds the allowed time limit. The time limit in this case is 10% more than the time it takes to fly stright to the target and come back.

More Examples:

References:

  • Peng Cheng and Vijay Kumar,"Sampling-based Falsification and Verification of Controllers for Continuous Dynamic Systems", The Seventh International Workshop on the Algorithmic Foundations of Robotics, 2006. (pdf).
  • Peng Cheng,"Verification Problem Formulation and Sampling-Based Methods" (pdf).
  • Jongwoo Kim, Joel M. Esposito, and Vijay Kumar, "An RRT-based Algorithm for Testing and Validating Multi-Robot Controllers," Robotics: Science and Systems, Cambridge, MA, June 2005. (pdf)

The code for this project can be found at https://svn.cis.upenn.edu/svnroot/popper. To receive access please contact Gilad Buchman.