TY - JOUR
AB - The fact that a sum of isotropic Gaussian kernels can have more modes than kernels is surprising. Extra (ghost) modes do not exist in ℝ1 and are generally not well studied in higher dimensions. We study a configuration of n+1 Gaussian kernels for which there are exactly n+2 modes. We show that all modes lie on a finite set of lines, which we call axes, and study the restriction of the Gaussian mixture to these axes in order to discover that there are an exponential number of critical points in this configuration. Although the existence of ghost modes remained unknown due to the difficulty of finding examples in ℝ2, we show that the resilience of ghost modes grows like the square root of the dimension. In addition, we exhibit finite configurations of isotropic Gaussian kernels with superlinearly many modes.
AU - Edelsbrunner, Herbert
AU - Fasy, Brittany Terese
AU - Rote, Günter
ID - 2815
IS - 4
JF - Discrete & Computational Geometry
TI - Add isotropic Gaussian kernels at own risk: More and more resilient modes in higher dimensions
VL - 49
ER -
TY - JOUR
AB - In solid tumors, targeted treatments can lead to dramatic regressions, but responses are often short-lived because resistant cancer cells arise. The major strategy proposed for overcoming resistance is combination therapy. We present a mathematical model describing the evolutionary dynamics of lesions in response to treatment. We first studied 20 melanoma patients receiving vemurafenib. We then applied our model to an independent set of pancreatic, colorectal, and melanoma cancer patients with metastatic disease. We find that dual therapy results in long-term disease control for most patients, if there are no single mutations that cause cross-resistance to both drugs; in patients with large disease burden, triple therapy is needed. We also find that simultaneous therapy with two drugs is much more effective than sequential therapy. Our results provide realistic expectations for the efficacy of new drug combinations and inform the design of trials for new cancer therapeutics.
AU - Božić, Ivana
AU - Reiter, Johannes
AU - Allen, Benjamin
AU - Antal, Tibor
AU - Chatterjee, Krishnendu
AU - Shah, Preya
AU - Moon, Yo
AU - Yaqubie, Amin
AU - Kelly, Nicole
AU - Le, Dung
AU - Lipson, Evan
AU - Chapman, Paul
AU - Diaz, Luis
AU - Vogelstein, Bert
AU - Nowak, Martin
ID - 2816
JF - eLife
TI - Evolutionary dynamics of cancer in response to targeted combination therapy
VL - 2
ER -
TY - JOUR
AB - The basic idea of evolutionary game theory is that payoff determines reproductive rate. Successful individuals have a higher payoff and produce more offspring. But in evolutionary and ecological situations there is not only reproductive rate but also carrying capacity. Individuals may differ in their exposure to density limiting effects. Here we explore an alternative approach to evolutionary game theory by assuming that the payoff from the game determines the carrying capacity of individual phenotypes. Successful strategies are less affected by density limitation (crowding) and reach higher equilibrium abundance. We demonstrate similarities and differences between our framework and the standard replicator equation. Our equation is defined on the positive orthant, instead of the simplex, but has the same equilibrium points as the replicator equation. Linear stability analysis produces the classical conditions for asymptotic stability of pure strategies, but the stability properties of internal equilibria can differ in the two frameworks. For example, in a two-strategy game with an internal equilibrium that is always stable under the replicator equation, the corresponding equilibrium can be unstable in the new framework resulting in a limit cycle.
AU - Novak, Sebastian
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 2817
JF - Journal of Theoretical Biology
TI - Density games
VL - 334
ER -
TY - JOUR
AB - Models of neural responses to stimuli with complex spatiotemporal correlation structure often assume that neurons are selective for only a small number of linear projections of a potentially high-dimensional input. In this review, we explore recent modeling approaches where the neural response depends on the quadratic form of the input rather than on its linear projection, that is, the neuron is sensitive to the local covariance structure of the signal preceding the spike. To infer this quadratic dependence in the presence of arbitrary (e.g., naturalistic) stimulus distribution, we review several inference methods, focusing in particular on two information theory–based approaches (maximization of stimulus energy and of noise entropy) and two likelihood-based approaches (Bayesian spike-triggered covariance and extensions of generalized linear models). We analyze the formal relationship between the likelihood-based and information-based approaches to demonstrate how they lead to consistent inference. We demonstrate the practical feasibility of these procedures by using model neurons responding to a flickering variance stimulus.
AU - Rajan, Kanaka
AU - Marre, Olivier
AU - Tkacik, Gasper
ID - 2818
IS - 7
JF - Neural Computation
TI - Learning quadratic receptive fields from neural responses to natural stimuli
VL - 25
ER -
TY - CONF
AB - We introduce quantatitive timed refinement metrics and quantitative timed simulation functions, incorporating zenoness checks, for timed systems. These functions assign positive real numbers between zero and infinity which quantify the timing mismatches between two timed systems, amongst non-zeno runs. We quantify timing mismatches in three ways: (1) the maximum timing mismatch that can arise, (2) the "steady-state" maximum timing mismatches, where initial transient timing mismatches are ignored; and (3) the (long-run) average timing mismatches amongst two systems. These three kinds of mismatches constitute three important types of timing differences. Our event times are the global times, measured from the start of the system execution, not just the time durations of individual steps. We present algorithms over timed automata for computing the three quantitative simulation functions to within any desired degree of accuracy. In order to compute the values of the quantitative simulation functions, we use a game theoretic formulation. We introduce two new kinds of objectives for two player games on finite state game graphs: (1) eventual debit-sum level objectives, and (2) average debit-sum level objectives. We present algorithms for computing the optimal values for these objectives for player 1, and then use these algorithms to compute the values of the quantitative timed simulation functions.
AU - Chatterjee, Krishnendu
AU - Prabhu, Vinayak
ID - 2819
T2 - Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control
TI - Quantitative timed simulation functions and refinement metrics for real-time systems
VL - 1
ER -
TY - CONF
AB - In this paper, we introduce the powerful framework of graph games for the analysis of real-time scheduling with firm deadlines. We introduce a novel instance of a partial-observation game that is suitable for this purpose, and prove decidability of all the involved decision problems. We derive a graph game that allows the automated computation of the competitive ratio (along with an optimal witness algorithm for the competitive ratio) and establish an NP-completeness proof for the graph game problem. For a given on-line algorithm, we present polynomial time solution for computing (i) the worst-case utility; (ii) the worst-case utility ratio w.r.t. a clairvoyant off-line algorithm; and (iii) the competitive ratio. A major strength of the proposed approach lies in its flexibility w.r.t. incorporating additional constraints on the adversary and/or the algorithm, including limited maximum or average load, finiteness of periods of overload, etc., which are easily added by means of additional instances of standard objective functions for graph games.
AU - Chatterjee, Krishnendu
AU - Kößler, Alexander
AU - Schmid, Ulrich
ID - 2820
SN - 978-1-4503-1567-8
T2 - Proceedings of the 16th International conference on Hybrid systems: Computation and control
TI - Automated analysis of real-time scheduling using graph games
ER -
TY - JOUR
AB - Many key aspects of plant development are regulated by the polarized transport of the phytohormone auxin. Cellular auxin efflux, the rate-limiting step in this process, has been shown to rely on the coordinated action of PIN-formed (PIN) and B-type ATP binding cassette (ABCB) carriers. Here, we report that polar auxin transport in the Arabidopsis thaliana root also requires the action of a Major Facilitator Superfamily (MFS) transporter, Zinc-Induced Facilitator-Like 1 (ZIFL1). Sequencing, promoter-reporter, and fluorescent protein fusion experiments indicate that the full-length ZIFL1.1 protein and a truncated splice isoform, ZIFL1.3, localize to the tonoplast of root cells and the plasma membrane of leaf stomatal guard cells, respectively. Using reverse genetics, we show that the ZIFL1.1 transporter regulates various root auxin-related processes, while the ZIFL1.3 isoform mediates drought tolerance by regulating stomatal closure. Auxin transport and immunolocalization assays demonstrate that ZIFL1.1 indirectly modulates cellular auxin efflux during shootward auxin transport at the root tip, likely by regulating plasma membrane PIN2 abundance. Finally, heterologous expression in yeast revealed that ZIFL1.1 and ZIFL1.3 share H+-coupled K+ transport activity. Thus, by determining the subcellular and tissue distribution of two isoforms, alternative splicing dictates a dual function for the ZIFL1 transporter. We propose that this MFS carrier regulates stomatal movements and polar auxin transport by modulating potassium and proton fluxes in Arabidopsis cells.
AU - Remy, Estelle
AU - Cabrito, Tânia
AU - Baster, Pawel
AU - Batista, Rita
AU - Teixeira, Miguel
AU - Friml, Jirí
AU - Sá Correia, Isabel
AU - Duque, Paula
ID - 2821
IS - 3
JF - Plant Cell
TI - A major facilitator superfamily transporter plays a dual role in polar auxin transport and drought stress tolerance in Arabidopsis
VL - 25
ER -
TY - JOUR
AB - Identification of genes that control root system architecture in crop plants requires innovations that enable high-throughput and accurate measurements of root system architecture through time. We demonstrate the ability of a semiautomated 3D in vivo imaging and digital phenotyping pipeline to interrogate the quantitative genetic basis of root system growth in a rice biparental mapping population, Bala x Azucena. We phenotyped >1,400 3D root models and >57,000 2D images for a suite of 25 traits that quantified the distribution, shape, extent of exploration, and the intrinsic size of root networks at days 12, 14, and 16 of growth in a gellan gum medium. From these data we identified 89 quantitative trait loci, some of which correspond to those found previously in soil-grown plants, and provide evidence for genetic tradeoffs in root growth allocations, such as between the extent and thoroughness of exploration. We also developed a multivariate method for generating and mapping central root architecture phenotypes and used it to identify five major quantitative trait loci (r2 = 24-37%), two of which were not identified by our univariate analysis. Our imaging and analytical platform provides a means to identify genes with high potential for improving root traits and agronomic qualities of crops.
AU - Topp, Christopher
AU - Iyer Pascuzzi, Anjali
AU - Anderson, Jill
AU - Lee, Cheng
AU - Zurek, Paul
AU - Symonova, Olga
AU - Zheng, Ying
AU - Bucksch, Alexander
AU - Mileyko, Yuriy
AU - Galkovskyi, Taras
AU - Moore, Brad
AU - Harer, John
AU - Edelsbrunner, Herbert
AU - Mitchell Olds, Thomas
AU - Weitz, Joshua
AU - Benfey, Philip
ID - 2822
IS - 18
JF - PNAS
TI - 3D phenotyping and quantitative trait locus mapping identify core regions of the rice genome controlling root architecture
VL - 110
ER -
TY - JOUR
AB - The primary goal of restoration is to create self-sustaining ecological communities that are resilient to periodic disturbance. Currently, little is known about how restored communities respond to disturbance events such as fire and how this response compares to remnant vegetation. Following the 2003 fires in south-eastern Australia we examined the post-fire response of revegetation plantings and compared this to remnant vegetation. Ten burnt and 10 unburnt (control) sites were assessed for each of three types of vegetation (direct seeding revegetation, revegetation using nursery seedlings (tubestock) and remnant woodland). Sixty sampling sites were surveyed 6months after fire to quantify the initial survival of mid- and overstorey plant species in each type of vegetation. Three and 5years after fire all sites were resurveyed to assess vegetation structure, species diversity and vigour, as well as indicators of soil function. Overall, revegetation showed high (>60%) post-fire survival, but this varied among species depending on regeneration strategy (obligate seeder or resprouter). The native ground cover, mid- and overstorey in both types of plantings showed rapid recovery of vegetation structure and cover within 3years of fire. This recovery was similar to the burnt remnant woodlands. Non-native (exotic) ground cover initially increased after fire, but was no different in burnt and unburnt sites 5years after fire. Fire had no effect on species richness, but burnt direct seeding sites had reduced species diversity (Simpson's Diversity Index) while diversity was higher in burnt remnant woodlands. Indices of soil function in all types of vegetation had recovered to levels found in unburnt sites 5years after fire. These results indicate that even young revegetation (stands <10years old) showed substantial recovery from disturbance by fire. This suggests that revegetation can provide an important basis for restoring woodland communities in the fire-prone Australian environment.
AU - Pickup, Melinda
AU - Wilson, Susie
AU - Freudenberger, David
AU - Nicholls, Nick
AU - Gould, Lori
AU - Hnatiuk, Sarah
AU - Delandre, Jeni
ID - 2823
IS - 3
JF - Austral Ecology
TI - Post-fire recovery of revegetated woodland communities in south-eastern Australia
VL - 38
ER -
TY - JOUR
AB - We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games.
AU - Chatterjee, Krishnendu
AU - Prabhu, Vinayak
ID - 2824
JF - Information and Computation
TI - Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
VL - 228-229
ER -
TY - JOUR
AB - Removal of cargos from the cell surface via endocytosis is an efficient mechanism to regulate activities of plasma membrane (PM)-resident proteins, such as receptors or transporters. Salicylic acid (SA) is an important plant hormone that is traditionally associated with pathogen defense. Here, we describe an unanticipated effect of SA on subcellular endocytic cycling of proteins. Both exogenous treatments and endogenously enhanced SA levels repressed endocytosis of different PM proteins. The SA effect on endocytosis did not involve transcription or known components of the SA signaling pathway for transcriptional regulation. SA likely targets an endocytic mechanism that involves the coat protein clathrin, because SA interfered with the clathrin incidence at the PM and clathrin-deficient mutants were less sensitive to the impact of SA on the auxin distribution and root bending during the gravitropic response. By contrast, SA did not affect the ligand-induced endocytosis of the FLAGELLIN SENSING2 (FLS2) receptor during pathogen responses. Our data suggest that the established SA impact on transcription in plant immunity and the nontranscriptional effect of SA on clathrin-mediated endocytosis are independent mechanisms by which SA regulates distinct aspects of plant physiology.
AU - Du, Yunlong
AU - Tejos, Ricardo
AU - Beck, Martina
AU - Himschoot, Ellie
AU - Li, Hongjiang
AU - Robatzek, Silke
AU - Vanneste, Steffen
AU - Friml, Jirí
ID - 2827
IS - 19
JF - PNAS
TI - Salicylic acid interferes with clathrin-mediated endocytic protein trafficking
VL - 110
ER -
TY - JOUR
AB - We study the complexity of valued constraint satisfaction problems (VCSPs) parametrized by a constraint language, a fixed set of cost functions over a finite domain. An instance of the problem is specified by a sum of cost functions from the language and the goal is to minimize the sum. Under the unique games conjecture, the approximability of finite-valued VCSPs is well understood, see Raghavendra [2008]. However, there is no characterization of finite-valued VCSPs, let alone general-valued VCSPs, that can be solved exactly in polynomial time, thus giving insights from a combinatorial optimization perspective. We consider the case of languages containing all possible unary cost functions. In the case of languages consisting of only {0, ∞}-valued cost functions (i.e., relations), such languages have been called conservative and studied by Bulatov [2003, 2011] and recently by Barto [2011]. Since we study valued languages, we call a language conservative if it contains all finite-valued unary cost functions. The computational complexity of conservative valued languages has been studied by Cohen et al. [2006] for languages over Boolean domains, by Deineko et al. [2008] for {0, 1}-valued languages (a.k.a Max-CSP), and by Takhanov [2010a] for {0, ∞}-valued languages containing all finite-valued unary cost functions (a.k.a. Min-Cost-Hom). We prove a Schaefer-like dichotomy theorem for conservative valued languages: if all cost functions in the language satisfy a certain condition (specified by a complementary combination of STP and MJN multimor-phisms), then any instance can be solved in polynomial time (via a new algorithm developed in this article), otherwise the language is NP-hard. This is the first complete complexity classification of general-valued constraint languages over non-Boolean domains. It is a common phenomenon that complexity classifications of problems over non-Boolean domains are significantly harder than the Boolean cases. The polynomial-time algorithm we present for the tractable cases is a generalization of the submodular minimization problem and a result of Cohen et al. [2008]. Our results generalize previous results by Takhanov [2010a] and (a subset of results) by Cohen et al. [2006] and Deineko et al. [2008]. Moreover, our results do not rely on any computer-assisted search as in Deineko et al. [2008], and provide a powerful tool for proving hardness of finite-valued and general-valued languages.
AU - Kolmogorov, Vladimir
AU - Živný, Stanislav
ID - 2828
IS - 2
JF - Journal of the ACM
TI - The complexity of conservative valued CSPs
VL - 60
ER -
TY - JOUR
AB - Laminar-turbulent intermittency is intrinsic to the transitional regime of a wide range of fluid flows including pipe, channel, boundary layer, and Couette flow. In the latter turbulent spots can grow and form continuous stripes, yet in the stripe-normal direction they remain interspersed by laminar fluid. We carry out direct numerical simulations in a long narrow domain and observe that individual turbulent stripes are transient. In agreement with recent observations in pipe flow, we find that turbulence becomes sustained at a distinct critical point once the spatial proliferation outweighs the inherent decaying process. By resolving the asymptotic size distributions close to criticality we can for the first time demonstrate scale invariance at the onset of turbulence.
AU - Shi, Liang
AU - Avila, Marc
AU - Hof, Björn
ID - 2829
IS - 20
JF - Physical Review Letters
TI - Scale invariance at the onset of turbulence in couette flow
VL - 110
ER -
TY - JOUR
AU - Moussion, Christine
AU - Sixt, Michael K
ID - 2830
IS - 5
JF - Immunity
TI - A conduit to amplify innate immunity
VL - 38
ER -
TY - JOUR
AB - We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps.
AU - Chatterjee, Krishnendu
AU - Henzinger, Monika
AU - Joglekar, Manas
AU - Shah, Nisarg
ID - 2831
IS - 3
JF - Formal Methods in System Design
TI - Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
VL - 42
ER -
TY - JOUR
AB - PIN-FORMED (PIN) proteins localize asymmetrically at the plasma membrane and mediate intercellular polar transport of the plant hormone auxin that is crucial for a multitude of developmental processes in plants. PIN localization is under extensive control by environmental or developmental cues, but mechanisms regulating PIN localization are not fully understood. Here we show that early endosomal components ARF GEF BEN1 and newly identified Sec1/Munc18 family protein BEN2 are involved in distinct steps of early endosomal trafficking. BEN1 and BEN2 are collectively required for polar PIN localization, for their dynamic repolarization, and consequently for auxin activity gradient formation and auxin-related developmental processes including embryonic patterning, organogenesis, and vasculature venation patterning. These results show that early endosomal trafficking is crucial for cell polarity and auxin-dependent regulation of plant architecture.
AU - Tanaka, Hirokazu
AU - Kitakura, Saeko
AU - Rakusová, Hana
AU - Uemura, Tomohiro
AU - Feraru, Mugurel
AU - De Rycke, Riet
AU - Robert, Stéphanie
AU - Kakimoto, Tatsuo
AU - Friml, Jirí
ID - 2832
IS - 5
JF - PLoS Genetics
TI - Cell polarity and patterning by PIN trafficking through early endosomal compartments in arabidopsis thaliana
VL - 9
ER -
TY - JOUR
AB - During development, mechanical forces cause changes in size, shape, number, position, and gene expression of cells. They are therefore integral to any morphogenetic processes. Force generation by actin-myosin networks and force transmission through adhesive complexes are two self-organizing phenomena driving tissue morphogenesis. Coordination and integration of forces by long-range force transmission and mechanosensing of cells within tissues produce large-scale tissue shape changes. Extrinsic mechanical forces also control tissue patterning by modulating cell fate specification and differentiation. Thus, the interplay between tissue mechanics and biochemical signaling orchestrates tissue morphogenesis and patterning in development.
AU - Heisenberg, Carl-Philipp J
AU - Bellaïche, Yohanns
ID - 2833
IS - 5
JF - Cell
TI - Forces in tissue morphogenesis and patterning
VL - 153
ER -
TY - JOUR
AB - Although the equations governing fluid flow are well known, there are no analytical expressions that describe the complexity of turbulent motion. A recent proposition is that in analogy to low dimensional chaotic systems, turbulence is organized around unstable solutions of the governing equations which provide the building blocks of the disordered dynamics. We report the discovery of periodic solutions which just like intermittent turbulence are spatially localized and show that turbulent transients arise from one such solution branch.
AU - Avila, Marc
AU - Mellibovsky, Fernando
AU - Roland, Nicolas
AU - Hof, Björn
ID - 2834
IS - 22
JF - Physical Review Letters
TI - Streamwise-localized solutions at the onset of turbulence in pipe flow
VL - 110
ER -
TY - JOUR
AB - The phytohormone auxin regulates virtually every aspect of plant development. To identify new genes involved in auxin activity, a genetic screen was performed for Arabidopsis (Arabidopsis thaliana) mutants with altered expression of the auxin-responsive reporter DR5rev:GFP. One of the mutants recovered in the screen, designated as weak auxin response3 (wxr3), exhibits much lower DR5rev:GFP expression when treated with the synthetic auxin 2,4-dichlorophenoxyacetic acid and displays severe defects in root development. The wxr3 mutant decreases polar auxin transport and results in a disruption of the asymmetric auxin distribution. The levels of the auxin transporters AUXIN1 and PIN-FORMED are dramatically reduced in the wxr3 root tip. Molecular analyses demonstrate that WXR3 is ROOT ULTRAVIOLET B-SENSITIVE1 (RUS1), a member of the conserved Domain of Unknown Function647 protein family found in diverse eukaryotic organisms. Our data suggest that RUS1/WXR3 plays an essential role in the regulation of polar auxin transport by maintaining the proper level of auxin transporters on the plasma membrane.
AU - Yu, Hong
AU - Karampelias, Michael
AU - Robert, Stéphanie
AU - Peer, Wendy
AU - Swarup, Ranjan
AU - Ye, Songqing
AU - Ge, Lei
AU - Cohen, Jerry
AU - Murphy, Angus
AU - Friml, Jirí
AU - Estelle, Mark
ID - 2835
IS - 2
JF - Plant Physiology
TI - Root ultraviolet b-sensitive1/weak auxin response3 is essential for polar auxin transport in arabidopsis
VL - 162
ER -
TY - JOUR
AB - We study the automatic synthesis of fair non-repudiation protocols, a class of fair exchange protocols, used for digital contract signing. First, we show how to specify the objectives of the participating agents and the trusted third party as path formulas in linear temporal logic and prove that the satisfaction of these objectives imply fairness; a property required of fair exchange protocols. We then show that weak (co-operative) co-synthesis and classical (strictly competitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS) succeeds. We demonstrate the success of AGS as follows: (a) any solution of AGS is attack-free; no subset of participants can violate the objectives of the other participants; (b) the Asokan-Shoup-Waidner certified mail protocol that has known vulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch non-repudiation protocol is a solution of AGS; and (d) AGS presents a new and symmetric fair non-repudiation protocol that is attack-free. To our knowledge this is the first application of synthesis to fair non-repudiation protocols, and our results show how synthesis can both automatically discover vulnerabilities in protocols and generate correct protocols. The solution to AGS can be computed efficiently as the secure equilibrium solution of three-player graph games.
AU - Chatterjee, Krishnendu
AU - Raman, Vishwanath
ID - 2836
IS - 4
JF - Formal Aspects of Computing
TI - Assume-guarantee synthesis for digital contract signing
VL - 26
ER -
TY - JOUR
AB - We consider a general class of N × N random matrices whose entries hij are independent up to a symmetry constraint, but not necessarily identically distributed. Our main result is a local semicircle law which improves previous results [17] both in the bulk and at the edge. The error bounds are given in terms of the basic small parameter of the model, maxi,j E|hij|2. As a consequence, we prove the universality of the local n-point correlation functions in the bulk spectrum for a class of matrices whose entries do not have comparable variances, including random band matrices with band width W ≫N1-εn with some εn > 0 and with a negligible mean-field component. In addition, we provide a coherent and pedagogical proof of the local semicircle law, streamlining and strengthening previous arguments from [17, 19, 6].
AU - Erdös, László
AU - Knowles, Antti
AU - Yau, Horng
AU - Yin, Jun
ID - 2837
IS - 59
JF - Electronic Journal of Probability
TI - The local semicircle law for a general class of random matrices
VL - 18
ER -
TY - JOUR
AB - Individuals with Down syndrome (DS) present important motor deficits that derive from altered motor development of infants and young children. DYRK1A, a candidate gene for DS abnormalities has been implicated in motor function due to its expression in motor nuclei in the adult brain, and its overexpression in DS mouse models leads to hyperactivity and altered motor learning. However, its precise role in the adult motor system, or its possible involvement in postnatal locomotor development has not yet been clarified. During the postnatal period we observed time-specific expression of Dyrk1A in discrete subsets of brainstem nuclei and spinal cord motor neurons. Interestingly, we describe for the first time the presence of Dyrk1A in the presynaptic terminal of the neuromuscular junctions and its axonal transport from the facial nucleus, suggesting a function for Dyrk1A in these structures. Relevant to DS, Dyrk1A overexpression in transgenic mice (TgDyrk1A) produces motor developmental alterations possibly contributing to DS motor phenotypes and modifies the numbers of motor cholinergic neurons, suggesting that the kinase may have a role in the development of the brainstem and spinal cord motor system.
AU - Arquè Fuste, Gloria
AU - Casanovas, Anna
AU - Dierssen, Mara
ID - 2838
IS - 1
JF - PLoS One
TI - Dyrk1A is dynamically expressed on subsets of motor neurons and in the neuromuscular junction: Possible role in Down syndrome
VL - 8
ER -
TY - JOUR
AB - Directional guidance of cells via gradients of chemokines is considered crucial for embryonic development, cancer dissemination, and immune responses. Nevertheless, the concept still lacks direct experimental confirmation in vivo. Here, we identify endogenous gradients of the chemokine CCL21 within mouse skin and show that they guide dendritic cells toward lymphatic vessels. Quantitative imaging reveals depots of CCL21 within lymphatic endothelial cells and steeply decaying gradients within the perilymphatic interstitium. These gradients match the migratory patterns of the dendritic cells, which directionally approach vessels from a distance of up to 90-micrometers. Interstitial CCL21 is immobilized to heparan sulfates, and its experimental delocalization or swamping the endogenous gradients abolishes directed migration. These findings functionally establish the concept of haptotaxis, directed migration along immobilized gradients, in tissues.
AU - Weber, Michele
AU - Hauschild, Robert
AU - Schwarz, Jan
AU - Moussion, Christine
AU - De Vries, Ingrid
AU - Legler, Daniel
AU - Luther, Sanjiv
AU - Bollenbach, Mark Tobias
AU - Sixt, Michael K
ID - 2839
IS - 6117
JF - Science
TI - Interstitial dendritic cell guidance by haptotactic chemokine gradients
VL - 339
ER -
TY - JOUR
AB - It is known that the entorhinal cortex plays a crucial role in spatial cognition in rodents. Neuroanatomical and electrophysiological data suggest that there is a functional distinction between 2 subregions within the entorhinal cortex, the medial entorhinal cortex (MEC), and the lateral entorhinal cortex (LEC). Rats with MEC or LEC lesions were trained in 2 navigation tasks requiring allothetic (water maze task) or idiothetic (path integration) information processing and 2-object exploration tasks allowing testing of spatial and nonspatial processing of intramaze objects. MEC lesions mildly affected place navigation in the water maze and produced a path integration deficit. They also altered the processing of spatial information in both exploration tasks while sparing the processing of nonspatial information. LEC lesions did not affect navigation abilities in both the water maze and the path integration tasks. They altered spatial and nonspatial processing in the object exploration task but not in the one-trial recognition task. Overall, these results indicate that the MEC is important for spatial processing and path integration. The LEC has some influence on both spatial and nonspatial processes, suggesting that the 2 kinds of information interact at the level of the EC.
AU - Van Cauter, Tiffany
AU - Camon, Jeremy
AU - Alvernhe, Alice
AU - Elduayen, Coralie
AU - Sargolini, Francesca
AU - Save, Étienne
ID - 2840
IS - 2
JF - Cerebral Cortex
TI - Distinct roles of medial and lateral entorhinal cortex in spatial cognition
VL - 23
ER -
TY - JOUR
AB - In zebrafish early development, blastoderm cells undergo extensive radial intercalations, triggering the spreading of the blastoderm over the yolk cell and thereby initiating embryonic body axis formation. Now reporting in Developmental Cell, Song et al. (2013) demonstrate a critical function for EGF-dependent E-cadherin endocytosis in promoting blastoderm cell intercalations.
AU - Morita, Hitoshi
AU - Heisenberg, Carl-Philipp J
ID - 2841
IS - 6
JF - Developmental Cell
TI - Holding on and letting go: Cadherin turnover in cell intercalation
VL - 24
ER -
TY - JOUR
AB - We outline two approaches to inference of neighbourhood size, N, and dispersal rate, σ2, based on either allele frequencies or on the lengths of sequence blocks that are shared between genomes. Over intermediate timescales (10-100 generations, say), populations that live in two dimensions approach a quasi-equilibrium that is independent of both their local structure and their deeper history. Over such scales, the standardised covariance of allele frequencies (i.e. pairwise FS T) falls with the logarithm of distance, and depends only on neighbourhood size, N, and a 'local scale', κ; the rate of gene flow, σ2, cannot be inferred. We show how spatial correlations can be accounted for, assuming a Gaussian distribution of allele frequencies, giving maximum likelihood estimates of N and κ. Alternatively, inferences can be based on the distribution of the lengths of sequence that are identical between blocks of genomes: long blocks (>0.1 cM, say) tell us about intermediate timescales, over which we assume a quasi-equilibrium. For large neighbourhood size, the distribution of long blocks is given directly by the classical Wright-Malécot formula; this relationship can be used to infer both N and σ2. With small neighbourhood size, there is an appreciable chance that recombinant lineages will coalesce back before escaping into the distant past. For this case, we show that if genomes are sampled from some distance apart, then the distribution of lengths of blocks that are identical in state is geometric, with a mean that depends on N and σ2.
AU - Barton, Nicholas H
AU - Etheridge, Alison
AU - Kelleher, Jerome
AU - Véber, Amandine
ID - 2842
IS - 1
JF - Theoretical Population Biology
TI - Inference in two dimensions: Allele frequencies versus lengths of shared sequence blocks
VL - 87
ER -
TY - CONF
AB - Mathematical objects can be measured unambiguously, but not so objects from our physical world. Even the total length of tubelike shapes has its difficulties. We introduce a combination of geometric, probabilistic, and topological methods to design a stable length estimate for tube-like shapes; that is: one that is insensitive to small shape changes.
AU - Edelsbrunner, Herbert
AU - Pausinger, Florian
ID - 2843
T2 - 17th IAPR International Conference on Discrete Geometry for Computer Imagery
TI - Stable length estimates of tube-like shapes
VL - 7749
ER -
TY - JOUR
AB - As soon as a seed germinates, plant growth relates to gravity to ensure that the root penetrates the soil and the shoot expands aerially. Whereas mechanisms of positive and negative orthogravitropism of primary roots and shoots are relatively well understood [1-3], lateral organs often show more complex growth behavior [4]. Lateral roots (LRs) seemingly suppress positive gravitropic growth and show a defined gravitropic set-point angle (GSA) that allows radial expansion of the root system (plagiotropism) [3, 4]. Despite its eminent importance for root architecture, it so far remains completely unknown how lateral organs partially suppress positive orthogravitropism. Here we show that the phytohormone auxin steers GSA formation and limits positive orthogravitropism in LR. Low and high auxin levels/signaling lead to radial or axial root systems, respectively. At a cellular level, it is the auxin transport-dependent regulation of asymmetric growth in the elongation zone that determines GSA. Our data suggest that strong repression of PIN4/PIN7 and transient PIN3 expression limit auxin redistribution in young LR columella cells. We conclude that PIN activity, by temporally limiting the asymmetric auxin fluxes in the tip of LRs, induces transient, differential growth responses in the elongation zone and, consequently, controls root architecture.
AU - Rosquete, Michel
AU - Von Wangenheim, Daniel
AU - Marhavy, Peter
AU - Barbez, Elke
AU - Stelzer, Ernst
AU - Benková, Eva
AU - Maizel, Alexis
AU - Kleine Vehn, Jürgen
ID - 2844
IS - 9
JF - Current Biology
TI - An auxin transport mechanism restricts positive orthogravitropism in lateral roots
VL - 23
ER -
TY - JOUR
AB - At synapses formed between dissociated neurons, about half of all synaptic vesicles are refractory to evoked release, forming the so-called "resting pool." Here, we use optical measurements of vesicular pH to study developmental changes in pool partitioning and vesicle cycling in cultured hippocampal slices. Two-photon imaging of a genetically encoded two-color release sensor (ratio-sypHy) allowed us to perform calibrated measurements at individual Schaffer collateral boutons. Mature boutons released a large fraction of their vesicles during simulated place field activity, and vesicle retrieval rates were 7-fold higher compared to immature boutons. Saturating stimulation mobilized essentially all vesicles at mature synapses. Resting pool formation and a concomitant reduction in evoked release was induced by chronic depolarization but not by acute inhibition of the protein phosphatase calcineurin. We conclude that synapses in CA1 undergo a prominent refinement of vesicle use during early postnatal development that is not recapitulated in dissociated neuronal culture.
AU - Rose, Tobias
AU - Schönenberger, Philipp
AU - Jezek, Karel
AU - Oertner, Thomas
ID - 2845
IS - 6
JF - Neuron
TI - Developmental refinement of vesicle cycling at Schaffer collateral synapses
VL - 77
ER -
TY - CONF
AB - Depth-Bounded Systems form an expressive class of well-structured transition systems. They can model a wide range of concurrent infinite-state systems including those with dynamic thread creation, dynamically changing communication topology, and complex shared heap structures. We present the first method to automatically prove fair termination of depth-bounded systems. Our method uses a numerical abstraction of the system, which we obtain by systematically augmenting an over-approximation of the system’s reachable states with a finite set of counters. This numerical abstraction can be analyzed with existing termination provers. What makes our approach unique is the way in which it exploits the well-structuredness of the analyzed system. We have implemented our work in a prototype tool and used it to automatically prove liveness properties of complex concurrent systems, including nonblocking algorithms such as Treiber’s stack and several distributed processes. Many of these examples are beyond the scope of termination analyses that are based on traditional counter abstractions.
AU - Bansal, Kshitij
AU - Koskinen, Eric
AU - Wies, Thomas
AU - Zufferey, Damien
ED - Piterman, Nir
ED - Smolka, Scott
ID - 2847
TI - Structural Counter Abstraction
VL - 7795
ER -
TY - JOUR
AB - Recent work emphasizes that the maximum entropy principle provides a bridge between statistical mechanics models for collective behavior in neural networks and experiments on networks of real neurons. Most of this work has focused on capturing the measured correlations among pairs of neurons. Here we suggest an alternative, constructing models that are consistent with the distribution of global network activity, i.e. the probability that K out of N cells in the network generate action potentials in the same small time bin. The inverse problem that we need to solve in constructing the model is analytically tractable, and provides a natural 'thermodynamics' for the network in the limit of large N. We analyze the responses of neurons in a small patch of the retina to naturalistic stimuli, and find that the implied thermodynamics is very close to an unusual critical point, in which the entropy (in proper units) is exactly equal to the energy. © 2013 IOP Publishing Ltd and SISSA Medialab srl.
AU - Tkacik, Gasper
AU - Marre, Olivier
AU - Mora, Thierry
AU - Amodei, Dario
AU - Berry, Michael
AU - Bialek, William
ID - 2850
IS - 3
JF - Journal of Statistical Mechanics Theory and Experiment
TI - The simplest maximum entropy model for collective behavior in a neural network
VL - 2013
ER -
TY - JOUR
AB - The number of possible activity patterns in a population of neurons grows exponentially with the size of the population. Typical experiments explore only a tiny fraction of the large space of possible activity patterns in the case of populations with more than 10 or 20 neurons. It is thus impossible, in this undersampled regime, to estimate the probabilities with which most of the activity patterns occur. As a result, the corresponding entropy - which is a measure of the computational power of the neural population - cannot be estimated directly. We propose a simple scheme for estimating the entropy in the undersampled regime, which bounds its value from both below and above. The lower bound is the usual 'naive' entropy of the experimental frequencies. The upper bound results from a hybrid approximation of the entropy which makes use of the naive estimate, a maximum entropy fit, and a coverage adjustment. We apply our simple scheme to artificial data, in order to check their accuracy; we also compare its performance to those of several previously defined entropy estimators. We then apply it to actual measurements of neural activity in populations with up to 100 cells. Finally, we discuss the similarities and differences between the proposed simple estimation scheme and various earlier methods. © 2013 IOP Publishing Ltd and SISSA Medialab srl.
AU - Berry, Michael
AU - Tkacik, Gasper
AU - Dubuis, Julien
AU - Marre, Olivier
AU - Da Silveira, Ravá
ID - 2851
IS - 3
JF - Journal of Statistical Mechanics Theory and Experiment
TI - A simple method for estimating the entropy of neural activity
VL - 2013
ER -
TY - JOUR
AB - 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 with 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.
AU - Refardt, Dominik
AU - Bergmiller, Tobias
AU - Kümmerli, Rolf
ID - 2853
IS - 1759
JF - Proceedings of the Royal Society of London Series B Biological Sciences
TI - Altruism can evolve when relatedness is low: Evidence from bacteria committing suicide upon phage infection
VL - 280
ER -
TY - JOUR
AB - We consider concurrent games played on graphs. At every round of a game, each player simultaneously and independently selects a move; the moves jointly determine the transition to a successor state. Two basic objectives are the safety objective to stay forever in a given set of states, and its dual, the reachability objective to reach a given set of states. First, we present a simple proof of the fact that in concurrent reachability games, for all ε>0, memoryless ε-optimal strategies exist. A memoryless strategy is independent of the history of plays, and an ε-optimal strategy achieves the objective with probability within ε of the value of the game. In contrast to previous proofs of this fact, our proof is more elementary and more combinatorial. Second, we present a strategy-improvement (a.k.a. policy-iteration) algorithm for concurrent games with reachability objectives. Finally, we present a strategy-improvement algorithm for turn-based stochastic games (where each player selects moves in turns) with safety objectives. Our algorithms yield sequences of player-1 strategies which ensure probabilities of winning that converge monotonically (from below) to the value of the game. © 2012 Elsevier Inc.
AU - Chatterjee, Krishnendu
AU - De Alfaro, Luca
AU - Henzinger, Thomas A
ID - 2854
IS - 5
JF - Journal of Computer and System Sciences
TI - Strategy improvement for concurrent reachability and turn based stochastic safety games
VL - 79
ER -
TY - JOUR
AB - Genomic imprinting leads to preferred expression of either the maternal or paternal alleles of a subset of genes. Imprinting is essential for mammalian development, and its deregulation causes many diseases. However, the functional relevance of imprinting at the cellular level is poorly understood for most imprinted genes. We used mosaic analysis with double markers (MADM) in mice to create uniparental disomies (UPDs) and to visualize imprinting effects with single-cell resolution. Although chromosome 12 UPD did not produce detectable phenotypes, chromosome 7 UPD caused highly significant paternal growth dominance in the liver and lung, but not in the brain or heart. A single gene on chromosome 7, encoding the secreted insulin-like growth factor 2 (IGF2), accounts for most of the paternal dominance effect. Mosaic analyses implied additional imprinted loci on chromosome 7 acting cell autonomously to transmit the IGF2 signal. Our study reveals chromosome- and cell-type specificity of genomic imprinting effects.
AU - Hippenmeyer, Simon
AU - Johnson, Randy
AU - Luo, Liqun
ID - 2855
IS - 3
JF - Cell Reports
TI - Mosaic analysis with double markers reveals cell type specific paternal growth dominance
VL - 3
ER -
TY - JOUR
AB - G protein–coupled receptors (GPCRs), the largest family of membrane signaling proteins, respond to neurotransmitters, hormones and small environmental molecules. The neuronal function of many GPCRs has been difficult to resolve because of an inability to gate them with subtype specificity, spatial precision, speed and reversibility. To address this, we developed an approach for opto-chemical engineering of native GPCRs. We applied this to the metabotropic glutamate receptors (mGluRs) to generate light-agonized and light-antagonized mGluRs (LimGluRs). The light-agonized LimGluR2, on which we focused, was fast, bistable and supported multiple rounds of on/off switching. Light gated two of the primary neuronal functions of mGluR2: suppression of excitability and inhibition of neurotransmitter release. We found that the light-antagonized tool LimGluR2-block was able to manipulate negative feedback of synaptically released glutamate on transmitter release. We generalized the optical control to two additional family members: mGluR3 and mGluR6. This system worked in rodent brain slices and in zebrafish in vivo, where we found that mGluR2 modulated the threshold for escape behavior. These light-gated mGluRs pave the way for determining the roles of mGluRs in synaptic plasticity, memory and disease.
AU - Levitz, Joshua
AU - Pantoja, Carlos
AU - Gaub, Benjamin
AU - Janovjak, Harald L
AU - Reiner, Andreas
AU - Hoagland, Adam
AU - Schoppik, David
AU - Kane, Brian
AU - Stawski, Philipp
AU - Schier, Alexander
AU - Trauner, Dirk
AU - Isacoff, Ehud
ID - 2856
JF - Nature Neuroscience
TI - Optical control of metabotropic glutamate receptors
VL - 16
ER -
TY - JOUR
AB - In the vibrant field of optogenetics, optics and genetic targeting are combined to commandeer cellular functions, such as the neuronal action potential, by optically stimulating light-sensitive ion channels expressed in the cell membrane. One broadly applicable manifestation of this approach are covalently attached photochromic tethered ligands (PTLs) that allow activating ligand-gated ion channels with outstanding spatial and temporal resolution. Here, we describe all steps towards the successful development and application of PTL-gated ion channels in cell lines and primary cells. The basis for these experiments forms a combination of molecular modeling, genetic engineering, cell culture, and electrophysiology. The light-gated glutamate receptor (LiGluR), which consists of the PTL-functionalized GluK2 receptor, serves as a model.
AU - Szobota, Stephanie
AU - Mckenzie, Catherine
AU - Janovjak, Harald L
ID - 2857
JF - Methods in Molecular Biology
TI - Optical control of ligand-gated ion channels
VL - 998
ER -
TY - JOUR
AB - Tumor growth is caused by the acquisition of driver mutations, which enhance the net reproductive rate of cells. Driver mutations may increase cell division, reduce cell death, or allow cells to overcome density-limiting effects. We study the dynamics of tumor growth as one additional driver mutation is acquired. Our models are based on two-type branching processes that terminate in either tumor disappearance or tumor detection. In our first model, both cell types grow exponentially, with a faster rate for cells carrying the additional driver. We find that the additional driver mutation does not affect the survival probability of the lesion, but can substantially reduce the time to reach the detectable size if the lesion is slow growing. In our second model, cells lacking the additional driver cannot exceed a fixed carrying capacity, due to density limitations. In this case, the time to detection depends strongly on this carrying capacity. Our model provides a quantitative framework for studying tumor dynamics during different stages of progression. We observe that early, small lesions need additional drivers, while late stage metastases are only marginally affected by them. These results help to explain why additional driver mutations are typically not detected in fast-growing metastases.
AU - Reiter, Johannes
AU - Božić, Ivana
AU - Allen, Benjamin
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 2858
IS - 1
JF - Evolutionary Applications
TI - The effect of one additional driver mutation on tumor progression
VL - 6
ER -
TY - JOUR
AB - Given a continuous function f:X-R on a topological space, we consider the preimages of intervals and their homology groups and show how to read the ranks of these groups from the extended persistence diagram of f. In addition, we quantify the robustness of the homology classes under perturbations of f using well groups, and we show how to read the ranks of these groups from the same extended persistence diagram. The special case X=R3 has ramifications in the fields of medical imaging and scientific visualization.
AU - Bendich, Paul
AU - Edelsbrunner, Herbert
AU - Morozov, Dmitriy
AU - Patel, Amit
ID - 2859
IS - 1
JF - Homology, Homotopy and Applications
TI - Homology and robustness of level and interlevel sets
VL - 15
ER -
TY - JOUR
AB - In the hippocampus, cell assemblies forming mnemonic representations of space are thought to arise as a result of changes in functional connections of pyramidal cells. We have found that CA1 interneuron circuits are also reconfigured during goal-oriented spatial learning through modification of inputs from pyramidal cells. As learning progressed, new pyramidal assemblies expressed in theta cycles alternated with previously established ones, and eventually overtook them. The firing patterns of interneurons developed a relationship to new, learning-related assemblies: some interneurons associated their activity with new pyramidal assemblies while some others dissociated from them. These firing associations were explained by changes in the weight of monosynaptic inputs received by interneurons from new pyramidal assemblies, as these predicted the associational changes. Spatial learning thus engages circuit modifications in the hippocampus that incorporate a redistribution of inhibitory activity that might assist in the segregation of competing pyramidal cell assembly patterns in space and time.
AU - Dupret, David
AU - O'Neill, Joseph
AU - Csicsvari, Jozsef L
ID - 2860
IS - 1
JF - Neuron
TI - Dynamic reconfiguration of hippocampal interneuron circuits during spatial learning
VL - 78
ER -
TY - JOUR
AB - We consider a two-parameter family of piecewise linear maps in which the moduli of the two slopes take different values. We provide numerical evidence of the existence of some parameter regions in which the Lyapunov exponent and the topological entropy remain constant. Analytical proof of this phenomenon is also given for certain cases. Surprisingly however, the systems with that property are not conjugate as we prove by using kneading theory.
AU - Botella Soler, Vicente
AU - Oteo, José
AU - Ros, Javier
AU - Glendinning, Paul
ID - 2861
IS - 12
JF - Journal of Physics A: Mathematical and Theoretical
TI - Lyapunov exponent and topological entropy plateaus in piecewise linear maps
VL - 46
ER -
TY - JOUR
AB - Motile cilia perform crucial functions during embryonic development and throughout adult life. Development of organs containing motile cilia involves regulation of cilia formation (ciliogenesis) and formation of a luminal space (lumenogenesis) in which cilia generate fluid flows. Control of ciliogenesis and lumenogenesis is not yet fully understood, and it remains unclear whether these processes are coupled. In the zebrafish embryo, lethal giant larvae 2 (lgl2) is expressed prominently in ciliated organs. Lgl proteins are involved in establishing cell polarity and have been implicated in vesicle trafficking. Here, we identified a role for Lgl2 in development of ciliated epithelia in Kupffer's vesicle, which directs left-right asymmetry of the embryo; the otic vesicles, which give rise to the inner ear; and the pronephric ducts of the kidney. Using Kupffer's vesicle as a model ciliated organ, we found that depletion of Lgl2 disrupted lumen formation and reduced cilia number and length. Immunofluorescence and time-lapse imaging of Kupffer's vesicle morphogenesis in Lgl2-deficient embryos suggested cell adhesion defects and revealed loss of the adherens junction component E-cadherin at lateral membranes. Genetic interaction experiments indicate that Lgl2 interacts with Rab11a to regulate E-cadherin and mediate lumen formation that is uncoupled from cilia formation. These results uncover new roles and interactions for Lgl2 that are crucial for both lumenogenesis and ciliogenesis and indicate that these processes are genetically separable in zebrafish.
AU - Tay, Hwee
AU - Schulze, Sabrina
AU - Compagnon, Julien
AU - Foley, Fiona
AU - Heisenberg, Carl-Philipp J
AU - Yost, H Joseph
AU - Abdelilah Seyfried, Salim
AU - Amack, Jeffrey
ID - 2862
IS - 7
JF - Development
TI - Lethal giant larvae 2 regulates development of the ciliated organ Kupffer’s vesicle
VL - 140
ER -
TY - JOUR
AB - Neural populations encode information about their stimulus in a collective fashion, by joint activity patterns of spiking and silence. A full account of this mapping from stimulus to neural activity is given by the conditional probability distribution over neural codewords given the sensory input. For large populations, direct sampling of these distributions is impossible, and so we must rely on constructing appropriate models. We show here that in a population of 100 retinal ganglion cells in the salamander retina responding to temporal white-noise stimuli, dependencies between cells play an important encoding role. We introduce the stimulus-dependent maximum entropy (SDME) model—a minimal extension of the canonical linear-nonlinear model of a single neuron, to a pairwise-coupled neural population. We find that the SDME model gives a more accurate account of single cell responses and in particular significantly outperforms uncoupled models in reproducing the distributions of population codewords emitted in response to a stimulus. We show how the SDME model, in conjunction with static maximum entropy models of population vocabulary, can be used to estimate information-theoretic quantities like average surprise and information transmission in a neural population.
AU - Granot Atedgi, Einat
AU - Tkacik, Gasper
AU - Segev, Ronen
AU - Schneidman, Elad
ID - 2863
IS - 3
JF - PLoS Computational Biology
TI - Stimulus-dependent maximum entropy models of neural population codes
VL - 9
ER -
TY - JOUR
AB - Lateral root (LR) formation is initiated when pericycle cells accumulate auxin, thereby acquiring founder cell (FC) status and triggering asymmetric cell divisions, giving rise to a new primordium. How this auxin maximum in pericycle cells builds up and remains focused is not understood. We report that the endodermis plays an active role in the regulation of auxin accumulation and is instructive for FCs to progress during the LR initiation (LRI) phase. We describe the functional importance of a PIN3 (PIN-formed) auxin efflux carrier-dependent hormone reflux pathway between overlaying endodermal and pericycle FCs. Disrupting this reflux pathway causes dramatic defects in the progress of FCs towards the next initiation phase. Our data identify an unexpected regulatory function for the endodermis in LRI as part of the fine-tuning mechanism that appears to act as a check point in LR organogenesis after FCs are specified.
AU - Marhavy, Peter
AU - Vanstraelen, Marleen
AU - De Rybel, Bert
AU - Zhaojun, Ding
AU - Bennett, Malcolm
AU - Beeckman, Tom
AU - Benková, Eva
ID - 2880
IS - 1
JF - EMBO Journal
TI - Auxin reflux between the endodermis and pericycle promotes lateral root initiation
VL - 32
ER -
TY - JOUR
AB - Gravitropic bending of plant organs is mediated by an asymmetric signaling of the plant hormone auxin between the upper and lower side of the respective organ. Here, we show that also another plant hormone, gibberellic acid (GA), shows asymmetric action during gravitropic responses. Immunodetection using an antibody against GA and monitoring GA signaling output by downstream degradation of DELLA proteins revealed an asymmetric GA distribution and response with the maximum at the lower side of gravistimulated roots. Genetic or pharmacological manipulation of GA levels or response affects gravity-mediated auxin redistribution and root bending response. The higher GA levels at the lower side of the root correlate with increased amounts of PIN-FORMED2 (PIN2) auxin transporter at the plasma membrane. The observed increase in PIN2 stability is caused by a specific GA effect on trafficking of PIN proteins to lytic vacuoles that presumably occurs downstream of brefeldin A-sensitive endosomes. Our results suggest that asymmetric auxin distribution instructive for gravity-induced differential growth is consolidated by the asymmetric action of GA that stabilizes the PIN-dependent auxin stream along the lower side of gravistimulated roots.
AU - Löfke, Christian
AU - Zwiewka, Marta
AU - Heilmann, Ingo
AU - Van Montagu, Marc
AU - Teichmann, Thomas
AU - Friml, Jirí
ID - 2882
IS - 9
JF - PNAS
TI - Asymmetric gibberellin signaling regulates vacuolar trafficking of PIN auxin transporters during root gravitropism
VL - 110
ER -
TY - JOUR
AB - Plant architecture is influenced by the polar, cell-to-cell transport of auxin that is primarily provided and regulated by plasma membrane efflux catalysts of the PIN-FORMED and B family of ABC transporter (ABCB) classes. The latter were shown to require the functionality of the FK506 binding protein42 TWISTED DWARF1 (TWD1), although underlying mechanisms are unclear. By genetic manipulation of TWD1 expression, we show here that TWD1 affects shootward root auxin reflux and, thus, downstream developmental traits, such as epidermal twisting and gravitropism of the root. Using immunological assays, we demonstrate a predominant lateral, mainly outward-facing, plasma membrane location for TWD1 in the root epidermis characterized by the lateral marker ABC transporter G36/PLEIOTROPIC DRUG-RESISTANCE8/PENETRATION3. At these epidermal plasma membrane domains, TWD1 colocalizes with nonpolar ABCB1. In planta bioluminescence resonance energy transfer analysis was used to verify specific ABC transporter B1 (ABCB1)-TWD1 interaction. Our data support a model in which TWD1 promotes lateral ABCB-mediated auxin efflux via protein-protein interaction at the plasma membrane, minimizing reflux from the root apoplast into the cytoplasm.
AU - Wang, Bangjun
AU - Bailly, Aurélien
AU - Zwiewk, Marta
AU - Henrichs, Sina
AU - Azzarello, Elisa
AU - Mancuso, Stefano
AU - Maeshima, Masayoshi
AU - Friml, Jirí
AU - Schulz, Alexander
AU - Geisler, Markus
ID - 2883
IS - 1
JF - Plant Cell
TI - Arabidopsis TWISTED DWARF1 functionally interacts with auxin exporter ABCB1 on the root plasma membrane
VL - 25
ER -
TY - JOUR
AU - Maître, Jean-Léon
AU - Berthoumieux, Hélène
AU - Krens, Gabriel
AU - Salbreux, Guillaume
AU - Julicher, Frank
AU - Paluch, Ewa
AU - Heisenberg, Carl-Philipp J
ID - 2884
IS - 2
JF - Medecine Sciences
TI - Cell adhesion mechanics of zebrafish gastrulation
VL - 29
ER -
TY - GEN
AB - This volume contains the post-proceedings of the 8th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2012, held in Znojmo, Czech Republic, in October, 2012. The 13 thoroughly revised papers were carefully selected out of 31 submissions and are presented together with 6 invited papers. The topics covered by the papers include: computer-aided analysis and verification, applications of game theory in computer science, networks and security, modern trends of graph theory in computer science, electronic systems design and testing, and quantum information processing.
ED - Kucera, Antonin
ED - Henzinger, Thomas A
ED - Nesetril, Jaroslav
ED - Vojnar, Tomas
ED - Antos, David
ID - 2885
TI - Mathematical and Engineering Methods in Computer Science
VL - 7721
ER -
TY - CONF
AB - We focus on the realizability problem of Message Sequence Graphs (MSG), i.e. the problem whether a given MSG specification is correctly distributable among parallel components communicating via messages. This fundamental problem of MSG is known to be undecidable. We introduce a well motivated restricted class of MSG, so called controllable-choice MSG, and show that all its models are realizable and moreover it is decidable whether a given MSG model is a member of this class. In more detail, this class of MSG specifications admits a deadlock-free realization by overloading existing messages with additional bounded control data. We also show that the presented class is the largest known subclass of MSG that allows for deadlock-free realization.
AU - Chmelik, Martin
AU - Řehák, Vojtěch
ID - 2886
TI - Controllable-choice message sequence graphs
VL - 7721
ER -
TY - JOUR
AB - Root system growth and development is highly plastic and is influenced by the surrounding environment. Roots frequently grow in heterogeneous environments that include interactions from neighboring plants and physical impediments in the rhizosphere. To investigate how planting density and physical objects affect root system growth, we grew rice in a transparent gel system in close proximity with another plant or a physical object. Root systems were imaged and reconstructed in three dimensions. Root-root interaction strength was calculated using quantitative metrics that characterize the extent towhich the reconstructed root systems overlap each other. Surprisingly, we found the overlap of root systems of the same genotype was significantly higher than that of root systems of different genotypes. Root systems of the same genotype tended to grow toward each other but those of different genotypes appeared to avoid each other. Shoot separation experiments excluded the possibility of aerial interactions, suggesting root communication. Staggered plantings indicated that interactions likely occur at root tips in close proximity. Recognition of obstacles also occurred through root tips, but through physical contact in a size-dependent manner. These results indicate that root systems use two different forms of communication to recognize objects and alter root architecture: root-root recognition, possibly mediated through root exudates, and root-object recognition mediated by physical contact at the root tips. This finding suggests that root tips act as local sensors that integrate rhizosphere information into global root architectural changes.
AU - Fang, Suqin
AU - Clark, Randy
AU - Zheng, Ying
AU - Iyer Pascuzzi, Anjali
AU - Weitz, Joshua
AU - Kochian, Leon
AU - Edelsbrunner, Herbert
AU - Liao, Hong
AU - Benfey, Philip
ID - 2887
IS - 7
JF - PNAS
TI - Genotypic recognition and spatial responses by rice roots
VL - 110
ER -
TY - CONF
AB - We introduce the M-modes problem for graphical models: predicting the M label configurations of highest probability that are at the same time local maxima of the probability landscape. M-modes have multiple possible applications: because they are intrinsically diverse, they provide a principled alternative to non-maximum suppression techniques for structured prediction, they can act as codebook vectors for quantizing the configuration space, or they can form component centers for mixture model approximation. We present two algorithms for solving the M-modes problem. The first algorithm solves the problem in polynomial time when the underlying graphical model is a simple chain. The second algorithm solves the problem for junction chains. In synthetic and real dataset, we demonstrate how M-modes can improve the performance of prediction. We also use the generated modes as a tool to understand the topography of the probability distribution of configurations, for example with relation to the training set size and amount of noise in the data.
AU - Chen, Chao
AU - Kolmogorov, Vladimir
AU - Yan, Zhu
AU - Metaxas, Dimitris
AU - Lampert, Christoph
ID - 2901
TI - Computing the M most probable modes of a graphical model
VL - 31
ER -
TY - CONF
AB - Motivated by an application in cell biology, we describe an extension of the kinetic data structures framework from Delaunay triangulations to fixed-radius alpha complexes. Our algorithm is implemented
using CGAL, following the exact geometric computation paradigm. We report on several
techniques to accelerate the computation that turn our implementation applicable to the underlying biological
problem.
AU - Kerber, Michael
AU - Edelsbrunner, Herbert
ID - 2906
T2 - 2013 Proceedings of the 15th Workshop on Algorithm Engineering and Experiments
TI - 3D kinetic alpha complexes and their implementation
ER -
TY - CHAP
AB - Sex and recombination are among the most striking features of the living world, and they play a crucial role in allowing the evolution of complex adaptation. The sharing of genomes through the sexual union of different individuals requires elaborate behavioral and physiological adaptations. At the molecular level, the alignment of two DNA double helices, followed by their precise cutting and rejoining, is an extraordinary feat. Sex and recombination have diverse—and often surprising—evolutionary consequences: distinct sexes, elaborate mating displays, selfish genetic elements, and so on.
AU - Barton, Nicholas H
ID - 2907
SN - 9780691149776
T2 - The Princeton Guide to Evolution
TI - Recombination and sex
ER -
TY - JOUR
AB - Hybridization is an almost inevitable component of speciation, and its study can tell us much about that process. However, hybridization itself may have a negligible influence on the origin of species: on the one hand, universally favoured alleles spread readily across hybrid zones, whilst on the other, spatially heterogeneous selection causes divergence despite gene flow. Thus, narrow hybrid zones or occasional hybridisation may hardly affect the process of divergence.
AU - Barton, Nicholas H
ID - 2908
IS - 2
JF - Journal of Evolutionary Biology
TI - Does hybridisation influence speciation?
VL - 26
ER -
TY - JOUR
AB - We survey a class of models for spatially structured populations
which we have called spatial Λ-Fleming–Viot processes. They arise from a flexible
framework for modelling in which the key innovation is that random genetic drift
is driven by a Poisson point process of spatial ‘events’. We demonstrate how this
overcomes some of the obstructions to modelling populations which evolve in two-
(and higher-) dimensional spatial continua, how its predictions match phenomena
observed in data and how it fits with classical models. Finally we outline some
directions for future research.
AU - Barton, Nicholas H
AU - Etheridge, Alison
AU - Véber, Amandine
ID - 2909
IS - 1
JF - Journal of Statistical Mechanics Theory and Experiment
TI - Modelling evolution in a spatial continuum
VL - 2013
ER -
TY - JOUR
AB - Coalescent simulation has become an indispensable tool in population genetics and many complex evolutionary scenarios have been incorporated into the basic algorithm. Despite many years of intense interest in spatial structure, however, there are no available methods to simulate the ancestry of a sample of genes that occupy a spatial continuum. This is mainly due to the severe technical problems encountered by the classical model of isolation
by distance. A recently introduced model solves these technical problems and provides a solid theoretical basis for the study of populations evolving in continuous space. We present a detailed algorithm to simulate the coalescent process in this model, and provide an efficient implementation of a generalised version of this algorithm as a freely available Python module.
AU - Kelleher, Jerome
AU - Barton, Nicholas H
AU - Etheridge, Alison
ID - 2910
IS - 7
JF - Bioinformatics
TI - Coalescent simulation in continuous space
VL - 29
ER -
TY - JOUR
AB - The ability of an organism to distinguish between various stimuli is limited by the structure and noise in the population code of its sensory neurons. Here we infer a distance measure on the stimulus space directly from the recorded activity of 100 neurons in the salamander retina. In contrast to previously used measures of stimulus similarity, this "neural metric" tells us how distinguishable a pair of stimulus clips is to the retina, based on the similarity between the induced distributions of population responses. We show that the retinal distance strongly deviates from Euclidean, or any static metric, yet has a simple structure: we identify the stimulus features that the neural population is jointly sensitive to, and show the support-vector-machine- like kernel function relating the stimulus and neural response spaces. We show that the non-Euclidean nature of the retinal distance has important consequences for neural decoding.
AU - Tkacik, Gasper
AU - Granot Atedgi, Einat
AU - Segev, Ronen
AU - Schneidman, Elad
ID - 2913
IS - 5
JF - Physical Review Letters
TI - Retinal metric: a stimulus distance measure derived from population neural responses
VL - 110
ER -
TY - JOUR
AB - The scale invariance of natural images suggests an analogy to the statistical mechanics of physical systems at a critical point. Here we examine the distribution of pixels in small image patches and show how to construct the corresponding thermodynamics. We find evidence for criticality in a diverging specific heat, which corresponds to large fluctuations in how "surprising" we find individual images, and in the quantitative form of the entropy vs energy. We identify special image configurations as local energy minima and show that average patches within each basin are interpretable as lines and edges in all orientations.
AU - Stephens, Greg
AU - Mora, Thierry
AU - Tkacik, Gasper
AU - Bialek, William
ID - 2914
IS - 1
JF - Physical Review Letters
TI - Statistical thermodynamics of natural images
VL - 110
ER -
TY - JOUR
AB - Oriented mitosis is essential during tissue morphogenesis. The Wnt/planar cell polarity (Wnt/PCP) pathway orients mitosis in a number of developmental systems, including dorsal epiblast cell divisions along the animal-vegetal (A-V) axis during zebrafish gastrulation. How Wnt signalling orients the mitotic plane is, however, unknown. Here we show that, in dorsal epiblast cells, anthrax toxin receptor 2a (Antxr2a) accumulates in a polarized cortical cap, which is aligned with the embryonic A-V axis and forecasts the division plane. Filamentous actin (F-actin) also forms an A-V polarized cap, which depends on Wnt/PCP and its effectors RhoA and Rock2. Antxr2a is recruited to the cap by interacting with actin. Antxr2a also interacts with RhoA and together they activate the diaphanous-related formin zDia2. Mechanistically, Antxr2a functions as a Wnt-dependent polarized determinant, which, through the action of RhoA and zDia2, exerts torque on the spindle to align it with the A-V axis.
AU - Castanon, Irinka
AU - Abrami, Laurence
AU - Holtzer, Laurent
AU - Heisenberg, Carl-Philipp J
AU - Van Der Goot, Françoise
AU - González Gaitán, Marcos
ID - 2918
IS - 1
JF - Nature Cell Biology
TI - Anthrax toxin receptor 2a controls mitotic spindle positioning
VL - 15
ER -
TY - JOUR
AB - The distribution of the phytohormone auxin regulates many aspects of plant development including growth response to gravity. Gravitropic root curvature involves coordinated and asymmetric cell elongation between the lower and upper side of the root, mediated by differential cellular auxin levels. The asymmetry in the auxin distribution is established and maintained by a spatio-temporal regulation of the PIN-FORMED (PIN) auxin transporter activity. We provide novel insights into the complex regulation of PIN abundance and activity during root gravitropism. We show that PIN2 turnover is differentially regulated on the upper and lower side of gravistimulated roots by distinct but partially overlapping auxin feedback mechanisms. In addition to regulating transcription and clathrin-mediated internalization, auxin also controls PIN abundance at the plasma membrane by promoting their vacuolar targeting and degradation. This effect of elevated auxin levels requires the activity of SKP-Cullin-F-box TIR1/AFB (SCF TIR1/AFB)-dependent pathway. Importantly, also suboptimal auxin levels mediate PIN degradation utilizing the same signalling pathway. These feedback mechanisms are functionally important during gravitropic response and ensure fine-tuning of auxin fluxes for maintaining as well as terminating asymmetric growth.
AU - Baster, Pawel
AU - Robert, Stéphanie
AU - Kleine Vehn, Jürgen
AU - Vanneste, Steffen
AU - Kania, Urszula
AU - Grunewald, Wim
AU - De Rybel, Bert
AU - Beeckman, Tom
AU - Friml, Jirí
ID - 2919
IS - 2
JF - EMBO Journal
TI - SCF^TIR1 AFB-auxin signalling regulates PIN vacuolar trafficking and auxin fluxes during root gravitropism
VL - 32
ER -
TY - JOUR
AB - Cell polarisation in development is a common and fundamental process underlying embryo patterning and morphogenesis, and has been extensively studied over the past years. Our current knowledge of cell polarisation in development is predominantly based on studies that have analysed polarisation of single cells, such as eggs, or cellular aggregates with a stable polarising interface, such as cultured epithelial cells (St Johnston and Ahringer, 2010). However, in embryonic development, particularly of vertebrates, cell polarisation processes often encompass large numbers of cells that are placed within moving and proliferating tissues, and undergo mesenchymal-to-epithelial transitions with a highly complex spatiotemporal choreography. How such intricate cell polarisation processes in embryonic development are achieved has only started to be analysed. By using live imaging of neurulation in the transparent zebrafish embryo, Buckley et al (2012) now describe a novel polarisation strategy by which cells assemble an apical domain in the part of their cell body that intersects with the midline of the forming neural rod. This mechanism, along with the previously described mirror-symmetric divisions (Tawk et al, 2007), is thought to trigger formation of both neural rod midline and lumen.
AU - Compagnon, Julien
AU - Heisenberg, Carl-Philipp J
ID - 2920
IS - 1
JF - EMBO Journal
TI - Neurulation coordinating cell polarisation and lumen formation
VL - 32
ER -
TY - JOUR
AB - To fight infectious diseases, host immune defenses are employed at multiple levels. Sanitary behavior, such as pathogen avoidance and removal, acts as a first line of defense to prevent infection [1] before activation of the physiological immune system. Insect societies have evolved a wide range of collective hygiene measures and intensive health care toward pathogen-exposed group members [2]. One of the most common behaviors is allogrooming, in which nestmates remove infectious particles from the body surfaces of exposed individuals [3]. Here we show that, in invasive garden ants, grooming of fungus-exposed brood is effective beyond the sheer mechanical removal of fungal conidiospores; it also includes chemical disinfection through the application of poison produced by the ants themselves. Formic acid is the main active component of the poison. It inhibits fungal growth of conidiospores remaining on the brood surface after grooming and also those collected in the mouth of the grooming ant. This dual function is achieved by uptake of the poison droplet into the mouth through acidopore self-grooming and subsequent application onto the infectious brood via brood grooming. This extraordinary behavior extends the current understanding of grooming and the establishment of social immunity in insect societies.
AU - Tragust, Simon
AU - Mitteregger, Barbara
AU - Barone, Vanessa
AU - Konrad, Matthias
AU - Ugelvig, Line V
AU - Cremer, Sylvia
ID - 2926
IS - 1
JF - Current Biology
TI - Ants disinfect fungus-exposed brood by oral uptake and spread of their poison
VL - 23
ER -
TY - JOUR
AB - In this paper, we present the first output-sensitive algorithm to compute the persistence diagram of a filtered simplicial complex. For any Γ > 0, it returns only those homology classes with persistence at least Γ. Instead of the classical reduction via column operations, our algorithm performs rank computations on submatrices of the boundary matrix. For an arbitrary constant δ ∈ (0, 1), the running time is O (C (1 - δ) Γ R d (n) log n), where C (1 - δ) Γ is the number of homology classes with persistence at least (1 - δ) Γ, n is the total number of simplices in the complex, d its dimension, and R d (n) is the complexity of computing the rank of an n × n matrix with O (d n) nonzero entries. Depending on the choice of the rank algorithm, this yields a deterministic O (C (1 - δ) Γ n 2.376) algorithm, an O (C (1 - δ) Γ n 2.28) Las-Vegas algorithm, or an O (C (1 - δ) Γ n 2 + ε{lunate}) Monte-Carlo algorithm for an arbitrary ε{lunate} > 0. The space complexity of the Monte-Carlo version is bounded by O (d n) = O (n log n).
AU - Chen, Chao
AU - Kerber, Michael
ID - 2939
IS - 4
JF - Computational Geometry: Theory and Applications
TI - An output sensitive algorithm for persistent homology
VL - 46
ER -
TY - CONF
AB - A chain rule for an entropy notion H(.) states that the entropy H(X) of a variable X decreases by at most l if conditioned on an l-bit string A, i.e., H(X|A)>= H(X)-l. More generally, it satisfies a chain rule for conditional entropy if H(X|Y,A)>= H(X|Y)-l.
All natural information theoretic entropy notions we are aware of (like Shannon or min-entropy) satisfy some kind of chain rule for conditional entropy. Moreover, many computational entropy notions (like Yao entropy, unpredictability entropy and several variants of HILL entropy) satisfy the chain rule for conditional entropy, though here not only the quantity decreases by l, but also the quality of the entropy decreases exponentially in l. However, for
the standard notion of conditional HILL entropy (the computational equivalent of min-entropy) the existence of such a rule was unknown so far.
In this paper, we prove that for conditional HILL entropy no meaningful chain rule exists, assuming the existence of one-way permutations: there exist distributions X,Y,A, where A is a distribution over a single bit, but $H(X|Y)>>H(X|Y,A)$, even if we simultaneously allow for a massive degradation in the quality of the entropy.
The idea underlying our construction is based on a surprising connection between the chain rule for HILL entropy and deniable encryption.
AU - Krenn, Stephan
AU - Pietrzak, Krzysztof Z
AU - Wadia, Akshay
ED - Sahai, Amit
ID - 2940
TI - A counterexample to the chain rule for conditional HILL entropy, and what deniable encryption has to do with it
VL - 7785
ER -
TY - JOUR
AB - We propose a two-step procedure for estimating multiple migration rates in an approximate Bayesian computation (ABC) framework, accounting for global nuisance parameters. The approach is not limited to migration, but generally of interest for inference problems with multiple parameters and a modular structure (e.g. independent sets of demes or loci). We condition on a known, but complex demographic model of a spatially subdivided population, motivated by the reintroduction of Alpine ibex (Capra ibex) into Switzerland. In the first step, the global parameters ancestral mutation rate and male mating skew have been estimated for the whole population in Aeschbacher et al. (Genetics 2012; 192: 1027). In the second step, we estimate in this study the migration rates independently for clusters of demes putatively connected by migration. For large clusters (many migration rates), ABC faces the problem of too many summary statistics. We therefore assess by simulation if estimation per pair of demes is a valid alternative. We find that the trade-off between reduced dimensionality for the pairwise estimation on the one hand and lower accuracy due to the assumption of pairwise independence on the other depends on the number of migration rates to be inferred: the accuracy of the pairwise approach increases with the number of parameters, relative to the joint estimation approach. To distinguish between low and zero migration, we perform ABC-type model comparison between a model with migration and one without. Applying the approach to microsatellite data from Alpine ibex, we find no evidence for substantial gene flow via migration, except for one pair of demes in one direction.
AU - Aeschbacher, Simon
AU - Futschik, Andreas
AU - Beaumont, Mark
ID - 2944
IS - 4
JF - Molecular Ecology
TI - Approximate Bayesian computation for modular inference problems with many parameters: the example of migration rates.
VL - 22
ER -
TY - CONF
AB - Many visual datasets are traditionally used to analyze the performance of different learning techniques. The evaluation is usually done within each dataset, therefore it is questionable if such results are a reliable indicator of true generalization ability. We propose here an algorithm to exploit the existing data resources when learning on a new multiclass problem. Our main idea is to identify an image representation that decomposes orthogonally into two subspaces: a part specific to each dataset, and a part generic to, and therefore shared between, all the considered source sets. This allows us to use the generic representation as un-biased reference knowledge for a novel classification task. By casting the method in the multi-view setting, we also make it possible to use different features for different databases. We call the algorithm MUST, Multitask Unaligned Shared knowledge Transfer. Through extensive experiments on five public datasets, we show that MUST consistently improves the cross-datasets generalization performance.
AU - Tommasi, Tatiana
AU - Quadrianto, Novi
AU - Caputo, Barbara
AU - Lampert, Christoph
ID - 2948
TI - Beyond dataset bias: Multi-task unaligned shared knowledge transfer
VL - 7724
ER -
TY - JOUR
AB - Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads. © 2012 Springer Science+Business Media, LLC.
AU - Chatterjee, Krishnendu
AU - De Alfaro, Luca
AU - Faella, Marco
AU - Majumdar, Ritankar
AU - Raman, Vishwanath
ID - 3116
IS - 2
JF - Formal Methods in System Design
TI - Code aware resource management
VL - 42
ER -
TY - GEN
AB - 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.
AU - Henzinger, Thomas A
AU - Payer, Hannes
AU - Sezgin, Ali
ID - 6440
SN - 2664-1690
TI - Replacing competition with cooperation to achieve scalable lock-free FIFO queues
ER -
TY - JOUR
AB - As sessile organisms, plants have to be able to adapt to a continuously changing environment. Plants that perceive some of these changes as stress signals activate signaling pathways to modulate their development and to enable them to survive. The complex responses to environmental cues are to a large extent mediated by plant hormones that together orchestrate the final plant response. The phytohormone cytokinin is involved in many plant developmental processes. Recently, it has been established that cytokinin plays an important role in stress responses, but does not act alone. Indeed, the hormonal control of plant development and stress adaptation is the outcome of a complex network of multiple synergistic and antagonistic interactions between various hormones. Here, we review the recent findings on the cytokinin function as part of this hormonal network. We focus on the importance of the crosstalk between cytokinin and other hormones, such as abscisic acid, jasmonate, salicylic acid, ethylene, and auxin in the modulation of plant development and stress adaptation. Finally, the impact of the current research in the biotechnological industry will be discussed.
AU - O'Brien, José
AU - Benková, Eva
ID - 827
JF - Frontiers in Plant Science
TI - Cytokinin cross talking during biotic and abiotic stress responses
VL - 4
ER -
TY - JOUR
AB - The plant root system is essential for providing anchorage to the soil, supplying minerals and water, and synthesizing metabolites. It is a dynamic organ modulated by external cues such as environmental signals, water and nutrients availability, salinity and others. Lateral roots (LRs) are initiated from the primary root post-embryonically, after which they progress through discrete developmental stages which can be independently controlled, providing a high level of plasticity during root system formation. Within this review, main contributions are presented, from the classical forward genetic screens to the more recent high-throughput approaches, combined with computer model predictions, dissecting how LRs and thereby root system architecture is established and developed.
AU - Cuesta, Candela
AU - Wabnik, Krzysztof T
AU - Benková, Eva
ID - 828
JF - Frontiers in Plant Science
TI - Systems approaches to study root architecture dynamics
VL - 4
ER -
TY - CONF
AB - We study two-player zero-sum games over infinite-state graphs equipped with ωB and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with ωB-conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.
AU - Chatterjee, Krishnendu
AU - Fijalkow, Nathanaël
ID - 1374
T2 - 22nd EACSL Annual Conference on Computer Science Logic
TI - Infinite-state games with finitary conditions
VL - 23
ER -
TY - CONF
AB - We consider the distributed synthesis problem for temporal logic specifications. Traditionally, the problem has been studied for LTL, and the previous results show that the problem is decidable iff there is no information fork in the architecture. We consider the problem for fragments of LTL and our main results are as follows: (1) We show that the problem is undecidable for architectures with information forks even for the fragment of LTL with temporal operators restricted to next and eventually. (2) For specifications restricted to globally along with non-nested next operators, we establish decidability (in EXPSPACE) for star architectures where the processes receive disjoint inputs, whereas we establish undecidability for architectures containing an information fork-meet structure. (3) Finally, we consider LTL without the next operator, and establish decidability (NEXPTIME-complete) for all architectures for a fragment that consists of a set of safety assumptions, and a set of guarantees where each guarantee is a safety, reachability, or liveness condition.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
AU - Pavlogiannis, Andreas
ID - 1376
T2 - 13th International Conference on Formal Methods in Computer-Aided Design
TI - Distributed synthesis for LTL fragments
ER -
TY - CONF
AB - It is often difficult to correctly implement a Boolean controller for a complex system, especially when concurrency is involved. Yet, it may be easy to formally specify a controller. For instance, for a pipelined processor it suffices to state that the visible behavior of the pipelined system should be identical to a non-pipelined reference system (Burch-Dill paradigm). We present a novel procedure to efficiently synthesize multiple Boolean control signals from a specification given as a quantified first-order formula (with a specific quantifier structure). Our approach uses uninterpreted functions to abstract details of the design. We construct an unsatisfiable SMT formula from the given specification. Then, from just one proof of unsatisfiability, we use a variant of Craig interpolation to compute multiple coordinated interpolants that implement the Boolean control signals. Our method avoids iterative learning and back-substitution of the control functions. We applied our approach to synthesize a controller for a simple two-stage pipelined processor, and present first experimental results.
AU - Hofferek, Georg
AU - Gupta, Ashutosh
AU - Könighofer, Bettina
AU - Jiang, Jie
AU - Bloem, Roderick
ID - 1385
T2 - 2013 Formal Methods in Computer-Aided Design
TI - Synthesizing multiple boolean functions using interpolation on a single proof
ER -
TY - CONF
AB - Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.
AU - Boker, Udi
AU - Kuperberg, Denis
AU - Kupferman, Orna
AU - Skrzypczak, Michał
ID - 1387
IS - PART 2
TI - Nondeterminism in the presence of a diverse or unknown future
VL - 7966
ER -
TY - THES
AB - Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. we present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the π-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more flexibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency.
First, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems. Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the PICASSO tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point.
AU - Zufferey, Damien
ID - 1405
TI - Analysis of dynamic message passing programs
ER -
TY - THES
AB - Epithelial spreading is a critical part of various developmental and wound repair processes. Here we use zebrafish epiboly as a model system to study the cellular and molecular mechanisms underlying the spreading of epithelial sheets. During zebrafish epiboly the enveloping cell layer (EVL), a simple squamous epithelium, spreads over the embryo to eventually cover the entire yolk cell by the end of gastrulation. The EVL leading edge is anchored through tight junctions to the yolk syncytial layer (YSL), where directly adjacent to the EVL margin a contractile actomyosin ring is formed that is thought to drive EVL epiboly. The prevalent view in the field was that the contractile ring exerts a pulling force on the EVL margin, which pulls the EVL towards the vegetal pole. However, how this force is generated and how it affects EVL morphology still remains elusive. Moreover, the cellular mechanisms mediating the increase in EVL surface area, while maintaining tissue integrity and function are still unclear. Here we show that the YSL actomyosin ring pulls on the EVL margin by two distinct force-generating mechanisms. One mechanism is based on contraction of the ring around its circumference, as previously proposed. The second mechanism is based on actomyosin retrogade flows, generating force through resistance against the substrate. The latter can function at any epiboly stage even in situations where the contraction-based mechanism is unproductive. Additionally, we demonstrate that during epiboly the EVL is subjected to anisotropic tension, which guides the orientation of EVL cell division along the main axis (animal-vegetal) of tension. The influence of tension in cell division orientation involves cell elongation and requires myosin-2 activity for proper spindle alignment. Strikingly, we reveal that tension-oriented cell divisions release anisotropic tension within the EVL and that in the absence of such divisions, EVL cells undergo ectopic fusions. We conclude that forces applied to the EVL by the action of the YSL actomyosin ring generate a tension anisotropy in the EVL that orients cell divisions, which in turn limit tissue tension increase thereby facilitating tissue spreading.
AU - Campinho, Pedro
ID - 1406
TI - Mechanics of zebrafish epiboly: Tension-oriented cell divisions limit anisotropic tissue tension in epithelial spreading
ER -
TY - JOUR
AB - Cells in a developing embryo have no direct way of "measuring" their physical position. Through a variety of processes, however, the expression levels of multiple genes come to be correlated with position, and these expression levels thus form a code for "positional information." We show how to measure this information, in bits, using the gap genes in the Drosophila embryo as an example. Individual genes carry nearly two bits of information, twice as much as expected if the expression patterns consisted only of on/off domains separated by sharp boundaries. Taken together, four gap genes carry enough information to define a cell's location with an error bar of ~1% along the anterior-posterior axis of the embryo. This precision is nearly enough for each cell to have a unique identity, which is the maximum information the system can use, and is nearly constant along the length of the embryo. We argue that this constancy is a signature of optimality in the transmission of information from primary morphogen inputs to the output of the gap gene network.
AU - Dubuis, Julien
AU - Tkacik, Gasper
AU - Wieschaus, Eric
AU - Gregor, Thomas
AU - Bialek, William
ID - 3261
IS - 41
JF - PNAS
TI - Positional information, in bits
VL - 110
ER -
TY - GEN
AU - Quadrianto, Novi
AU - Lampert, Christoph
ED - Dubitzky, Werner
ED - Wolkenhauer, Olaf
ED - Cho, Kwang
ED - Yokota, Hiroki
ID - 3321
T2 - Encyclopedia of Systems Biology
TI - Kernel based learning
VL - 3
ER -
TY - CONF
AB - Leakage resilient cryptography attempts to incorporate side-channel leakage into the black-box security model and designs cryptographic schemes that are provably secure within it. Informally, a scheme is leakage-resilient if it remains secure even if an adversary learns a bounded amount of arbitrary information about the schemes internal state. Unfortunately, most leakage resilient schemes are unnecessarily complicated in order to achieve strong provable security guarantees. As advocated by Yu et al. [CCS’10], this mostly is an artefact of the security proof and in practice much simpler construction may already suffice to protect against realistic side-channel attacks. In this paper, we show that indeed for simpler constructions leakage-resilience can be obtained when we aim for relaxed security notions where the leakage-functions and/or the inputs to the primitive are chosen non-adaptively. For example, we show that a three round Feistel network instantiated with a leakage resilient PRF yields a leakage resilient PRP if the inputs are chosen non-adaptively (This complements the result of Dodis and Pietrzak [CRYPTO’10] who show that if a adaptive queries are allowed, a superlogarithmic number of rounds is necessary.) We also show that a minor variation of the classical GGM construction gives a leakage resilient PRF if both, the leakage-function and the inputs, are chosen non-adaptively.
AU - Faust, Sebastian
AU - Pietrzak, Krzysztof Z
AU - Schipper, Joachim
ID - 2048
T2 - Conference proceedings CHES 2012
TI - Practical leakage-resilient symmetric cryptography
VL - 7428
ER -
TY - CONF
AB - We propose a new authentication protocol that is provably secure based on a ring variant of the learning parity with noise (LPN) problem. The protocol follows the design principle of the LPN-based protocol from Eurocrypt’11 (Kiltz et al.), and like it, is a two round protocol secure against active attacks. Moreover, our protocol has small communication complexity and a very small footprint which makes it applicable in scenarios that involve low-cost, resource-constrained devices.
Performance-wise, our protocol is more efficient than previous LPN-based schemes, such as the many variants of the Hopper-Blum (HB) protocol and the aforementioned protocol from Eurocrypt’11. Our implementation results show that it is even comparable to the standard challenge-and-response protocols based on the AES block-cipher. Our basic protocol is roughly 20 times slower than AES, but with the advantage of having 10 times smaller code size. Furthermore, if a few hundred bytes of non-volatile memory are available to allow the storage of some off-line pre-computations, then the online phase of our protocols is only twice as slow as AES.
AU - Heyse, Stefan
AU - Kiltz, Eike
AU - Lyubashevsky, Vadim
AU - Paar, Christof
AU - Pietrzak, Krzysztof Z
ID - 2049
T2 - Conference proceedings FSE 2012
TI - Lapin: An efficient authentication protocol based on ring-LPN
VL - 7549
ER -
TY - JOUR
AB - Nestin-cre transgenic mice have been widely used to direct recombination to neural stem cells (NSCs) and intermediate neural progenitor cells (NPCs). Here we report that a readily utilized, and the only commercially available, Nestin-cre line is insufficient for directing recombination in early embryonic NSCs and NPCs. Analysis of recombination efficiency in multiple cre-dependent reporters and a genetic mosaic line revealed consistent temporal and spatial patterns of recombination in NSCs and NPCs. For comparison we utilized a knock-in Emx1cre line and found robust recombination in NSCs and NPCs in ventricular and subventricular zones of the cerebral cortices as early as embryonic day 12.5. In addition we found that the rate of Nestin-cre driven recombination only reaches sufficiently high levels in NSCs and NPCs during late embryonic and early postnatal periods. These findings are important when commercially available cre lines are considered for directing recombination to embryonic NSCs and NPCs.
AU - Liang, Huixuan
AU - Hippenmeyer, Simon
AU - Ghashghaei, H.
ID - 2263
IS - 12
JF - Biology open
TI - A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic neural progenitors
VL - 1
ER -
TY - JOUR
AB - We introduce propagation models (PMs), a formalism able to express several kinds of equations that describe the behavior of biochemical reaction networks. Furthermore, we introduce the propagation abstract data type (PADT), which separates concerns regarding different numerical algorithms for the transient analysis of biochemical reaction networks from concerns regarding their implementation, thus allowing for portable and efficient solutions. The state of a propagation abstract data type is given by a vector that assigns mass values to a set of nodes, and its (next) operator propagates mass values through this set of nodes. We propose an approximate implementation of the (next) operator, based on threshold abstraction, which propagates only "significant" mass values and thus achieves a compromise between efficiency and accuracy. Finally, we give three use cases for propagation models: the chemical master equation (CME), the reaction rate equation (RRE), and a hybrid method that combines these two equations. These three applications use propagation models in order to propagate probabilities and/or expected values and variances of the model's variables.
AU - Henzinger, Thomas A
AU - Mateescu, Maria
ID - 2302
IS - 2
JF - IEEE ACM Transactions on Computational Biology and Bioinformatics
TI - The propagation approach for computing biochemical reaction networks
VL - 10
ER -
TY - JOUR
AB - We show that bosons interacting via pair potentials with negative scattering length form bound states for a suitable number of particles. In other words, the absence of many-particle bound states of any kind implies the non-negativity of the scattering length of the interaction potential.
AU - Seiringer, Robert
ID - 2318
IS - 3
JF - Journal of Spectral Theory
TI - Absence of bound states implies non-negativity of the scattering length
VL - 2
ER -
TY - JOUR
AB - The kingdom of fungi provides model organisms for biotechnology, cell biology, genetics, and life sciences in general. Only when their phylogenetic relationships are stably resolved, can individual results from fungal research be integrated into a holistic picture of biology. However, and despite recent progress, many deep relationships within the fungi remain unclear. Here, we present the first phylogenomic study of an entire eukaryotic kingdom that uses a consistency criterion to strengthen phylogenetic conclusions. We reason that branches (splits) recovered with independent data and different tree reconstruction methods are likely to reflect true evolutionary relationships. Two complementary phylogenomic data sets based on 99 fungal genomes and 109 fungal expressed sequence tag (EST) sets analyzed with four different tree reconstruction methods shed light from different angles on the fungal tree of life. Eleven additional data sets address specifically the phylogenetic position of Blastocladiomycota, Ustilaginomycotina, and Dothideomycetes, respectively. The combined evidence from the resulting trees supports the deep-level stability of the fungal groups toward a comprehensive natural system of the fungi. In addition, our analysis reveals methodologically interesting aspects. Enrichment for EST encoded data-a common practice in phylogenomic analyses-introduces a strong bias toward slowly evolving and functionally correlated genes. Consequently, the generalization of phylogenomic data sets as collections of randomly selected genes cannot be taken for granted. A thorough characterization of the data to assess possible influences on the tree reconstruction should therefore become a standard in phylogenomic analyses.
AU - Ebersberger, Ingo
AU - De Matos Simoes, Ricardo
AU - Kupczok, Anne
AU - Gube, Matthias
AU - Kothe, Erika
AU - Voigt, Kerstin
AU - Von Haeseler, Arndt
ID - 2411
IS - 5
JF - Molecular Biology and Evolution
TI - A consistent phylogenetic backbone for the fungi
VL - 29
ER -
TY - JOUR
AB - The BCI competition IV stands in the tradition of prior BCI competitions that aim to provide high quality neuroscientific data for open access to the scientific community. As experienced already in prior competitions not only scientists from the narrow field of BCI compete, but scholars with a broad variety of backgrounds and nationalities. They include high specialists as well as students.The goals of all BCI competitions have always been to challenge with respect to novel paradigms and complex data. We report on the following challenges: (1) asynchronous data, (2) synthetic, (3) multi-class continuous data, (4) sessionto-session transfer, (5) directionally modulated MEG, (6) finger movements recorded by ECoG. As after past competitions, our hope is that winning entries may enhance the analysis methods of future BCIs.
AU - Tangermann, Michael
AU - Müller, Klaus
AU - Aertsen, Ad
AU - Birbaumer, Niels
AU - Braun, Christoph
AU - Brunner, Clemens
AU - Leeb, Robert
AU - Mehring, Carsten
AU - Miller, Kai
AU - Müller Putz, Gernot
AU - Nolte, Guido
AU - Pfurtscheller, Gert
AU - Preissl, Hubert
AU - Schalk, Gerwin
AU - Schlögl, Alois
AU - Vidaurre, Carmen
AU - Waldert, Stephan
AU - Blankertz, Benjamin
ID - 493
JF - Frontiers in Neuroscience
TI - Review of the BCI competition IV
VL - 6
ER -
TY - JOUR
AB - We solve the longstanding open problems of the blow-up involved in the translations, when possible, of a nondeterministic Büchi word automaton (NBW) to a nondeterministic co-Büchi word automaton (NCW) and to a deterministic co-Büchi word automaton (DCW). For the NBW to NCW translation, the currently known upper bound is 2o(nlog n) and the lower bound is 1.5n. We improve the upper bound to n2n and describe a matching lower bound of 2ω(n). For the NBW to DCW translation, the currently known upper bound is 2o(nlog n). We improve it to 2 o(n), which is asymptotically tight. Both of our upper-bound constructions are based on a simple subset construction, do not involve intermediate automata with richer acceptance conditions, and can be implemented symbolically. We continue and solve the open problems of translating nondeterministic Streett, Rabin, Muller, and parity word automata to NCW and to DCW. Going via an intermediate NBW is not optimal and we describe direct, simple, and asymptotically tight constructions, involving a 2o(n) blow-up. The constructions are variants of the subset construction, providing a unified approach for translating all common classes of automata to NCW and DCW. Beyond the theoretical importance of the results, we point to numerous applications of the new constructions. In particular, they imply a simple subset-construction based translation, when possible, of LTL to deterministic Büchi word automata.
AU - Boker, Udi
AU - Kupferman, Orna
ID - 494
IS - 4
JF - ACM Transactions on Computational Logic (TOCL)
TI - Translating to Co-Büchi made tight, unified, and useful
VL - 13
ER -
TY - CONF
AB - An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice.
AU - Kruckman, Alex
AU - Rubin, Sasha
AU - Sheridan, John
AU - Zax, Ben
ID - 495
T2 - Proceedings GandALF 2012
TI - A Myhill Nerode theorem for automata with advice
VL - 96
ER -
TY - CONF
AB - We study the expressive power of logical interpretations on the class of scattered trees, namely those with countably many infinite branches. Scattered trees can be thought of as the tree analogue of scattered linear orders. Every scattered tree has an ordinal rank that reflects the structure of its infinite branches. We prove, roughly, that trees and orders of large rank cannot be interpreted in scattered trees of small rank. We consider a quite general notion of interpretation: each element of the interpreted structure is represented by a set of tuples of subsets of the interpreting tree. Our trees are countable, not necessarily finitely branching, and may have finitely many unary predicates as labellings. We also show how to replace injective set-interpretations in (not necessarily scattered) trees by 'finitary' set-interpretations.
AU - Rabinovich, Alexander
AU - Rubin, Sasha
ID - 496
TI - Interpretations in trees with countably many branches
ER -
TY - CONF
AB - One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n 3·m) time as compared to the previous known O(n 6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n·m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm. © Krishnendu Chatterjee, Siddhesh Chaubal, and Pritish Kamath.
AU - Chatterjee, Krishnendu
AU - Chaubal, Siddhesh
AU - Kamath, Pritish
ID - 497
TI - Faster algorithms for alternating refinement relations
VL - 16
ER -
TY - JOUR
AB - Understanding patterns and correlates of local adaptation in heterogeneous landscapes can provide important information in the selection of appropriate seed sources for restoration. We assessed the extent of local adaptation of fitness components in 12 population pairs of the perennial herb Rutidosis leptorrhynchoides (Asteraceae) and examined whether spatial scale (0.7-600 km), environmental distance, quantitative (QST) and neutral (FST) genetic differentiation, and size of the local and foreign populations could predict patterns of adaptive differentiation. Local adaptation varied among populations and fitness components. Including all population pairs, local adaptation was observed for seedling survival, but not for biomass, while foreign genotype advantage was observed for reproduction (number of inflorescences). Among population pairs, local adaptation increased with QST and local population size for biomass. QST was associated with environmental distance, suggesting ecological selection for phenotypic divergence. However, low FST and variation in population structure in small populations demonstrates the interaction of gene flow and drift in constraining local adaptation in R. leptorrhynchoides. Our study indicates that for species in heterogeneous landscapes, collecting seed from large populations from similar environments to candidate sites is likely to provide the most appropriate seed sources for restoration.
AU - Pickup, Melinda
AU - Field, David
AU - Rowell, David
AU - Young, Andrew
ID - 498
IS - 8
JF - Evolutionary Applications
TI - Predicting local adaptation in fragmented plant populations: Implications for restoration genetics
VL - 5
ER -
TY - JOUR
AU - Sixt, Michael K
ID - 506
IS - 3
JF - Journal of Cell Biology
TI - Cell migration: Fibroblasts find a new way to get ahead
VL - 197
ER -
TY - GEN
AB - Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work we consider solving recursive game graphs (or pushdown game graphs) that can model the control flow of sequential programs with recursion. While pushdown games have been studied before with qualitative objectives, such as reachability and ω-regular objectives, in this work we study for the first time such games with the most well-studied quantitative objective, namely, mean-payoff objectives. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation, but only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two- player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP- hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games; and memoryless modular strategies are sufficient in two- player pushdown games. Finally we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.
AU - Chatterjee, Krishnendu
AU - Velner, Yaron
ID - 5377
SN - 2664-1690
TI - Mean-payoff pushdown games
ER -
TY - GEN
AB - One central issue in the formal design and analysis of reactive systems is the notion of refinement that asks whether all behaviors of the implementation is allowed by the specification. The local interpretation of behavior leads to the notion of simulation. Alternating transition systems (ATSs) provide a general model for composite reactive systems, and the simulation relation for ATSs is known as alternating simulation. The simulation relation for fair transition systems is called fair simulation. In this work our main contributions are as follows: (1) We present an improved algorithm for fair simulation with Büchi fairness constraints; our algorithm requires O(n3 · m) time as compared to the previous known O(n6)-time algorithm, where n is the number of states and m is the number of transitions. (2) We present a game based algorithm for alternating simulation that requires O(m2)-time as compared to the previous known O((n · m)2)-time algorithm, where n is the number of states and m is the size of transition relation. (3) We present an iterative algorithm for alternating simulation that matches the time complexity of the game based algorithm, but is more space efficient than the game based algorithm.
AU - Chatterjee, Krishnendu
AU - Chaubal, Siddhesh
AU - Kamath, Pritish
ID - 5378
SN - 2664-1690
TI - Faster algorithms for alternating refinement relations
ER -
TY - GEN
AB - We consider the problem of inference in agraphical model with binary variables. While in theory it is arguably preferable to compute marginal probabilities, in practice researchers often use MAP inference due to the availability of efficient discrete optimization algorithms. We bridge the gap between the two approaches by introducing the Discrete Marginals technique in which approximate marginals are obtained by minimizing an objective function with unary and pair-wise terms over a discretized domain. This allows the use of techniques originally devel-oped for MAP-MRF inference and learning. We explore two ways to set up the objective function - by discretizing the Bethe free energy and by learning it from training data. Experimental results show that for certain types of graphs a learned function can out-perform the Bethe approximation. We also establish a link between the Bethe free energy and submodular functions.
AU - Korc, Filip
AU - Kolmogorov, Vladimir
AU - Lampert, Christoph
ID - 5396
SN - 2664-1690
TI - Approximating marginals using discrete energy minimization
ER -
TY - GEN
AB - This document is created as a part of the project “Repository for Research Data on IST Austria”. It summarises the actual state of research data at IST Austria, based on survey results. It supports the choice of appropriate software, which would best fit the requirements of their users, the researchers.
AU - Porsche, Jana
ID - 5398
TI - Actual state of research data @ ISTAustria
ER -
TY - CHAP
AU - Gupta, Ashutosh
ID - 5745
SN - 0302-9743
T2 - Automated Technology for Verification and Analysis
TI - Improved Single Pass Algorithms for Resolution Proof Reduction
VL - 7561
ER -
TY - CONF
AB - We consider Markov decision processes (MDPs) with specifications given as Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning vertices from where the objective can be ensured with probability 1. We study for the first time the average case complexity of the classical algorithm for computing the set of almost-sure winning vertices for MDPs with Büchi objectives. Our contributions are as follows: First, we show that for MDPs with constant out-degree the expected number of iterations is at most logarithmic and the average case running time is linear (as compared to the worst case linear number of iterations and quadratic time complexity). Second, for the average case analysis over all MDPs we show that the expected number of iterations is constant and the average case running time is linear (again as compared to the worst case linear number of iterations and quadratic time complexity). Finally we also show that given that all MDPs are equally likely, the probability that the classical algorithm requires more than constant number of iterations is exponentially small.
AU - Chatterjee, Krishnendu
AU - Joglekar, Manas
AU - Shah, Nisarg
ID - 2715
TI - Average case analysis of the classical algorithm for Markov decision processes with Büchi objectives
VL - 18
ER -
TY - CONF
AB - We study the problem of maximum marginal prediction (MMP) in probabilistic graphical models, a task that occurs, for example, as the Bayes optimal decision rule under a Hamming loss. MMP is typically performed as a two-stage procedure: one estimates each variable's marginal probability and then forms a prediction from the states of maximal probability. In this work we propose a simple yet effective technique for accelerating MMP when inference is sampling-based: instead of the above two-stage procedure we directly estimate the posterior probability of each decision variable. This allows us to identify the point of time when we are sufficiently certain about any individual decision. Whenever this is the case, we dynamically prune the variables we are confident about from the underlying factor graph. Consequently, at any time only samples of variables whose decision is still uncertain need to be created. Experiments in two prototypical scenarios, multi-label classification and image inpainting, show that adaptive sampling can drastically accelerate MMP without sacrificing prediction accuracy.
AU - Lampert, Christoph
ID - 2825
TI - Dynamic pruning of factor graphs for maximum marginal prediction
VL - 1
ER -
TY - JOUR
AB - We study evolutionary game theory in a setting where individuals learn from each other. We extend the traditional approach by assuming that a population contains individuals with different learning abilities. In particular, we explore the situation where individuals have different search spaces, when attempting to learn the strategies of others. The search space of an individual specifies the set of strategies learnable by that individual. The search space is genetically given and does not change under social evolutionary dynamics. We introduce a general framework and study a specific example in the context of direct reciprocity. For this example, we obtain the counter intuitive result that cooperation can only evolve for intermediate benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection. Our paper is a step toward making a connection between computational learning theory and evolutionary game dynamics.
AU - Chatterjee, Krishnendu
AU - Zufferey, Damien
AU - Nowak, Martin
ID - 2848
JF - Journal of Theoretical Biology
TI - Evolutionary game dynamics in populations with different learners
VL - 301
ER -
TY - JOUR
AU - Edelsbrunner, Herbert
AU - Strelkova, Nataliya
ID - 2849
IS - 6
JF - Russian Mathematical Surveys
TI - On the configuration space of Steiner minimal trees
VL - 67
ER -