TY - THES
AB - In this thesis we study persistence of multi-covers of Euclidean balls and the geometric structures underlying their computation, in particular Delaunay mosaics and Voronoi tessellations.
The k-fold cover for some discrete input point set consists of the space where at least k balls of radius r around the input points overlap. Persistence is a notion that captures, in some sense, the topology of the shape underlying the input. While persistence is usually computed for the union of balls, the k-fold cover is of interest as it captures local density,
and thus might approximate the shape of the input better if the input data is noisy. To compute persistence of these k-fold covers, we need a discretization that is provided by higher-order Delaunay mosaics.
We present and implement a simple and efficient algorithm for the computation of higher-order Delaunay mosaics, and use it to give experimental results for their combinatorial properties. The algorithm makes use of a new geometric structure, the rhomboid tiling. It contains the higher-order Delaunay mosaics as slices, and by introducing a filtration
function on the tiling, we also obtain higher-order α-shapes as slices. These allow us to compute persistence of the multi-covers for varying radius r; the computation for varying k is less straight-foward and involves the rhomboid tiling directly. We apply our algorithms to experimental sphere packings to shed light on their structural properties. Finally, inspired by periodic structures in packings and materials, we propose and implement an algorithm for periodic Delaunay triangulations to be integrated into the Computational Geometry Algorithms Library (CGAL), and discuss
the implications on persistence for periodic data sets.
AU - Osang, Georg F
ID - 9056
SN - 2663-337X
TI - Multi-cover persistence and Delaunay mosaics
ER -
TY - THES
AB - In this thesis, we consider several of the most classical and fundamental problems in static analysis and formal verification, including invariant generation, reachability analysis, termination analysis of probabilistic programs, data-flow analysis, quantitative analysis of Markov chains and Markov decision processes, and the problem of data packing in cache management.
We use techniques from parameterized complexity theory, polyhedral geometry, and real algebraic geometry to significantly improve the state-of-the-art, in terms of both scalability and completeness guarantees, for the mentioned problems. In some cases, our results are the first theoretical improvements for the respective problems in two or three decades.
AU - Goharshady, Amir Kafshdar
ID - 8934
SN - 2663-337X
TI - Parameterized and algebro-geometric advances in static program analysis
ER -
TY - THES
AB - Algorithms in computational 3-manifold topology typically take a triangulation as an input and return topological information about the underlying 3-manifold. However, extracting the desired information from a triangulation (e.g., evaluating an invariant) is often computationally very expensive. In recent years this complexity barrier has been successfully tackled in some cases by importing ideas from the theory of parameterized algorithms into the realm of 3-manifolds. Various computationally hard problems were shown to be efficiently solvable for input triangulations that are sufficiently “tree-like.”
In this thesis we focus on the key combinatorial parameter in the above context: we consider the treewidth of a compact, orientable 3-manifold, i.e., the smallest treewidth of the dual graph of any triangulation thereof. By building on the work of Scharlemann–Thompson and Scharlemann–Schultens–Saito on generalized Heegaard splittings, and on the work of Jaco–Rubinstein on layered triangulations, we establish quantitative relations between the treewidth and classical topological invariants of a 3-manifold. In particular, among other results, we show that the treewidth of a closed, orientable, irreducible, non-Haken 3-manifold is always within a constant factor of its Heegaard genus.
AU - Huszár, Kristóf
ID - 8032
SN - 2663-337X
TI - Combinatorial width parameters for 3-dimensional manifolds
ER -
TY - THES
AB - In the thesis we focus on the interplay of the biophysics and evolution of gene regulation. We start by addressing how the type of prokaryotic gene regulation – activation and repression – affects spurious binding to DNA, also known as
transcriptional crosstalk. We propose that regulatory interference caused by excess regulatory proteins in the dense cellular medium – global crosstalk – could be a factor in determining which type of gene regulatory network is evolutionarily preferred. Next,we use a normative approach in eukaryotic gene regulation to describe minimal
non-equilibrium enhancer models that optimize so-called regulatory phenotypes. We find a class of models that differ from standard thermodynamic equilibrium models by a single parameter that notably increases the regulatory performance. Next chapter addresses the question of genotype-phenotype-fitness maps of higher dimensional phenotypes. We show that our biophysically realistic approach allows us to understand how the mechanisms of promoter function constrain genotypephenotype maps, and how they affect the evolutionary trajectories of promoters.
In the last chapter we ask whether the intrinsic instability of gene duplication and amplification provides a generic alternative to canonical gene regulation. Using mathematical modeling, we show that amplifications can tune gene expression in many environments, including those where transcription factor-based schemes are
hard to evolve or maintain.
AU - Grah, Rok
ID - 8155
SN - 2663-337X
TI - Gene regulation across scales – how biophysical constraints shape evolution
ER -
TY - THES
AB - Designing and verifying concurrent programs is a notoriously challenging, time consuming, and error prone task, even for experts. This is due to the sheer number of possible interleavings of a concurrent program, all of which have to be tracked and accounted for in a formal proof. Inventing an inductive invariant that captures all interleavings of a low-level implementation is theoretically possible, but practically intractable. We develop a refinement-based verification framework that provides mechanisms to simplify proof construction by decomposing the verification task into smaller subtasks.
In a first line of work, we present a foundation for refinement reasoning over structured concurrent programs. We introduce layered concurrent programs as a compact notation to represent multi-layer refinement proofs. A layered concurrent program specifies a sequence of connected concurrent programs, from most concrete to most abstract, such that common parts of different programs are written exactly once. Each program in this sequence is expressed as structured concurrent program, i.e., a program over (potentially recursive) procedures, imperative control flow, gated atomic actions, structured parallelism, and asynchronous concurrency. This is in contrast to existing refinement-based verifiers, which represent concurrent systems as flat transition relations. We present a powerful refinement proof rule that decomposes refinement checking over structured programs into modular verification conditions. Refinement checking is supported by a new form of modular, parameterized invariants, called yield invariants, and a linear permission system to enhance local reasoning.
In a second line of work, we present two new reduction-based program transformations that target asynchronous programs. These transformations reduce the number of interleavings that need to be considered, thus reducing the complexity of invariants. Synchronization simplifies the verification of asynchronous programs by introducing the fiction, for proof purposes, that asynchronous operations complete synchronously. Synchronization summarizes an asynchronous computation as immediate atomic effect. Inductive sequentialization establishes sequential reductions that captures every behavior of the original program up to reordering of coarse-grained commutative actions. A sequential reduction of a concurrent program is easy to reason about since it corresponds to a simple execution of the program in an idealized synchronous environment, where processes act in a fixed order and at the same speed.
Our approach is implemented the CIVL verifier, which has been successfully used for the verification of several complex concurrent programs. In our methodology, the overall correctness of a program is established piecemeal by focusing on the invariant required for each refinement step separately. While the programmer does the creative work of specifying the chain of programs and the inductive invariant justifying each link in the chain, the tool automatically constructs the verification conditions underlying each refinement step.
AU - Kragl, Bernhard
ID - 8332
SN - 2663-337X
TI - Verifying concurrent programs: Refinement, synchronization, sequentialization
ER -
TY - THES
AB - Fabrication of curved shells plays an important role in modern design, industry, and science. Among their remarkable properties are, for example, aesthetics of organic shapes, ability to evenly distribute loads, or efficient flow separation. They find applications across vast length scales ranging from sky-scraper architecture to microscopic devices. But, at
the same time, the design of curved shells and their manufacturing process pose a variety of challenges. In this thesis, they are addressed from several perspectives. In particular, this thesis presents approaches based on the transformation of initially flat sheets into the target curved surfaces. This involves problems of interactive design of shells with nontrivial mechanical constraints, inverse design of complex structural materials, and data-driven modeling of delicate and time-dependent physical properties. At the same time, two newly-developed self-morphing mechanisms targeting flat-to-curved transformation are presented.
In architecture, doubly curved surfaces can be realized as cold bent glass panelizations. Originally flat glass panels are bent into frames and remain stressed. This is a cost-efficient fabrication approach compared to hot bending, when glass panels are shaped plastically. However such constructions are prone to breaking during bending, and it is highly
nontrivial to navigate the design space, keeping the panels fabricable and aesthetically pleasing at the same time. We introduce an interactive design system for cold bent glass façades, while previously even offline optimization for such scenarios has not been sufficiently developed. Our method is based on a deep learning approach providing quick
and high precision estimation of glass panel shape and stress while handling the shape
multimodality.
Fabrication of smaller objects of scales below 1 m, can also greatly benefit from shaping originally flat sheets. In this respect, we designed new self-morphing shell mechanisms transforming from an initial flat state to a doubly curved state with high precision and detail. Our so-called CurveUps demonstrate the encodement of the geometric information
into the shell. Furthermore, we explored the frontiers of programmable materials and showed how temporal information can additionally be encoded into a flat shell. This allows prescribing deformation sequences for doubly curved surfaces and, thus, facilitates self-collision avoidance enabling complex shapes and functionalities otherwise impossible.
Both of these methods include inverse design tools keeping the user in the design loop.
AU - Guseinov, Ruslan
ID - 8366
KW - computer-aided design
KW - shape modeling
KW - self-morphing
KW - mechanical engineering
SN - 2663-337X
TI - Computational design of curved thin shells: From glass façades to programmable matter
ER -
TY - THES
AB - Form versus function is a long-standing debate in various design-related fields, such as architecture as well as graphic and industrial design. A good design that balances form and function often requires considerable human effort and collaboration among experts from different professional fields. Computational design tools provide a new paradigm for designing functional objects. In computational design, form and function are represented as mathematical
quantities, with the help of numerical and combinatorial algorithms, they can assist even novice users in designing versatile models that exhibit their desired functionality. This thesis presents three disparate research studies on the computational design of functional objects: The appearance of 3d print—we optimize the volumetric material distribution for faithfully replicating colored surface texture in 3d printing; the dynamic motion of mechanical structures—
our design system helps the novice user to retarget various mechanical templates with different functionality to complex 3d shapes; and a more abstract functionality, multistability—our algorithm automatically generates models that exhibit multiple stable target poses. For each of these cases, our computational design tools not only ensure the functionality of the results but also permit the user aesthetic freedom over the form. Moreover, fabrication constraints
were taken into account, which allow for the immediate creation of physical realization via 3D printing or laser cutting.
AU - Zhang, Ran
ID - 8386
SN - 2663-337X
TI - Structure-aware computational design and its application to 3D printable volume scattering, mechanism, and multistability
ER -
TY - THES
AB - Mutations are the raw material of evolution and come in many different flavors. Point mutations change a single letter in the DNA sequence, while copy number mutations like duplications or deletions add or remove many letters of the DNA sequence simultaneously. Each type of mutation exhibits specific properties like its rate of formation and reversal.
Gene expression is a fundamental phenotype that can be altered by both, point and copy number mutations. The following thesis is concerned with the dynamics of gene expression evolution and how it is affected by the properties exhibited by point and copy number mutations. Specifically, we are considering i) copy number mutations during adaptation to fluctuating environments and ii) the interaction of copy number and point mutations during adaptation to constant environments.
AU - Tomanek, Isabella
ID - 8653
KW - duplication
KW - amplification
KW - promoter
KW - CNV
KW - AMGET
KW - experimental evolution
KW - Escherichia coli
SN - 2663-337X
TI - The evolution of gene expression by copy number and point mutations
ER -
TY - THES
AB - Many methods for the reconstruction of shapes from sets of points produce ordered simplicial complexes, which are collections of vertices, edges, triangles, and their higher-dimensional analogues, called simplices, in which every simplex gets assigned a real value measuring its size. This thesis studies ordered simplicial complexes, with a focus on their topology, which reflects the connectedness of the represented shapes and the presence of holes. We are interested both in understanding better the structure of these complexes, as well as in developing algorithms for applications.
For the Delaunay triangulation, the most popular measure for a simplex is the radius of the smallest empty circumsphere. Based on it, we revisit Alpha and Wrap complexes and experimentally determine their probabilistic properties for random data. Also, we prove the existence of tri-partitions, propose algorithms to open and close holes, and extend the concepts from Euclidean to Bregman geometries.
AU - Ölsböck, Katharina
ID - 7460
KW - shape reconstruction
KW - hole manipulation
KW - ordered complexes
KW - Alpha complex
KW - Wrap complex
KW - computational topology
KW - Bregman geometry
SN - 2663-337X
TI - The hole system of triangulated shapes
ER -
TY - THES
AB - We study the interacting homogeneous Bose gas in two spatial dimensions in the thermodynamic limit at fixed density. We shall be concerned with some mathematical aspects of this complicated problem in many-body quantum mechanics. More specifically, we consider the dilute limit where the scattering length of the interaction potential, which is a measure for the effective range of the potential, is small compared to the average distance between the particles. We are interested in a setting with positive (i.e., non-zero) temperature. After giving a survey of the relevant literature in the field, we provide some facts and examples to set expectations for the two-dimensional system. The crucial difference to the three-dimensional system is that there is no Bose–Einstein condensate at positive temperature due to the Hohenberg–Mermin–Wagner theorem. However, it turns out that an asymptotic formula for the free energy holds similarly to the three-dimensional case.
We motivate this formula by considering a toy model with δ interaction potential. By restricting this model Hamiltonian to certain trial states with a quasi-condensate we obtain an upper bound for the free energy that still has the quasi-condensate fraction as a free parameter. When minimizing over the quasi-condensate fraction, we obtain the Berezinskii–Kosterlitz–Thouless critical temperature for superfluidity, which plays an important role in our rigorous contribution. The mathematically rigorous result that we prove concerns the specific free energy in the dilute limit. We give upper and lower bounds on the free energy in terms of the free energy of the non-interacting system and a correction term coming from the interaction. Both bounds match and thus we obtain the leading term of an asymptotic approximation in the dilute limit, provided the thermal wavelength of the particles is of the same order (or larger) than the average distance between the particles. The remarkable feature of this result is its generality: the correction term depends on the interaction potential only through its scattering length and it holds for all nonnegative interaction potentials with finite scattering length that are measurable. In particular, this allows to model an interaction of hard disks.
AU - Mayer, Simon
ID - 7514
SN - 2663-337X
TI - The free energy of a dilute two-dimensional Bose gas
ER -