Stefan Ratschan

Stefan Ratschan

In this paper, we present an algorithm for synthesizing certificates---so-called barrier certificates---for safety of hybrid dynamical systems. Unlike the usual approach of using constraint solvers to compute the certificate from the system dynamics, we synthesize the certificate from system simulations. This makes the algorithm applicable even in cases where the dynamics is either not explicitly available, or too complicated to be analyzed by constraint solvers, for example, due to the presence of transcendental function symbols. The algorithm itself allows the usage of heuristic techniques in which case it does not formally guarantee correctness of the result. However, in cases that do allow rigorous constraint solving, the computed barrier certificate can be rigorously verified, if desired. Hence, in such cases, our algorithm reduces the problem of finding a barrier certificate to the problem of formally verifying a given barrier certificate.

Stefan Ratschan

An important tool for proving safety of dynamical systems is the notion of a barrier certificate. In this paper we prove that every robustly safe ordinary differential equation has a barrier certificate. Moreover, we show a construction of such a barrier certificate based on a set of states that is reachable in finite time.

Jiří Fejlek, Stefan Ratschan

In this paper, we present an~algorithm that computes funnels along trajectories of systems of ordinary differential equations. A funnel is a time-varying set of states containing the given trajectory, for which the evolution from within the set at any given time stays in the funnel. Hence it generalizes the behavior of single trajectories to sets around them, which is an important task, for example, in robot motion planning. In contrast to approaches based on sum-of-squares programming, which poorly scale to high dimensions, our approach is based on falsification and tackles the funnel computation task directly, through numerical optimization. This approach computes accurate funnel estimates far more efficiently and leaves formal verification to the end, outside all funnel size optimization loops.