Meeko M. K. Oishi

Abraham P. Vinod, Meeko M. K. Oishi

Probabilistic guarantees of safety and performance are important in constrained dynamical systems with stochastic uncertainty. We consider the stochastic reachability problem, which maximizes the probability that the state remains within time-varying state constraints (i.e., a ``target tube''), despite bounded control authority. This problem subsumes the stochastic viability and terminal hitting-time stochastic reach-avoid problems. Of special interest is the stochastic reach set, the set of all initial states from which it is possible to stay in the target tube with a probability above a desired threshold. We provide sufficient conditions under which the stochastic reach set is closed, compact, and convex, and provide an underapproximative interpolation technique for stochastic reach sets. Utilizing convex optimization, we propose a scalable and grid-free algorithm that computes a polytopic underapproximation of the stochastic reach set and synthesizes an open-loop controller. This algorithm is anytime, i.e., it produces a valid output even on early termination. We demonstrate the efficacy and scalability of our approach on several numerical examples, and show that our algorithm outperforms existing software tools for verification of linear systems.

Abraham P. Vinod, Baisravan Homchaudhuri, Meeko M. K. Oishi

We propose a scalable method for forward stochastic reachability analysis for uncontrolled linear systems with affine disturbance. Our method uses Fourier transforms to efficiently compute the forward stochastic reach probability measure (density) and the forward stochastic reach set. This method is applicable to systems with bounded or unbounded disturbance sets. We also examine the convexity properties of the forward stochastic reach set and its probability density. Motivated by the problem of a robot attempting to capture a stochastically moving, non-adversarial target, we demonstrate our method on two simple examples. Where traditional approaches provide approximations, our method provides exact analytical expressions for the densities and probability of capture.

Joshua Pilipovsky, Vignesh Sivaramakrishnan, Meeko M. K. Oishi et al.

Verifying the input-output relationships of a neural network so as to achieve some desired performance specification is a difficult, yet important, problem due to the growing ubiquity of neural nets in many engineering applications. We use ideas from probability theory in the frequency domain to provide probabilistic verification guarantees for ReLU neural networks. Specifically, we interpret a (deep) feedforward neural network as a discrete dynamical system over a finite horizon that shapes distributions of initial states, and use characteristic functions to propagate the distribution of the input data through the network. Using the inverse Fourier transform, we obtain the corresponding cumulative distribution function of the output set, which can be used to check if the network is performing as expected given any random point from the input set. The proposed approach does not require distributions to have well-defined moments or moment generating functions. We demonstrate our proposed approach on two examples, and compare its performance to related approaches.

Adam J. Thorpe, Cyrus Neary, Franck Djeumou et al.

Data-driven control algorithms use observations of system dynamics to construct an implicit model for the purpose of control. However, in practice, data-driven techniques often require excessive sample sizes, which may be infeasible in real-world scenarios where only limited observations of the system are available. Furthermore, purely data-driven methods often neglect useful a priori knowledge, such as approximate models of the system dynamics. We present a method to incorporate such prior knowledge into data-driven control algorithms using kernel embeddings, a nonparametric machine learning technique based in the theory of reproducing kernel Hilbert spaces. Our proposed approach incorporates prior knowledge of the system dynamics as a bias term in the kernel learning problem. We formulate the biased learning problem as a least-squares problem with a regularization term that is informed by the dynamics, that has an efficiently computable, closed-form solution. Through numerical experiments, we empirically demonstrate the improved sample efficiency and out-of-sample generalization of our approach over a purely data-driven baseline. We demonstrate an application of our method to control through a target tracking problem with nonholonomic dynamics, and on spring-mass-damper and F-16 aircraft state prediction tasks.

Abraham P. Vinod, Meeko M. K. Oishi

We present a scalable underapproximation of the terminal hitting time stochastic reach-avoid probability at a given initial condition, for verification of high-dimensional stochastic LTI systems. While several approximation techniques have been proposed to alleviate the curse of dimensionality associated with dynamic programming, these techniques are limited and cannot handle larger, more realistic systems. We present a scalable method that uses Fourier transforms to compute an underapproximation of the reach-avoid probability for systems with disturbances with arbitrary probability densities. We characterize sufficient conditions for Borel-measurability of the value functions. We exploit fixed control sequences parameterized by the initial condition (an open-loop control policy) to generate the underapproximation. For Gaussian disturbances, the underapproximation can be obtained using existing efficient algorithms by solving a convex optimization problem. Our approach produces non-trivial lower bounds and is demonstrated on a chain of integrators with 40 states.

Baisravan HomChaudhuri, Abraham P. Vinod, Meeko M. K. Oishi

