In reinforcement learning (RL), it is often advantageous to consider additional constraints on the action space to ensure safety or action relevance. Existing work on such action-constrained RL faces challenges regarding effective policy updates, computational efficiency, and predictable runtime. Recent work proposes to use truncated normal distributions for stochastic policy gradient methods. However, the computation of key characteristics, such as the entropy, log-probability, and their gradients, becomes intractable under complex constraints. Hence, prior work approximates these using the non-truncated distributions, which severely degrades performance. We argue that accurate estimation of these characteristics is crucial in the action-constrained RL setting, and propose efficient numerical approximations for them. We also provide an efficient sampling strategy for truncated policy distributions and validate our approach on three benchmark environments, which demonstrate significant performance improvements when using accurate estimations.

Abstract Agents in cyber-physical systems are increasingly entrusted with safety-critical tasks. Ensuring the safety of these agents often requires localizing their pose for subsequent actions. Pose estimates can, e.g., be obtained from various combinations of lidar sensors, cameras, and external services such as GPS. Crucially, in safety-critical domains, a rough estimate is insufficient to formally determine safety, i.e., to guarantee safety even in extreme scenarios, and external services may additionally be untrustworthy. We address this problem by presenting an approach for certified pose estimation in 3D solely from a camera image and a well-known target geometry. This is realized by formally bounding the pose, which is computed by leveraging recent results from reachability analysis and formal neural network verification. Our experiments demonstrate that our approach efficiently and accurately localizes agents in both synthetic and real-world experiments.

Imagine an automated vehicle violating a traffic rule and, by that, causing an accident. This would not only be devastating for a responsible operator, but more importantly, each such incident would erode the trust of the public in automated vehicles. Fortunately, compliance with traffic rules can be fully controlled, unless other traffic participants breach them—this causality obviously makes it possible for responsible operators to avoid liability claims. Traffic rules can be seen as guardrails for automated driving and should take center stage. Unfortunately, this is currently not the case. Many traffic rules are typically implicitly embedded in various fragments of the software stack of automated vehicles. Instead, the considered traffic rules should be explicitly and centrally provided. Adherence to traffic rules should also be ensured by formal methods to gain the trust needed in the public. This article provides all the steps required to achieve this goal. Due to the interdisciplinary nature of this topic (law, engineering, and computer science), we aim to address a broad audience by focusing on the governing principles of the presented methods, and we refer to more technical works for details.

Modular robots have the potential to revolutionize automation, as one can optimize their composition for any given task. However, finding optimal compositions is non-trivial. In addition, different compositions require different base positions and trajectories to fully use the potential of modular robots. We address this problem holistically for the first time by jointly optimizing the composition, base placement, and trajectory to minimize the cycle time of a given task. Our approach is evaluated on over 300 industrial benchmarks requiring point-to-point movements. Overall, we reduce cycle time by up to 25% and find feasible solutions in twice as many benchmarks compared to optimizing the module composition alone. In the first real-world validation of modular robots optimized for point-to-point movement, we find that the optimized robot is successfully deployed in nine out of ten cases in less than an hour.

Autonomous vehicles must obey the rules of the road to safely participate in road traffic. To enforce these rules during motion planning, they are often formalized in temporal logic. Such formalizations need to be very general to cover all possible traffic situations, resulting in large and complex logic formulas. During motion planning, however, we are usually confronted with a concrete scenario in which parts of the formulas may be irrelevant. Since specification-compliant motion planning under complex specifications is computationally challenging, we aim to simplify the traffic rules by removing these irrelevant parts. To this end, we first present a general algorithm that augments linear temporal logic formulas with scenario-specific knowledge. Then, we provide a method for extracting knowledge from traffic scenarios to augment traffic rules. We can formally guarantee that the augmented specification is equivalent to the original formula in the given scenario. Therefore, subsequent motion planning modules that handle temporal logic specifications need only consider the augmented formulas. We benchmark our approach in recorded real-world scenarios to demonstrate that it can significantly accelerate specification-compliant motion planning.

Autonomous robots are projected to significantly augment the manual workforce, especially in repetitive and hazardous tasks. For a successful deployment of such robots in human environments, it is crucial to guarantee human safety. State-of-the-art approaches to ensure human safety are either too conservative to permit a natural human-robot collaboration or make strong assumptions that do not hold for autonomous robots, e.g., knowledge of a pre-defined trajectory. Therefore, we propose the shield for Safe Autonomous human-robot collaboration through Reachability Analysis (SARA shield). This novel power and force limiting framework provides formal safety guarantees for manipulation in human environments while realizing fast robot speeds. As unconstrained contacts allow for significantly higher contact forces than constrained contacts (also known as clamping), we use reachability analysis to classify potential contacts by their type in a formally correct way. For each contact type, we formally verify that the kinetic energy of the robot is below pain and injury thresholds for the respective human body part in contact. Our experiments show that SARA shield satisfies the contact safety constraints while significantly improving the robot performance in comparison to state-of-the-art approaches.

Training and running inference of large neural networks comes with excessive cost and power consumption. Thus, realizing these networks as analog circuits is an energy-and areaefficient alternative. However, analog neural networks suffer from inherent deviations within their circuits, requiring extensive testing for their correct behavior under these deviations. Unfortunately, tests based on Monte Carlo simulations are extremely time- and resource-intensive. We present an alternative approach to proving the correctness of the neural network using formal neural network verification techniques and developing a modeling methodology for these analog neural circuits. Our experimental results compare two methods based on reachability analysis showing their effectiveness by reducing the test time from days to milliseconds. Thus, they offer a faster, more scalable solution for verifying the correctness of analog neural circuits.

Despite significant advancements in post-hoc explainability techniques for neural networks, many current methods rely on heuristics and do not provide formally provable guarantees over the explanations provided. Recent work has shown that it is possible to obtain explanations with formal guarantees by identifying subsets of input features that are sufficient to determine that predictions remain unchanged using neural network verification techniques. Despite the appeal of these explanations, their computation faces significant scalability challenges. In this work, we address this gap by proposing a novel abstraction-refinement technique for efficiently computing provably sufficient explanations of neural network predictions. Our method *abstracts* the original large neural network by constructing a substantially reduced network, where a sufficient explanation of the reduced network is also *provably sufficient* for the original network, hence significantly speeding up the verification process. If the explanation is insufficient on the reduced network, we iteratively *refine* the network size by gradually increasing it until convergence. Our experiments demonstrate that our approach enhances the efficiency of obtaining provably sufficient explanations for neural network predictions while additionally providing a fine-grained interpretation of the network's predictions across different abstraction levels.

Formulating the intended behavior of a dynamic system can be challenging. Signal temporal logic (STL) is frequently used for this purpose due to its suitability in formalizing comprehensible, modular, and versatile spatiotemporal specifications. Due to scaling issues with respect to the complexity of the specifications and the potential occurrence of non-differentiable terms, classical optimization methods often solve STL-based problems inefficiently. Smoothing and approximation techniques can alleviate these issues but require changing the optimization problem. This paper proposes a novel sampling-based method based on model predictive path integral control to solve optimal control problems with STL cost functions. We demonstrate the effectiveness of our method on benchmark motion planning problems and compare its performance with state-of-the-art methods. The results show that our method efficiently solves optimal control problems with STL costs.

Efficient and safe integration of robots into human workspaces remains a significant challenge. The ISO 10218-2 standard defines permissible force thresholds that a robot is allowed to exert on humans, along with a simple model to estimate the impact force based on the impact velocity, the involved human body part, and the effective mass of the robot. In this work, we experimentally demonstrate that state-of-the-art approaches fail to compute the effective robot mass accurately, leading to unsafe or overly-restrictive robot behavior. We address this shortcoming by presenting a data-driven collision mass map that accurately predicts the effective mass perceived at the end effector for a given collision location for the entire workspace. These maps are trained using a limited set of impact data selected by our proposed measurement procedure and can serve as valuable references for safety-critical applications. We validate our method on two robots, demonstrating accurate force predictions in compliance with ISO 10218-2. In our experiments, we show that our approach greatly reduces the required force measurements compared to state-of-the-art data-driven methods for risk assessment. Furthermore, our approach allows one to easily integrate different payloads, making it highly adaptable to various collaborative tasks. The proposed collision mass map can be standardized and deployed for any collaborative robot, enabling simple integration of robots for safe and more efficient human-robot interaction.

