Search

In 2017 Day et al. introduced the notion of locality as a structural complexity-measure for patterns in the field of pattern matching established by Angluin in 1980. In 2019 Casel et al. showed that determining the locality of an arbitrary pattern is NP-complete. Inspired by hierarchical clustering, we extend the notion to coloured graphs, i.e., given a coloured graph determine an enumeration of the colours such that colouring the graph stepwise according to the enumeration leads to as few clusters as possible. Next to first theoretical results on graph classes, we propose a priority search algorithm to compute the $k$-locality of a graph. The algorithm is optimal in the number of marking prefix expansions, and is faster by orders of magnitude than an exhaustive search. Finally, we perform a case study on a DBLP subgraph to demonstrate the potential of $k$-locality for knowledge discovery.

In this paper we investigate the problem of detecting, counting, and enumerating (generating) all maximum length plateau-$k$-rollercoasters appearing as a subsequence of some given word (sequence, string), while allowing for plateaus. We define a plateau-$k$-rollercoaster as a word consisting of an alternating sequence of (weakly) increasing and decreasing \emph{runs}, with each run containing at least $k$ \emph{distinct} elements, allowing the run to contain multiple copies of the same symbol consecutively. This differs from previous work, where runs within rollercoasters have been defined only as sequences of distinct values. Here, we are concerned with rollercoasters of \emph{maximum} length embedded in a given word $w$, that is, the longest rollercoasters that are a subsequence of $w$. We present algorithms allowing us to determine the longest plateau-$k$-roller\-coasters appearing as a subsequence in any given word $w$ of length $n$ over an alphabet of size $\sigma$ in $O(n \sigma k)$ time, to count the number of plateau-$k$-rollercoasters in $w$ of maximum length in $O(n \sigma k)$ time, and to output all of them with $O(n)$ delay after $O(n \sigma k)$ preprocessing. Furthermore, we present an algorithm to determine the longest common plateau-$k$-rollercoaster within a set of words in $O(N k \sigma)$ where $N$ is the product of all word lengths within the set.

A scattered factor of a word $w$ is a word $u$ that can be obtained by deleting arbitary letters from $w$ and keep the order of the remaining. Barker et al. introduced the notion of $k$-universality, calling a word $k$-universal, if it contains all possible words of length $k$ over a given alphabet $\Sigma$ as a scattered factor. Kosche et al. introduced the notion of absent scattered factors to categorise the words not being scattered factors of a given word. In this paper, we investigate tight bounds on the possible number of absent scattered factors of a given length $k$ (also strictly longer than the shortest absent scattered factors) among all words with the same universality extending the results of Kosche et al. Specifically, given a length $k$ and universality index $\iota$, we characterize $\iota$-universal words with both the maximal and minimal number of absent scattered factors of length $k$. For the lower bound, we provide the exact number in a closed form. For the upper bound, we offer efficient algorithms to compute the number based on the constructed words. Moreover, by combining old results, we present an enumeration with constant delay of the set of scattered factors of a fixed length in time $O(|\Sigma||w|)$.

Existing statistical methods for the analysis of micro-randomized trials (MRTs) are designed to estimate causal excursion effects using data from a single MRT. In practice, however, researchers can often find previous MRTs that employ similar interventions. In this paper, we develop data integration methods that capitalize on this additional information, leading to statistical efficiency gains. To further increase efficiency, we demonstrate how to combine these approaches according to a generalization of multivariate precision weighting that allows for correlation between estimates, and we show that the resulting meta-estimator possesses an asymptotic optimality property. We illustrate our methods in simulation and in a case study involving two MRTs in the area of smoking cessation.

Mobile health leverages personalized, contextually-tailored interventions optimized through bandit and reinforcement learning algorithms. Despite its promise, challenges like participant heterogeneity, nonstationarity, and nonlinearity in rewards hinder algorithm performance. We propose a robust contextual bandit algorithm, termed "DML-TS-NNR", that simultaneously addresses these challenges via (1) modeling the differential reward with user- and time-specific incidental parameters, (2) network cohesion penalties, and (3) debiased machine learning for flexible estimation of baseline rewards. We establish a high-probability regret bound that depends solely on the dimension of the differential reward model. This feature enables us to achieve robust regret bounds even when the baseline reward is highly complex. We demonstrate the superior performance of the DML-TS-NNR algorithm in a simulation and two off-policy evaluation studies.

