## Dissertation

### Filtern

#### Fachbereich / Organisatorische Einheit

- Fachbereich Mathematik (185)
- Fachbereich Informatik (95)
- Fachbereich Maschinenbau und Verfahrenstechnik (58)
- Fachbereich Chemie (39)
- Fachbereich Elektrotechnik und Informationstechnik (37)
- Fachbereich Biologie (21)
- Fachbereich Sozialwissenschaften (12)
- Fachbereich ARUBI (5)
- Fachbereich Physik (5)
- Fraunhofer (ITWM) (4)

#### Erscheinungsjahr

#### Dokumenttyp

- Dissertation (462) (entfernen)

#### Sprache

- Englisch (462) (entfernen)

#### Schlagworte

- Visualisierung (10)
- finite element method (6)
- Algebraische Geometrie (4)
- Finite-Elemente-Methode (4)
- Navier-Stokes-Gleichung (4)
- Numerische Strömungssimulation (4)
- Optimization (4)
- verification (4)
- Computeralgebra (3)
- Computergraphik (3)

- C-H Activation mediated by Transition Metal (2016)
- C-H activations(C-H bond weakening effects) under impact of transition metal atoms are theoretically investigated, two model systems are used, one is CH3MX, the other is n-ButMX, (X=F,Cl,Br,I,H,CN, M include all transition metal atoms from group 4 to group 10).

- Advances in Theory and Applicability of Stochastic Network Calculus (2016)
- Stochastic Network Calculus (SNC) emerged from two branches in the late 90s: the theory of effective bandwidths and its predecessor the Deterministic Network Calculus (DNC). As such SNC’s goal is to analyze queueing networks and support their design and control. In contrast to queueing theory, which strives for similar goals, SNC uses in- equalities to circumvent complex situations, such as stochastic dependencies or non-Poisson arrivals. Leaving the objective to compute exact distributions behind, SNC derives stochastic performance bounds. Such a bound would, for example, guarantee a system’s maximal queue length that is violated by a known small prob- ability only. This work includes several contributions towards the theory of SNC. They are sorted into four main contributions: (1) The first chapters give a self-contained introduction to deterministic net- work calculus and its two branches of stochastic extensions. The focus lies on the notion of network operations. They allow to derive the performance bounds and simplifying complex scenarios. (2) The author created the first open-source tool to automate the steps of cal- culating and optimizing MGF-based performance bounds. The tool automatically calculates end-to-end performance bounds, via a symbolic approach. In a second step, this solution is numerically optimized. A modular design allows the user to implement their own functions, like traffic models or analysis methods. (3) The problem of the initial modeling step is addressed with the development of a statistical network calculus. In many applications the properties of included elements are mostly unknown. To that end, assumptions about the underlying processes are made and backed by measurement-based statistical methods. This thesis presents a way to integrate possible modeling errors into the bounds of SNC. As a byproduct a dynamic view on the system is obtained that allows SNC to adapt to non-stationarities. (4) Probabilistic bounds are fundamentally different from deterministic bounds: While deterministic bounds hold for all times of the analyzed system, this is not true for probabilistic bounds. Stochastic bounds, although still valid for every time t, only hold for one time instance at once. Sample path bounds are only achieved by using Boole’s inequality. This thesis presents an alternative method, by adapting the theory of extreme values. (5) A long standing problem of SNC is the construction of stochastic bounds for a window flow controller. The corresponding problem for DNC had been solved over a decade ago, but remained an open problem for SNC. This thesis presents two methods for a successful application of SNC to the window flow controller.

- Numerical Modeling for the Static and Dynamic Analysis of Nearly Incompressible Dielectric Elastomers (2016)
- This thesis investigates the electromechanic coupling of dielectric elastomers for the static and dynamic case by numerical simulations. To this end, the fundamental equations of the coupled field problem are introduced and the discretisation procedure for the numerical implementation is described. Furthermore, a three field formulation is proposed and implemented to treat the nearly incompressible behaviour of the elastomer. Because of the reduced electric permittivity of the material, very high electric fields are required for actuation purposes. To improve the electromechanic coupling a heterogeneous microstructure consisting of an elastomer matrix with barium titanate inclusions is proposed and studied.