Motion planning for cyber-physical systems requires addressing numerous system objectives and constraints, including satisfying physical limitations, ensuring safety, reaching goal areas, or reducing energy consumption. Typically, it is only possible to achieve some of the objectives simultaneously since they may contradict. The objectives are usually weighted to specify which plans are preferred in such situations, resulting in a cumbersome tuning process. In this work, we use a weight-free prioritization of the objectives through preorders and introduce a novel sampling-based motion planner designed to efficiently generate trajectories optimizing preordered objectives. We ensure that only the smallest number of required objectives is evaluated to reduce computational time. Our approach can holistically define and solve many types of multi-objective optimization problems, and its usefulness is demonstrated for a Mars rover and an autonomous vehicle.

Motion planning for autonomous driving depends on or greatly benefits from global information, such as routes, reference paths, and velocity profiles. Existing global planning toolboxes (1) do not use provably unique curvilinear coordinates, (2) are mostly limited to racing scenarios, and (3) are not compatible with large scenario benchmarks. We present CommonRoad Global Planner, an open-source toolbox11pip install commonroad-global-planner, pip install commonroad-route-planner, pip install commonroad-velocity-plannerwithin the CommonRoad framework for global motion planning on roads, comprising the CommonRoad Route Planner for generating routes and smooth reference paths as well as the CommonRoad Velocity Planner, which implements several algorithms for planning velocity profiles. Our contributions are threefold: (1) our toolbox uses reference paths with provably correct curvilinear coordinates and returns velocity profiles that meet user-specified constraints; (2) the implemented algorithms are compatible with the CommonRoad benchmark suite; and (3) to the best of our knowledge, our toolbox for global planning is the first which is evaluated on large-scale numerical experiments on an open-source benchmark.

Conformal prediction is a popular uncertainty quantification method that augments a base predictor to return sets of predictions with statistically valid coverage guarantees. However, current methods are often computationally expensive and data-intensive, as they require constructing an uncertainty model before calibration. Moreover, existing approaches typically represent the prediction sets with intervals, which limits their ability to capture dependencies in multi-dimensional outputs. We address these limitations by introducing zono-conformal prediction, a novel approach inspired by interval predictor models and reachset-conformant identification that constructs prediction zonotopes with assured coverage. By placing zonotopic uncertainty sets directly into the model of the base predictor, zono-conformal predictors can be identified via a single, data-efficient linear program. While we can apply zono-conformal prediction to arbitrary nonlinear base predictors, we focus on feed-forward neural networks in this work. Aside from regression tasks, we also construct optimal zono-conformal predictors in classification settings where the output of an uncertain predictor is a set of possible classes. We provide probabilistic coverage guarantees and present methods for detecting outliers in the identification data. In extensive numerical experiments, we show that zono-conformal predictors are less conservative than interval predictor models and standard conformal prediction methods, while achieving a similar coverage over the test data.

In situ robotic automation in construction is challenging due to constantly changing environments, a shortage of robotic experts, and a lack of standardized frameworks bridging robotics and construction practices. This work proposes a holistic framework for construction task specification, optimization of robot morphology, and mission execution using a mobile modular reconfigurable robot. Users can specify and monitor the desired robot behavior through a graphical interface. In contrast to existing, monolithic solutions, we automatically identify a new task-tailored robot for every task by integrating Building Information Modeling (BIM). Our framework leverages modular robot components that enable the fast adaption of robot hardware to the specific demands of the construction task. Other than previous works on modular robot optimization, we consider multiple competing objectives, which allow us to explicitly model the challenges of real-world transfer, such as calibration errors. We demonstrate our framework in simulation by optimizing robots for drilling and spray painting. Finally, experimental validation demonstrates that our approach robustly enables the autonomous execution of robotic drilling.

Complying with traffic rules is challenging for automated vehicles, as numerous rules need to be considered simultaneously. If a planned trajectory violates traffic rules, it is common to replan a new trajectory from scratch. We instead propose a trajectory repair technique to save computation time. By coupling satisfiability modulo theories with set-based reachability analysis, we determine if and in what manner the initial trajectory can be repaired. Experiments in high-fidelity simulators and in the real world demonstrate the benefits of our proposed approach in various scenarios. Even in complex environments with intricate rules, we efficiently and reliably repair rule-violating trajectories, enabling automated vehicles to swiftly resume legally safe operation in real time.

Formal verification of neural networks is a challenging problem due to the complexity and nonlinearity of neural networks. It has been shown that polynomial zonotopes can tightly enclose the output set of a neural network. Unfortunately, the tight enclosure comes with additional complexity in the set representation, thus, rendering subsequent operations expensive to compute, such as computing interval bounds and intersection checking. To address this issue, we present a novel approach to restructure a polynomial zonotope to tightly enclose the original polynomial zonotope while drastically reducing its complexity. The restructuring is achieved by relaxing the exponents of the dependent factors of polynomial zonotopes and finding an appropriate approximation error. We demonstrate the applicability of our approach on output sets of neural networks, where we obtain tighter results in various subsequent operations, such as order reduction, zonotope enclosure, and range bounding.

Abstract Hybrid systems are often safety-critical and at the same time difficult to formally verify due to their mixed discrete and continuous behavior. To address this issue, we propose a novel incremental verification algorithm for hybrid systems based on online monitoring techniques and reachability analysis. To this end, we develop a four-valued semantics for signal temporal logic that allows us to distinguish two types of uncertainty: one arising from set-based evaluation and another one from the incremental nature of our algorithm. Using these semantics to continuously update the verification verdict, our verification algorithm is the first to run alongside the reachability analysis of the system to be verified. This makes it possible to stop the reachability analysis as soon as we obtain a conclusive verdict. We demonstrate the usefulness of our novel approach by several experiments.

Industrial robots are designed as general-purpose hardware with limited ability to adapt to changing task requirements or environments. Modular robots, on the other hand, offer flexibility and can be easily customized to suit diverse needs. The morphology, i.e., the form and structure of a robot, significantly impacts the primary performance metrics acquisition cost, cycle time, and energy efficiency. However, identifying an optimal module composition for a specific task remains an open problem, presenting a substantial hurdle in developing task-tailored modular robots. Previous approaches either lack adequate exploration of the design space or the possibility to adapt to complex tasks. We propose combining a genetic algorithm with a lexicographic evaluation of solution candidates to overcome this problem and navigate search spaces exceeding those in prior work by magnitudes in the number of possible compositions. We demonstrate that our approach outperforms a state-of-the-art baseline and is able to synthesize modular robots for industrial tasks in cluttered environments.

Selecting an optimal robot, its base pose, and trajectory for a given task is currently mainly done by human expertise or trial and error. To evaluate automatic approaches to this combined optimization problem, we introduce a benchmark suite encompassing a unified format for robots, environments, and task descriptions. Our benchmark suite is especially useful for modular robots, where the multitude of robots that can be assembled creates a host of additional parameters to optimize. We include tasks such as machine tending and welding in synthetic environments and 3D scans of real-world machine shops. All benchmarks are accessible through cobra.cps.cit.tum.de, a platform to conveniently share, reference, and compare tasks, robot models, and solutions.

Deep reinforcement learning (RL) has shown promising results in robot motion planning with first attempts in human-robot collaboration (HRC). However, a fair comparison of RL approaches in HRC under the constraint of guaranteed safety is yet to be made. We, therefore, present human-robot gym, a benchmark suite for safe RL in HRC. We provide challenging, realistic HRC tasks in a modular simulation framework. Most importantly, human-robot gym is the first benchmark suite that includes a safety shield to provably guarantee human safety. This bridges a critical gap between theoretic RL research and its real-world deployment. Our evaluation of six tasks led to three key results: (a) the diverse nature of the tasks offered by human-robot gym creates a challenging benchmark for state-of-the-art RL methods, (b) by leveraging expert knowledge in form of an action imitation reward, the RL agent can outperform the expert, and (c) our agents negligibly overfit to training data.

Industrial robots are essential for modern production but often struggle to adapt to new tasks. Modular (reconfigurable) robots can overcome this challenge by eliminating the need to replace the whole robot. However, finding the optimal assembly for a task remains difficult because a valid path has to be computed for each generated assembly – consuming a significant fraction of the computation time. Similar to online path planning, where previous approaches adapt known paths to a changing environment, we show that transferring paths from previously considered module assemblies accelerates path planning for the next assemblies. On average, our method reduces the planning time for single-goal tasks by 50%. The usefulness of our method is evaluated by integrating it in a genetic algorithm (GA) for optimizing assemblies and evaluating it on our benchmark suite CoBRA. Within the optimization loop for modular robots, the time used to check a single assembly is shortened by up to 50%.

Formal verification of robotic tasks requires a simple yet conformant model of the used robot. We present the first work on generating reachset conformant models for robotic contact tasks considering hybrid (mixed continuous and discrete) dynamics. Reachset conformance requires that the set of reachable outputs of the abstract model encloses all previous measurements to transfer safety properties. Aiming for industrial applications, we describe the system using a simple hybrid automaton with linear dynamics. We inject non-determinism into the continuous dynamics and the discrete transitions, and we optimally identify all model parameters together with the non-determinism required to capture the recorded behaviors. Using two 3-DOF robots, we show that our approach can effectively generate models to capture uncertainties in system behavior and substantially reduce the required testing effort in industrial applications.