A subsequence of a word $w$ is a word $u$ such that $u = w[i_1] w[i_2] \dots w[i_{k}]$, for some set of indices $1 \leq i_1 < i_2 < \dots < i_k \leq \lvert w\rvert$. A word $w$ is $k$-subsequence universal over an alphabet $\Sigma$ if every word in $\Sigma^k$ appears in $w$ as a subsequence. In this paper, we study the intersection between the set of $k$-subsequence universal words over some alphabet $\Sigma$ and regular languages over $\Sigma$. We call a regular language $L$ \emph{$k$-$\exists$-subsequence universal} if there exists a $k$-subsequence universal word in $L$, and \emph{$k$-$\forall$-subsequence universal} if every word of $L$ is $k$-subsequence universal. We give algorithms solving the problems of deciding if a given regular language, represented by a finite automaton recognising it, is \emph{$k$-$\exists$-subsequence universal} and, respectively, if it is \emph{$k$-$\forall$-subsequence universal}, for a given $k$. The algorithms are FPT w.r.t.~the size of the input alphabet, and their run-time does not depend on $k$; they run in polynomial time in the number $n$ of states of the input automaton when the size of the input alphabet is $O(\log n)$. Moreover, we show that the problem of deciding if a given regular language is \emph{$k$-$\exists$-subsequence universal} is NP-complete, when the language is over a large alphabet. Further, we provide algorithms for counting the number of $k$-subsequence universal words (paths) accepted by a given deterministic (respectively, nondeterministic) finite automaton, and ranking an input word (path) within the set of $k$-subsequence universal words accepted by a given finite automaton.

Reliable detection and tracking of surrounding objects are indispensable for comprehensive motion prediction and planning of autonomous vehicles. Due to the limitations of individual sensors, the fusion of multiple sensor modalities is required to improve the overall detection capabilities. Additionally, robust motion tracking is essential for reducing the effect of sensor noise and improving state estimation accuracy. The reliability of the autonomous vehicle software becomes even more relevant in complex, adversarial high-speed scenarios at the vehicle handling limits in autonomous racing. In this paper, we present a modular multi-modal sensor fusion and tracking method for high-speed applications. The method is based on the Extended Kalman Filter (EKF) and is capable of fusing heterogeneous detection inputs to track surrounding objects consistently. A novel delay compensation approach enables to reduce the influence of the perception software latency and to output an updated object list. It is the first fusion and tracking method validated in high-speed real-world scenarios at the Indy Autonomous Challenge 2021 and the Autonomous Challenge at CES (AC@CES) 2022, proving its robustness and computational efficiency on embedded systems. It does not require any labeled data and achieves position tracking residuals below 0.1 m. The related code is available as open-source software at https://github.com/TUMFTM/FusionTracking.

While current research and development of autonomous driving primarily focuses on developing new features and algorithms, the transfer from isolated software components into an entire software stack has been covered sparsely. Besides that, due to the complexity of autonomous software stacks and public road traffic, the optimal validation of entire stacks is an open research problem. Our paper targets these two aspects. We present our autonomous research vehicle EDGAR and its digital twin, a detailed virtual duplication of the vehicle. While the vehicle's setup is closely related to the state of the art, its virtual duplication is a valuable contribution as it is crucial for a consistent validation process from simulation to real-world tests. In addition, different development teams can work with the same model, making integration and testing of the software stacks much easier, significantly accelerating the development process. The real and virtual vehicles are embedded in a comprehensive development environment, which is also introduced. All parameters of the digital twin are provided open-source at https://github.com/TUMFTM/edgar_digital_twin.

