Lukas Westhofen 0001

dblp:180/5683-1 · DBLP profile ↗
← Back
7ranked-venue papers
3as first author
5since 2021 · last 2026
0000-0003-1065-4182ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 4 · 2 first-author · 3 since 2021Artificial intelligence and machine learning · 3 · 1 first-author · 2 since 2021Graphics, computer vision, multimedia, augmented reality and games · 1 · 1 first-author · 1 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
YearPublicationVenuePosition
2026 Test Coverage of Automated Robotic Systems in Open World Environments
abstract
Abstract Automated robotic systems operating in real-world environments require thorough test campaigns before deployment, in which engineers assess whether the system is actually exposed to critical scenarios. A well-established way to judge the efficacy of test campaigns in controlled environments is scenario coverage: It quantifies the quality of recorded data from test campaigns w.r.t. a set of (critical) scenario classes of interest. Challenges arise when transferring coverage from controlled to open environments, as it may no longer be exactly determined to which scenario class the recorded test data belongs to: sensors offer limited observability, e.g., by occlusions or hardware failures, and specifications might be inherently vague, e.g., via imprecise traffic regulations. We leverage the Open World Assumption to formally extend scenario coverage to such ambiguous test data and present algorithms for computing guaranteed lower and upper bounds on coverage. Whereas deciding the lower bound problem is $$D^p$$ D p -complete, the upper bound can be computed in polynomial time. We extend an existing coverage software tool with two approaches for incorporating the Open World Assumption, grounded in LTL f . Our evaluation shows that meaningful statements on scenario coverage are feasible, even under intricacies of the real world.
Lukas Westhofen 0001, Till Schallau, Dominik Schmid 0001, Stefan Naujokat, Falk Howar, Daniel Neider
FM (1)1
2025 Temporal Conjunctive Query Answering via Rewriting
abstract
Querying temporal data has recently gained traction in several artificial intelligence applications. As operational domains of intelligent agents are constantly being expanded, there is a strong need for representing domain knowledge. This comes in the form of ontologies, which are predominantly expressed in description logics and enrich time-stamped data to temporal knowledge bases. For modeling highly complex system environments, expressive description logics are often the formalism of choice. Querying such temporal knowledge bases is a challenging task, but recently a first practical solution has been put forward. We propose a novel approach to the query answering problem based on two well-known rewriting rules from temporal logic. After a careful theoretical analysis of our algorithm, we show in a practical evaluation on several benchmarks that it outperforms state of the art, sometimes by orders of magnitude. Based on our findings, we also propose a fragment of temporal conjunctive queries which guides users towards well-performing queries.
Lukas Westhofen 0001, Jean Christoph Jung, Daniel Neider
AAAI1
2025 TSC2CARLA: An abstract scenario-based verification toolchain for automated driving systems
abstract
Transitioning automated driving systems to complex operational domains disproportionally increases demands on verification activities . In the worst case, the operational domain can not be covered by a manageable set of logical scenarios. An anticipated solution is to use abstract scenarios, which increase coverage while still enabling formal methods. However, established verification approaches must be adapted for abstract scenarios. In this work, we consider the generation of simulatable test suites from abstract scenarios. For this, we use Traffic Sequence Charts (TSCs), a visual yet formal scenario description language based on first order logic. We propose an SMT-based process for generating concrete test cases that can be simulated in e.g. CARLA. This theoretical framework is compiled into an architecture and a prototypical implementation called TSC2CARLA. An evaluation on a set of non-trivial examples yields initial evidence for the feasibility of our approach.
Philipp Borchers, Tjark Koopmann, Lukas Westhofen 0001, Jan Steffen Becker, Lina Putze, Dominik Grundt, Thies de Graaff, Vincent Kalwa, Christian Neurohr
Sci. Comput. Program.3
2024 Answering Temporal Conjunctive Queries over Description Logic Ontologies for Situation Recognition in Complex Operational Domains
abstract
Abstract For developing safe automated systems, recognizing safety-critical situations in data from their complex operational domain is imperative. This capability is, for example, essential when evaluating the system’s conformance to specified requirements in test run data. The requirements involve a temporal dimension, as the system operates over time. Moreover, the generated data are usually relational and require additional background knowledge about the domain for correctly recognizing the situation. This fact makes propositional temporal logics, an established tool, unsuitable for the task. We address this issue by developing a tailored temporal logic to query for situations in relational data over complex domains. Our language combines mission-time linear temporal logic with conjunctive queries to access time-stamped data with background knowledge formulated in an expressive description logic. Currently, however, no tools exist for answering queries in such settings. We hence also contribute an implementation in the logic reasoner Openllet, leveraging the efficacy of well-established conjunctive query answering. Moreover, we present a benchmark generator in the setting of automated driving and demonstrate that our tool performs well when tasked with recognizing safety-critical situations in road traffic.
Lukas Westhofen 0001, Christian Neurohr, Jean Christoph Jung, Daniel Neider
TACAS (1)1
2023 On Quantification for SOTIF Validation of Automated Driving Systems
abstract
Automated driving systems are safety-critical cyber-physical systems whose safety of the intended functionality (SOTIF) can not be assumed without proper argumentation based on appropriate evidences. Recent advances in standards and regulations on the safety of driving automation are therefore intensely concerned with demonstrating that the intended functionality of these systems does not introduce unreasonable risks to stakeholders. In this work, we critically analyze the ISO 21448 standard which contains requirements and guidance on how the SOTIF can be provably validated. Emphasis lies on developing a consistent terminology as a basis for the subsequent definition of a validation strategy when using quantitative acceptance criteria. In the broad picture, we aim to achieve a well-defined risk decomposition that enables rigorous, quantitative validation approaches for the SOTIF of automated driving systems.
Lina Putze, Lukas Westhofen 0001, Tjark Koopmann, Eckard Böde, Christian Neurohr
IV2
2020 Fundamental Considerations around Scenario-Based Testing for Automated Driving
abstract
The homologation of automated vehicles, being safety-critical complex systems, requires sound evidence for their safe operability. Traditionally, verification and validation activities are guided by a combination of ISO 26262 and ISO/PAS 21448, together with distance-based testing. Starting at SAE Level 3, such approaches become infeasible, resulting in the need for novel methods. Scenario-based testing is regarded as a possible enabler for verification and validation of automated vehicles. Its effectiveness, however, rests on the consistency and substantiality of the arguments used in each step of the process. In this work, we sketch a generic framework around scenario-based testing and analyze contemporary approaches to the individual steps. For each step, we describe its function, discuss proposed approaches and solutions, and identify the underlying arguments, principles and assumptions. As a result, we present a list of fundamental considerations for which evidences need to be gathered in order for scenario-based testing to support the homologation of automated vehicles.
Christian Neurohr, Lukas Westhofen 0001, Tabea Henning, Thies de Graaff, Eike Möhlmann, Eckard Böde
IV2
2016 Bounded Model Checking for Probabilistic Programs
Nils Jansen 0001, Christian Hensel, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen 0001
ATVA5