IST PubRep
Not a member yet
752 research outputs found
Sort by
Invasive parasites habitat change and heavy rainfall reduce breeding success in Darwin's finches
Get PDFInvasive alien parasites and pathogens are a growing threat to biodiversity worldwide, which can contribute to the extinction of endemic species. On the Galapagos Islands, the invasive parasitic fly Philornis downsi poses a major threat to the endemic avifauna. Here, we investigated the influence of this parasite on the breeding success of two Darwin's finch species, the warbler finch (Certhidea olivacea) and the sympatric small tree finch (Camarhynchus parvulus), on Santa Cruz Island in 2010 and 2012. While the population of the small tree finch appeared to be stable, the warbler finch has experienced a dramatic decline in population size on Santa Cruz Island since 1997. We aimed to identify whether warbler finches are particularly vulnerable during different stages of the breeding cycle. Contrary to our prediction, breeding success was lower in the small tree finch than in the warbler finch. In both species P. downsi had a strong negative impact on breeding success and our data suggest that heavy rain events also lowered the fledging success. On the one hand parents might be less efficient in compensating their chicks'; energy loss due to parasitism as they might be less efficient in foraging on days of heavy rain. On the other hand, intense rainfalls might lead to increased humidity and more rapid cooling of the nests. In the case of the warbler finch we found that the control of invasive plant species with herbicides had a significant additive negative impact on the breeding success. It is very likely that the availability of insects (i.e. food abundance) is lower in such controlled areas, as herbicide usage led to the removal of the entire understory. Predation seems to be a minor factor in brood loss
Games with a Weak Adversary
Get PDFWe consider multi-player graph games with partial-observation and parity objective. While the decision problem for three-player games with a coalition of the first and second players against the third player is undecidable, we present a decidability result for partial-observation games where the first and third player are in a coalition against the second player, thus where the second player is adversarial but weaker due to partial-observation. We establish tight complexity bounds in the case where player 1 is less informed than player 2, namely 2-EXPTIME-completeness for parity objectives. The symmetric case of player 1 more informed than player 2 is much more complicated, and we show that already in the case where player 1 has perfect observation, memory of size non-elementary is necessary in general for reachability objectives, and the problem is decidable for safety and reachability objectives. Our results have tight connections with partial-observation stochastic games for which we derive new complexity results
The Value 1 Problem for Concurrent Mean-payoff Games
Get PDFWe consider concurrent mean-payoff games, a very well-studied class of two-player (player 1 vs player 2) zero-sum games on finite-state graphs where every transition is assigned a reward between 0 and 1, and the payoff function is the long-run average of the rewards. The value is the maximal expected payoff that player 1 can guarantee against all strategies of player 2. We consider the computation of the set of states with value 1 under finite-memory strategies for player 1, and our main results for the problem are as follows: (1) we present a polynomial-time algorithm; (2) we show that whenever there is a finite-memory strategy, there is a stationary strategy that does not need memory at all; and (3) we present an optimal bound (which is double exponential) on the patience of stationary strategies (where patience of a distribution is the inverse of the smallest positive probability and represents a complexity measure of a stationary strategy)
CEGAR for Qualitative Analysis of Probabilistic Systems
Get PDFWe consider Markov decision processes (MDPs) which are a standard model
for probabilistic systems. We focus on qualitative properties for MDPs
that can express that desired behaviors of the system arise almost-surely
(with probability 1) or with positive probability.
We introduce a new simulation relation to capture the refinement relation
of MDPs with respect to qualitative properties, and present discrete graph
theoretic algorithms with quadratic complexity to compute the simulation
relation.
We present an automated technique for assume-guarantee style reasoning
for compositional analysis of MDPs with qualitative properties by
giving a counter-example guided abstraction-refinement approach to compute
our new simulation relation.
We have implemented our algorithms and show that the compositional analysis
leads to significant improvements
Cost-Aware Automatic Program Repair
Get PDFWe present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a
proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a cost-aware formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstraction-based solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in
benchmark C programs
Habitat heterogeneities versus spatial type frequency variances as driving forces of dispersal evolution
No full textUnderstanding the evolution of dispersal is essential for understanding and predicting the dynamics of natural populations. Two main factors are known to influence dispersal evolution: spatio-temporal variation in the environment and relatedness between individuals. However, the relation between these factors is still poorly understood, and they are usually treated separately. In this article, I present a theoretical framework that contains and connects effects of both environmental variation and relatedness, and reproduces and extends their known features. Spatial habitat variation selects for balanced dispersal strategies, whereby the population is kept at an ideal free distribution. Within this class of dispersal strategies, I explain how increased dispersal is promoted by perturbations to the dispersal type frequencies. An explicit formula shows the magnitude of the selective advantage of increased dispersal in terms of the spatial variability in the frequencies of the different dispersal strategies present. These variances are capable of capturing various sources of stochasticity and hence establish a common scale for their effects on the evolution of dispersal. The results furthermore indicate an alternative approach to identifying effects of relatedness on dispersal evolution
Extensional crisis and proving identity
Get PDFExtensionality axioms are common when reasoning about data collections, such as arrays and functions in program analysis, or sets in mathematics. An extensionality axiom asserts that two collections are equal if they consist of the same elements at the same indices. Using extensionality is often required to show that two collections are equal. A typical example is the set theory theorem (∀x)(∀y)x∪y = y ∪x. Interestingly, while humans have no problem with proving such set identities using extensionality, they are very hard for superposition theorem provers because of the calculi they use. In this paper we show how addition of a new inference rule, called extensionality resolution, allows first-order theorem provers to easily solve problems no modern first-order theorem prover can solve. We illustrate this by running the VAMPIRE theorem prover with extensionality resolution on a number of set theory and array problems. Extensionality resolution helps VAMPIRE to solve problems from the TPTP library of first-order problems that were never solved before by any prover
Local semicircle law with imprimitive variance matrix
No full textWe extend the proof of the local semicircle law for generalized Wigner matrices given in MR3068390 to the case when the matrix of variances has an eigenvalue -1. In particular, this result provides a short proof of the optimal local Marchenko-Pastur law at the hard edge (i.e. around zero) for sample covariance matrices X*X, where the variances of the entries of X may vary
Isotropic local laws for sample covariance and generalized Wigner matrices
No full textWe consider sample covariance matrices of the form X∗X, where X is an M×N matrix with independent random entries. We prove the isotropic local Marchenko-Pastur law, i.e. we prove that the resolvent (X∗X−z)−1 converges to a multiple of the identity in the sense of quadratic forms. More precisely, we establish sharp high-probability bounds on the quantity ⟨v,(X∗X−z)−1w⟩−⟨v,w⟩m(z), where m is the Stieltjes transform of the Marchenko-Pastur law and v,w∈CN. We require the logarithms of the dimensions M and N to be comparable. Our result holds down to scales Iz≥N−1+ε and throughout the entire spectrum away from 0. We also prove analogous results for generalized Wigner matrices
An American in Allied-occupied Austria: John Dos Passos Reports on Postwar Vienna
Get PDFJohn Dos Passos was working as a LIFE correspondent when he visited Austria in early November 1945. Starting out from Bad Wiessee in Bavaria, he went through American-held territory and, after crossing into the Russian zone at Linz, on to Vienna. In the war-ravaged city, where American and Red Army troops were eyeing each other with suspicion, he witnessed the growing tensions between the Western Allies and the Soviet Union, thereby anticipating the atmosphere of the Cold War era. Although cold and hunger could be found almost everywhere in Vienna, the Allied-occupied city was recovering traces of its former grace and gaiety, almost like “an old musical comedy queen”, with its clubs and theatres providing entertainment.
The report that John Dos Passos wrote about Vienna reflects his cross-cultural encounters in Allied-occupied Austria. Published in the March 4, 1946 issue of LIFE magazine and in Tour of Duty of August 1946, it presents the Viennese as victimized by Nazi butcheries and Soviet brutalities who welcomed their American liberators. Its ideological bias is conveyed by the author’s use of literary images and political rhetoric well known to American readers, ranging from the (inverted) frontier myth, to the image of Vienna as a home to music and theater, and the stereotype of the crude and evil Bolshevik. Analyzing and interpreting Dos Passos’s report from a cultural studies’ perspective sheds light on America’s relationship with Austria in the early Post-World War II years