In 1991 H\'ebrard introduced a factorization of words that turned out to be a powerful tool for the investigation of a word's scattered factors (also known as (scattered) subwords or subsequences). Based on this, first Karandikar and Schnoebelen introduced the notion of $k$-richness and later on Barker et al. the notion of $k$-universality. In 2022 Fleischmann et al. presented a generalization of the arch factorization by intersecting the arch factorization of a word and its reverse. While the authors merely used this factorization for the investigation of shortest absent scattered factors, in this work we investigate this new $\alpha$-$\beta$-factorization as such. We characterize the famous Simon congruence of $k$-universal words in terms of $1$-universal words. Moreover, we apply these results to binary words. In this special case, we obtain a full characterization of the classes and calculate the index of the congruence. Lastly, we start investigating the ternary case, present a full list of possibilities for $\alpha\beta\alpha$-factors, and characterize their congruence.

Autonomous vehicles demand high accuracy and robustness of perception algorithms. To develop efficient and scalable perception algorithms, the maximum information should be extracted from the available sensor data. In this work, we present our concept for an end-to-end perception architecture, named DeepSTEP. The deep learning-based architecture processes raw sensor data from the camera, LiDAR, and RaDAR, and combines the extracted data in a deep fusion network. The output of this deep fusion network is a shared feature space, which is used by perception head networks to fulfill several perception tasks, such as object detection or local mapping. DeepSTEP incorporates multiple ideas to advance state of the art: First, combining detection and localization into a single pipeline allows for efficient processing to reduce computational overhead and further improves overall performance. Second, the architecture leverages the temporal domain by using a self-attention mechanism that focuses on the most important features. We believe that our concept of DeepSTEP will advance the development of end-to-end perception systems. The network will be deployed on our research vehicle, which will be used as a platform for data collection, real-world testing, and validation. In conclusion, DeepSTEP represents a significant advancement in the field of perception for autonomous vehicles. The architecture's end-to-end design, time-aware attention mechanism, and integration of multiple perception tasks make it a promising solution for real-world deployment. This research is a work in progress and presents the first concept of establishing a novel perception pipeline., Comment: Accepted to be published as part of the 5th Workshop on 3D-Deep Learning for Automated Driving on the 34th IEEE Intelligent Vehicles Symposium (IV), Anchorage, Alaska, USA, June 4-7, 2023

Speed-of-sound (SoS) is a novel imaging biomarker for assessing biomechanical characteristics of soft tissues. SoS imaging in pulse-echo mode using conventional ultrasound systems with hand-held transducers has the potential to enable new clinical uses. Recent work demonstrated diverging waves from single-element (SE) transmits to outperform plane-wave sequences. However, single-element transmits have severely limited power and hence produce low signal-to-noise ratio (SNR) in echo data. We herein propose Walsh-Hadamard (WH) coded and virtual-source (VS) transmit sequences for improved SNR in SoS imaging. We additionally present an iterative method of estimating beamforming SoS in the medium, which otherwise confound SoS reconstructions due to beamforming inaccuracies in the images used for reconstruction. Through numerical simulations, phantom experiments, and in-vivo imaging data, we show that WH is not robust against motion, which is often unavoidable in clinical imaging scenarios. Our proposed virtual-source sequence is shown to provide the highest SoS reconstruction performance, especially robust to motion artifacts. In phantom experiments, despite having a comparable SoS root-mean-square-error (RMSE) of 17.5 to 18.0 m/s at rest, with a minor axial probe motion of ~0.67 mm/s the RMSE for SE, WH, and VS already deteriorate to 20.2, 105.4, 19.0 m/s, respectively; showing that WH produces unacceptable results, not robust to motion. In the clinical data, the high SNR and motion-resilience of VS sequence is seen to yield superior contrast compared to SE and WH sequences.

LiDAR object detection algorithms based on neural networks for autonomous driving require large amounts of data for training, validation, and testing. As real-world data collection and labeling are time-consuming and expensive, simulation-based synthetic data generation is a viable alternative. However, using simulated data for the training of neural networks leads to a domain shift of training and testing data due to differences in scenes, scenarios, and distributions. In this work, we quantify the sim-to-real domain shift by means of LiDAR object detectors trained with a new scenario-identical real-world and simulated dataset. In addition, we answer the questions of how well the simulated data resembles the real-world data and how well object detectors trained on simulated data perform on real-world data. Further, we analyze point clouds at the target-level by comparing real-world and simulated point clouds within the 3D bounding boxes of the targets. Our experiments show that a significant sim-to-real domain shift exists even for our scenario-identical datasets. This domain shift amounts to an average precision reduction of around 14 % for object detectors trained with simulated data. Additional experiments reveal that this domain shift can be lowered by introducing a simple noise model in simulation. We further show that a simple downsampling method to model real-world physics does not influence the performance of the object detectors.