Cooperative platooning is a promising method for improving energy efficiency and traffic throughput on interstates. Ensuring collision avoidance is particularly difficult in platooning due to the small desired inter-vehicle spacing. We propose a safety protocol that can be applied to arbitrary controllers in platooning to prevent collisions in a provably correct manner while still realizing a small distance to the preceding vehicle. Our protocol intervenes as rarely and smoothly as possible, and its safety is ensured even if communication fails. In addition, we propose a safety protocol for consensus techniques where the vehicles of the platoon successively agree on a common braking limit. Our safety protocols are evaluated on various scenarios using the CommonRoad benchmark suite.

Compliance with the rules of the road is crucial for the safe operation of autonomous vehicles. Previous work has shown that one can expedite rule-compliant motion planning by constraining the search space based on the reachable states of the vehicle. We propose an algorithm to overapproximate the states that a vehicle can reach while adhering to a linear temporal logic specification. By integrating model checking into reachability analysis, we can exclude many non-compliant states early. Moreover, we only have to semantically split the reachable set when necessary to decide the validity of the specification. This significantly reduces the computation time compared to existing approaches. We benchmark our approach in recorded real-world scenarios to demonstrate its real-time capability.

Motion planning algorithms should be tested on a large, diverse, and realistic set of scenarios before deploying them in real vehicles. However, existing 3D simulators usually focus on perception and end-to-end learning, lacking specific interfaces for motion planning. We present an interface for the CARLA simulator focusing on motion planning, e.g., to create configurable test scenarios and execute motion planners in interactive environments. Additionally, we introduce a converter from lanelet-based maps to OpenDRIVE, making it possible to use CommonRoad and Lanelet2 maps in CARLA. Our evaluation shows that our interface is easy to use, creates new scenarios efficiently, and can successfully integrate motion planners to solve CommonRoad scenarios. Our tool is published as an open-source toolbox at commonroad.in.tum.de.

Multi-agent cooperative motion planning offers the potential to improve safety and the overall traffic flow. However, many approaches for multi-agent driving do not incorporate traffic rules or do not generalize to arbitrary scenarios. To address these open problems, we propose a novel method to negotiate individual rule-compliant driving corridors and independently plan trajectories for each controlled agent in them. We incorporate predictions into the conflict negotiation process to enable decision-making over long time horizons. Our approach is applicable to arbitrary scenarios, including mixed cooperative and non-cooperative traffic participants, as demonstrated through our numerical experiments

Curvilinear coordinate frames are a widespread representation for motion planners of automated vehicles. In structured environments, the required reference path is often extracted from map data, e.g., by linearly interpolating the center points of lanes. Often, these reference paths are not directly suited for curvilinear frames, as the representation of points is not guaranteed to be unique for relevant parts of the road. Artifacts arising from faulty coordinate conversions can impede the robustness of downstream planning tasks and may result in safety-critical situations. We present an iterative procedure to adapt a reference path, ensuring a unique representation of all points within a provided subset of a map. Our numerical experiments demonstrate the efficacy of our method when combined with two motion planning tasks: Computing the reachable set of the ego vehicle and planning trajectories using a sampling-based approach.

Validating motion planning algorithms for autonomous vehicles on a real system is essential to improve their safety in the real world. Open-source initiatives, such as Autoware, provide a deployable software stack for real vehicles. However, such driving stacks have a high entry barrier, so that integrating new algorithms is tedious. Especially new research results are thus mostly evaluated only in simulation, e.g., within the CommonRoad benchmark suite. To address this problem, we present CR2AW, a publicly available interface between the CommonRoad framework and Autoware. CR2AW significantly simplifies the sim-to-real transfer of motion planning research, by allowing users to easily integrate their CommonRoad planning modules into Autoware. Our experiments both in simulation and on our research vehicle showcase the usefulness of CR2AW.

Continuous action spaces in reinforcement learning (RL) are commonly defined as multidimensional intervals. While intervals usually reflect the action boundaries for tasks well, they can be challenging for learning because the typically large global action space leads to frequent exploration of irrelevant actions. Yet, little task knowledge can be sufficient to identify significantly smaller state-specific sets of relevant actions. Focusing learning on these relevant actions can significantly improve training efficiency and effectiveness. In this paper, we propose to focus learning on the set of relevant actions and introduce three continuous action masking methods for exactly mapping the action space to the state-dependent set of relevant actions. Thus, our methods ensure that only relevant actions are executed, enhancing the predictability of the RL agent and enabling its use in safety-critical applications. We further derive the implications of the proposed methods on the policy gradient. Using proximal policy optimization ( PPO), we evaluate our methods on four control tasks, where the relevant action set is computed based on the system dynamics and a relevant state set. Our experiments show that the three action masking methods achieve higher final rewards and converge faster than the baseline without action masking.

Forecasting the motion of others in shared spaces is a key for intelligent agents to operate safely and smoothly. We present an approach for probabilistic prediction of pedestrian motion incorporating various context cues. Our approach is based on goal-oriented prediction, yielding interpretable results for the predicted pedestrian intention, even without the prior knowledge of goal positions. By using Markov chains, the resulting probability distribution is deterministic—a beneficial property for motion planning or risk assessment in automated and assisted driving. Our approach outperforms a physics-based approach and improves over state-of-the-art approaches by reducing standard deviations of prediction errors and improving robustness against realistic, noisy measurements.

The formal verification of neural networks is essential for their application in safety-critical environments. However, the set-based verification of neural networks using linear approximations often obtains overly conservative results, while nonlinear approximations quickly become computationally infeasible in deep neural networks. We address this issue for the first time by automatically balancing between precision and computation time without splitting the propagated set. Our work introduces a novel automatic abstraction refinement approach using sensitivity analysis to iteratively reduce the abstraction error at the neuron level until either the specifications are met or a maximum number of iterations is reached. Our evaluation shows that we can tightly over-approximate the output sets of deep neural networks and that our approach is up to a thousand times faster than a naive approach. We further demonstrate the applicability of our approach in closed-loop settings.

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.

Manually specifying features that capture the diversity in traffic environments is impractical. Consequently, learning-based agents cannot realize their full potential as neural motion planners for autonomous vehicles. Instead, this work proposes to learn which features are task-relevant. Given its immediate relevance to motion planning, our proposed architecture encodes the probabilistic occupancy map as a proxy for obtaining pre-trained state representations of the environment. By leveraging a map-aware traffic graph formulation, our agent-centric encoder generalizes to arbitrary road networks and traffic situations. We show that our approach significantly improves the downstream performance of a reinforcement learning agent operating in urban traffic environments.

Modular Reconfigurable Robots (MRRs) represent an exciting path forward for industrial robotics, opening up new possibilities for robot design. Compared to monolithic manipulators, they promise greater flexibility, improved maintainability, and cost-efficiency. However, there is no tool or standardized way to model and simulate assemblies of modules in the same way it has been done for robotic manipulators for decades. We introduce the Toolbox for Industrial Modular Robotics (Timor), a Python toolbox to bridge this gap and integrate modular robotics into existing simulation and optimization pipelines. Our open-source library offers model generation and task-based configuration optimization for MRRs. It can easily be integrated with existing simulation tools - not least by offering URDF export of arbitrary modular robot assemblies. Moreover, our experimental study demonstrates the effectiveness of Timor as a tool for designing modular robots optimized for specific use cases.

Deep Reinforcement Learning (RL) has shown promise in addressing complex robotic challenges. In real-world applications, RL is often accompanied by failsafe controllers as a last resort to avoid catastrophic events. While necessary for safety, these interventions can result in undesirable behaviors, such as abrupt braking or aggressive steering. This paper proposes two safety intervention reduction methods: proactive replacement and proactive projection, which change the action of the agent if it leads to a potential failsafe intervention. These approaches are compared to state-of-the-art constrained RL on the OpenAI safety gym benchmark and a human-robot collab-oration task. Our study demonstrates that the combination of our method with provably safe RL leads to high-performing policies with zero safety violations and a low number of failsafe interventions. Our versatile method can be applied to a wide range of real-world robotic tasks, while effectively improving safety without sacrificing task performance.

