We propose a counterexample-guided inductive synthesis framework for the formal synthesis of closed-form sampled-data controllers for nonlinear systems to meet STL specifications over finite-time trajectories. Rather than stating the STL specification for a single initial condition, we consider an (infinite and bounded) set of initial conditions. Candidate solutions are proposed using genetic programming, which evolves controllers based on a finite number of simulations. Subsequently, the best candidate is verified using reachability analysis; if the candidate solution does not satisfy the specification, an initial condition violating the specification is extracted as a counterexample. Based on this counterexample, candidate solutions are refined until eventually a solution is found (or a user-specified number of iterations is met). The resulting sampled-data controller is expressed as a closed-form expression, enabling both interpretability and the implementation in embedded hardware with limited memory and computation power. The effectiveness of our approach is demonstrated for multiple systems.

@en

The computational effort of trajectory planning for automated vehicles often increases with the complexity of the traffic situation. This is particularly problematic in safety-critical situations, in which the vehicle must react in a timely manner. We present a novel motion planning approach for automated vehicles, which combines set-based reachability analysis with convex optimization to address this issue. This combination makes it possible to find driving maneuvers even in small and convoluted solution spaces. In contrast to existing work, the computation time of our approach typically decreases, the more complex situations become. We demonstrate the benefits of our motion planner in scenarios from the CommonRoad benchmark suite and validate the approach on a real test vehicle.

@en

Safe motion planning for autonomous vehicles is a challenging task, since the exact future motion of other traffic participant is usually unknown. In this article, we present a verification technique ensuring that autonomous vehicles do not cause collisions by using fail-safe trajectories. Fail-safe trajectories are executed if the intended motion of the autonomous vehicle causes a safety-critical situation. Our verification technique is real-time capable and operates under the premise that intended trajectories are only executed if they have been verified as safe. The benefits of our proposed approach are demonstrated in different scenarios on an actual vehicle. Moreover, we present the first in-depth analysis of our verification technique used in dense urban traffic. Our results indicate that fail-safe motion planning has the potential to drastically reduce accidents while not resulting in overly conservative behaviors of the autonomous vehicle.

@en

Adaptive cruise control is one of the most common comfort features of road vehicles. Despite its large market penetration, current systems are not safe in all driving conditions and require supervision by human drivers. While several previous works have proposed solutions for safe adaptive cruise control, none of these works considers comfort, especially in the event of cut-ins. We provide a novel solution that simultaneously meets our specifications and provides comfort in all driving conditions, including cut-ins. This is achieved by an exchangeable nominal controller ensuring comfort, combined with a provably correct fail-safe controller that gradually engages an emergency maneuver - this ensures comfort, since most threats are already cleared before emergency braking is fully activated. As a consequence, one can easily exchange the nominal controller without having to have the overall system safety re-certified. We also provide the first user study into a provably-correct adaptive cruise controller. It shows that even though our approach never causes an accident, passengers rate the performance as good as a state-of-the-art solution that does not ensure safety.

@en

Collision avoidance, kinematic feasibility, and road-compliance must be validated to ensure the drivability of planned motions for autonomous vehicles. Although these tasks are highly repetitive, computationally efficient toolboxes are still unavailable. The CommonRoad Drivability Checker - an open-source toolbox - unifies these mentioned checks. It is compatible with the CommonRoad benchmark suite, which additionally facilitates the development of motion planners. Our toolbox drastically reduces the effort of developing and validating motion planning algorithms. Numerical experiments show that our toolbox is real-time capable and can be used in real test vehicles.

@en

Ensuring that autonomous vehicles do not cause accidents remains a challenge. We present a formal verification technique for guaranteeing legal safety in arbitrary urban traffic situations. Legal safety means that autonomous vehicles never cause accidents although other traffic participants are allowed to perform any behaviour in accordance with traffic rules. Our technique serves as a safety layer for existing motion planning frameworks that provide intended trajectories for autonomous vehicles. We verify whether intended trajectories comply with legal safety and provide fallback solutions in safety-critical situations. The benefits of our verification technique are demonstrated in critical urban scenarios, which have been recorded in real traffic. The autonomous vehicle executed only safe trajectories, even when using an intended trajectory planner that was not aware of other traffic participants. Our results indicate that our online verification technique can drastically reduce the number of traffic accidents.

@en

We address the problem of provably-safe cooperative driving for a group of vehicles that operate in mixed traffic scenarios, where both autonomous and human-driven vehicles are present. Our method is based on Invariably Safe Sets (ISSs), which are sets of states that let each of the cooperative vehicles remain safe for an infinite time horizon. The potential conflicts between the ISSs of a group of cooperative vehicles are resolved by examining and negotiating their Safe Maneuver Corridors. As a result, each vehicle obtains its negotiated ISS, which is used as target sets for motion planning. We demonstrate the applicability and benefits of our method on various traffic scenarios from the CommonRoad benchmark suite.

@en

Falsification aims to disprove the safety of systems by providing counter-examples that lead to a violation of safety properties. In this work, we present two novel falsification methods to reveal safety flaws in adaptive cruise control (ACC) systems of automated vehicles. Our methods use rapidly-exploring random trees to generate motions for a leading vehicle such that the ACC under test causes a rear-end collision. By considering unsafe states and searching backward in time, we are able to drastically improve computation times and falsify even sophisticated ACC systems. The obtained collision scenarios reveal safety flaws of the ACC under test and can be directly used to improve the system's design. We demonstrate the benefits of our methods by successfully falsifying the safety of state-of-the-art ACC systems and comparing the results to that of existing approaches.@en