For a century, clinical X-ray imaging has visualised only the attenuation properties of tissue, which fundamentally limits the contrast, particularly in soft tissues like the breast. Imaging based on refraction can overcome this limitation, but so far has been constrained to high-dose ex-vivo applications or required highly coherent X-ray sources, like synchrotrons. It has been predicted that grating interferometry (GI) could eventually allow computed tomography (CT) to be more dose-efficient. However, the benefit of refraction in clinical CT has not been demonstrated so far. Here we show that GI-CT is more dose-efficient in imaging of breast tissue than conventional CT. Our system, based on a 70kVp X-ray tube source and commercially available gratings, demonstrated superior quality, in terms of adipose-to-glandular tissue contrast-to-noise ratio (CNR), of refraction-contrast compared to the attenuation images. The fusion of the two modes of contrast outperformed conventional CT for spatial resolutions better than 263{\mu}m and an average dose to the breast of 16mGy, which is in the clinical breast CT range. Our results show that grating interferometry can significantly reduce the dose, while maintaining the image quality, in diagnostic breast CT. Unlike conventional absorption-based CT, the sensitivity of refraction-based imaging is far from being fully exploited, and further progress will lead to significant improvements of clinical X-ray CT.

Choosing hardware for theorem proving is no simple task: automated provers are highly complex and optimized programs, often utilizing a parallel computation model, and there is little prior research on the hardware impact on prover performance. To alleviate the problem for Isabelle, we initiated a community benchmark where the build time of HOL-Analysis is measured. On $54$ distinct CPUs, a total of $669$ runs with different Isabelle configurations were reported by Isabelle users. Results range from $107$s to over $11$h. We found that current consumer CPUs performed best, with an optimal number of $8$ to $16$ threads, largely independent of heap memory. As for hardware parameters, CPU base clock affected multi-threaded execution most with a linear correlation of $0.37$, whereas boost frequency was the most influential parameter for single-threaded runs (correlation coefficient $0.55$); cache size played no significant role. When comparing our benchmark scores with popular high-performance computing benchmarks, we found a strong linear relationship with Dolfyn ($R^2 = 0.79$) in the single-threaded scenario. Using data from the 3DMark CPU Profile consumer benchmark, we created a linear model for optimal (multi-threaded) Isabelle performance. When validating, the model has an average $R^2$-score of $0.87$; the mean absolute error in the final model corresponds to a wall-clock time of $46.6$s. With a dataset of true median values for the 3DMark, the error improves to $37.1$s.

The Isabelle Archive of Formal Proofs has grown to a significant size in the past years. It makes up for an impressive body of research, which enables a number of statistical approaches to various aspects in theorem proving, and has not yet been utilized exhaustively. However, the growing size also poses some challenges to address: Material becomes increasingly harder to find, reusability and ease of understanding become more important. This thesis abstract summarizes my research plans on those topics and briefly touches on preliminary results, which indicate that the node in-degree of the dependency graph of the archive follows a scale-free distribution., Comment: Extended abstract

In interactive theorem proving, formalization quality is a key factor for maintainability and re-usability of developments and can also impact proof-checking performance. Commonly, anti-patterns that cause quality issues are known to experienced users. However, in many theorem prover systems, there are no automatic tools to check for their presence and make less experienced users aware of them. We attempt to fill this gap in the Isabelle environment by developing a linter as a publicly available add-on component. The linter offers basic configurability, extensibility, Isabelle/jEdit integration, and a standalone command-line tool. We uncovered 480 potential problems in Isabelle/HOL, 14016 in other formalizations of the Isabelle distribution, and an astonishing 59573 in the AFP. With a specific lint bundle for AFP submissions, we found that submission guidelines were violated in 1595 cases. We set out to alleviate problems in Isabelle/HOL and solved 168 of them so far; we found that high-severity lints corresponded to actual problems most of the time, individual users often made the same mistakes in many places, and that solving those problems retrospectively amounts to a substantial amount of work. In contrast, solving these problems interactively for new developments usually incurs only little overhead, as we found in a quantitative user survey with 22 participants (less than a minute for more than 60% of participants). We also found that a good explanation of problems is key to the users' ease of solving these problems (correlation coefficient 0.48), and their satisfaction with the end result (correlation coefficient 0.62)., Comment: Isabelle Workshop 2022