Criticality measures are essential for autonomous vehicles to capture the complexity of the surrounding environment, trigger emergency maneuvers, and verify safety. However, there is currently no publicly available toolbox that allows researchers to use or evaluate a large number of criticality measures on arbitrary traffic scenarios. To address this issue, we present CommonRoad-CriMe, an open-source toolbox for measuring the criticality of autonomous vehicles in a unified framework. Our toolbox covers a wide range of state-of-the-art criticality measures and provides visualized information to facilitate debugging and showcasing. Numerical experiments demonstrate how our toolbox facilitates the comparison of different criticality measures and the analysis of traffic conflicts. Our toolbox is available at commonroad.in.tum.de.

Heterogeneous graphs offer powerful data representations for traffic, given their ability to model the complex interaction effects among a varying number of traffic participants and the underlying road infrastructure. With the recent advent of graph neural networks (GNNs) as the accompanying deep learning framework, the graph structure can be efficiently leveraged for various machine learning applications such as trajectory prediction. As a first of its kind, our proposed Python framework offers an easy-to-use and fully customizable data processing pipeline to extract standardized graph datasets from traffic scenarios. Providing a platform for GNN-based autonomous driving research, it improves comparability between approaches and allows researchers to focus on model implementation instead of dataset curation.

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.

Guaranteeing safety for humans in shared workspaces is not trivial. Not only must all possible situations be provably safe, but the human must feel safe as well. While robots are gradually leaving their cages, due to strict safety requirements, engineers often only replace physical cages with static safety zones—when the safety zone is entered, the robot is forced to stop. This can lead to excessive robot downtime. Note to Practitioners—We present a concept for guaranteeing non-collision between humans and robots whilst maximising robot uptime and staying on-path. We evaluate how users react to this approach, in a trial over three non-consecutive days, compared to a control approach of static safety zones. We measure working efficiency as well as human factors such as trust, understanding of the robot, and perceived safety. Using our approach, the robot is indeed more efficient compared to static safety zones and the effect persists over multiple trials on separate days. We also observed that understanding of the robot’s movement increased for our method over the course of trials, and the perceived safety of the robot increased for both our method and the control.

Robots are used increasingly often in safety-critical scenarios, such as robotic surgery or human–robot interaction. To ensure stringent performance criteria, formal controller synthesis is a promising direction to guarantee that robots behave as desired. However, formally ensured properties only transfer to the real robot when the model is appropriate. In this article, we address this problem by combining the identification of a reachset-conformant model with controller synthesis. Since the reachset-conformant model contains all the measured behaviors of the real robot, the safety properties of the model transfer to the real robot. The transferability is demonstrated by experiments on a real robot, for which we synthesize tracking controllers.

Future power systems will rely heavily on micro grids with a high share of decentralised renewable energy sources and energy storage systems. The high complexity and uncertainty in this context might make conventional power dispatch strategies infeasible. Reinforcement-learning-based (RL) controllers can address this challenge, however, cannot themselves provide safety guarantees, preventing their deployment in practice. To overcome this limitation, we propose a formally validated RL controller for economic dispatch. We extend conventional constraints by a time-dependent constraint encoding the islanding contingency. The contingency constraint is computed using set-based backwards reachability analysis, and actions of the RL agent are verified through a safety layer. Unsafe actions are projected into the safe action space while leveraging constrained zonotope set representations for computational efficiency. The developed approach is demonstrated on a residential use case considering real-world measurements.

Current safety mechanisms implementing industry standards for human-robot coexistence separate humans and robots through caging. Other approaches allowing humans to enter the workspace of manipulators do not provide formal safety guarantees. Thus, this study aims to facilitate the widespread adoption of collaborative robots by presenting SaRA, an extensible tool that performs set-based reachability analysis and formally guarantees safety. Our experimental results show that the set-based prediction of a human can be computed in a few microseconds, using SaRA, allowing for real-time consideration of many surrounding humans in an environment.

Deep reinforcement learning (RL) has shown promising results in the motion planning of manipulators. However, no method guarantees the safety of highly dynamic obstacles, such as humans, in RL-based manipulator control. This lack of formal safety assurances prevents the application of RL for manipulators in real-world human environments. Therefore, we propose a shielding mechanism that ensures ISO- verified human safety while training and deploying RL algorithms on manipulators. We utilize a fast reachability analysis of humans and manipulators to guarantee that the manipulator comes to a complete stop before a human is within its range. Our proposed method guarantees safety and significantly improves the RL performance by preventing episode-ending collisions. We demonstrate the performance of our proposed method in simulation using human motion capture data.

Autonomous vehicles must comply with traffic rules. However, most motion planners do not explicitly consider all relevant traffic rules. Once traffic rule violations of an initially-planned trajectory are detected, there is often not enough time to replan the entire trajectory. To solve this problem, we propose to repair the initial trajectory by investigating the satisfiability modulo theories paradigm. This framework makes it efficient to reason whether and how the trajectory can be repaired and, at the same time, determine the part along the trajectory that can remain unchanged. Moreover, the robustness of traffic rule satisfaction is used to formulate a convex optimization problem for generating rule-compliant trajectories. We compare our approach with trajectory replanning and demonstrate its usefulness with traffic scenarios from the CommonRoad benchmark suite and recorded data. The evaluation result shows that rule-compliant trajectory repairing is computationally efficient and widely applicable.

Intersections are difficult to navigate for both human drivers and autonomous vehicles because several diverse traffic rules must be considered. In addition, current traffic rules are ambiguous and cannot be applied directly by autonomous vehicles. Therefore, national traffic rules must be concretized and formalized so that they are machine-interpretable. We present formalized intersection traffic rules in temporal logic and use the German traffic regulations as a concrete example. Our formalization considers different types of intersections, i.e., signalized, traffic-sign-regulated, and unregulated intersections. We also define predicates and functions that can be easily reused for other national traffic laws. We evaluate our formalized traffic rules on recorded real-world scenarios and manually-created test scenarios. Our evaluation validates the formalization from different legal sources.

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.

Reachability analysis fails to produce tight reachable sets if certain algorithm parameters are poorly tuned, such as the time step size or the accuracy of the set representation. The tuning is especially difficult in the context of nonlinear systems where over-approximation errors accumulate over time due to the so-called wrapping effect, often requiring expert knowledge. In order to widen the applicability of reachability analysis for practitioners, we propose the first adaptive parameter tuning approach for reachability analysis of nonlinear continuous systems tuning all algorithm parameters. Our modular approach can be applied to different reachability algorithms as well as various set representations. Finally, an evaluation on numerous benchmark systems shows that the adaptive parameter tuning approach efficiently computes very tight enclosures of reachable sets.

Humans must remain unharmed during their interaction with robots. We present a new method guaranteeing impact force limits when humans and robots share a workspace. Formal guarantees are realized using an online verification method, which plans and verifies fail-safe maneuvers through predicting reachable impact forces by considering all future possible scenarios. We model collisions as a coupled human-robot dynamical system with uncertainties and identify reachset-conforming models based on real-world collision experiments. The effectiveness of our approach for human-robot co-existence is demonstrated for the human hand interacting with the end effector of a six-axis robot manipulator with force sensing. By integrating a human pose detection system, the efficiency of robot movements increases.

Autonomous vessels have to adhere to marine traffic rules to ensure traffic safety and reduce the liability of manufacturers. However, autonomous systems can only evaluate rule compliance if rules are formulated in a precise and mathematical way. This paper formalizes marine traffic rules from the Convention on the International Regulations for Preventing Collisions at Sea (COLREGS) using temporal logic. In particular, the collision prevention rules between two power-driven vessels are delineated. The formulation is based on modular predicates and adjustable parameters. We evaluate the formalized rules in three US coastal areas for over 1,200 vessels using real marine traffic data.

To safely and effectively participate in road traffic, automated vehicles should explicitly consider compliance with traffic rules and high-level specifications. We propose a method that can incorporate traffic and handcrafted rules expressed in time-labeled propositional logic into our reach ability analysis, which computes the over-approximative set of states reachable by vehicles. These reachable sets serve as low-level trajectory planning constraints to expedite the search for specification-compliant trajectories. Depending on the adopted specifications, related semantic labels are generated from predicates considering positions, velocities, accelerations, and general traffic situations. We exhibit the applicability of the proposed method with scenarios from the CommonRoad benchmark suite.

Autonomous vehicles (AVs) must share space with pedestrians, both in carriageway cases such as cars at pedestrian crossings and off-carriageway cases such as delivery vehicles navigating through crowds on pedestrianized high-streets. Unlike static obstacles, pedestrians are active agents with complex, interactive motions. Planning AV actions in the presence of pedestrians thus requires modelling of their probable future behavior as well as detecting and tracking them. This narrative review article is Part I of a pair, together surveying the current technology stack involved in this process, organising recent research into a hierarchical taxonomy ranging from low-level image detection to high-level psychology models, from the perspective of an AV designer. This self-contained Part I covers the lower levels of this stack, from sensing, through detection and recognition, up to tracking of pedestrians. Technologies at these levels are found to be mature and available as foundations for use in high-level systems, such as behavior modelling, prediction and interaction control.