We propose a method to efficiently compute the forward stochastic reach (FSR) set and its probability measure for nonlinear systems with an affine disturbance input, that is stochastic and bounded. This method is applicable to systems with an a priori known controller, or to uncontrolled systems, and often arises in problems in obstacle avoidance in mobile robotics. When used as a constraint in finite horizon controller synthesis, the FSR set, and its probability measure facilitates probabilistic collision avoidance, in contrast to methods which presume the obstacles act in a worst-case fashion and generate hard constraints that cannot be violated. We tailor our approach to accommodate rigid body constraints, and show convexity is assured so long as the rigid body shape of each obstacle is also convex. We extend methods for multi-obstacle avoidance through mixed integer linear programming (with linear robot and obstacle dynamics) to accommodate chance constraints that represent the FSR set probability measure. We demonstrate our method on a rigid-body obstacle avoidance scenario, in which a receding horizon controller is designed to avoid several stochastically moving obstacles while reaching the desired goal. Our approach can provide solutions when approaches that presume a worst-case action from the obstacle fail.

Adam J. Thorpe, Meeko M. K. Oishi

We present SOCKS, a data-driven stochastic optimal control toolbox based in kernel methods. SOCKS is a collection of data-driven algorithms that compute approximate solutions to stochastic optimal control problems with arbitrary cost and constraint functions, including stochastic reachability, which seeks to determine the likelihood that a system will reach a desired target set while respecting a set of pre-defined safety constraints. Our approach relies upon a class of machine learning algorithms based in kernel methods, a nonparametric technique which can be used to represent probability distributions in a high-dimensional space of functions known as a reproducing kernel Hilbert space. As a nonparametric technique, kernel methods are inherently data-driven, meaning that they do not place prior assumptions on the system dynamics or the structure of the uncertainty. This makes the toolbox amenable to a wide variety of systems, including those with nonlinear dynamics, black-box elements, and poorly characterized stochastic disturbances. We present the main features of SOCKS and demonstrate its capabilities on several benchmarks.

Adam J. Thorpe, Thomas Lew, Meeko M. K. Oishi et al.

We present a data-driven algorithm for efficiently computing stochastic control policies for general joint chance constrained optimal control problems. Our approach leverages the theory of kernel distribution embeddings, which allows representing expectation operators as inner products in a reproducing kernel Hilbert space. This framework enables approximately reformulating the original problem using a dataset of observed trajectories from the system without imposing prior assumptions on the parameterization of the system dynamics or the structure of the uncertainty. By optimizing over a finite subset of stochastic open-loop control trajectories, we relax the original problem to a linear program over the control parameters that can be efficiently solved using standard convex optimization techniques. We demonstrate our proposed approach in simulation on a system with nonlinear non-Markovian dynamics navigating in a cluttered environment.

Joseph D. Gleason, Abraham P. Vinod, Meeko M. K. Oishi

In this paper we examine how Lagrangian techniques can be used to compute underapproximations and overapproximation of the finite-time horizon, stochastic reach-avoid level sets for discrete-time, nonlinear systems. This approach is applicable for a generic nonlinear system without any convexity assumptions on the safe and target sets. We examine and apply our methods on the reachability of a target tube problem, a more generalized version of the finite-time horizon reach-avoid problem. Because these methods utilize a Lagrangian (set theoretic) approach, we eliminate the necessity to grid the state, input, and disturbance spaces allowing for increased scalability and faster computation. The methods scalability are currently limited by the computational requirements for performing the necessary set operations by current computational geometry tools. The primary trade-off for this improved extensibility is conservative approximations of actual stochastic reach set. We demonstrate these methods on several examples including the standard double-integrator, a chain of integrators, and a 4-dimensional space vehicle rendezvous docking problem.

Abraham P. Vinod, Meeko M. K. Oishi

We present theory and algorithms for the computation of probability-weighted "keep-out" sets to assure probabilistically safe navigation in the presence of multiple rigid body obstacles with stochastic dynamics. Our forward stochastic reachability-based approach characterizes the stochasticity of the future obstacle states in a grid-free and recursion-free manner, using Fourier transforms and computational geometry. We consider discrete-time Markovian switched systems with affine parameter-varying stochastic subsystems (DMSP) as the obstacle dynamics, which includes Markov jump affine systems and discrete-time affine parameter-varying stochastic systems (DPV). We define a probabilistic occupancy function, to describe the probability that a given state is occupied by a rigid body obstacle with stochastic dynamics at a given time; keep-out sets are the super-level sets of this occupancy function. We provide sufficient conditions that ensure convexity and compactness of these keep-out sets for DPV obstacle dynamics. We also propose two computationally efficient algorithms to overapproximate the keep-out sets --- a tight polytopic approximation using projections, and an overapproximation using Minkowski sum. For DMSP obstacle dynamics, we compute a union of convex and compact sets that covers the potentially non-convex keep-out set. Numerical simulations show the efficacy of the proposed algorithms for a modified version of the classical unicycle dynamics, modeled as a DMSP.