 NSFPAR ID:
 10233215
 Date Published:
 Journal Name:
 Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science, vol 12224
 Volume:
 12224
 Page Range / eLocation ID:
 604628
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this

In this paper, we study efficient approaches to reachability analysis for discretetime nonlinear dynamical systems when the dependencies among the variables of the system have low treewidth. Reachability analysis over nonlinear dynamical systems asks if a given set of target states can be reached, starting from an initial set of states. This is solved by computing conservative over approximations of the reachable set using abstract domains to represent these approximations. However, most approaches must tradeoff the level of conservatism against the cost of performing analysis, especially when the number of system variables increases. This makes reachability analysis challenging for nonlinear systems with a large number of state variables. Our approach works by constructing a dependency graph among the variables of the system. The tree decomposition of this graph builds a tree wherein each node of the tree is labeled with subsets of the state variables of the system. Furthermore, the tree decomposition satisfies important structural properties. Using the tree decomposition, our approach abstracts a set of states of the high dimensional system into a tree of sets of lower dimensional projections of this state. We derive various properties of this abstract domain, including conditions under which the original high dimensional set can be fully recovered from its low dimensional projections. Next, we use ideas from message passing developed originally for belief propagation over Bayesian networks to perform reachability analysis over the full state space in an efficient manner. We illustrate our approach on some interesting nonlinear systems with low treewidth to demonstrate the advantages of our approach.more » « less

N. Matni, M. Morari (Ed.)This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuoustime dynamical systems with neural network controllers. Given a neural network, we use an existing verification algorithm to construct inclusion functions for its inputoutput behavior. Inspired by mixed monotone theory, we embed the closedloop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the openloop system. This embedding provides a scalable approach for safety analysis of the neural control loop while preserving the nonlinear structure of the system. We show that one can efficiently compute hyperrectangular overapproximations of the reachable sets using a single trajectory of the embedding system. We design an algorithm to leverage this computational advantage through partitioning strategies, improving our reachable set estimates while balancing its runtime with tunable parameters. We demonstrate the performance of this algorithm through two case studies. First, we demonstrate this method’s strength in complex nonlinear environments. Then, we show that our approach matches the performance of the stateofthe art verification algorithm for linear discretized systems.more » « less

In this work, we consider twostage quadratic optimization problems under ellipsoidal uncertainty. In the first stage, one needs to decide upon the values of a subset of optimization variables (control variables). In the second stage, the uncertainty is revealed, and the rest of the optimization variables (state variables) are set up as a solution to a known system of possibly nonlinear equations. This type of problem occurs, for instance, in optimization for dynamical systems, such as electric power systems as well as gas and water networks. We propose a convergent iterative algorithm to build a sequence of approximately robustly feasible solutions with an improving objective value. At each iteration, the algorithm optimizes over a subset of the feasible set and uses affine approximations of the secondstage equations while preserving the nonlinearity of other constraints. We implement our approach and demonstrate its performance on Matpower instances of AC optimal power flow. Although this paper focuses on quadratic problems, the approach is suitable for more general setups.more » « less

Deshmukh, Jyotirmoy V. ; Havelund, Klaus ; Perez, Ivan (Ed.)Reachability analysis is a fundamental problem in verification that checks for a given model and set of initial states if the system will reach a given set of unsafe states. Its importance lies in the ability to exhaustively explore the behaviors of a model over a finite or infinite time horizon. The problem of reachability analysis for CyberPhysical Systems (CPS) is especially challenging because it involves reasoning about the continuous states of the system as well as its switching behavior. Each of these two aspects can by itself cause the reachability analysis problem to be undecidable. In this paper, we survey recent progress in this field beginning with the success of hybrid systems with affine dynamics. We then examine the current stateoftheart for CPS with nonlinear dynamics and those driven by ``learningenabled'' components such as neural networks. We conclude with an examination of some promising directions and open challenges.more » « less

We investigate approximate Bayesian inference techniques for nonlinear systems described by ordinary differential equation (ODE) models. In particular, the approximations will be based on setvalued reachability analysis approaches, yielding approximate models for the posterior distribution. Nonlinear ODEs are widely used to mathematically describe physical and biological models. However, these models are often described by parameters that are not directly measurable and have an impact on the system behaviors. Often, noisy measurement data combined with physical/biological intuition serve as the means for finding appropriate values of these parameters.Our approach operates under a Bayesian framework, given prior distribution over the parameter space and noisy observations under a known sampling distribution. We explore subsets of the space of model parameters, computing bounds on the likelihood for each subset. This is performed using nonlinear setvalued reachability analysis that is made faster by means of linearization around a reference trajectory. The tiling of the parameter space can be adaptively refined to make bounds on the likelihood tighter. We evaluate our approach on a variety of nonlinear benchmarks and compare our results with Markov Chain Monte Carlo and Sequential Monte Carlo approaches.