Autonomous vehicles (AVs) must share space with pedestrians, both in carriageway cases such as cars at pedestrian crossings and off-carriageway cases such as delivery vehicles navigating through crowds on pedestrianized high-streets. Unlike static obstacles, pedestrians are active agents with complex, interactive motions. Planning AV actions in the presence of pedestrians thus requires modelling of their probable future behavior as well as detecting and tracking them. This narrative review article is Part II of a pair, together surveying the current technology stack involved in this process, organising recent research into a hierarchical taxonomy ranging from low-level image detection to high-level psychological models, from the perspective of an AV designer. This self-contained Part II covers the higher levels of this stack, consisting of models of pedestrian behavior, from prediction of individual pedestrians' likely destinations and paths, to game-theoretic models of interactions between pedestrians and autonomous vehicles. This survey clearly shows that, although there are good models for optimal walking behavior, high-level psychological and social modelling of pedestrian behavior still remains an open research question that requires many conceptual issues to be clarified. Early work has been done on descriptive and qualitative models of behavior, but much work is still needed to translate them into quantitative algorithms for practical AV control.

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.

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.

Reinforcement learning (RL) has achieved enormous progress in solving various sequential decision-making problems, such as control tasks in robotics. Since policies are overfitted to training environments, RL methods have often failed to be generalized to safety-critical test scenarios. Robust adversarial RL (RARL) was previously proposed to train an adversarial network that applies disturbances to a system, which improves the robustness in test scenarios. However, an issue of neural network-based adversaries is that integrating system requirements without handcrafting sophisticated reward signals are difficult. Safety falsification methods allow one to find a set of initial conditions and an input sequence, such that the system violates a given property formulated in temporal logic. In this paper, we propose falsification-based RARL (FRARL): this is the first generic framework for integrating temporal logic falsification in adversarial learning to improve policy robustness. By applying our falsification method, we do not need to construct an extra reward function for the adversary. Moreover, we evaluate our approach on a braking assistance system and an adaptive cruise control system of autonomous vehicles. Our experimental results demonstrate that policies trained with a falsification-based adversary generalize better and show less violation of the safety specification in test scenarios than those trained without an adversary or with an adversarial network.

Flexible manufacturing and automation require robots that can be adapted to changing tasks. We propose to use modular robots that are customized from given modules for a specific task. This work presents an algorithm for proposing a module composition that is optimal with respect to performance metrics such as cycle time and energy efficiency, while considering kinematic, dynamic, and obstacle constraints. Tasks are defined as trajectories in Cartesian space, as a list of poses for the robot to reach as fast as possible, or as dexterity in a desired workspace. In a simulated comparison with commercially available industrial robots, we demonstrate the superiority of our approach in randomly generated tasks with respect to the chosen performance metrics. We use our modular robot proModular.1 for the comparison.

Humans and robots are increasingly sharing their workspaces to benefit from the precision, endurance, and strength of machines and the universal capabilities of humans. Instead of performing time-consuming real experiments, computer simulations of humans could help to optimally orchestrate human and robotic tasks—either for setting up new production cells or by optimizing the motion planning of already installed robots. Especially when human-robot coexistence is optimized using machine learning, being able to synthesize a huge number of human motions is indispensable. However, no solution exists that automatically creates a range of human motions from a high-level specification of tasks. We propose a novel method that automatically generates human motions from linear temporal logic specifications and demonstrate our approach by numerical examples.

Virtual testing plays an important role in the validation and verification of automated vehicles. State-of-the-art approaches first generate a huge amount of test scenarios through simulations or test drives, which are later filtered to obtain relevant scenarios for a given set of specifications. However, only few works exist on synthesizing scenarios directly from specifications. In this work, we present an optimization-based approach to synthesize scenarios only from formal specifications and a given map. To concretize the specifications, we formulate predicates, which are subsequently converted to a mixed-integer quadratic optimization problem. We demonstrate how our method can generate scenarios for maps featuring merging lanes and intersections given a variety of specifications.

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.

To allow autonomous vehicles to safely participate in traffic and to avoid liability claims for car manufacturers, autonomous vehicles must obey traffic rules. However, current traffic rules are not formulated in a precise and mathematical way, so that they cannot be directly applied to autonomous vehicles. Additionally, several legal sources other than national traffic laws must be considered to infer detailed traffic rules. Thus, we formalize traffic rules for interstates based on the German Road Traffic Regulation, the Vienna Convention on Road Traffic, and legal decisions from courts. This makes it possible to automatically and unambiguously check whether traffic rules are being met by autonomous vehicles. Temporal logic is used to express the obtained rules mathematically. Our formalized traffic rules are evaluated for recorded data on more than 2,500 vehicles.

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.

Virtual testing of automated vehicles using simulations is essential during their development. When it comes to the testing of motion planning algorithms, one is mainly interested in challenging, critical scenarios for which it is hard to find a feasible solution. However, these situations are rare under usual traffic conditions, demanding an automatic generation of critical test scenarios. We present an approach that automatically generates critical scenarios based on a minimization of the solution space of the vehicle under test. By formulating a scenario parametrization and automatic determination of relevant parameter intervals, we are able to optimize the criticality of complex scenarios. We use evolutionary algorithms to tackle the resulting highly nonlinear optimization problem. Compared to our previous approach, we are now able to handle complex situations, in particular those involving intersections. Finally, we demonstrate our approach by generating critical scenarios from initially uncritical scenarios.

Model-based development is an important paradigm for developing cyber-physical systems (CPS). The underlying assumption is that the functional behavior of a model is related to the behavior of a more concretized model or the real system. A formal definition of such a relation is called conformance relation. There are a variety of conformance relations, and the question arises of how to select a conformance relation for the development of CPS. The contribution of this article is a survey of the definitions and algorithms of conformance relations for CPS. Additionally, the article compares several conformance relations and provides guidance on which relation to select for specific problems. Finally, we discuss how to select inputs for testing conformance.

Model-based design of robotic systems has many advantages, among them faster development cycles and reduced costs due to early detections of design flaws. Approximate models are sufficient for many classical robotic applications; however, they no longer suffice for safety-critical applications. For instance, a dangerous situation which has not been detected by model-based testing might occur in a human-robot co-existence scenario since models do not exactly replicate behaviors of real systems-this problem arises no matter how accurate a model is, since even disturbances and sensor noise can cause a mismatch. We address this issue by adding non-determinism to robotic models and by computing the whole set of possible behaviors using reachability analysis. By using reachset conformance, we automatically adjust the required non-determinism so that all recorded behaviors are captured. For the first time this approach is demonstrated for a real robot.

This paper presents a hierarchical path planner consisting of two stages: a global planner that uses workspace information to create collision-free paths for the robot end-effector to follow, and multiple local planners running in parallel that verify the paths in the configuration space by expanding a task-space rapidly-exploring random tree (RRT). We demonstrate the practicality of our approach by comparing it with state-of-the-art planners in several challenging path planning problems. While using a single tree, our planner outperforms other single tree approaches in task-space or configuration space (C-space), while its performance and robustness are comparable to or better than that of parallelized bidirectional C-space planners.

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.

It is apparent that one cannot rely solely on physical test drives for ensuring the correct functionality of autonomous vehicles. Since physical test drives are costly and time consuming, it is advantageous to accompany them with computer simulations. However, since most traffic scenarios are not challenging, even simulations are often too time consuming. To address this issue, we present an approach that creates automatically critical driving situations, i.e., situations with a small solution space for avoiding a collision. Our approach combines reachability analysis for determining the size of the solution space with optimization techniques to shrink it. The solution space is reduced by shifting the initial states of traffic participants, demanding an immediate and correct action of the vehicle under test. We demonstrate our approach by automatically increasing the criticality of several initially uncritical situations recorded from real traffic.

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.

Collision mitigation and collision avoidance systems in intelligent vehicles reduce the severity and number of accidents. To determine the optimal point in time at which such systems should intervene, time-based criticality metrics such as the Time-To-React (TTR) are commonly used. The TTR describes the last point in time along the current trajectory at which an evasive trajectory exists. In this paper, we present a novel approach to determine the point in time after which it is guaranteed that no evasive maneuver exists, i.e., by using reachable sets, we over-approximate the TTR. Our deterministic upper bound of the TTR can be used to trigger a collision mitigation system or to find a feasible emergency maneuver which avoids the collision. We demonstrate the efficient computation of the tight over-approximated TTR in different urban and rural traffic scenarios, and compare our results to an estimated TTR using an optimization-based trajectory planner.