- Symbolic Simulation of Mixed-Signal Systems with Extended Affine Arithmetic (2016)
- Mixed-signal systems combine analog circuits with digital hardware and software systems. A particular challenge is the sensitivity of analog parts to even small deviations in parameters, or inputs. Parameters of circuits and systems such as process, voltage, and temperature are never accurate; we hence model them as uncertain values (‘uncertainties’). Uncertain parameters and inputs can modify the dynamic behavior and lead to properties of the system that are not in specified ranges. For verification of mixed- signal systems, the analysis of the impact of uncertainties on the dynamical behavior plays a central role. Verification of mixed-signal systems is usually done by numerical simulation. A single numerical simulation run allows designers to verify single parameter values out of often ranges of uncertain values. Multi-run simulation techniques such as Monte Carlo Simulation, Corner Case simulation, and enhanced techniques such as Importance Sampling or Design-of-Experiments allow to verify ranges – at the cost of a high number of simulation runs, and with the risk of not finding potential errors. Formal and symbolic approaches are an interesting alternative. Such methods allow a comprehensive verification. However, formal methods do not scale well with heterogeneity and complexity. Also, formal methods do not support existing and established modeling languages. This fact complicates its integration in industrial design flows. In previous work on verification of Mixed-Signal systems, Affine Arithmetic is used for symbolic simulation. This allows combining the high coverage of formal methods with the ease-of use and applicability of simulation. Affine Arithmetic computes the propagation of uncertainties through mostly linear analog circuits and DSP methods in an accurate way. However, Affine Arithmetic is currently only able to compute with contiguous regions, but does not permit the representation of and computation with discrete behavior, e.g. introduced by software. This is a serious limitation: in mixed-signal systems, uncertainties in the analog part are often compensated by embedded software; hence, verification of system properties must consider both analog circuits and embedded software. The objective of this work is to provide an extension to Affine Arithmetic that allows symbolic computation also for digital hardware and software systems, and to demonstrate its applicability and scalability. Compared with related work and state of the art, this thesis provides the following achievements: 1. The thesis introduces extended Affine Arithmetic Forms (XAAF) for the representation of branch and merge operations. 2. The thesis describes arithmetic and relational operations on XAAF, and reduces over-approximation by using an LP solver. 3. The thesis shows and discusses ways to integrate this XAAF into existing modeling languages, in particular SystemC. This way, breaks in the design flow can be avoided. The applicability and scalability of the approach is demonstrated by symbolic simulation of a Delta-Sigma Modulator and a PLL circuit of an IEEE 802.15.4 transceiver system.

- Rydberg-ground state interaction in ultracold quantum gases (2016)
- Combining ultracold atomic gases with the peculiar properties of Rydberg excited atoms gained a lot of theoretical and experimental attention in recent years. Embedded in the ultracold gas, an interaction between the Rydberg atom and the surrounding ground state atoms arises through the scattering of the Rydberg electron from an intruding perturber atom. This peculiar interaction gives rise to a plenitude of previously unobserved effects. Within the framework of the present thesis, this interaction is studied in detail for Rydberg \(P\)-states in rubidium. Due to their long lifetime, atoms in Rydberg states are subject to scattering with the surrounding ground state atoms in the ultracold cloud. By measuring their lifetime as a function of the ground state atom flux, we are able to obtain the total inelastic scattering cross section as well as the partial cross section for associative ionisation. The fact that the latter is three orders of magnitude larger than the size of the formed molecular ion indicates the presence of an efficient mass transport mechanism that is mediated by the Rydberg–ground state interaction. The immense acceleration of the collisional process shows a close analogy to a catalytic process. The increase of the scattering cross section renders associative ionisation an important process that has to be considered for experiments in dense ultracold systems. The interaction of the Rydberg atom with a ground state perturber gives rise to a highly oscillatory potential that supports molecular bound states. These so-called ultralong-range Rydberg molecules are studied with high resolution time-of-flight spectroscopy, where we are able to determine the binding energies and lifetimes of the molecular states between the two fine structure split \(25P\)-states. Inside an electric field, we observe a broadening of the molecular lines that indicates the presence of a permanent electric dipole moment, induced by the mixing with high angular momentum states. Due to the mixing of the ground state atom’s hyperfine states by the molecular interaction, we are able to observe a spin-flip of the perturber upon creation of a Rydberg molecule. Furthermore, an incidental near-degeneracy in the underlying level scheme of the \(25P\)-state gives rise to highly entangled states between the Rydberg fine structure state and the perturber’s hyperfine structure. These mechanisms can be used to manipulate the quantum state of a remote particle over distances that exceed by far the typical contact interaction range. Apart from the ultralong-range Rydberg molecules that predominantly consist of only one low angular momentum state, a class of Rydberg molecules is predicted to exist that strongly mixes the high angular momentum states of the degenerate hydrogenic manifolds. These states, the so-called trilobite- and butterfly Rydberg molecules, show very peculiar properties that cannot be observed for conventional molecules. Here we present the first experimental observation of butterfly Rydberg molecules. In addition to an extensive spectroscopy that reveals the binding energy, we are also able to observe the rotational structure of these exotic molecules. The arising pendular states inside an electric field allow us, in comparison to the model of a dipolar rotor, to extract the precise bond length and dipole moment of the molecule. With the information obtained in the present study, it is possible to photoassociate butterfly molecules with a selectable bond length, vibrational state, rotational state, and orientation inside an electric field. By shedding light on various previously unrevealed aspects, the experiments presented in this thesis significantly deepen our knowledge on the Rydberg–ground state interaction and the peculiar effects arising from it. The obtained spectroscopic information on Rydberg molecules and the changed reaction dynamics for molecular ion creation will surely provide valuable data for quantum chemical simulations and provide necessary data to plan future experiments. Beyond that, our study reveals that the hyperfine interaction in Rydberg molecules and the peculiar properties of butterfly states provide very promising new ways to alter the short- and long-range interactions in ultracold many-body systems. In this sense the investigated Rydberg–ground state interaction not only lies right at the interface between quantum chemistry, quantum many-body systems, and Rydberg physics, but also creates many new and fascinating possibilities by combining these fields.

