View: session overviewtalk overview

10:30 | Falsification of Hybrid Systems using Symbolic Reachability and Trajectory Splicing ABSTRACT. The falsification of a hybrid system aims at finding trajectories that violate a given safety property. This is a challenging problem, and the practical applicability of current falsification algorithms still suffers from their high time complexity. In contrast to falsification, verification algorithms aim at providing guarantees that no such trajectories exist. Recent symbolic reachability techniques are capable of efficiently computing linear constraints that enclose all trajectories of the system with reasonable precision. In this paper, we leverage the power of symbolic reachability algorithms to improve the scalability of falsification techniques. Recent approaches to falsification reduce the problem to a nonlinear optimization problem. We propose to reduce the search space of the optimization problem by adding linear state constraints obtained with a reachability algorithm. We showcase the efficiency of our approach on a number of standard hybrid systems benchmarks. |

11:00 | Inner and Outer Reachability for the Verification of Control Systems ABSTRACT. We investigate the information and guarantees provided by different inner and outer approximated reachability analyses, for proving properties of dynamical systems.We explore the connection of these approximated sets with the maximal and minimal reachable sets of Mitchell [33], with an additional notion of robustness to disturbance, as well as invariance and viability kernels. We demonstrate the practical use of a specific computation of these approximated reachable sets. We revisit in particular the reach-avoid properties. We also show how we can prove some new properties, such as every state of a given region is sure to be reached by the system, in presence of disturbances. |

11:30 | ABSTRACT. Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models that have inputs, nonlinear differential equations, and hybrid dynamics. As such, the scalability of affine systems verification is a prerequisite to the scalability of analysis methods for more complex systems. In this paper, we strive to improve the scalability of affine systems verification, in terms of the number of dimensions (variables) in the system. One benefit of affine systems is that their reachable states can be written in terms of the matrix exponential, and safety checking can be performed at specific time steps with linear programming. Unfortunately, for large systems with many state variables, this direct approach requires an intractable amount of memory while using an intractable amount of computation time. We overcome these two problems by combining several methods that leverage common problem structure. Memory demands can be reduced by taking advantage of both initial states that are not full-dimensional, and safety properties (outputs) that only need a few linear projections of the state variables. Computation time is saved by using numerical simulations to compute only projections of the matrix exponential relevant for the verification problem. Since large systems often have sparse dynamics, we use fast Krylov-subspace simulation methods based on the Arnoldi or Lanczos iterations. Our implementation produces accurate counter-examples when properties are violated and, in the extreme case with sufficient problem structure, is shown to analyze a system with one billion real-valued state variables. |

12:00 | SReachTools: A MATLAB Stochastic Reachability Toolbox ABSTRACT. We present SReachTools, an open-source MATLAB toolbox for performing stochastic reachability of linear discrete-time systems that are perturbed by additive Gaussian noise. The toolbox addresses the problem of stochastic reachability of a target tube, which also encompasses the terminal-time hitting reach-avoid and viability problems. The stochastic reachability of a target tube problem maximizes the likelihood that the state of a stochastic system will remain within a time-varying target tube for a give time horizon, while respecting the system dynamics and bounded control authority. SReachTools implements several new algorithms, based on convex optimization, computational geometry, and on Fourier transforms, to efficiently compute over- and under-approximations of the stochastic reach set. SReachTools can be used to perform probabilistic verification of closed-loop systems, by providing probabilistic guarantees of safety and performance. In addition, SReachTools can also perform controller synthesis to assure probabilistic safety or performance, via open-loop or affine controllers. The code base is designed to be extensible and user friendly. |

12:15 | JuliaReach: a Toolbox for Set-Based Reachability SPEAKER: Kostiantyn Potomkin ABSTRACT. We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems. |