Self-driving vehicles must be able to safely navigate in any traffic scenario. However, all situations are different; even when clustering them, an impractical amount of scenarios would have to be verified. Thus, we propose a safety framework to verify the safety of each planned trajectory on-the-fly, using formal methods to handle uncertain measurements and future behaviors of traffic participants and disturbances acting on the ego vehicle, among others. Our framework can easily be integrated in existing motion planning architectures and enables fail-safe operation of self-driving vehicles, since we provide a safe plan for any given point in time. We demonstrate the benefits of our framework in different highway and urban scenarios of the CommonRoad benchmark suite. @en

Ensuring the safety of self-driving vehicles is a challenging task, especially if other traffic participants severely deviate from the predicted behavior. One solution is to ensure that the vehicle is able to execute a collision-free evasive trajectory at any time. However, a fast method to plan these socalled fail-safe trajectories does not yet exist. Our new approach plans fail-safe trajectories in arbitrary traffic scenarios by incorporating convex optimization techniques. By integrating safety verification in the planner, we are able to generate fail-safe trajectories in real-time, which are guaranteed to be safe. At the same time, we minimize jerk to provide enhanced comfort for passengers. The proposed benefits are demonstrated in different urban and highway scenarios using the CommonRoad benchmark suite and compared to a widely-used sampling-based planner.@en

The application of continuous optimization to motion planning of autonomous vehicles has enjoyed increasing popularity in recent years. In order to maintain low computation times, it is advantageous to have a convex formulation, in general requiring the planning problem to be separated into a longitudinal and lateral component. However, this decoupling of the motion often results in infeasible trajectories in situations in which both components need to be heavily linked, e.g., when planning swerving maneuvers to avoid a collision with obstacles. In this work, we propose an approach which extends the convex optimization problem of the longitudinal component to incorporate changing constraints, allowing us to guarantee feasibility of the resulting combined trajectory. Furthermore, we provide additional safety guarantees for the planned motion by integrating formal safety distances assuming infinite precision arithmetic. Our approach is demonstrated using simulated lane change maneuvers.@en

Set-based predictions can ensure the safety of planned motions, since they provide a bounded region which includes all possible future states of nondeterministic models of other traffic participants. However, while autonomous vehicles are tested in urban environments, a set-based prediction tailored to pedestrians does not exist yet. This paper addresses this problem and presents an approach for set-based predictions of pedestrians using reachability analysis. We obtain tight over-approximations of pedestrians' reachable occupancy by incorporating the dynamics of pedestrians, contextual information, and traffic rules. In addition, since pedestrians often disregard traffic rules, our constraints automatically adapt so that such behaviors are included in the prediction. Using datasets of recorded pedestrians, we validate our proposed method and demonstrate its use for evasive maneuver planning of automated vehicles.@en

Machine learning techniques have been shown to outperform many rule-based systems for the decision-making of autonomous vehicles. However, applying machine learning is challenging due to the possibility of executing unsafe actions and slow learning rates. We address these issues by presenting a reinforcement learning-based approach, which is combined with formal safety verification to ensure that only safe actions are chosen at any time. We let a deep reinforcement learning (RL) agent learn to drive as close as possible to a desired velocity by executing reasonable lane changes on simulated highways with an arbitrary number of lanes. By making use of a minimal state representation, consisting of only 13 continuous features, and a Deep Q-Network (DQN), we are able to achieve fast learning rates. Our RL agent is able to learn the desired task without causing collisions and outperforms a complex, rule-based agent that we use for benchmarking. @en

Safe motion planning requires that a vehicle reaches a set of safe states at the end of the planning horizon. However, safe states of vehicles have not yet been systematically defined in the literature, nor does a computationally efficient way to obtain them for online motion planning exist. To tackle the aforementioned issues, we introduce invariably safe sets. These are regions that allow vehicles to remain safe for an infinite time horizon. We show how invariably safe sets can be computed and propose a tight under-approximation which can be obtained efficiently in linear time with respect to the number of traffic participants. We use invariably safe sets to lift safety verification from finite to infinite time horizons. In addition, our sets can be used to determine the existence of feasible evasive maneuvers and the criticality of scenarios by computing the time-to-react metric.@en

Safety is the most important aspect of systems which have to perform collision-free motions in dynamic environments. Formal verification methods, such as reachability analysis, are capable of guaranteeing safety for a given model and given assumptions (e. g. bounded velocity and acceleration). However, certain assumptions can be violated by dynamic obstacles during the execution of the verified motion plan, exposing the system to potential collisions. To compensate for the invalidated verification, this paper introduces the Point of No Return (PNR) and the Point of Guaranteed Arrival (PGA) by incorporating invariably safe sets. These concepts allow one to divide the planned trajectory into safe sections and safety-critical passageways. For the former, we are able to provide safety guarantees for an infinite time horizon. For the latter, we present a method to minimize such safety-critical passageways prior to execution and thus reduce the risk of potential collisions if assumptions are violated during execution. The safety benefits are highlighted by a numerical example of overtaking maneuvers of self-driving vehicles.@en

Validating the safety of self-driving vehicles requires an enormous amount of testing. By applying formal verification methods, we can prove the correctness of the vehicles' behavior, which at the same time reduces remaining risks and the need for extensive testing. However, current safety approaches do not consider liabilities of traffic participants if a collision occurs. Utilizing formalized traffic rules to verify motion plans allows this problem to be solved. We present a novel approach for verifying the safety of lane change maneuvers, using formalized traffic rules according to the Vienna Convention on Road Traffic. This allows us to provide additional guarantees that if a collision occurs, the self-driving vehicle is not responsible. Furthermore, we consider misbehavior of other traffic participants during lane changes and propose feasible solutions to avoid or mitigate a potential collision. The approach has been evaluated using real traffic data provided by the NGSIM project as well as simulated lane changes.@en