IST Austria: PubRep (Institute of Science and Technology)
Not a member yet
6140 research outputs found
Sort by
A life-cycle approach to understand consequences of silvopastoral use on two native tree species of Northern Patagonia
No full textSilvopastoral use in native forests could impact population dynamics of key tree species, with contrasting effects at different life cycle stages. Prior studies in South American temperate forests have mainly focused on initial stages, lacking a comprehensive understanding of the entire life cycle within productive systems. We assessed the population dynamics of two key species of mixed forests in northern Patagonia (Austrocedrus chilensis and Nothofagus dombeyi) under two silvopastoral use intensities (high vs. low), using demographic techniques and population projection models. Over 3 years, we quantified vital rates (survival, fertility, growth, reversion and stasis) and used matrix models to calculate deterministic population growth rates (λ). High-intensity silvopastoral use had predominantly negative effects on the elements of the projection matrices of A. chilensis, whereas N. dombeyi exhibited mostly positive or no changes. As a result, projections indicated slight population decreases for A. chilensis (mostly λ < 1) at high silvopastoral use levels compared to low levels, while N. dombeyi showed similar projections (λ ≅ 1) between use levels. Decreased λ for A. chilensis resulted mainly from lower adult tree survival, while early life stages had limited influence on λ for these long-lived species. In summary, silvopastoral use affects population dynamics of key tree species of these mixed forests of northern Patagonia, with implications for sustainable management. Our findings highlight the importance of considering the entire life cycle and suggest targeted practices to enhance A. chilensis populations
Can quasars, triggered by mergers, account for NANOGrav’s stochastic gravitational wave background?
No full textThe stochastic gravitational wave (GW) background recently discovered by several pulsar timing array experiments is consistent with arising from a population of coalescing super-massive black hole binaries. The amplitude of the background is somewhat higher than expected in most previous population models or from the local mass density observations. Such binaries are expected to be produced in galaxy mergers, which are also thought to trigger bright quasar activity. Under the assumptions that (i) a fraction fbin∼1 of all quasars are associated with mergers, (ii) the typical quasar lifetime is tQ∼108 yr, and (iii) adopting Eddington ratios fEdd∼0.25 for the luminosity of quasars, we compute the GW background associated directly with the empirically measured quasar luminosity function. This approach bypasses the need to model the cosmological evolution of black holes or galaxy mergers from simulations or semi-analytical models. We find the amplitude matching the value measured by NANOGrav. Our results are consistent with most quasars being associated with black hole binaries and being the sources of the GW background, and imply a joint constraint on tQ, fEdd and the typical mass ratio q≡M2/M1. The signal in this case would be dominated by relatively distant ∼109M⊙ sources at z≈2−3, at the peak of quasar activity. Similarly to other models, our results remain in tension with the local super-massive black hole mass density
Random zero-sum dynamic games on infinite directed graphs
No full textWe consider random two-player zero-sum dynamic games with perfect information on a class of infinite directed graphs. Starting from a fixed vertex, the players take turns to move a token along the edges of the graph. Every vertex is assigned a payoff known in advance by both players. Every time the token visits a vertex, Player 2 pays Player 1 the corresponding payoff. We consider a distribution over such games by assigning i.i.d. payoffs to the vertices. On the one hand, for acyclic directed graphs of bounded degree and sub-exponential expansion, we show that, when the duration of the game tends to infinity, the value converges almost surely to a constant at an exponential rate dominated in terms of the expansion. On the other hand, for the infinite d-ary tree (that does not fall into the previous class of graphs), we show convergence at a double-exponential rate
Colonization times in Moran process on graphs
No full textMoran Birth-death process is a standard stochastic process that is used to model natural selection in spatially structured populations. A newly occurring mutation that invades a population of residents can either fixate on the whole population or it can go extinct due to random drift. The duration of the process depends not only on the total population size n, but also on the spatial structure of the population. In this work, we consider the Moran process with a single type of individuals who invade and colonize an otherwise empty environment. Mathematically, this corresponds to the setting where the residents have zero reproduction rate, thus they never reproduce. The spatial structure is represented by a graph. We present two main contributions. First, in contrast to the Moran process in which residents do reproduce, we show that the colonization time is always at most a polynomial function of the population size n. Namely, we show that colonization always takes at most 1/2n^3 - 1/2n^2 expected steps, and for each n, we identify the slowest graph where it takes exactly that many steps. Moreover, we establish a stronger bound of roughly n^2.5 steps for undirected graphs and an even stronger bound of roughly n^2 steps for so-called regular graphs. Second, we discuss various complications that one faces when attempting to measure fixation times and colonization times in spatially structured populations, and we propose to measure the real duration of the process, rather than counting the steps of the classic Moran process
LNCS
No full textCooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though).
Bubaak is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. Bubaak starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with Bubaak as an intermediary
Optic nerve crush does not induce retinal ganglion cell loss in the contralateral eye
No full textPurpose: Optic nerve crush (ONC) is a model for studying optic nerve trauma. Unilateral ONC induces massive retinal ganglion cell (RGC) degeneration in the affected eye, leading to vision loss within a month. A common assumption has been that the non-injured contralateral eye is unaffected due to the minimal retino-retinal projections of the RGCs at the chiasm. Yet, recently, microglia, the brain-resident macrophages, have shown a responsive phenotype in the contralateral eye after ONC. Whether RGC loss accompanies this phenotype is still controversial.
Methods: Using the available RGCode algorithm and developing our own RGC-Quant deep-learning-based tool, we quantify RGC's total number and density across the entire retina after ONC.
Results: We confirm a short-term microglia response in the contralateral eye after ONC, but this did not affect the microglia number. Furthermore, we cannot confirm the previously reported RGC loss between naïve and contralateral retinas 5 weeks after ONC induction across the commonly used Cx3cr1creERT2 and C57BL6/J mouse models. Neither sex nor the direct comparison of the RGC markers Brn3a and RBPMS, with Brn3a co-labeling, on average, 89% of the RBPMS+-cells, explained this discrepancy, suggesting that the early microglia-responsive phenotype does not have immediate consequences on the RGC number.
Conclusions: Our results corroborate that unilateral optic nerve injury elicits a microglial response in the uninjured contralateral eye but without RGC loss. Therefore, the contralateral eye should be treated separately and not as an ONC control
ISTA Thesis
No full textThis thesis deals with several different models for complex quantum mechanical systems and is structured in three main parts.
In Part I, we study mean field random matrices as models for quantum Hamiltonians. Our focus lies on proving concentration estimates for resolvents of random matrices, so-called local laws, mostly in the setting of multiple resolvents. These estimates have profound consequences for eigenvector overlaps and thermalization problems. More concretely, we obtain, e.g., the optimal eigenstate thermalization hypothesis (ETH) uniformly in the spectrum for Wigner matrices, an optimal lower bound on non-Hermitian eigenvector overlaps, and prethermalization for deformed Wigner matrices. In order to prove our novel multi-resolvent local laws, we develop and devise two main methods, the static Psi-method and the dynamical Zigzag strategy.
In Part II, we study Bardeen-Cooper-Schrieffer (BCS) theory, the standard mean field microscopic theory of superconductivity. We focus on asymptotic formulas for the characteristic critical temperature and energy gap of a superconductor and prove universality of their ratio in various physical regimes. Additionally, we investigate multi-band superconductors and show that inter-band coupling effects can only enhance the critical temperature.
In Part III, we study quantum lattice systems. On the one hand, we show a strong version of the local-perturbations-perturb-locally (LPPL) principle for the ground state of weakly interacting quantum spin systems with a uniform on-site gap. On the other hand, we introduce a notion of a local gap and rigorously justify response theory and the Kubo formula under the weakened assumption of a local gap.
Additionally, we discuss two classes of problems which do not fit into the three main parts of the thesis. These are deformational rigidity of Liouville metrics on the torus and relativistic toy models of particle creation via interior-boundary-conditions (IBCs)
Destabilizing Iris
No full textThe separation logic framework Iris has been built on the premise that all assertions are stable, meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, heap-dependent expression assertions, which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation.
In this paper, we bring heap-dependent expression assertions to Iris with Daenerys. To do so, we must first revisit the very core of Iris, extending it with a new form of unstable resources (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT
VAMOS: Middleware for best-effort third-party monitoring
No full textAs the complexity and criticality of software increase every year, so does the importance of runtime monitoring. Third-party and best-effort monitoring are especially valuable, yet under-explored areas of runtime monitoring. In this context, third-party monitoring means monitoring with a limited knowledge of the monitored software (as it has been developed by a third party). Best-effort monitoring keeps pace with the monitored software at the cost of possibly imprecise verdicts when keeping up with the monitored software would not be feasible. Most existing monitoring frameworks do not support the combination of third-party and best-effort monitoring because they either require the full access to the monitored code or the ability to process all observable events, or both.
We present a middleware framework, Vamos, for the runtime monitoring of software. Vamos is explicitly designed to support third-party and best-effort scenarios. The design goals of Vamos are (i) efficiency (tracing events with low overhead), (ii) flexibility (the ability to monitor a variety of different event channels, and to connect to a wide range of monitors), and (iii) ease-of-use. To achieve its goals, Vamos combines aspects of event broker and event recognition systems with aspects of stream processing systems.
We implemented a prototype toolchain for Vamos and conducted a set of experiments demonstrating the usability of the scheme. The results indicate that Vamos enables writing useful yet efficient monitors, and simplifies key aspects of setting up a monitoring system from scratch