As pedestrians are one of the most vulnerable traffic participants, their motion prediction is of utmost importance for intelligent transportation systems. Predicting motions of pedestrians is especially hard since they move in less structured environments and have less inertia compared to road vehicles. To account for this uncertainty, we present an approach for probabilistic prediction of pedestrian motion using Markov chains. In contrast to previous work, we not only consider motion models, constraints from a semantic map, and various goals, but also explicitly adapt the prediction based on crash probabilities with other traffic participants. Also, our approach works in any situation; this is typically challenging for pure machine learning techniques that learn behaviors for a particular road section and which might consequently struggle with a different road section. The usefulness of combining the aforementioned aspects in a single approach is demonstrated by an evaluation using recordings of real pedestrians.

This work presents techniques for efficiently checking location compliance of automated road vehicles. We refer to location compliance as an allowed translational and rotational positioning of a vehicle on a road network, i.e., the vehicle does not enter forbidden lanes or regions reserved for other traffic participants, such as bike lanes or dedicated bus routes. Previous work has mostly focused on efficient collision detection between traffic participants and static obstacles represented as bounded sets. We formulate location compliance as a set enclosure problem, which cannot be solved directly with collision detection; thus, different algorithms from computational geometry have to be applied. We present polygon enclosure and boundary mesh generation approaches and evaluate them using existing road geometries from the CommonRoad database. For a fair comparison, we generate thousands of random instances which are evaluated statistically.

Predicting the occupancy of a human in real time is of great interest in human-robot coexistence for obtaining regions that a robot should avoid in safe motion planning. The human body is composed of joints and links, suiting approximation by a kinematic chain, but the control strategy of the human is completely unknown, meaning the potential occupancy grows very fast and it is difficult to compute tightly in real time. As such, most previous work considers only specific, known, or probable movements, and usually does not account for a range of human dimensions. Focusing on the human arm, we analyze archetypal movements performed by test subjects to create a dynamic model. Motion-capture data of subjects are fitted, for modeling purposes, to two abstractions: a 4-degree of freedom (DOF) model and a 3-DOF model, to obtain dynamic parameters. We validate our approach on movements from a publicly available database. The prediction is shown to be computationally fast, and reachable sets of the abstraction are shown to enclose all possible future occupancies of the arm for different subjects, tightly but overapproximatively. The 3DOF model has advantages over the 4-DOF in terms of speed, though the 4-DOF model is tighter at smaller time horizons. Such an overapproximative representation is intended for certifiable safety-guaranteed collision avoidance algorithms for robots.

This paper presents an algorithm for overapproximating the drivable area of road vehicles in the presence of time-varying obstacles. The drivable area can be used to detect whether a feasible trajectory exists and in which area one can limit the search of drivable trajectories. For this purpose, we abstract the considered road vehicle by a point mass with bounded velocity and acceleration. Our algorithm calculates the reachable occupancy at discrete time steps. At each time step, the set is represented by a union of finitely many sets, which are each the Cartesian product of two 2-D convex polytopes. We demonstrate our method with three examples: i) a traffic situation with identical dynamic constraints in the x- and y-directions; ii) a highway scenario with different lateral and longitudinal constraints of the dynamics; and iii) a highway scenario with different traffic predictions. The examples demonstrate that we can compute the drivable area quickly enough to deploy our approach in real vehicles.

In this paper, we present a novel global tracking control approach for elastic-joint robots that can be efficiently computed and is robust against model uncertainties and input disturbances. Elastic-joint robots provide enhanced safety and resiliency for interaction with the environment and humans. On the other hand, the joint elasticity complicates the motion-control problem especially when robust and precise trajectory tracking is required. Our proposed control approach allows us to merge the main benefits of the two well-known control schemes: inverse-dynamics (ID) control, which can be efficiently computed thanks to modern recursive algorithms, and passivity-based (PB) tracking control, which provides enhanced robustness to model uncertainty and external disturbances. As an extension of our previous work, we present a detailed robustness analysis of our combined ID/PB controller, a new variant of the original scheme that shows practically relevant implications, and finally, experimental results that verify the effectiveness of the approach.

A new control method for nonlinear systems is presented which solves reach-avoid problems by interpolating optimal solutions using convex combinations. It also provides formal guarantees for constraint satisfaction and safety. Reach-avoid problems are important control tasks, which arise in many modern cyber-physical systems, including autonomous driving and robotic path planning. We obtain our control policy by computing the optimal input trajectories for finitely many extreme states only and combining them using convex combinations for all states in a continuous set. Our approach has very low online computation complexity, making it applicable for fast dynamical systems. Iterating through our approach leads to a new form of feedback control with formal guarantees in the presence of disturbances. We demonstrate the new control method for a control problem in automated driving and show the advantages compared to a classical control method.

We consider the global tracking control problem of robots with elastic joints. Even if joint elasticity introduces beneficial features for modern applications which require physically resilient and safer robots that can interact with the environment or humans, it challenges the achievable control performance. We propose a novel controller which combines the benefits of two approaches: the intrinsic robustness to model uncertainty from passivity-based control and the implementation efficiency of inverse-dynamics control schemes using a modern recursive algorithm. The novel controller is applied to an elastic-joint reconfigurable robotic arm using a recently proposed framework for on-the-fly control design. Simulation and experimental results validate our proposed approach.

Commercially available robots cannot always be adapted to arbitrary tasks or environments, particularly when the task would exceed the kinematic or dynamic limits of the robot. Modular robots offer a solution to this problem, since they can be reconfigured in various ways from a set of modules. The challenge of choosing the optimal composition for a given task, however, is hard since the search space of compositions is vast. Our approach addresses this problem: instead of finding the cost-optimal solution over all possible compositions individually, we propose a time-efficient composition synthesis method which uses evolutionary algorithms by taking task-related objectives into account. Simulations show that our algorithm finds the cost-optimal module composition with less computation time than other methods in the literature.

Mobile robots operating in a shared environment with pedestrians are required to move provably safe to avoid harming pedestrians. Current approaches like safety fields use conservative obstacle models for guaranteeing safety, which leads to degraded performance in populated environments. In this paper, we introduce an online verification approach that uses information about the current pedestrian velocities to compute possible occupancies based on a kinematic model of pedestrian motion. We demonstrate that our method reduces the need for stopping while retaining safety guarantees, and thus goals are reached between 1.4 and 3.5 times faster than the standard ROS navigation stack in the tested scenarios.

We address the problem of overapproximative short-term prediction of arm movement, for safe human-robot co-existence. A trajectory planner for a robot manipulator which formally verifies non-collision requires fast prediction of human future occupancy, which must be accurate yet still account for all possible human movement. This work presents two approaches to this: a novel, simple approach calculated directly in task space, and another approach using a kinematic model of the human based on the authors' previous work. We compare both approaches in an experimental setup with a robot manipulator. To the best of our knowledge, this is the first implementation and comparison of approaches to formally verified trajectory planning in human-robot co-working. We find that the novel approach has advantages in terms of ease and speed of computation and tightness at short time horizons and is more intuitive to extend to the whole human body; the previous approach offers advantages at longer prediction horizons. We also perform conformance checking to show that both approaches do indeed account for all relevant movement.

Numerical experiments for motion planning of road vehicles require numerous components: vehicle dynamics, a road network, static obstacles, dynamic obstacles and their movement over time, goal regions, a cost function, etc. Providing a description of the numerical experiment precise enough to reproduce it might require several pages of information. Thus, only key aspects are typically described in scientific publications, making it impossible to reproduce results - yet, re-producibility is an important asset of good science. Composable benchmarks for motion planning on roads (CommonRoad) are proposed so that numerical experiments are fully defined by a unique ID; all information required to reconstruct the experiment can be found on the CommonRoad website. Each benchmark is composed by a vehicle model, a cost function, and a scenario (including goals and constraints). The scenarios are partly recorded from real traffic and partly hand-crafted to create dangerous situations. We hope that CommonRoad saves researchers time since one does not have to search for realistic parameters of vehicle dynamics or realistic traffic situations, yet provides the freedom to compose a benchmark that fits one's needs.

Predicting the movement of other traffic participants is an integral part in the motion planning of most automated road vehicles. While simple predictions, e.g. based on assuming constant velocity, may suffice for deciding a driving strategy, predicting the set of all possible behaviors is required to ensure safe motion plans. In this work, we propose a novel tool for the latter problem based on reachability analysis: Set-Based Prediction Of Traffic Participants (SPOT). Our tool can predict the future occupancy of other traffic participants, including all possible maneuvers (e.g. full acceleration, full braking, and arbitrary lane changes), by considering physical constraints and assuming that the traffic participants abide by the traffic rules. However, we remove assumptions for each traffic participant individually as soon as a violation of a traffic rule is detected. Removal of assumptions automatically results in larger occupancies and thus a smaller drivable area for the ego vehicle, ensuring that the ego vehicle does not cause a collision during the time horizon of the prediction. Experimental results show that we obtain the set of future occupancies within a fraction of the prediction horizon. Our tool is available at spot.in.tum.de.

