In recent years, many different methods for identifying hybrid automata from data have been proposed. However, most of these methods consider clean simulator data, and consequently do not perform well for noisy data measured from real systems. We address this shortcoming with a new approach for the identification of hybrid automata that is specifically designed to be robust to noise. In particular, we propose a new high-level strategy consisting of the following three steps: clustering based on the dynamics identified from a local dataset, state space partitioning using decision trees, and conversion of the decision tree to a hybrid automaton. In addition, we introduce several new concepts for the realization of the single steps. For example, we propose an automated regularization of the dynamic models used for clustering via rank adaption, as well as a new variant of the Gini impurity index for decision tree learning, tailored toward hybrid systems where different dynamics can be active within the same state space region. As our experiments on 19 challenging benchmarks with different characteristics demonstrate, in addition to being robust to both process and measurement noise, our approach avoids the need for extensive hyper-parameter tuning and also performs well for clean data without noise.

Black-box falsification problems are most often solved by numerical optimization algorithms. In this work, we propose an alternative approach, where simulations are used to construct a surrogate model for the system dynamics using data-driven Koopman operator linearization. Since the dynamics of the Koopman model are linear, the reachable set of states can be computed and combined with an encoding of the signal temporal logic specification in a mixed-integer linear program (MILP). To determine the next sample, an MILP solver computes the least robust trajectory inside the reachable set of the surrogate model. The trajectory’s initial state and input signal are then executed on the original black-box system, where the specification is either falsified or additional simulation data is generated that we use to retrain the surrogate Koopman model and repeat the process.

Despite large advances in recent years, real-time capable motion planning for autonomous road vehicles remains a huge challenge. In this work, we present a decision module that is based on set-based reachability analysis: First, we identify all possible driving corridors by computing the reachable set for the longitudinal position of the vehicle along the lanelets of the road network, where lane changes are modeled as discrete events. Next, we select the best driving corridor based on a cost function that penalizes lane changes and deviations from a desired velocity profile. Finally, we generate a reference trajectory inside the selected driving corridor, which can be used to guide or warm start low-level trajectory planners. For the numerical evaluation we combine our decision module with a motion-primitive-based and an optimization-based planner and evaluate the performance on 2000 challenging CommonRoad traffic scenarios as well in the realistic CARLA simulator. The results demonstrate that our decision module is real-time capable and yields significant speed-ups compared to executing a motion planner standalone without a decision module.

In real world applications, uncertain parameters are the rule rather than the exception. We present a reachability algorithm for linear systems with uncertain parameters and inputs using set propagation of polynomial zonotopes. In contrast to previous methods, our approach is able to tightly capture the non-convexity of the reachable set. Building up on our main result, we show how our reachability algorithm can be extended to handle linear time-varying systems as well as linear systems with time-varying parameters. Moreover, our approach opens up new possibilities for reachability analysis of linear time-invariant systems, nonlinear systems, and hybrid systems. We compare our approach to other state of the art methods, with superior tightness on two benchmarks including a 9-dimensional vehicle platooning system.

While reachability analysis is one of the major techniques for formal verification of dynamical systems, the requirement to adequately tune algorithm parameters often prevents its widespread use in practical applications. In this work, we fully automate the verification process for linear time-invariant systems: Based on the computation of tight upper and lower bounds for the support function of the reachable set along a given direction, we present a fully-automated verification algorithm, which is based on iterative refinement of the upper and lower bounds and thus always returns the correct result in decidable cases. While this verification algorithm is particularly well suited for cases where the specifications are represented by halfspace constraints, we extend it to arbitrary convex unsafe sets using the Gilbert-Johnson-Keerthi algorithm. In summary, our automated verifier is applicable to arbitrary convex initial sets, input sets, as well as unsafe sets, can handle time-varying inputs, automatically returns a counterexample in case of a safety violation, and scales to previously unanalyzable high-dimensional state spaces. Our evaluation on several challenging benchmarks shows significant improvements in computational efficiency compared to verification using other state-of-the-art reachability tools.