- Verification Techniques for TSO-Relaxed Programs (2016)
- Knowing the extent to which we rely on technology one may think that correct programs are nowadays the norm. Unfortunately, this is far from the truth. Luckily, possible reasons why program correctness is difficult often come hand in hand with some solutions. Consider concurrent program correctness under Sequential Consistency (SC). Under SC, instructions of each program's concurrent component are executed atomically and in order. By using logic to represent correctness specifications, model checking provides a successful solution to concurrent program verification under SC. Alas, SC’s atomicity assumptions do not reflect the reality of hardware architectures. Total Store Order (TSO) is a less common memory model implemented in SPARC and in Intel x86 multiprocessors that relaxes the SC constraints. While the architecturally de-atomized execution of stores under TSO speeds up program execution, it also complicates program verification. To be precise, due to TSO’s unbounded store buffers, a program’s semantics under TSO might be infinite. This, for example, turns reachability under SC (a PSPACE-complete task) into a non-primitive-recursive-complete problem under TSO. This thesis develops verification techniques targeting TSO-relaxed programs. To be precise, we present under- and over-approximating heuristics for checking reachability in TSO-relaxed programs as well as state-reducing methods for speeding up such heuristics. In a first contribution, we propose an algorithm to check reachability of TSO-relaxed programs lazily. The under-approximating refinement algorithm uses auxiliary variables to simulate TSO’s buffers along instruction sequences suggested by an oracle. The oracle’s deciding characteristic is that if it returns the empty sequence then the program’s SC- and TSO-reachable states are the same. Secondly, we propose several approaches to over-approximate TSO buffers. Combined in a refinement algorithm, these approaches can be used to determine safety with respect to TSO reachability for a large class of TSO-relaxed programs. On the more technical side, we prove that checking reachability is decidable when TSO buffers are approximated by multisets with tracked per address last-added-values. Finally, we analyze how the explored state space can be reduced when checking TSO and SC reachability. Intuitively, through the viewpoint of Shasha-and-Snir-like traces, we exploit the structure of program instructions to explain several state-space reducing methods including dynamic and cartesian partial order reduction.

- Modeling Road Roughness with Conditional Random Fields (2016)
- A vehicles fatigue damage is a highly relevant figure in the complete vehicle design process. Long term observations and statistical experiments help to determine the influence of differnt parts of the vehicle, the driver and the surrounding environment. This work is focussing on modeling one of the most important influence factors of the environment: road roughness. The quality of the road is highly dependant on several surrounding factors which can be used to create mathematical models. Such models can be used for the extrapolation of information and an estimation of the environment for statistical studies. The target quantity we focus on in this work ist the discrete International Roughness Index or discrete IRI. The class of models we use and evaluate is a discriminative classification model called Conditional Random Field. We develop a suitable model specification and show new variants of stochastic optimizations to train the model efficiently. The model is also applied to simulated and real world data to show the strengths of our approach.