We introduce a novel concept based on maneuver templates, which are formalized collaborative maneuvers, to select cooperative driving strategies. The approach is based on the exclusion principle, where we derive provable conditions to discard unsafe cooperative maneuvers for a given traffic situation. We thereby consider the full action set of all cooperative vehicles and do not discretize the action space. We demonstrate the applicability of our approach with numerical examples.

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.

Motion planing in dynamic traffic scenes is a challenging problem. In particular, since it is unknown during planning whether a certain decision, such as passing another traffic participant on the left or right, will result in a safe and comfortable motion. Exhaustive exploration of all principle driving paths is computationally expensive, so that one typically reverts to heuristics - this, however can be unsatisfactory in situations when the heuristics fail to find a solution although it exists. We address this problem by computing the union of all possible motions for a sequence of high-level decisions (e.g. overtake vehicle on the left and then another one on the right), which we refer to as a driving corridor. Our proposed algorithm is over-approximative, i.e. the union of driving corridors provably encloses all possible motions. Thus, if the set of reachable positions within a driving corridor becomes empty, the corresponding sequence of high-level decisions is infeasible and can be discarded by the motion planner. Driving corridors also facilitate selecting high-level plans: Large driving corridors should be preferred since they provide more opportunities for optimizing motions and are more robust towards unpredicted changes. Numerical examples demonstrate the usefulness of our approach.

Industrial-sized hybrid systems are typically not amenable to formal verification techniques. For this reason, a common approach is to formally verify abstractions of (parts of) the original system. However, we need to show that this abstraction conforms to the actual system implementation including its physical dynamics. In particular, verified properties of the abstract system need to transfer to the implementation. To this end, we introduce a formal conformance relation, called reachset conformance, which guarantees transference of safety properties, while being a weaker relation than the existing trace inclusion conformance. Based on this formal relation, we present a conformance testing method which allows us to tune the trade-off between accuracy and computational load. Additionally, we present a test selection algorithm that uses a coverage measure to reduce the number of test cases for conformance testing. We experimentally show the benefits of our novel techniques based on an example from autonomous driving.

This paper presents a time-efficient, task-based configuration synthesis algorithm for modular robot manipulators. One of the main challenges in modular manipulators is to find possible combinations of modules that are able to complete given tasks while avoiding obstacles in the environment. Most studies on modular robots focus on obtaining combinations of modules to achieve a given task without considering the required path planning in an environment with obstacles. In contrast to previous works, we present a configuration synthesis method for modular manipulators, considering collision detection and path planning in task space. Our simulations show that our approach finds possible combinations with reduced computational time compared to previous techniques.

Human motion is fast and hard to predict. To implement a provably safe collision-avoidance strategy for robots in collaborative spaces with humans, an overapproximative prediction of the occupancy of the human is required, which needs to be calculated faster than real time. We present a method for computing volumes containing the entire possible future occupancy of the human, given its state, faster than real time. The dynamic model of the human is built from analysing a set of archetypal movements performed by test subjects. The occupancy prediction is tested on a publicly available database of motion capture data, and shown to be overapproximative for all movements relating to everyday activities, sport and dance. Our novel algorithm is useful to guarantee safety in human-robot collaboration scenarios.

We present a framework for online coordinated obstacle avoidance with formal safety guarantees. Such a formally verified trajectory planner can be used in shared human-robot workspaces to guarantee safety. The obstacle avoidance is based on estimation of the human occupancy on two different time scales. A long-term plan is created based on a probabilistic task representation, learned by demonstration, and an estimate of the human occupancy to be avoided. Using an additional overapproximative, short-term prediction of human motion we guarantee that the robot can always account for sudden or reflex movements. We demonstrate our two-level obstacle avoidance in simulation. The results show that our method reduces the number of safety stops one would encounter when using only the formal safety verification, and synthesizes alternative movement plans that preserves the coordination observed in the original demonstrations.

We address the problem of formally verifying nonlinear analog circuits with an uncertain initial set by computing their reachable set. A reachable set contains the union of all possible system trajectories for a set of uncertain states and as such can be used to provably check whether undesired behavior is possible or not. Our method is based on local linearizations of the nonlinear circuit, which naturally results in a piecewise-linear system. To substantially limit the number of required locations, our approach computes linearized locations on-the-fly depending on which states are reachable. We can show that without the proposed on-the-fly technique, the conversion to piecewise-linear systems is infeasible even for a few nonlinear semiconductor devices (discrete state-space explosion problem). Our method is fully automatic and only requires a circuit netlist. Piecewise-linear systems have gained popularity not only for verification, but also for accelerated simulation of nonlinear circuits. Our method provides a guaranteed bound on the number of linearization locations that have to be explicitly computed for such a nonlinear circuit.

A failsafe control strategy is presented for online safety certification of robot movements in a collaborative workspace with humans. This approach plans, predicts and uses formal guarantees on reachable sets of a robot arm and a human obstacle to verify the safety and feasibility of a trajectory in real time. The robots considered are serial link robots under Computed Torque schemes of control. We drastically reduce the computation time of our novel verification procedure through precomputation of non-linear terms and use of interval arithmetic, as well as representation of reachable sets by zonotopes, which scale easily to high dimensions and are easy to convert between joint space and Cartesian space. The approach is implemented in a simulation, to show that real time is computationally within reach.

We address the problem of verifying motion plans for aerial robots in uncertain and partially-known environments. Thereby, the initial state of the robot is uncertain due to errors from the state estimation and the motion is uncertain due to wind disturbances and control errors caused by sensor noise. Since the environment is perceived at runtime, the verification of partial motion plans must be performed online (i.e. during operation) to ensure safety within the planning horizon and beyond. This is achieved by efficiently generating robust control invariant sets based on so-called loiter circles, where the position of the aerial robot follows a circular pattern. Verification of aerial robots is challenging due to the nonlinearity of their dynamics, the high dimensionality of their state space, and their potentially high velocities. We use novel techniques from reachability analysis to overcome those challenges. In order to ensure that the robot never finds itself in a situation for which no safe maneuver exists, we provide a technique that ensures safety of aerial robots beyond the planning horizon. Our method is applicable to all kinds of robotic systems that follow reference trajectories, such as bipedal robotic walking, robotic manipulators, automated vehicles, and the like. We evaluate our method by simulations of high speed helicopter flights.

We address the problem of controlling modular robot manipulators. The challenge of modular-robot control is that the overall system dynamics are unknown due to its flexible composition from given modules. Most previous work has faced this problem by designing decentralized controllers. Simple decentralized controllers do not guarantee global asymptotic stability without knowledge of the overall system dynamics and alternative versions involving communication with neighboring modules result in complicated control concepts. Our approach is completely different: we store parameters regarding the dynamics and kinematics of each module and a unique identification number in itself. After finishing the assembly of the modules, the parameters are gathered in a central controller, which also detects the configuration using the identification numbers. Our centralized controller uses this information to synthesize model-based control laws on-the-fly as if the full system dynamics are known beforehand. We introduce a novel and compact notation to automate this procedure and to generalize the derivation of the kinematic and dynamic model for heterogeneous modules. Finally, a possible application is shown using simulations.

Future collision avoidance systems, which are capable of fully controlling the vehicle, have to make critical decisions in a very short time. To do this, they need to check constantly if their own vehicle's occupancy collides with the other traffic participants' occupancy. Those collision checks consume a substantial amount of time and consequently, the collision avoidance systems could fail to intervene in complex scenarios. We propose a new approach to reduce the computation time for collision checks significantly. Instead of using geometric methods, we store finitely many possible collision scenarios between two objects in a table and thus collision checks become a matter of lookup table queries. To ensure that the finite number of configurations cover all possible scenarios, we use a novel abstraction technique which guarantees that every collision will be detected. The approach works for arbitrarily many traffic participants by applying the approach pairwise (own vehicle and other object) to each traffic participant. Randomly generated scenarios show that the new approach can be several times faster than geometric intersection techniques thanks to the trade-off between memory consumption and computation time.

