Sampling-based algorithms for analysis and design of hybrid and embedded systems

This dissertation considers the problem of safety analysis of hybrid and embedded systems using sampling-based incremental search algorithms. The safety specifications are a set of conditions that the states (or the trajectories) of the system must satisfy for the system to be considered safe. The safety analysis problem is known to be undecidable for dynamical systems.;Most of the existing approaches for analyzing the safety specifications of a dynamical system are liable to give inconclusive results in general. This is because of the fact that each of these approaches can either only construct a safety certificate for a safe system, or, a feasible counterexample for an unsafe system.;Sampling-based incremental search algorithms have been very successful for motion planning problems in robotics and the counterexample generation problem for dynamical systems. In this dissertation, we propose a novel approach that uses sampling-based incremental search algorithms to search for feasible counterexamples to safety and uses the sampled trajectories to construct a safety certificate in case no counterexample is found.;We do so by introducing a notion of completeness for such algorithms that we call as resolution completeness. A sampling-based algorithm is called resolution-complete for safety analysis of a given system, if for any given resolution of controls it is guaranteed to terminate, producing, either a feasible counterexample to safety or a certificate that guarantees safe behavior of the system at the given resolution.;We propose a variety of sampling-based resolution-complete algorithms for safety analysis of hybrid and embedded systems. The algorithms construct feasible trajectories at increasing levels of resolution of the controls and use structural properties of the system to make reachability claims for states in the neighborhood of the constructed trajectories. Conditions guaranteeing completeness of the proposed algorithms are derived for the case of linear hybrid systems and the applicability of the approach is shown using several examples.;The proposed framework and the algorithms can be used for analysis and design of hybrid and embedded systems, including but not limited to, aerospace and robotic systems.