For decades, motorsport has been an incubator for innovations in the automotive sector and brought forth systems like disk brakes or rearview mirrors. Autonomous racing series such as Roborace, F1Tenth, or the Indy Autonomous Challenge (IAC) are envisioned as playing a similar role within the autonomous vehicle sector, serving as a proving ground for new technology at the limits of the autonomous systems capabilities. This paper outlines the software stack and approach of the TUM Autonomous Motorsport team for their participation in the Indy Autonomous Challenge, which holds two competitions: A single-vehicle competition on the Indianapolis Motor Speedway and a passing competition at the Las Vegas Motor Speedway. Nine university teams used an identical vehicle platform: A modified Indy Lights chassis equipped with sensors, a computing platform, and actuators. All the teams developed different algorithms for object detection, localization, planning, prediction, and control of the race cars. The team from TUM placed first in Indianapolis and secured second place in Las Vegas. During the final of the passing competition, the TUM team reached speeds and accelerations close to the limit of the vehicle, peaking at around 270 km/h and 28 ms2. This paper will present details of the vehicle hardware platform, the developed algorithms, and the workflow to test and enhance the software applied during the two-year project. We derive deep insights into the autonomous vehicle's behavior at high speed and high acceleration by providing a detailed competition analysis. Based on this, we deduce a list of lessons learned and provide insights on promising areas of future work based on the real-world evaluation of the displayed concepts., Comment: 37 pages, 18 figures, 2 tables

The Isabelle Archive of Formal Proofs (AFP) has grown to over 500 articles in late 2019. Meanwhile, finding formalizations in it has not exactly become easier. At the time of writing, the site-specific AFP google search and the Isabelle find_theories resp. find_consts commands (that only work on imported theories) are still the only tools readily available to find formalizations in Isabelle. We present FindFacts, a novel domain-specific search tool for formal Isabelle theory content. Instead of utilizing term unification, we solve the problem with a classical drill-down search engine. We put special emphasis on scalability of the search system, so that the whole AFP can be searched interactively., Comment: Isabelle Workshop 2020

Determining the index of the Simon congruence is a long outstanding open problem. Two words $u$ and $v$ are called Simon congruent if they have the same set of scattered factors, which are parts of the word in the correct order but not necessarily consecutive, e.g., $\mathtt{oath}$ is a scattered factor of $\mathtt{logarithm}$. Following the idea of scattered factor $k$-universality, we investigate $m$-nearly $k$-universality, i.e., words where $m$ scattered factors of length $k$ are absent, w.r.t. Simon congruence. We present a full characterisation as well as the index of the congruence for $m=1$. For $m\neq 1$, we show some results if in addition $w$ is $(k-1)$-universal as well as some further insights for different $m$.

Motorsport has always been an enabler for technological advancement, and the same applies to the autonomous driving industry. The team TUM Auton-omous Motorsports will participate in the Indy Autonomous Challenge in Octo-ber 2021 to benchmark its self-driving software-stack by racing one out of ten autonomous Dallara AV-21 racecars at the Indianapolis Motor Speedway. The first part of this paper explains the reasons for entering an autonomous vehicle race from an academic perspective: It allows focusing on several edge cases en-countered by autonomous vehicles, such as challenging evasion maneuvers and unstructured scenarios. At the same time, it is inherently safe due to the motor-sport related track safety precautions. It is therefore an ideal testing ground for the development of autonomous driving algorithms capable of mastering the most challenging and rare situations. In addition, we provide insight into our soft-ware development workflow and present our Hardware-in-the-Loop simulation setup. It is capable of running simulations of up to eight autonomous vehicles in real time. The second part of the paper gives a high-level overview of the soft-ware architecture and covers our development priorities in building a high-per-formance autonomous racing software: maximum sensor detection range, relia-ble handling of multi-vehicle situations, as well as reliable motion control under uncertainty.