An increasing amount of robotic systems is developed for safety-critical scenarios, such as automated cars operating in public road traffic or robots collaborating with humans in flexible manufacturing systems. For this reason, it is important to provide methods that formally verify the safety of robotic systems. This is challenging since robots operate in continuous action spaces in partially unknown environments so that there exists no finite set of scenarios that can be verified before deployment. Verifying the safety during the operation based on the current perception of the environment is often infeasible due to the computational demand of formal verification methods. In this work, we compute sets of behaviors for parameterized motion primitives using reachability analysis, which is used to build a maneuver automaton that connects motion primitives in a safe way. Thus, the computationally expensive task of building a maneuver automaton is performed offline. The proposed analysis method provides the whole set of possible behaviors so that it can be verified whether forbidden state-space regions are avoided during the operation of the robot, to e.g. avoid colliding with obstacles. The method is applied to continuous sets of parameterized motion primitives, making it possible to verify infinitely many motions within the parameter space, which to the best knowledge of the authors has not been published before. The approach is demonstrated for collision avoidance of road vehicles.

An approach for formally verifying the safety of automated vehicles is proposed. Due to the uniqueness of each traffic situation, we verify safety online, i.e., during the operation of the vehicle. The verification is performed by predicting the set of all possible occupancies of the automated vehicle and other traffic participants on the road. In order to capture all possible future scenarios, we apply reachability analysis to consider all possible behaviors of mathematical models considering uncertain inputs (e.g., sensor noise, disturbances) and partially unknown initial states. Safety is guaranteed with respect to the modeled uncertainties and behaviors if the occupancy of the automated vehicle does not intersect that of other traffic participants for all times. The applicability of the approach is demonstrated by test drives with an automated vehicle at the Robotics Institute at Carnegie Mellon University.

A new technique for computing the reachable set of hybrid systems with nonlinear continuous dynamics is presented. Previous work showed that abstracting the nonlinear continuous dynamics to linear differential inclusions results in a scalable approach for reachability analysis. However, when the abstraction becomes inaccurate, linearization techniques require splitting of reachable sets, resulting in an exponential growth of required linearizations. In this work, the nonlinearity of the dynamics is more accurately abstracted to polynomial difference inclusions. As a consequence, it is no longer guaranteed that reachable sets of consecutive time steps are mapped to convex sets as typically used in previous works. Thus, a non-convex set representation is developed in order to better capture the nonlinear dynamics, requiring no or much less splitting. The new approach has polynomial complexity with respect to the number of continuous state variables when splitting can be avoided and is thus promising when a linearization technique requires splitting for the same problem. The benefits are presented by numerical examples.

Over the last years a number of different vehicle controllers has been proposed for tracking planned paths or trajectories. Most of previously published works do not compare their results with other approaches or limit the comparison to a few scenarios. Unfortunately, comparisons with existing controller concepts are very rare and a ranking is hard to establish from the literature. In this work, we rigorously compare inversion-based trajectory tracking controllers by systematically exploring the set of possible solutions when disturbances vary over time and initial states and parameters are uncertain. By using Monte-Carlo simulation, we determine the average performance and by using rapidly exploring random trees, we determine the worst-case performance, which is especially important in emergency situations when avoiding a crash is essential. The tested scenarios and the applied methodologies are documented in detail so that they serve as benchmark problems for other control concepts. The results show that the controller with smaller relative degree performs better with respect to the worst-case deviation computed by rapidly exploring random trees, while conventional simulations of random scenarios would not reveal any difference.

Although a growing number of dynamical systems studied in various fields are hybrid in nature, the verification of properties, such as stability, safety, etc., is still a challenging problem. Reachability analysis is one of the promising methods for hybrid system verification, which together with all other verification techniques faces the challenge of making the analysis scale with respect to the number of continuous state variables. The bottleneck of many reachability analysis techniques for hybrid systems is the geometrically computed intersection with guard sets. In this work, we replace the intersection operation by a nonlinear mapping onto the guard, which is not only numerically stable, but also scalable, making it possible to verify systems which were previously out of reach. The approach can be applied to the fairly common class of hybrid systems with piecewise continuous solutions, guard sets modeled as halfspaces, and urgent semantics, i.e. discrete transitions are immediately taken when enabled by guard sets. We demonstrate the usefulness of the new approach by a mechanical system with backlash which has 101 continuous state variables.

This paper presents a method for using set-based approximations to the Peano-Baker series to compute overapproximations of reachable sets for linear systems with uncertain, time-varying parameters and inputs. Alternative representations for sets of uncertain system matrices are considered, including matrix polytopes, matrix zonotopes, and interval matrices. For each representation, the computational efficiency and resulting approximation error for reachable set computations are evaluated analytically and empirically. As an application, reachable sets are computed for a truck with hybrid dynamics due to a gain-scheduled yaw controller. As an alternative to computing reachable sets for the hybrid model, for which switching introduces an additional overapproximation error, the gain-scheduled controller is approximated with uncertain time-varying parameters, which leads to more efficient and more accurate reachable set computations.

We present an approach for verifying locking of charge-pump phase-locked loops by performing reachability analysis on a behavioral model of the circuit. Bounded uncertain parameters in the behavioral model make it possible to represent all possible behaviors of more detailed models. The dynamics of the behavioral model is hybrid (i.e., discrete and continuous) due to the switching of charge pumps that drive the analog control circuits. A unique feature of phase-locked loops compared to most other hybrid systems is that they require thousands of switchings in the continuous dynamics to converge sufficiently close to a limit cycle. This makes reachability analysis a challenging task since switches in the dynamics are expensive to compute and result in conservative overapproximations. We solve this problem by overapproximating the effects of the switching conditions with uncertain parameters in linear continuous models, a method we call continuization. Using efficient reachability algorithms for discrete-time linear systems, locking is verified over the complete range of possible initial states of a charge-pump PLL designed in 32nm CMOS SOI technology in comparable time required for Monte Carlo simulations of the same behavioral model.

The probabilistic prediction of road traffic scenarios is addressed. One result is a probabilistic occupancy of traffic participants, and the other result is the collision risk for autonomous vehicles when executing a planned maneuver. The probabilistic occupancy of surrounding traffic participants helps to plan the maneuver of an autonomous vehicle, whereas the computed collision risk helps to decide if a planned maneuver should be executed. Two methods for the probabilistic prediction are presented and compared: 1) Markov chain abstraction and 2) Monte Carlo simulation. The performance of both methods is evaluated with respect to the prediction of the probabilistic occupancy and the collision risk. For each comparison test, we use the same models that generate the probabilistic behavior of traffic participants, where the generation of these data is not compared with real-world data. However, the results independently show the behavior generation that Markov chains are preferred for the probabilistic occupancy, whereas Monte Carlo simulation is clearly preferred for determining the collision risk.

For path planning algorithms of robots it is important that the robot does not reach a state of inevitable collision. In crowded environments with many humans or robots, the set of possible inevitable collision states (ICS) is often unacceptably high, such that the robot has to stop and wait in too many situations. For this reason, the concept of ICS is extended to probabilistic collision states (PCS), which estimates the collision probability for a given state. This allows to efficiently run planning algorithms through crowded environments when accepting a certain collision probability. A further novelty is that the obstacles possibly react to the robot in order to mitigate the risk of a collision. The results show a significant difference in interaction behavior. Thus, this approach is especially suited for active and non-deterministic moving obstacles in the robot workspace.

The verification of evasive maneuvers for autonomous vehicles driving with constant velocity is considered. Modeling uncertainties, uncertain measurements, and disturbances can cause substantial deviations from an initially planned evasive maneuver. From this follows that the maneuver, which is safe under perfect conditions, might become unsafe. In this work, the possible set of deviations is computed with methods from reachability analysis, which allows to verify evasive maneuvers under consideration of the mentioned uncertainties. Since the presented approach has a short response time, it can be applied for real time safety decisions. The methods are presented for a numerical example where two autonomous cars plan a coordinated evasive maneuver in order to prevent a collision with a wrong-way driver.

The safety of the planned paths of autonomous cars with respect to the movement of other traffic participants is considered. Therefore, the stochastic occupancy of the road by other vehicles is predicted. The prediction considers uncertainties originating from the measurements and the possible behaviors of other traffic participants. In addition, the interaction of traffic participants, as well as the limitation of driving maneuvers due to the road geometry, is considered. The result of the presented approach is the probability of a crash for a specific trajectory of the autonomous car. The presented approach is efficient as most of the intensive computations are performed offline, which results in a lean online algorithm for real-time application.

Robots acting in populated environments must be capable of safe but also time efficient navigation. Trying to completely avoid regions resulting from worst case predictions of the obstacle dynamics may leave no free space for a robot to move, especially in environments with high dynamic. This work presents an algorithm for a ldquosoftrdquo risk mapping of dynamic objects leaving the complete space free of static objects for path planning. Markov Chains are used to model the dynamics of moving persons and predict their potential future locations. These occlusion estimations are mapped into risk regions which serve to plan a path through potentially obstructed space searching for the trade-off between detour and time delay. The offline computation of the Markov Chain model keeps the computational effort low, making the approach suitable for online applications.