- Dual-Pivot Quicksort and Beyond: Analysis of Multiway Partitioning and Its Practical Potential (2016)
- Multiway Quicksort, i.e., partitioning the input in one step around several pivots, has received much attention since Java 7’s runtime library uses a new dual-pivot method that outperforms by far the old Quicksort implementation. The success of dual-pivot Quicksort is most likely due to more efficient usage of the memory hierarchy, which gives reason to believe that further improvements are possible with multiway Quicksort. In this dissertation, I conduct a mathematical average-case analysis of multiway Quicksort including the important optimization to choose pivots from a sample of the input. I propose a parametric template algorithm that covers all practically relevant partitioning methods as special cases, and analyze this method in full generality. This allows me to analytically investigate in depth what effect the parameters of the generic Quicksort have on its performance. To model the memory-hierarchy costs, I also analyze the expected number of scanned elements, a measure for the amount of data transferred from memory that is known to also approximate the number of cache misses very well. The analysis unifies previous analyses of particular Quicksort variants under particular cost measures in one generic framework. A main result is that multiway partitioning can reduce the number of scanned elements significantly, while it does not save many key comparisons; this explains why the earlier studies of multiway Quicksort did not find it promising. A highlight of this dissertation is the extension of the analysis to inputs with equal keys. I give the first analysis of Quicksort with pivot sampling and multiway partitioning on an input model with equal keys.

- Signature Standard Bases over Principal Ideal Rings (2016)
- By using Gröbner bases of ideals of polynomial algebras over a field, many implemented algorithms manage to give exciting examples and counter examples in Commutative Algebra and Algebraic Geometry. Part A of this thesis will focus on extending the concept of Gröbner bases and Standard bases for polynomial algebras over the ring of integers and its factors \(\mathbb{Z}_m[x]\). Moreover we implemented two algorithms for this case in Singular which use different approaches in detecting useless computations, the classical Buchberger algorithm and a F5 signature based algorithm. Part B includes two algorithms that compute the graded Hilbert depth of a graded module over a polynomial algebra \(R\) over a field, as well as the depth and the multigraded Stanley depth of a factor of monomial ideals of \(R\). The two algorithms provide faster computations and examples that lead B. Ichim and A. Zarojanu to a counter example of a question of J. Herzog. A. Duval, B. Goeckner, C. Klivans and J. Martin have recently discovered a counter example for the Stanley Conjecture. We prove in this thesis that the Stanley Conjecture holds in some special cases. Part D explores the General Neron Desingularization in the frame of Noetherian local domains of dimension 1. We have constructed and implemented in Singular and algorithm that computes a strong Artin Approximation for Cohen-Macaulay local rings of dimension 1.

- Integrating Security Concerns into Safety Analysis of Embedded Systems Using Component Fault Trees (2016)
- Nowadays, almost every newly developed system contains embedded systems for controlling system functions. An embedded system perceives its environment via sensors, and interacts with it using actuators such as motors. For systems that might damage their environment by faulty behavior usually a safety analysis is performed. Security properties of embedded systems are usually not analyzed at all. New developments in the area of Industry 4.0 and Internet of Things lead to more and more networking of embedded systems. Thereby, new causes for system failures emerge: Vulnerabilities in software and communication components might be exploited by attackers to obtain control over a system. By targeted actions a system may also be brought into a critical state in which it might harm itself or its environment. Examples for such vulnerabilities, and also successful attacks, became known over the last few years. For this reason, in embedded systems safety as well as security has to be analyzed at least as far as it may cause safety critical failures of system components. The goal of this thesis is to describe in one model how vulnerabilities from the security point of view might influence the safety of a system. The focus lies on safety analysis of systems, so the safety analysis is extended to encompass security problems that may have an effect on the safety of a system. Component Fault Trees are very well suited to examine causes of a failure and to find failure scenarios composed of combinations of faults. A Component Fault Tree of an analyzed system is extended by additional Basic Events that may be caused by targeted attacks. Qualitative and quantitative analyses are extended to take the additional security events into account. Thereby, causes of failures that are based on safety as well as security problems may be found. Quantitative or at least semi-quantitative analyses allow to evaluate security measures more detailed, and to justify the need of such. The approach was applied to several example systems: The safety chain of the off-road robot RAVON, an adaptive cruise control, a smart farming scenario, and a model of a generic infusion pump were analyzed. The result of all example analyses was that additional failure causes were found which would not have been detected in traditional Component Fault Trees. In the analyses also failure scenarios were found that are caused solely by attacks, and that are not depending on failures of system components. These are especially critical scenarios which should not happen in this way, as they are not found in a classical safety analysis. Thus the approach shows its additional benefit to a safety analysis which is achieved by the application of established techniques with only little additional effort.