Abstract We introduce constrained polynomial zonotopes, a novel non-convex set representation that is closed under linear map, Minkowski sum, Cartesian product, convex hull, intersection, union, and quadratic as well as higher-order maps. We show that the computational complexity of the above-mentioned set operations for constrained polynomial zonotopes is at most polynomial in the representation size. The fact that constrained polynomial zonotopes are generalizations of zonotopes, polytopes, polynomial zonotopes, Taylor models, and ellipsoids further substantiates the relevance of this new set representation. In addition, the conversion from other set representations to constrained polynomial zonotopes is at most polynomial with respect to the dimension, and we present efficient methods for representation size reduction and for enclosing constrained polynomial zonotopes by simpler set representations.

Abstract Koopman operator linearization approximates nonlinear systems of differential equations with higher-dimensional linear systems. For formal verification using reachability analysis, this is an attractive conversion, as highly scalable methods exist to compute reachable sets for linear systems. However, two main challenges are present with this approach, both of which are addressed in this work. First, the approximation must be sufficiently accurate for the result to be meaningful, which is controlled by the choice ofobservable functionsduring Koopman operator linearization. By using random Fourier features as observable functions, the process becomes more systematic than earlier work, while providing a higher-accuracy approximation. Second, although the higher-dimensional system is linear, simple convex initial sets in the original space can become complex non-convex initial sets in the linear system. We overcome this using a combination of Taylor model arithmetic and polynomial zonotope refinement. Compared with prior work, the result is more efficient, more systematic and more accurate.

We present a MATLAB toolbox for Automated Reachset Optimal Control (AROC) that automatically synthesizes verified controllers for solving reach-avoid problems using reachability analysis. The toolbox implements two different types of control approaches: When using our verified model predictive controller, a feasible control law is constructed and verified on-the-fly during online application of the system. For motion-primitive-based control, on the other hand, controllers for many motion primitives are synthesized offline and then used for online motion planning with a maneuver automaton. Since our toolbox considers general nonlinear systems with input constraints, state constraints, and bounded disturbances, it is applicable to a very broad class of systems, as we demonstrate with several numerical examples. AROC is available at https://aroc.in.tum.de.

We present the first work on the automated generation of reachset conformant models for analog circuits. Our approach applies reachset conformant synthesis to add nondeterminism to piecewise-linear circuit models so that they enclose all recorded behaviors of the real system. To achieve this, we present a novel technique to compute the required nondeterminism for the piecewise-linear models. The effectiveness of our approach is demonstrated on a real analog circuit. Since the resulting models enclose all measurements, they can be used for formal verification.

Reachability analysis is one of the most important methods for formal verification of hybrid systems. The main difficulty for hybrid system reachability analysis is to calculate the intersection between reachable set and guard sets. While there exist several approaches for guard sets defined by hyperplanes or polytopes, only few methods are able to handle nonlinear guard sets. In this work we present a novel approach to tightly enclose the intersections of reachable sets with nonlinear guard sets. One major advantage of our method is its polynomial complexity with respect to the system dimension, which makes it applicable for high-dimensional systems. Furthermore, our approach can be combined with different reachability algorithms for continuous systems due to its modular design. We demonstrate the advantages of our novel approach compared to existing methods with numerical examples.

Reachability analysis, in general, is a fundamental method that supports formally-correct synthesis, robust model predictive control, set-based observers, fault detection, invariant computation, and conformance checking, to name but a few. In many of these applications, one requires to compute a reachable set starting within a previously computed reachable set. While it was previously required to re-compute the entire reachable set, we demonstrate that one can leverage the dependencies of states within the previously computed set. As a result, we almost instantly obtain an over-approximative subset of a previously computed reachable set by evaluating analytical maps. The advantages of our novel method are demonstrated for falsification of systems, optimization over reachable sets, and synthesizing safe maneuver automata. In all of these applications, the computation time is reduced significantly.