Biblio

While automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We introduce an approach to logically reason about functional properties of crossing maneuvers at intersections. To this end, we introduce an abstract model for urban traffic situations and extended timed automata crossing controllers using formulas of our traffic logic Urban Multi-lane Spatial Logic (UMLSL) for turn maneuvers at intersections. We show that even at complex intersections we can use purely spatial reasoning, detached from the underlying car dynamics, to prove safety (collision freedom) of the crossing controllers. We also examine liveness (something good finally happens) and fairness (no queue-jumping) of the controllers with the help of UPPAAL, a model checker for (extended) timed automata. Furthermore, we introduce a case study, where we adapt the approach to a hazard warning communication protocol.

Accountability is an often called for property of technical systems. It is a requirement for algorithmic decision systems, autonomous cyber-physical systems, and for software systems in general. As a concept, accountability goes back to the early history of Liberalism and is suggested as a tool to limit the use of power. This long history has also given us many, often slightly differing, definitions of accountability. The problem that software developers now face is to understand what accountability means for their systems and how to reflect it in a system's design. To enable the rigorous study of accountability in a system, we need models that are suitable for capturing such a varied concept. In this paper, we present a method to express and compare different definitions of accountability using Structural Causal Models. We show how these models can be used to evaluate a system's design and present a small use case based on an autonomous car.

In an effort towards predicting mental workload while driving, previous research found interactions between working memory load and visuospatial demands, which complicates the accurate prediction of momentary mental workload. To investigate this interaction, the cognitive concepts working memory load and visuospatial attention were integrated into a cognitive driving model using the cognitive architecture ACT-R. The model was developed to safely drive on a multi-lane highway with ongoing traffic while performing a secondary n-back task using speed signs. To manipulate visuospatial demands, the model must drive through a construction site with reduced lane-width in certain blocks of the experiment. Furthermore, it is able to handle complex driving situations such as overtaking traffic while adjusting the speed according to the n-back task. The behavioral results show a negative effect on driving performance with increasing task difficulty of the secondary task. Additionally, the model indicates an interaction at a common, task-unspecific level.