Die vorliegende Dissertation behandelt die Sicherheitsverifikation von dynamischen Systemen mittels Erreichbarkeitsanalyse. Neuartige Lösungen wurden für klassische Erreichbarkeitsanalyse, stochastische Erreichbarkeitsanalyse und deren Anwendung auf die Sicherheitsbewertung von autonomen Autos entwickelt. Klassische Erreichbarkeitsanalyse berechnet die Menge an Zuständen, die von einem System erreicht werden kann. Falls die Erreichbarkeitsmenge keine Menge mit unsicheren Zuständen schneidet, ist die Sicherheit des Systems garantiert. Algorithmen für diese Aufgabe wurden für lineare, nichtlineare und hybride Systeme entwickelt. Stochastische Erreichbarkeitsanalyse schätzt ab mit welcher Wahrscheinlichkeit eine unsichere Menge erreicht wird. Ein verfolgter Ansatz berechnet eine überapproximierte Lösung für lineare Systeme. Ein Anderer erzeugt eine Markov Kette, die die stochastische Erreichbarkeitsmenge einer beliebigen Dynamik näherungsweise berechnet.

This thesis is about the safety verification of dynamical systems using reachability analysis. Novel solutions have been developed for classical reachability analysis, stochastic reachability analysis, and their application to the safety assessment of autonomous cars. Classical reachability analysis computes the set of states that can be reached by a system. If the reachable set does not intersect any set of unsafe states, the safety of the system is guaranteed. Algorithms for this problem have been developed for linear, nonlinear, and hybrid systems. Stochastic reachability analysis measures the probability of reaching an unsafe set. One pursued approach computes over-approximative solutions for linear systems; another one generates a Markov chain which approximately computes the stochastic reachable set of arbitrary dynamics