In this paper, we consider an analysis of temporal properties of hybrid systems based on simulations, so-called falsification of requirements. We present a novel exploration-based algorithm for falsification of black-box models of hybrid systems based on the Voronoi bias. This approach is inspired by techniques used originally in motion planning: rapidly exploring random trees. Instead of commonly employed exploration that is based on coverage of inputs, the proposed exploration algorithm aims to explore possible outputs directly. It achieves that by covering a feature space that is associated with some spatial and temporal properties of output signals. This approach also does not require robustness or other guidance metrics tied to a specific behavior that is being falsified. This allows our algorithm to falsify specifications for which robustness is not conclusive enough to guide the falsification procedure.

This paper introduces an extension of the LQR-tree algorithm, which is a feedback-motion-planning algorithm for stabilizing a system of ordinary differential equations from a bounded set of initial conditions to a goal. The constructed policies are represented by a tree of exemplary system trajec-tories, so called demonstrations, and linear-quadratic regulator (LQR) feedback controllers. Consequently, the crucial component of any LQR-tree algorithm is a demonstrator that provides suitable demonstrations. In previous work, such a demonstrator was given by a local trajectory optimizer. However, these require appropriate initial guesses of solutions to provide valid results, which was pointed out, but largely unresolved in previous implementations. In this paper, we augment the LQR-tree algorithm with a randomized motion-planning procedure to discover new valid demonstration candidates to initialize the demonstrator in parts of state space not yet covered by the LQR-tree. In comparison to the previous versions of the LQR-tree algorithm, the resulting exploring LQR-tree algorithm reliably synthesizes feedback control laws for a far more general set of problems.

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.