IST Austria: PubRep (Institute of Science and Technology)
Not a member yet
6140 research outputs found
Sort by
Protecting centrosomes from fracturing enables efficient cell navigation
No full textThe centrosome is a microtubule orchestrator, nucleating and anchoring microtubules that grow radially and exert forces on cargos. At the same time, mechanical stresses from the microenvironment and cellular shape changes compress and bend microtubules. Yet, centrosomes are membraneless organelles, raising the question of how centrosomes withstand mechanical forces. Here, we discover that centrosomes can deform and even fracture. We reveal that centrosomes experience deformations during navigational pathfinding within motile cells. Coherence of the centrosome is maintained by Dyrk3 and cNAP1, preventing fracturing by forces. While cells can compensate for the depletion of centriolar-based centrosomes, the fracturing of centrosomes impedes cellular function by generating coexisting microtubule organizing centers that compete during path navigation and thereby cause cellular entanglement in the microenvironment. Our findings show that cells actively maintain the integrity of the centrosome to withstand mechanical forces. These results suggest that centrosome stability preservation is fundamental, given that almost all cells in multicellular organisms experience forces
Quantified linear and polynomial arithmetic satisfiability via template-based skolemization
No full textThe problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredient in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state of the art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks
LNCS
No full textWe study recent algebraic attacks (Briaud-Øygarden EC’23) on the Regular Syndrome Decoding (RSD) problem and the assumptions underlying the correctness of their attacks’ complexity estimates. By relating these assumptions to interesting algebraic-combinatorial problems, we prove that they do not hold in full generality. However, we show that they are (asymptotically) true for most parameter sets, supporting the soundness of algebraic attacks on RSD. Further, we prove—without any heuristics or assumptions—that RSD can be broken in polynomial time whenever the number of error blocks times the square of the size of error blocks is larger than 2 times the square of the dimension of the code.
Additionally, we use our methodology to attack a variant of the Learning With Errors problem where each error term lies in a fixed set of constant size. We prove that this problem can be broken in polynomial time, given a sufficient number of samples. This result improves on the seminal work by Arora and Ge (ICALP’11), as the attack’s time complexity is independent of the LWE modulus
Early emergence of projection-subtype fate-restricted radial glial progenitors orchestrates neocortical neurogenesis
No full textRadial glial progenitors (RGPs) generate all projection neurons (PNs) in the cerebral cortex through incompletely understood processes. Herein, we combine Mosaic Analysis with Double Markers (MADM)-based clonal analysis at embryonic days 12.5 and 13.5 with early postnatal callosal tracing to reveal a lineage progression that challenges the inside-outside model of cortical development and the conventional view of an invariable sequence of asymmetric neurogenic divisions. Our data demonstrate that early multipotent RGPs generate all extra-telencephalic (ET) and intra-telencephalic (IT) PNs across all layers through parallel sublineages and the random specification, during the earliest neurogenic divisions, of fate-restricted daughter RGPs. While the neuronal production of the parental multipotent RGPs consists of small ET-PN or IT-PN outputs, fate-restricted RGPs produce larger translaminar outputs spanning deep and upper layers of only IT-PNs, the predominant mammalian PN subtype. We further show that the emergence of IT-PN fate-restricted RGPs also leads to quantitatively and temporally stereotyped neurogenesis population-wise
Rigid fibre transport in a periodic non-homogeneous geophysical turbulent flow
No full textFrom anthropogenic litter carried by ocean currents to plant stems travelling through the atmosphere, geophysical flows are often seeded with elongated, fibre-like particles. In this study, we used a large-scale laboratory model of a tidal current – representative of a widespread class of geophysical flows – to investigate the tumbling motion of long, slender and floating fibres in the complex turbulence generated by flow interactions with a tidal inlet. Despite the non-stationary, non-homogeneous and anisotropic nature of this turbulence, we find that long fibres statistically rotate at the same frequency as eddies of similar size, a phenomenon called scale selection, which is known to occur in ideal turbulence. Furthermore, we report that the signal of the instantaneous transverse velocity difference between the fibre ends changes significantly from the signal produced by the flow in the fibre surroundings, although the two are statistically equivalent. These observations have twofold implications. On the one hand, they confirm the reliability of using the end-to-end velocity signal of rigid fibres to probe the two-point transverse statistics of the flow, even under realistic conditions: oceanographers could exploit this observation to measure transverse velocity differences through elongated floats in the field, where superdiffusion complicates collecting sufficient data to probe two-point turbulence statistics at a fixed separation effectively. On the other hand, by addressing the dynamics of inertial range particles floating in the coastal zone, these observations are crucial to improving our ability to predict the fate of meso- and macro-litter, a size class that is currently understudied
Non–Hermitian spectral universality at critical points
No full textFor general large non–Hermitian random matrices X and deterministic normal deformations A, we prove that the local eigenvalue statistics of A + X close to the critical edge points of its spectrum are universal. This concludes the proof of the third and last remaining typical universality class for non–Hermitian random matrices (for normal deformations), after bulk and sharp edge universalities have been established in recent years
LNCS
No full textTwo standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature
Artifact: Fixed point certificates for reachability and expected rewards in MDPs
No full textThis artifact allows to review and reproduce the Isabelle proofs and practical experiments from the paper *Fixed Point Certificates for Reachability and Expected Rewards in MDPs*.
The contents are two-fold:
First, the artifact contains a formally verified certificate checker for the certificates presented in the paper.
The formal Isabelle/HOL proofs of the background theory can be inspected, checked by Isabelle and the code extraction can be retraced.
Second, the artifact contains a modified version of the model checking tool `Storm` with support for certificate generation. Together with the provided scripts and benchmark files, this allows to reproduce the experiments from the paper.
An appropriate subset of the experiments is given to allow a review in a timely manner. In addition, original logfiles from our experiments are provided, allowing a detailed inspection.
The package includes convenient installation scripts for [the TACAS 2023 VM](https://doi.org/10.5281/zenodo.7113223) (based on Ubuntu 22.04).
A native installation on Linux or macOS systems (including the newer ARM-based machines) is also possible
Nonlocal‐to‐local convergence for a Cahn–Hilliard tumor growth model
No full textWe consider a local Cahn–Hilliard‐type model for tumor growth as well as a nonlocal model where, compared to the local system, the Laplacian in the equation for the chemical potential is replaced by a nonlocal operator. The latter is defined as a convolution integral with suitable kernels parametrized by a small parameter. For sufficiently smooth bounded domains in three dimensions, we prove convergence of weak solutions of the nonlocal model toward strong solutions of the local model together with convergence rates with respect to the small parameter. The proof is done via a Gronwall‐type argument and a convergence result with rates for the nonlocal integral operator toward the Laplacian due to Abels and Hurm
Research Data for "Mass-Assisted Local Deconfinement in a Confined Z2 Lattice Gauge Theory"
No full textConfinement is a prominent phenomenon in condensed matter and high-energy physics that has recently become the focus of quantum-simulation experiments of lattice gauge theories (LGTs). As such, a theoretical understanding of the effect of confinement on LGT dynamics is not only of fundamental importance, but can lend itself to upcoming experiments. Here, we show how confinement in a Z2 LGT can be locally avoided by proximity to a resonance between the fermion mass and the electric field strength. Furthermore, we show that this local deconfinement can become global for certain initial conditions, where information transport occurs over the entire chain. In addition, we show how this can lead to strong quantum many-body scarring starting in different initial states. Our findings provide deeper insights into the nature of confinement in Z2 LGTs and can be tested on current and near-term quantum devices