@techreport{5407, abstract = {This document is created as a part of the project “Repository for Research Data at IST Austria”. It summarises the mandatory features, which need to be fulfilled to provide an institutional repository as a platform and also a service to the scientists at the institute. It also includes optional features, which would be of strong benefit for the scientists and would increase the usage of the repository, and hence the visibility of research at IST Austria.}, author = {Porsche, Jana}, publisher = {IST Austria}, title = {{Technical requirements and features}}, year = {2013}, } @misc{5408, abstract = {We consider two-player partial-observation stochastic games where player 1 has partial observation and player 2 has perfect observation. The winning condition we study are omega-regular conditions specified as parity objectives. The qualitative analysis problem given a partial-observation stochastic game and a parity objective asks whether there is a strategy to ensure that the objective is satisfied with probability 1 (resp. positive probability). While the qualitative analysis problems are known to be undecidable even for very special cases of parity objectives, they were shown to be decidable in 2EXPTIME under finite-memory strategies. We improve the complexity and show that the qualitative analysis problems for partial-observation stochastic parity games under finite-memory strategies are EXPTIME-complete; and also establish optimal (exponential) memory bounds for finite-memory strategies required for qualitative analysis. }, author = {Chatterjee, Krishnendu and Doyen, Laurent and Nain, Sumit and Vardi, Moshe}, issn = {2664-1690}, pages = {17}, publisher = {IST Austria}, title = {{The complexity of partial-observation stochastic parity games with finite-memory strategies}}, doi = {10.15479/AT:IST-2013-141-v1-1}, year = {2013}, } @misc{5409, abstract = {The edit distance between two (untimed) traces is the minimum cost of a sequence of edit operations (insertion, deletion, or substitution) needed to transform one trace to the other. Edit distances have been extensively studied in the untimed setting, and form the basis for approximate matching of sequences in different domains such as coding theory, parsing, and speech recognition. In this paper, we lift the study of edit distances from untimed languages to the timed setting. We define an edit distance between timed words which incorporates both the edit distance between the untimed words and the absolute difference in timestamps. Our edit distance between two timed words is computable in polynomial time. Further, we show that the edit distance between a timed word and a timed language generated by a timed automaton, defined as the edit distance between the word and the closest word in the language, is PSPACE-complete. While computing the edit distance between two timed automata is undecidable, we show that the approximate version, where we decide if the edit distance between two timed automata is either less than a given parameter or more than delta away from the parameter, for delta>0, can be solved in exponential space and is EXPSPACE-hard. Our definitions and techniques can be generalized to the setting of hybrid systems, and we show analogous decidability results for rectangular automata.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Majumdar, Rupak}, issn = {2664-1690}, pages = {12}, publisher = {IST Austria}, title = {{Edit distance for timed automata}}, doi = {10.15479/AT:IST-2013-144-v1-1}, year = {2013}, } @misc{5410, abstract = {Board games, like Tic-Tac-Toe and CONNECT-4, play an important role not only in development of mathematical and logical skills, but also in emotional and social development. In this paper, we address the problem of generating targeted starting positions for such games. This can facilitate new approaches for bringing novice players to mastery, and also leads to discovery of interesting game variants. Our approach generates starting states of varying hardness levels for player 1 in a two-player board game, given rules of the board game, the desired number of steps required for player 1 to win, and the expertise levels of the two players. Our approach leverages symbolic methods and iterative simulation to efficiently search the extremely large state space. We present experimental results that include discovery of states of varying hardness levels for several simple grid-based board games. Also, the presence of such states for standard game variants like Tic-Tac-Toe on board size 4x4 opens up new games to be played that have not been played for ages since the default start state is heavily biased. }, author = {Ahmed, Umair and Chatterjee, Krishnendu and Gulwani, Sumit}, issn = {2664-1690}, pages = {13}, publisher = {IST Austria}, title = {{Automatic generation of alternative starting positions for traditional board games}}, doi = {10.15479/AT:IST-2013-146-v1-1}, year = {2013}, } @inbook{5747, author = {Dragoi, Cezara and Gupta, Ashutosh and Henzinger, Thomas A}, booktitle = {Computer Aided Verification}, isbn = {9783642397981}, issn = {1611-3349}, location = {Saint Petersburg, Russia}, pages = {174--190}, publisher = {Springer Berlin Heidelberg}, title = {{Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates}}, doi = {10.1007/978-3-642-39799-8_11}, volume = {8044}, year = {2013}, } @misc{6440, abstract = {In order to guarantee that each method of a data structure updates the logical state exactly once, al-most all non-blocking implementations employ Compare-And-Swap (CAS) based synchronization. For FIFO queue implementations this translates into concurrent enqueue or dequeue methods competing among themselves to update the same variable, the tail or the head, respectively, leading to high contention and poor scalability. Recent non-blocking queue implementations try to alleviate high contentionby increasing the number of contention points, all the while using CAS-based synchronization. Furthermore, obtaining a wait-free implementation with competition is achieved by additional synchronization which leads to further degradation of performance.In this paper we formalize the notion of competitiveness of a synchronizing statement which can beused as a measure for the scalability of concurrent implementations. We present a new queue implementation, the Speculative Pairing (SP) queue, which, as we show, decreases competitiveness by using Fetch-And-Increment (FAI) instead of CAS. We prove that the SP queue is linearizable and lock-free.We also show that replacing CAS with FAI leads to wait-freedom for dequeue methods without an adverse effect on performance. In fact, our experiments suggest that the SP queue can perform and scale better than the state-of-the-art queue implementations.}, author = {Henzinger, Thomas A and Payer, Hannes and Sezgin, Ali}, issn = {2664-1690}, pages = {23}, publisher = {IST Austria}, title = {{Replacing competition with cooperation to achieve scalable lock-free FIFO queues }}, doi = {10.15479/AT:IST-2013-124-v1-1}, year = {2013}, } @article{10396, abstract = {Stimfit is a free cross-platform software package for viewing and analyzing electrophysiological data. It supports most standard file types for cellular neurophysiology and other biomedical formats. Its analysis algorithms have been used and validated in several experimental laboratories. Its embedded Python scripting interface makes Stimfit highly extensible and customizable.}, author = {Schlögl, Alois and Jonas, Peter M and Schmidt-Hieber, C. and Guzman, S. J.}, issn = {1862-278X}, journal = {Biomedical Engineering / Biomedizinische Technik}, keywords = {biomedical engineering, data analysis, free software}, location = {Graz, Austria}, number = {SI-1-Track-G}, publisher = {De Gruyter}, title = {{Stimfit: A fast visualization and analysis environment for cellular neurophysiology}}, doi = {10.1515/bmt-2013-4181}, volume = {58}, year = {2013}, } @misc{9749, abstract = {Cooperative behavior, where one individual incurs a cost to help another, is a wide spread phenomenon. Here we study direct reciprocity in the context of the alternating Prisoner's Dilemma. We consider all strategies that can be implemented by one and two-state automata. We calculate the payoff matrix of all pairwise encounters in the presence of noise. We explore deterministic selection dynamics with and without mutation. Using different error rates and payoff values, we observe convergence to a small number of distinct equilibria. Two of them are uncooperative strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium is mixed and represents a cooperative alliance of several strategies, dominated by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent has cooperated; it defects once when the opponent has defected, but subsequently Forgiver attempts to re-establish cooperation even if the opponent has defected again. Forgiver is not an evolutionarily stable strategy, but the alliance, which it rules, is asymptotically stable. For a wide range of parameter values the most commonly observed outcome is convergence to the mixed equilibrium, dominated by Forgiver. Our results show that although forgiving might incur a short-term loss it can lead to a long-term gain. Forgiveness facilitates stable cooperation in the presence of exploitation and noise.}, author = {Zagorsky, Benjamin and Reiter, Johannes and Chatterjee, Krishnendu and Nowak, Martin}, publisher = {Public Library of Science}, title = {{Forgiver triumphs in alternating prisoner's dilemma }}, doi = {10.1371/journal.pone.0080814.s001}, year = {2013}, } @misc{9751, abstract = {High relatedness among interacting individuals has generally been considered a precondition for the evolution of altruism. However, kin-selection theory also predicts the evolution of altruism when relatedness is low, as long as the cost of the altruistic act is minor compared to its benefit. Here, we demonstrate evidence for a low-cost altruistic act in bacteria. We investigated Escherichia coli responding to the attack of an obligately lytic phage by committing suicide in order to prevent parasite transmission to nearby relatives. We found that bacterial suicide provides large benefits to survivors at marginal costs to committers. The cost of suicide was low because infected cells are moribund, rapidly dying upon phage infection, such that no more opportunity for reproduction remains. As a consequence of its marginal cost, host suicide was selectively favoured even when relatedness between committers and survivors approached zero. Altogether, our findings demonstrate that low-cost suicide can evolve with ease, represents an effective host-defence strategy, and seems to be widespread among microbes. Moreover, low-cost suicide might also occur in higher organisms as exemplified by infected social insect workers leaving the colony to die in isolation.}, author = {Refardt, Dominik and Bergmiller, Tobias and Kümmerli, Rolf}, publisher = {Dryad}, title = {{Data from: Altruism can evolve when relatedness is low: evidence from bacteria committing suicide upon phage infection}}, doi = {10.5061/dryad.b1q2n}, year = {2013}, } @misc{9754, abstract = {Short-read sequencing technologies have in principle made it feasible to draw detailed inferences about the recent history of any organism. In practice, however, this remains challenging due to the difficulty of genome assembly in most organisms and the lack of statistical methods powerful enough to discriminate among recent, non-equilibrium histories. We address both the assembly and inference challenges. We develop a bioinformatic pipeline for generating outgroup-rooted alignments of orthologous sequence blocks from de novo low-coverage short-read data for a small number of genomes, and show how such sequence blocks can be used to fit explicit models of population divergence and admixture in a likelihood framework. To illustrate our approach, we reconstruct the Pleistocene history of an oak-feeding insect (the oak gallwasp Biorhiza pallida) which, in common with many other taxa, was restricted during Pleistocene ice ages to a longitudinal series of southern refugia spanning theWestern Palaearctic. Our analysis of sequence blocks sampled from a single genome from each of three major glacial refugia reveals support for an unexpected history dominated by recent admixture. Despite the fact that 80% of the genome is affected by admixture during the last glacial cycle, we are able to infer the deeper divergence history of these populations. These inferences are robust to variation in block length, mutation model, and the sampling location of individual genomes within refugia. This combination of de novo assembly and numerical likelihood calculation provides a powerful framework for estimating recent population history that can be applied to any organism without the need for prior genetic resources.}, author = {Hearn, Jack and Stone, Graham and Barton, Nicholas H and Lohse, Konrad and Bunnefeld, Lynsey}, publisher = {Dryad}, title = {{Data from: Likelihood-based inference of population history from low coverage de novo genome assemblies}}, doi = {10.5061/dryad.r3r60}, year = {2013}, } @article{2443, abstract = {The mode of action of auxin is based on its non-uniform distribution within tissues and organs. Despite the wide use of several auxin analogues in research and agriculture, little is known about the specificity of different auxin-related transport and signalling processes towards these compounds. Using seedlings of Arabidopsis thaliana and suspension-cultured cells of Nicotiana tabacum (BY-2), the physiological activity of several auxin analogues was investigated, together with their capacity to induce auxin-dependent gene expression, to inhibit endocytosis and to be transported across the plasma membrane. This study shows that the specificity criteria for different auxin-related processes vary widely. Notably, the special behaviour of some synthetic auxin analogues suggests that they might be useful tools in investigations of the molecular mechanism of auxin action. Thus, due to their differential stimulatory effects on DR5 expression, indole-3-propionic (IPA) and 2,4,5-trichlorophenoxy acetic (2,4,5-T) acids can serve in studies of TRANSPORT INHIBITOR RESPONSE 1/AUXIN SIGNALLING F-BOX (TIR1/AFB)-mediated auxin signalling, and 5-fluoroindole-3-acetic acid (5-F-IAA) can help to discriminate between transcriptional and non-transcriptional pathways of auxin signalling. The results demonstrate that the major determinants for the auxin-like physiological potential of a particular compound are very complex and involve its chemical and metabolic stability, its ability to distribute in tissues in a polar manner and its activity towards auxin signalling machinery.}, author = {Simon, Sibu and Kubeš, Martin and Baster, Pawel and Robert, Stéphanie and Dobrev, Petre and Friml, Jirí and Petrášek, Jan and Zažímalová, Eva}, journal = {New Phytologist}, number = {4}, pages = {1034 -- 1048}, publisher = {Wiley}, title = {{Defining the selectivity of processes along the auxin response chain: A study using auxin analogues}}, doi = {10.1111/nph.12437}, volume = {200}, year = {2013}, } @inproceedings{2444, abstract = {We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.}, author = {Chatterjee, Krishnendu and Ła̧Cki, Jakub}, location = {St. Petersburg, Russia}, pages = {543 -- 558}, publisher = {Springer}, title = {{Faster algorithms for Markov decision processes with low treewidth}}, doi = {10.1007/978-3-642-39799-8_36}, volume = {8044}, year = {2013}, } @misc{3321, author = {Quadrianto, Novi and Lampert, Christoph}, booktitle = {Encyclopedia of Systems Biology}, editor = {Dubitzky, Werner and Wolkenhauer, Olaf and Cho, Kwang and Yokota, Hiroki}, pages = {1069 -- 1069}, publisher = {Springer}, title = {{Kernel based learning}}, doi = {10.1007/978-1-4419-9863-7_604}, volume = {3}, year = {2013}, } @article{450, abstract = {Understanding the relative importance of heterosis and outbreeding depression over multiple generations is a key question in evolutionary biology and is essential for identifying appropriate genetic sources for population and ecosystem restoration. Here we use 2455 experimental crosses between 12 population pairs of the rare perennial plant Rutidosis leptorrhynchoides (Asteraceae) to investigate the multi-generational (F1, F2, F3) fitness outcomes of inter-population hybridization. We detected no evidence of outbreeding depression, with inter-population hybrids and backcrosses showing either similar fitness or significant heterosis for fitness components across the three generations. Variation in heterosis among population pairs was best explained by characteristics of the foreign source or home population, and was greatest when the source population was large, with high genetic diversity and low inbreeding, and the home population was small and inbred. Our results indicate that the primary consideration for maximizing progeny fitness following population augmentation or restoration is the use of seed from large, genetically diverse populations.}, author = {Pickup, Melinda and Field, David and Rowell, David and Young, Andrew}, journal = {Proceedings of the Royal Society of London Series B Biological Sciences}, number = {1750}, publisher = {Royal Society, The}, title = {{Source population characteristics affect heterosis following genetic rescue of fragmented plant populations}}, doi = {10.1098/rspb.2012.2058}, volume = {280}, year = {2013}, } @article{476, abstract = {Maternal exposure to infection occurring mid-gestation produces a three-fold increase in the risk of schizophrenia in the offspring. The critical initiating factor appears to be the maternal immune activation (MIA) that follows infection. This process can be induced in rodents by exposure of pregnant dams to the viral mimic Poly I:C, which triggers an immune response that results in structural, functional, behavioral, and electrophysiological phenotypes in the adult offspring that model those seen in schizophrenia. We used this model to explore the role of synchronization in brain neural networks, a process thought to be dysfunctional in schizophrenia and previously associated with positive, negative, and cognitive symptoms of schizophrenia. Exposure of pregnant dams to Poly I:C on GD15 produced an impairment in long-range neural synchrony in adult offspring between two regions implicated in schizophrenia pathology; the hippocampus and the medial prefrontal cortex (mPFC). This reduction in synchrony was ameliorated by acute doses of the antipsychotic clozapine. MIA animals have previously been shown to have impaired pre-pulse inhibition (PPI), a gold-standard measure of schizophrenia-like deficits in animal models. Our data showed that deficits in synchrony were positively correlated with the impairments in PPI. Subsequent analysis of LFP activity during the PPI response also showed that reduced coupling between the mPFC and the hippocampus following processing of the pre-pulse was associated with reduced PPI. The ability of the MIA intervention to model neurodevelopmental aspects of schizophrenia pathology provides a useful platform from which to investigate the ontogeny of aberrant synchronous processes. Further, the way in which the model expresses translatable deficits such as aberrant synchrony and reduced PPI will allow researchers to explore novel intervention strategies targeted to these changes. }, author = {Dickerson, Desiree and Bilkey, David}, journal = {Frontiers in Behavioral Neuroscience}, number = {DEC}, publisher = {Frontiers Research Foundation}, title = {{Aberrant neural synchrony in the maternal immune activation model: Using translatable measures to explore targeted interventions}}, doi = {10.3389/fnbeh.2013.00217}, volume = {7}, year = {2013}, } @article{499, abstract = {Exposure of an isogenic bacterial population to a cidal antibiotic typically fails to eliminate a small fraction of refractory cells. Historically, fractional killing has been attributed to infrequently dividing or nondividing "persisters." Using microfluidic cultures and time-lapse microscopy, we found that Mycobacterium smegmatis persists by dividing in the presence of the drug isoniazid (INH). Although persistence in these studies was characterized by stable numbers of cells, this apparent stability was actually a dynamic state of balanced division and death. Single cells expressed catalase-peroxidase (KatG), which activates INH, in stochastic pulses that were negatively correlated with cell survival. These behaviors may reflect epigenetic effects, because KatG pulsing and death were correlated between sibling cells. Selection of lineages characterized by infrequent KatG pulsing could allow nonresponsive adaptation during prolonged drug exposure.}, author = {Wakamoto, Yurichi and Dhar, Neraaj and Chait, Remy P and Schneider, Katrin and Signorino Gelo, François and Leibler, Stanislas and Mckinney, John}, journal = {Science}, number = {6115}, pages = {91 -- 95}, publisher = {American Association for the Advancement of Science}, title = {{Dynamic persistence of antibiotic-stressed mycobacteria}}, doi = {10.1126/science.1229858}, volume = {339}, year = {2013}, } @article{500, abstract = {Background: Reassortment between the RNA segments encoding haemagglutinin (HA) and neuraminidase (NA), the major antigenic influenza proteins, produces viruses with novel HA and NA subtype combinations and has preceded the emergence of pandemic strains. It has been suggested that productive viral infection requires a balance in the level of functional activity of HA and NA, arising from their closely interacting roles in the viral life cycle, and that this functional balance could be mediated by genetic changes in the HA and NA. Here, we investigate how the selective pressure varies for H7 avian influenza HA on different NA subtype backgrounds. Results: By extending Bayesian stochastic mutational mapping methods to calculate the ratio of the rate of non-synonymous change to the rate of synonymous change (d N/d S), we found the average d N/d S across the avian influenza H7 HA1 region to be significantly greater on an N2 NA subtype background than on an N1, N3 or N7 background. Observed differences in evolutionary rates of H7 HA on different NA subtype backgrounds could not be attributed to underlying differences between avian host species or virus pathogenicity. Examination of d N/d S values for each subtype on a site-by-site basis indicated that the elevated d N/d S on the N2 NA background was a result of increased selection, rather than a relaxation of selective constraint. Conclusions: Our results are consistent with the hypothesis that reassortment exposes influenza HA to significant changes in selective pressure through genetic interactions with NA. Such epistatic effects might be explicitly accounted for in future models of influenza evolution.}, author = {Ward, Melissa and Lycett, Samantha and Avila, Dorita and Bollback, Jonathan P and Leigh Brown, Andrew}, journal = {BMC Evolutionary Biology}, number = {1}, publisher = {BioMed Central}, title = {{Evolutionary interactions between haemagglutinin and neuraminidase in avian influenza}}, doi = {10.1186/1471-2148-13-222}, volume = {13}, year = {2013}, } @article{501, abstract = {All known species of extant tapirs are allopatric: 1 in southeastern Asia and 3 in Central and South America. The fossil record for tapirs, however, is much wider in geographical range, including Europe, Asia, and North and South America, going back to the late Oligocene, making the present distribution a relict of the original one. We here describe a new species of living Tapirus from the Amazon rain forest, the 1st since T. bairdii Gill, 1865, and the 1st new Perissodactyla in more than 100 years, from both morphological and molecular characters. It is shorter in stature than T. terrestris (Linnaeus, 1758) and has distinctive skull morphology, and it is basal to the clade formed by T. terrestris and T. pinchaque (Roulin, 1829). This highlights the unrecognized biodiversity in western Amazonia, where the biota faces increasing threats. Local peoples have long recognized our new species, suggesting a key role for traditional knowledge in understanding the biodiversity of the region.}, author = {Cozzuol, Mario and Clozato, Camila and Holanda, Elizete and Rodrigues, Flávio and Nienow, Samuel and De Thoisy, Benoit and Fernandes Redondo, Rodrigo A and Santos, Fabrício}, journal = {Journal of Mammalogy}, number = {6}, pages = {1331 -- 1345}, publisher = {Oxford University Press}, title = {{A new species of tapir from the Amazon}}, doi = {10.1644/12-MAMM-A-169.1}, volume = {94}, year = {2013}, } @article{502, abstract = {Blind signatures allow users to obtain signatures on messages hidden from the signer; moreover, the signer cannot link the resulting message/signature pair to the signing session. This paper presents blind signature schemes, in which the number of interactions between the user and the signer is minimal and whose blind signatures are short. Our schemes are defined over bilinear groups and are proved secure in the common-reference-string model without random oracles and under standard assumptions: CDH and the decision-linear assumption. (We also give variants over asymmetric groups based on similar assumptions.) The blind signatures are Waters signatures, which consist of 2 group elements. Moreover, we instantiate partially blind signatures, where the message consists of a part hidden from the signer and a commonly known public part, and schemes achieving perfect blindness. We propose new variants of blind signatures, such as signer-friendly partially blind signatures, where the public part can be chosen by the signer without prior agreement, 3-party blind signatures, as well as blind signatures on multiple aggregated messages provided by independent sources. We also extend Waters signatures to non-binary alphabets by proving a new result on the underlying hash function. }, author = {Blazy, Olivier and Fuchsbauer, Georg and Pointcheval, David and Vergnaud, Damien}, journal = {Journal of Computer Security}, number = {5}, pages = {627 -- 661}, publisher = {IOS Press}, title = {{Short blind signatures}}, doi = {10.3233/JCS-130477}, volume = {21}, year = {2013}, } @article{505, abstract = {Alkyd resins are polyesters containing unsaturated fatty acids that are used as binding agents in paints and coatings. Chemical drying of these polyesters is based on heavy metal catalyzed cross-linking of the unsaturated fatty acid moieties. Among the heavy-metal catalysts, cobalt complexes are the most effective, yet they have been proven to be carcinogenic. Therefore, strategies to replace the cobalt-based catalyst by environmentally friendlier and less toxic alternatives are under development. Here, we demonstrate for the first time that a laccase-mediator system can effectively replace the heavy-metal catalyst and cross-link alkyd resins. Interestingly, the biocatalytic reaction does not only work in aqueous media, but also in a solid film, where enzyme diffusion is limited. Within the catalytic cycle, the mediator oxidizes the alkyd resin and is regenerated by the laccase, which is uniformly distributed within the drying film as evidenced by confocal laser scanning microscopy. During gradual build-up of molecular weight, there is a concomitant decrease of the oxygen content in the film. A new optical sensor to follow oxygen consumption during the cross-linking reaction was developed and validated with state of the art techniques. A remarkable feature is the low sample amount required, which allows faster screening of new catalysts.}, author = {Greimel, Katrin and Perz, Veronika and Koren, Klaus and Feola, Roland and Temel, Armin and Sohar, Christian and Herrero Acero, Enrique and Klimant, Ingo and Guebitz, Georg}, journal = {Green Chemistry}, number = {2}, pages = {381 -- 388}, publisher = {Royal Society of Chemistry}, title = {{Banning toxic heavy-metal catalysts from paints: Enzymatic cross-linking of alkyd resins}}, doi = {10.1039/c2gc36666e}, volume = {15}, year = {2013}, }