Abstract: We present a methodology for the verification of continuous and piecewise continuous systems, based on the use of a finite number of individual trajectories. We start by addressing the sampling-based reachability problem. Considering a dense set of initial conditions, the goal is to sample with a desired precision (or dispersion) the set reachable by the system with a finite number of simulations. We introduce and use the concept of expansion function to measure how a set of trajectories cover the reachable set. From there we deduce a verification algorithm which, by an iterative and hierarchical selection of the trajectories, finds quickly a bad behavior or proves that none exists. We show how these techniques can be efficiently implemented using standard results from dynamical systems theory on sensitivity analysis.

Alexandre Donzé graduated from the Engineer School of Computer Science and Applied Mathematics of Grenoble (ENSIMAG) in 2002. He also obtained a MSc in Applied Mathematics and a MSc of Computer Science from the University of Joseph Fourier (Grenoble 1) in 2002 and 2003. From 2003 to 2007 he did his Phd under the supervision of Oded Maler and Thao Dang at the VERIMAG laboratory in Grenoble, France. It is entitled 'Trajectory-based Verification and Controller Synthesis of Continuous and Hybrid Systems' and he defended on the 25th of June, 2007. Since October 2007, he holds a post-doctoral position at the School of Computer Science of Carnegie Mellon University. Appointments: dcm@cs.cmu.edu