TY - JOUR
AB - We perform precision measurements on a Mott-insulator quantum state of ultracold atoms with tunable interactions. We probe the dependence of the superfluid-to-Mott-insulator transition on the interaction strength and explore the limits of the standard Bose-Hubbard model description. By tuning the on-site interaction energies to values comparable to the interband separation, we are able to quantitatively measure number-dependent shifts in the excitation spectrum caused by effective multibody interactions.
AU - Mark, Manfred
AU - Haller, Elmar
AU - Lauber, Katharina
AU - Danzl, Johann G
AU - Daley, Andrew
AU - Nägerl, Hanns
ID - 1053
IS - 17
JF - Physical Review Letters
TI - Precision measurements on a tunable Mott insulator of ultracold atoms
VL - 107
ER -
TY - JOUR
AB - We investigate local three-body correlations for bosonic particles in three dimensions and one dimension as a function of the interaction strength. The three-body correlation function g(3) is determined by measuring the three-body recombination rate in an ultracold gas of Cs atoms. In three dimensions, we measure the dependence of g(3) on the gas parameter in a BEC, finding good agreement with the theoretical prediction accounting for beyond-mean-field effects. In one dimension, we observe a reduction of g( 3) by several orders of magnitude upon increasing interactions from the weakly interacting BEC to the strongly interacting Tonks-Girardeau regime, in good agreement with predictions from the Lieb-Liniger model for all strengths of interaction.
AU - Haller, Elmar
AU - Rabie, Mahmoud
AU - Mark, Manfred
AU - Danzl, Johann G
AU - Hart, Russell
AU - Lauber, Katharina
AU - Pupillo, Guido
AU - Nägerl, Hanns
ID - 1054
IS - 23
JF - Physical Review Letters
TI - Three-body correlation functions and recombination rates for bosons in three dimensions and one dimension
VL - 107
ER -
TY - JOUR
AB - Particle beams are important tools for probing atomic and molecular interactions. Here we demonstrate that particle beams also offer a unique opportunity to investigate interactions in macroscopic systems, such as granular media. Motivated by recent experiments on streams of grains that exhibit liquid-like breakup into droplets, we use molecular dynamics simulations to investigate the evolution of a dense stream of macroscopic spheres accelerating out of an opening at the bottom of a reservoir. We show how nanoscale details associated with energy dissipation during collisions modify the stream\'s macroscopic behavior. We find that inelastic collisions collimate the stream, while the presence of short-range attractive interactions drives structure formation. Parameterizing the collision dynamics by the coefficient of restitution (i.e., the ratio of relative velocities before and after impact) and the strength of the cohesive interaction, we map out a spectrum of behaviors that ranges from gaslike jets in which all grains drift apart to liquid-like streams that break into large droplets containing hundreds of grains. We also find a new, intermediate regime in which small aggregates form by capture from the gas phase, similar to what can be observed in molecular beams. Our results show that nearly all aspects of stream behavior are closely related to the velocity gradient associated with vertical free fall. Led by this observation, we propose a simple energy balance model to explain the droplet formation process. The qualitative as well as many quantitative features of the simulations and the model compare well with available experimental data and provide a first quantitative measure of the role of attractions in freely cooling granular streams.
AU - Waitukaitis, Scott R
AU - Grütjen, Helge
AU - Royer, John
AU - Jaeger, Heinrich
ID - 112
IS - 5
JF - Physical Review E
TI - Droplet and cluster formation in freely falling granular streams
VL - 83
ER -
TY - JOUR
AB - A cloud-resolving model is used to investigate the effect of warming on high percentiles of precipitation (precipitation extremes) in the idealized setting of radiative-convective equilibrium. While this idealized setting does not allow for several factors that influence precipitation in the tropics, it does allow for an evaluation of the response of precipitation extremes to warming in simulations with resolved rather than parameterized convection. The methodology developed should also be applicable to less idealized simulations.
Modeled precipitation extremes are found to increase in magnitude in response to an increase in sea surface temperature. A dry static energy budget is used to relate the changes in precipitation extremes to changes in atmospheric temperature, vertical velocity, and precipitation efficiency. To first order, the changes in precipitation extremes are captured by changes in the mean temperature structure of the atmosphere. Changes in vertical velocities play a secondary role and tend to weaken the strength of precipitation extremes, despite an intensification of updraft velocities in the upper troposphere. The influence of changes in condensate transports on precipitation extremes is quantified in terms of a precipitation efficiency; it does not change greatly with warming.
Tropical precipitation extremes have previously been found to increase at a greater fractional rate than the amount of atmospheric water vapor in observations of present-day variability and in some climate model simulations with parameterized convection. But the fractional increases in precipitation extremes in the cloud-resolving simulations are comparable in magnitude to those in surface water vapor concentrations (owing to a partial cancellation between dynamical and thermodynamical changes), and are substantially less than the fractional increases in column water vapor.
AU - MULLER, Caroline J
AU - O’Gorman, Paul A.
AU - Back, Larissa E.
ID - 9144
IS - 11
JF - Journal of Climate
KW - Atmospheric Science
SN - 0894-8755
TI - Intensification of precipitation extremes with warming in a cloud-resolving model
VL - 24
ER -
TY - JOUR
AB - The conserved role of Notch signaling in controlling intestinal cell fate specification and homeostasis has been extensively studied. Nevertheless, the precise identity of the cells in which Notch signaling is active and the role of different Notch receptor paralogues in the intestine remain ambiguous, due to the lack of reliable tools to investigate Notch expression and function in vivo. We generated a new series of transgenic mice that allowed us, by lineage analysis, to formally prove that Notch1 and Notch2 are specifically expressed in crypt stem cells. In addition, a novel Notch reporter mouse, Hes1-EmGFP SAT, demonstrated exclusive Notch activity in crypt stem cells and absorptive progenitors. This roster of knock-in and reporter mice represents a valuable resource to functionally explore the Notch pathway in vivo in virtually all tissues.
AU - Fré, Silvia
AU - Hannezo, Edouard B
AU - Šale, Sanja
AU - Huyghe, Mathilde
AU - Lafkas, Daniel
AU - Kissel, Holger
AU - Louvi, Angeliki
AU - Greve, Jeffrey
AU - Louvard, Daniel
AU - Artavanis Tsakonas, Spyros
ID - 923
IS - 10
JF - PLoS One
TI - Notch lineages and activity in intestinal stem cells determined by a new set of knock in mice
VL - 6
ER -
TY - JOUR
AB - Motivated by recent experiments on the material Ba3NiSb 2O9, we consider a spin-one quantum antiferromagnet on a triangular lattice with the Heisenberg bilinear and biquadratic exchange interactions and a single-ion anisotropy. Using a fermionic "triplon" representation for spins, we study the phase diagram within mean-field theory. In addition to a fully gapped spin-liquid ground state, we find a state where one gapless triplon mode with a Fermi surface coexists with d+id topological pairing of the other triplons. Despite the existence of a Fermi surface, this ground state has fully gapped bulk spin excitations. Such a state has linear in-temperature specific heat and constant in-plane spin susceptibility, with an unusually high Wilson ratio.
AU - Maksym Serbyn
AU - Senthil, Todadri S
AU - Lee, Patrick
ID - 967
IS - 18
JF - Physical Review B - Condensed Matter and Materials Physics
TI - Exotic S=1 spin-liquid state with fermionic excitations on the triangular lattice
VL - 84
ER -
TY - JOUR
AB - We investigate the isotope effect on the London penetration depth of a superconductor which measures n S/m*, the ratio of superfluid density to effective mass. We use a simplified model of electrons weakly coupled to a single phonon frequency ω E, but assume that the energy gap Δ does not have any isotope effect. Nevertheless, we find an isotope effect for n S/m* which is significant if Δ is sufficiently large that it becomes comparable to ω E, a regime of interest to high-T c cuprate superconductors and possibly other families of unconventional superconductors with relatively high T c. Our model is too simple to describe the cuprates and it gives the wrong sign of the isotope effect when compared with experiment, but it is a proof of principle that the isotope effect exists for n S/m* in materials where the pairing gap and T c are not of phonon origin and have no isotope effect.
AU - Maksym Serbyn
AU - Lee, Patrick
ID - 969
IS - 2
JF - Physical Review B - Condensed Matter and Materials Physics
TI - Isotope effect on the superfluid density in conventional and high-temperature superconductors
VL - 83
ER -
TY - JOUR
AU - Barton, Nicholas H
ID - 3778
IS - 2
JF - Heredity
TI - Estimating linkage disequilibria
VL - 106
ER -
TY - JOUR
AB - Advanced stages of Scyllarus phyllosoma larvae were collected by demersal trawling during fishery research surveys in the western Mediterranean Sea in 2003–2005. Nucleotide sequence analysis of the mitochondrial 16S rDNA gene allowed the final-stage phyllosoma of Scyllarus arctus to be identified among these larvae. Its morphology is described and illustrated. This constitutes the second complete description of a Scyllaridae phyllosoma with its specific identity being validated by molecular techniques (the first was S. pygmaeus). These results also solved a long lasting taxonomic anomaly of several species assigned to the ancient genus Phyllosoma Leach, 1814. Detailed examination indicated that the final-stage phyllosoma of S. arctus shows closer affinities with the American scyllarid Scyllarus depressus or with the Australian Scyllarus sp. b (sensu Phillips et al., 1981) than to its sympatric species S. pygmaeus.
AU - Palero, Ferran
AU - Guerao, Guillermo
AU - Clark, Paul
AU - Abello, Pere
ID - 3784
IS - 2
JF - Journal of the Marine Biological Association of the United Kingdom
TI - Scyllarus arctus (Crustacea: Decapoda: Scyllaridae) final stage phyllosoma identified by DNA analysis, with morphological description
VL - 91
ER -
TY - CHAP
AB - We address the problem of covering ℝ n with congruent balls, while minimizing the number of balls that contain an average point. Considering the 1-parameter family of lattices defined by stretching or compressing the integer grid in diagonal direction, we give a closed formula for the covering density that depends on the distortion parameter. We observe that our family contains the thinnest lattice coverings in dimensions 2 to 5. We also consider the problem of packing congruent balls in ℝ n , for which we give a closed formula for the packing density as well. Again we observe that our family contains optimal configurations, this time densest packings in dimensions 2 and 3.
AU - Edelsbrunner, Herbert
AU - Kerber, Michael
ED - Calude, Cristian
ED - Rozenberg, Grzegorz
ED - Salomaa, Arto
ID - 3796
T2 - Rainbow of Computer Science
TI - Covering and packing with spheres by diagonal distortion in R^n
VL - 6570
ER -
TY - JOUR
AB - We present a detailed study of the local density of states (LDOS) associated with the surface-state band near a step edge of the strong topological insulator Bi2Te3 and reveal a one-dimensional bound state that runs parallel to the step edge and is bound to it at some characteristic distance. This bound state is clearly observed in the bulk gap region, while it becomes entangled with the oscillations of the warped surface band at high energy, and with the valence-band states near the Dirac point. We obtain excellent fits to theoretical predictions [Alpichshev, 2011] that properly incorporate the three-dimensional nature of the problem to the surface state. Fitting the data at different energies, we can recalculate the LDOS originating from the Dirac band without the contribution of the bulk bands or incoherent tunneling effects.
AU - Alpichshev, Zhanybek
AU - Analytis, J G
AU - Chu, J H
AU - Fisher, I R
AU - Kapitulnik, A
ID - 386
IS - 4
JF - Physical Review B - Condensed Matter and Materials Physics
TI - STM imaging of a bound state along a step on the surface of the topological insulator Bi2Te3
VL - 84
ER -
TY - JOUR
AU - Sauer, Michael
AU - Friml, Jirí
ID - 3091
JF - Molecular Systems Biology
TI - Fleeting hormone cues get stabilized for plant organogenesis
VL - 7
ER -
TY - JOUR
AB - The phytohormone auxin is vital to plant growth and development. A unique property of auxin among all other plant hormones is its cell-to-cell polar transport that requires activity of polarly localized PIN-FORMED (PIN) auxin efflux transporters. Despite the substantial molecular insight into the cellular PIN polarization, the mechanistic understanding for developmentally and environmentally regulated PIN polarization is scarce. The long-standing belief that auxin modulates its own transport by means of a positive feedback mechanism has inspired both experimentalists and theoreticians for more than two decades. Recently, theoretical models for auxin-dependent patterning in plants include the feedback between auxin transport and the PIN protein localization. These computer models aid to assess the complexity of plant development by testing and predicting plausible scenarios for various developmental processes that occur in planta. Although the majority of these models rely on purely heuristic principles, the most recent mechanistic models tentatively integrate biologically testable components into known cellular processes that underlie the PIN polarity regulation. The existing and emerging computational approaches to describe PIN polarization are presented and discussed in the light of recent experimental data on the PIN polar targeting.
AU - Wabnik, Krzysztof T
AU - Govaerts, Willy
AU - Friml, Jirí
AU - Kleine Vehn, Jürgen
ID - 3092
IS - 8
JF - Molecular BioSystems
TI - Feedback models for polarized auxin transport: An emerging trend
VL - 7
ER -
TY - JOUR
AB - In multicellular organisms, morphogenesis relies on a strict coordination in time and space of cell proliferation and differentiation. In contrast to animals, plant development displays continuous organ formation and adaptive growth responses during their lifespan relying on a tight coordination of cell proliferation. How developmental signals interact with the plant cell-cycle machinery is largely unknown. Here, we characterize plant A2-type cyclins, a small gene family of mitotic cyclins, and show how they contribute to the fine-tuning of local proliferation during plant development. Moreover, the timely repression of CYCA2;3 expression in newly formed guard cells is shown to require the stomatal transcription factors FOUR LIPS/MYB124 and MYB88, providing a direct link between developmental programming and cell-cycle exit in plants. Thus, transcriptional downregulation of CYCA2s represents a critical mechanism to coordinate proliferation during plant development.
AU - Vanneste, Steffen
AU - Coppens, Frederik
AU - Lee, EunKyoung
AU - Donner, Tyler J
AU - Xie, Zidian
AU - Van Isterdael, Gert
AU - Dhondt, Stijn
AU - De Winter, Freya
AU - De Rybel, Bert
AU - Vuylsteke, Marnik
AU - De Veylder, Lieven
AU - Jirí Friml
AU - Inzé, Dirk
AU - Grotewold, Erich
AU - Scarpella, Enrico
AU - Sack, Fred
AU - Beemster, Gerrit T
AU - Beeckman, Tom
ID - 3100
IS - 16
JF - EMBO Journal
TI - Developmental regulation of CYCA2s contributes to tissue-specific proliferation in Arabidopsis
VL - 30
ER -
TY - JOUR
AB - Subcellular trafficking is required for a multitude of functions in eukaryotic cells. It involves regulation of cargo sorting, vesicle formation, trafficking and fusion processes at multiple levels. Adaptor protein (AP) complexes are key regulators of cargo sorting into vesicles in yeast and mammals but their existence and function in plants have not been demonstrated. Here we report the identification of the protein-affected trafficking 4 (pat4) mutant defective in the putative δ subunit of the AP-3 complex. pat4 and pat2, a mutant isolated from the same GFP imaging-based forward genetic screen that lacks a functional putative AP-3 β, as well as dominant negative AP-3 μ transgenic lines display undistinguishable phenotypes characterized by largely normal morphology and development, but strong intracellular accumulation of membrane proteins in aberrant vacuolar structures. All mutants are defective in morphology and function of lytic and protein storage vacuoles (PSVs) but show normal sorting of reserve proteins to PSVs. Immunoprecipitation experiments and genetic studies revealed tight functional and physical associations of putative AP-3 β and AP-3 δ subunits. Furthermore, both proteins are closely linked with putative AP-3 μ and σ subunits and several components of the clathrin and dynamin machineries. Taken together, these results demonstrate that AP complexes, similar to those in other eukaryotes, exist in plants, and that AP-3 plays a specific role in the regulation of biogenesis and function of vacuoles in plant cells. © 2011 IBCB, SIBS, CAS All rights reserved
AU - Zwiewka, Marta
AU - Feraru, Elena
AU - Möller, Barbara
AU - Hwang, Inhwan
AU - Feraru, Mugurel I
AU - Kleine-Vehn, Jürgen
AU - Weijers, Dolf
AU - Jirí Friml
ID - 3101
IS - 12
JF - Cell Research
TI - The AP 3 adaptor complex is required for vacuolar function in Arabidopsis
VL - 21
ER -
TY - JOUR
AB - The unintentional scattering of light between neighboring surfaces in complex projection environments increases the brightness and decreases the contrast, disrupting the appearance of the desired imagery. To achieve satisfactory projection results, the inverse problem of global illumination must be solved to cancel this secondary scattering. In this paper, we propose a global illumination cancellation method that minimizes the perceptual difference between the desired imagery and the actual total illumination in the resulting physical environment. Using Gauss-Newton and active set methods, we design a fast solver for the bound constrained nonlinear least squares problem raised by the perceptual error metrics. Our solver is further accelerated with a CUDA implementation and multi-resolution method to achieve 1–2 fps for problems with approximately 3000 variables. We demonstrate the global illumination cancellation algorithm with our multi-projector system. Results show that our method preserves the color fidelity of the desired imagery significantly better than previous methods.
AU - Sheng, Yu
AU - Cutler, Barbara
AU - Chen, Chao
AU - Nasman, Joshua
ID - 3269
IS - 4
JF - Computer Graphics Forum
TI - Perceptual global illumination cancellation in complex projection environments
VL - 30
ER -
TY - JOUR
AB - We present an algorithm to identify individual neural spikes observed on high-density multi-electrode arrays (MEAs). Our method can distinguish large numbers of distinct neural units, even when spikes overlap, and accounts for intrinsic variability of spikes from each unit. As MEAs grow larger, it is important to find spike-identification methods that are scalable, that is, the computational cost of spike fitting should scale well with the number of units observed. Our algorithm accomplishes this goal, and is fast, because it exploits the spatial locality of each unit and the basic biophysics of extracellular signal propagation. Human interaction plays a key role in our method; but effort is minimized and streamlined via a graphical interface. We illustrate our method on data from guinea pig retinal ganglion cells and document its performance on simulated data consisting of spikes added to experimentally measured background noise. We present several tests demonstrating that the algorithm is highly accurate: it exhibits low error rates on fits to synthetic data, low refractory violation rates, good receptive field coverage, and consistency across users.
AU - Prentice, Jason S
AU - Homann, Jan
AU - Simmons, Kristina D
AU - Gasper Tkacik
AU - Balasubramanian, Vijay
AU - Nelson, Philip C
ID - 3276
IS - 7
JF - PLoS One
TI - Fast, scalable, Bayesian spike identification for multi-electrode arrays
VL - 6
ER -
TY - JOUR
AB - The zonula adherens (ZA) of epithelial cells is a site of cell-cell adhesion where cellular forces are exerted and resisted. Increasing evidence indicates that E-cadherin adhesion molecules at the ZA serve to sense force applied on the junctions and coordinate cytoskeletal responses to those forces. Efforts to understand the role that cadherins play in mechanotransduction have been limited by the lack of assays to measure the impact of forces on the ZA. In this study we used 4D imaging of GFP-tagged E-cadherin to analyse the movement of the ZA. Junctions in confluent epithelial monolayers displayed prominent movements oriented orthogonal (perpendicular) to the ZA itself. Two components were identified in these movements: a relatively slow unidirectional (translational) component that could be readily fitted by least-squares regression analysis, upon which were superimposed more rapid oscillatory movements. Myosin IIB was a dominant factor responsible for driving the unilateral translational movements. In contrast, frequency spectrum analysis revealed that depletion of Myosin IIA increased the power of the oscillatory movements. This implies that Myosin IIA may serve to dampen oscillatory movements of the ZA. This extends our recent analysis of Myosin II at the ZA to demonstrate that Myosin IIA and Myosin IIB make distinct contributions to junctional movement at the ZA.
AU - Smutny, Michael
AU - Wu, Selwin
AU - Gomez, Guillermo
AU - Mangold, Sabine
AU - Yap, Alpha
AU - Hamilton, Nicholas
ID - 3288
IS - 7
JF - PLoS One
TI - Multicomponent analysis of junctional movements regulated by Myosin II isoforms at the epithelial zonula adherens
VL - 6
ER -
TY - JOUR
AB - Analysis of genomic data requires an efficient way to calculate likelihoods across very large numbers of loci. We describe a general method for finding the distribution of genealogies: we allow migration between demes, splitting of demes [as in the isolation-with-migration (IM) model], and recombination between linked loci. These processes are described by a set of linear recursions for the generating function of branch lengths. Under the infinite-sites model, the probability of any configuration of mutations can be found by differentiating this generating function. Such calculations are feasible for small numbers of sampled genomes: as an example, we show how the generating function can be derived explicitly for three genes under the two-deme IM model. This derivation is done automatically, using Mathematica. Given data from a large number of unlinked and nonrecombining blocks of sequence, these results can be used to find maximum-likelihood estimates of model parameters by tabulating the probabilities of all relevant mutational configurations and then multiplying across loci. The feasibility of the method is demonstrated by applying it to simulated data and to a data set previously analyzed by Wang and Hey (2010) consisting of 26,141 loci sampled from Drosophila simulans and D. melanogaster. Our results suggest that such likelihood calculations are scalable to genomic data as long as the numbers of sampled individuals and mutations per sequence block are small.
AU - Lohse, Konrad
AU - Harrison, Richard
AU - Barton, Nicholas H
ID - 3290
IS - 3
JF - Genetics
TI - A general method for calculating likelihoods under the coalescent process
VL - 189
ER -
TY - CONF
AB - Animating detailed liquid surfaces has always been a challenge for computer graphics researchers and visual effects artists. Over the past few years, researchers in this field have focused on mesh-based surface tracking to synthesize extremely detailed liquid surfaces as efficiently as possible. This course provides a solid understanding of the steps required to create a fluid simulator with a mesh-based liquid surface.
The course begins with an overview of several existing liquid-surface-tracking techniques and the pros and cons of each method. Then it explains how to embed a triangle mesh into a finite-difference-based fluid simulator and describes several methods for allowing the liquid surface to merge together or break apart. The final section showcases the benefits and further applications of a mesh-based liquid surface, highlighting state-of-the-art methods for tracking colors and textures, maintaining liquid volume, preserving small surface features, and simulating realistic surface-tension waves.
AU - Wojtan, Christopher J
AU - Müller Fischer, Matthias
AU - Brochu, Tyson
ID - 3297
TI - Liquid simulation with mesh-based surface tracking
ER -
TY - CONF
AB - We present a new algorithm for enforcing incompressibility for Smoothed Particle Hydrodynamics (SPH) by preserving uniform density across the domain. We propose a hybrid method that uses a Poisson solve on a coarse grid to enforce a divergence free velocity ﬁeld, followed by a local density correction of the particles. This avoids typical grid artifacts and maintains the Lagrangian nature of SPH by directly transferring pressures onto particles. Our method can be easily integrated with existing SPH techniques such as the incompressible PCISPH method as well as weakly compressible SPH by adding an additional force term. We show that this hybrid method accelerates convergence towards uniform density and permits a signiﬁcantly larger time step compared to earlier approaches while producing similar results. We demonstrate our approach in a variety of scenarios with signiﬁcant pressure gradients such as splashing liquids.
AU - Raveendran, Karthik
AU - Wojtan, Christopher J
AU - Turk, Greg
ED - Spencer, Stephen
ID - 3298
TI - Hybrid smoothed particle hydrodynamics
ER -
TY - CONF
AB - We introduce propagation models, a formalism designed to support general and efficient data structures for the transient analysis of biochemical reaction networks. We give two use cases for propagation abstract data types: the uniformization method and numerical integration. We also sketch an implementation of a propagation abstract data type, which uses abstraction to approximate states.
AU - Henzinger, Thomas A
AU - Mateescu, Maria
ID - 3299
TI - Propagation models for computing biochemical reaction networks
ER -
TY - CONF
AB - The chemical master equation is a differential equation describing the time evolution of the probability distribution over the possible “states” of a biochemical system. The solution of this equation is of interest within the systems biology field ever since the importance of the molec- ular noise has been acknowledged. Unfortunately, most of the systems do not have analytical solutions, and numerical solutions suffer from the course of dimensionality and therefore need to be approximated. Here, we introduce the concept of tail approximation, which retrieves an approximation of the probabilities in the tail of a distribution from the total probability of the tail and its conditional expectation. This approximation method can then be used to numerically compute the solution of the chemical master equation on a subset of the state space, thus fighting the explosion of the state space, for which this problem is renowned.
AU - Henzinger, Thomas A
AU - Mateescu, Maria
ID - 3301
TI - Tail approximation for the chemical master equation
ER -
TY - CONF
AB - Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We present a new job execution environment Flextic that exploits scal- able static scheduling techniques to provide the user with a flexible pricing model, such as a tradeoff between dif- ferent degrees of execution speed and execution price, and at the same time, reduce scheduling overhead for the cloud provider. We have evaluated a prototype of Flextic on Amazon EC2 and compared it against Hadoop. For various data parallel jobs from machine learning, im- age processing, and gene sequencing that we considered, Flextic has low scheduling overhead and reduces job du- ration by up to 15% compared to Hadoop, a dynamic cloud scheduler.
AU - Henzinger, Thomas A
AU - Singh, Anmol
AU - Singh, Vasu
AU - Wies, Thomas
AU - Zufferey, Damien
ID - 3302
TI - Static scheduling in clouds
ER -
TY - GEN
AB - We study the 3D reconstruction of plant roots from multiple 2D images. To meet the challenge caused by the delicate nature of thin branches, we make three innovations to cope with the sensitivity to image quality and calibration. First, we model the background as a harmonic function to improve the segmentation of the root in each 2D image. Second, we develop the concept of the regularized visual hull which reduces the effect of jittering and refraction by ensuring consistency with one 2D image. Third, we guarantee connectedness through adjustments to the 3D reconstruction that minimize global error. Our software is part of a biological phenotype/genotype study of agricultural root systems. It has been tested on more than 40 plant roots and results are promising in terms of reconstruction quality and efficiency.
AU - Zheng, Ying
AU - Gu, Steve
AU - Edelsbrunner, Herbert
AU - Tomasi, Carlo
AU - Benfey, Philip
ID - 3312
T2 - Proceedings of the IEEE International Conference on Computer Vision
TI - Detailed reconstruction of 3D plant root shape
ER -
TY - CONF
AB - Interpreting an image as a function on a compact sub- set of the Euclidean plane, we get its scale-space by diffu- sion, spreading the image over the entire plane. This gener- ates a 1-parameter family of functions alternatively defined as convolutions with a progressively wider Gaussian ker- nel. We prove that the corresponding 1-parameter family of persistence diagrams have norms that go rapidly to zero as time goes to infinity. This result rationalizes experimental observations about scale-space. We hope this will lead to targeted improvements of related computer vision methods.
AU - Chen, Chao
AU - Edelsbrunner, Herbert
ID - 3313
T2 - Proceedings of the IEEE International Conference on Computer Vision
TI - Diffusion runs low on persistence fast
ER -
TY - JOUR
AB - We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are concurrent in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to turn-based (i.e., not concurrent) finite-state (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, limit-robust and bounded-robust winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Prabhu, Vinayak
ID - 3315
IS - 4
JF - Logical Methods in Computer Science
TI - Timed parity games: Complexity and robustness
VL - 7
ER -
TY - CONF
AB - In addition to being correct, a system should be robust, that is, it should behave reasonably even after receiving unexpected inputs. In this paper, we summarize two formal notions of robustness that we have introduced previously for reactive systems. One of the notions is based on assigning costs for failures on a user-provided notion of incorrect transitions in a specification. Here, we define a system to be robust if a finite number of incorrect inputs does not lead to an infinite number of incorrect outputs. We also give a more refined notion of robustness that aims to minimize the ratio of output failures to input failures. The second notion is aimed at liveness. In contrast to the previous notion, it has no concept of recovery from an error. Instead, it compares the ratio of the number of liveness constraints that the system violates to the number of liveness constraints that the environment violates.
AU - Bloem, Roderick
AU - Chatterjee, Krishnendu
AU - Greimel, Karin
AU - Henzinger, Thomas A
AU - Jobstmann, Barbara
ID - 3316
T2 - 6th IEEE International Symposium on Industrial and Embedded Systems
TI - Specification-centered robustness
ER -
TY - JOUR
AB - Parvalbumin is thought to act in a manner similar to EGTA, but how a slow Ca2+ buffer affects nanodomain-coupling regimes at GABAergic synapses is unclear. Direct measurements of parvalbumin concentration and paired recordings in rodent hippocampus and cerebellum revealed that parvalbumin affects synaptic dynamics only when expressed at high levels. Modeling suggests that, in high concentrations, parvalbumin may exert BAPTA-like effects, modulating nanodomain coupling via competition with local saturation of endogenous fixed buffers.
AU - Eggermann, Emmanuel
AU - Jonas, Peter M
ID - 3318
JF - Nature Neuroscience
TI - How the “slow” Ca(2+) buffer parvalbumin affects transmitter release in nanodomain coupling regimes at GABAergic synapses
VL - 15
ER -
TY - JOUR
AB - Powerful statistical models that can be learned efficiently from large amounts of data are currently revolutionizing computer vision. These models possess a rich internal structure reflecting task-specific relations and constraints. This monograph introduces the reader to the most popular classes of structured models in computer vision. Our focus is discrete undirected graphical models which we cover in detail together with a description of algorithms for both probabilistic inference and maximum a posteriori inference. We discuss separately recently successful techniques for prediction in general structured models. In the second part of this monograph we describe methods for parameter learning where we distinguish the classic maximum likelihood based methods from the more recent prediction-based parameter learning methods. We highlight developments to enhance current models and discuss kernelized models and latent variable models. To make the monograph more practical and to provide links to further study we provide examples of successful application of many methods in the computer vision literature.
AU - Nowozin, Sebastian
AU - Lampert, Christoph
ID - 3320
IS - 3-4
JF - Foundations and Trends in Computer Graphics and Vision
TI - Structured learning and prediction in computer vision
VL - 6
ER -
TY - CONF
AB - Automated termination provers often use the following schema to prove that a program terminates: construct a relational abstraction of the program's transition relation and then show that the relational abstraction is well-founded. The focus of current tools has been on developing sophisticated techniques for constructing the abstractions while relying on known decidable logics (such as linear arithmetic) to express them. We believe we can significantly increase the class of programs that are amenable to automated termination proofs by identifying more expressive decidable logics for reasoning about well-founded relations. We therefore present a new decision procedure for reasoning about multiset orderings, which are among the most powerful orderings used to prove termination. We show that, using our decision procedure, one can automatically prove termination of natural abstractions of programs.
AU - Piskac, Ruzica
AU - Wies, Thomas
ED - Jhala, Ranjit
ED - Schmidt, David
ID - 3324
TI - Decision procedures for automating termination proofs
VL - 6538
ER -
TY - CONF
AB - Weighted automata map input words to numerical values. Ap- plications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. A weighted au- tomaton is defined with respect to a semiring. For the tropical semiring, the weight of a run is the sum of the weights of the transitions taken along the run, and the value of a word is the minimal weight of an accepting run on it. In the 90’s, Krob studied the decidability of problems on rational series defined with respect to the tropical semiring. Rational series are strongly related to weighted automata, and Krob’s results apply to them. In par- ticular, it follows from Krob’s results that the universality problem (that is, deciding whether the values of all words are below some threshold) is decidable for weighted automata defined with respect to the tropical semir- ing with domain ∪ {∞}, and that the equality problem is undecidable when the domain is ∪ {∞}. In this paper we continue the study of the borders of decidability in weighted automata, describe alternative and direct proofs of the above results, and tighten them further. Unlike the proofs of Krob, which are algebraic in their nature, our proofs stay in the terrain of state machines, and the reduction is from the halting problem of a two-counter machine. This enables us to significantly simplify Krob’s reasoning, make the un- decidability result accessible to the automata-theoretic community, and strengthen it to apply already to a very simple class of automata: all the states are accepting, there are no initial nor final weights, and all the weights on the transitions are from the set {−1, 0, 1}. The fact we work directly with the automata enables us to tighten also the decidability re- sults and to show that the universality problem for weighted automata defined with respect to the tropical semiring with domain ∪ {∞}, and in fact even with domain ≥0 ∪ {∞}, is PSPACE-complete. Our results thus draw a sharper picture about the decidability of decision problems for weighted automata, in both the front of containment vs. universality and the front of the ∪ {∞} vs. the ∪ {∞} domains.
AU - Almagor, Shaull
AU - Boker, Udi
AU - Kupferman, Orna
ID - 3326
TI - What’s decidable about weighted automata
VL - 6996
ER -
TY - CONF
AB - We report on a generic uni- and bivariate algebraic kernel that is publicly available with CGAL 3.7. It comprises complete, correct, though efficient state-of-the-art implementations on polynomials, roots of polynomial systems, and the support to analyze algebraic curves defined by bivariate polynomials. The kernel design is generic, that is, various number types and substeps can be exchanged. It is accompanied with a ready-to-use interface to enable arrangements induced by algebraic curves, that have already been used as basis for various geometric applications, as arrangements on Dupin cyclides or the triangulation of algebraic surfaces. We present two novel applications: arrangements of rotated algebraic curves and Boolean set operations on polygons bounded by segments of algebraic curves. We also provide experiments showing that our general implementation is competitive and even often clearly outperforms existing implementations that are explicitly tailored for specific types of non-linear curves that are available in CGAL.
AU - Berberich, Eric
AU - Hemmer, Michael
AU - Kerber, Michael
ID - 3328
TI - A generic algebraic kernel for non linear geometric applications
ER -
TY - CONF
AB - We consider the offset-deconstruction problem: Given a polygonal shape Q with n vertices, can it be expressed, up to a tolerance µ in Hausdorff distance, as the Minkowski sum of another polygonal shape P with a disk of fixed radius? If it does, we also seek a preferably simple-looking solution shape P; then, P's offset constitutes an accurate, vertex-reduced, and smoothened approximation of Q. We give an O(n log n)-time exact decision algorithm that handles any polygonal shape, assuming the real-RAM model of computation. An alternative algorithm, based purely on rational arithmetic, answers the same deconstruction problem, up to an uncertainty parameter, and its running time depends on the parameter δ (in addition to the other input parameters: n, δ and the radius of the disk). If the input shape is found to be approximable, the rational-arithmetic algorithm also computes an approximate solution shape for the problem. For convex shapes, the complexity of the exact decision algorithm drops to O(n), which is also the time required to compute a solution shape P with at most one more vertex than a vertex-minimal one. Our study is motivated by applications from two different domains. However, since the offset operation has numerous uses, we anticipate that the reverse question that we study here will be still more broadly applicable. We present results obtained with our implementation of the rational-arithmetic algorithm.
AU - Berberich, Eric
AU - Halperin, Dan
AU - Kerber, Michael
AU - Pogalnikova, Roza
ID - 3329
T2 - Proceedings of the twenty-seventh annual symposium on Computational geometry
TI - Deconstructing approximate offsets
ER -
TY - CONF
AB - We consider the problem of approximating all real roots of a square-free polynomial f. Given isolating intervals, our algorithm refines each of them to a width at most 2-L, that is, each of the roots is approximated to L bits after the binary point. Our method provides a certified answer for arbitrary real polynomials, only requiring finite approximations of the polynomial coefficient and choosing a suitable working precision adaptively. In this way, we get a correct algorithm that is simple to implement and practically efficient. Our algorithm uses the quadratic interval refinement method; we adapt that method to be able to cope with inaccuracies when evaluating f, without sacrificing its quadratic convergence behavior. We prove a bound on the bit complexity of our algorithm in terms of degree, coefficient size and discriminant. Our bound improves previous work on integer polynomials by a factor of deg f and essentially matches best known theoretical bounds on root approximation which are obtained by very sophisticated algorithms.
AU - Kerber, Michael
AU - Sagraloff, Michael
ID - 3330
TI - Root refinement for real polynomials
ER -
TY - JOUR
AB - Given an algebraic hypersurface O in ℝd, how many simplices are necessary for a simplicial complex isotopic to O? We address this problem and the variant where all vertices of the complex must lie on O. We give asymptotically tight worst-case bounds for algebraic plane curves. Our results gradually improve known bounds in higher dimensions; however, the question for tight bounds remains unsolved for d ≥ 3.
AU - Kerber, Michael
AU - Sagraloff, Michael
ID - 3332
IS - 3
JF - Graphs and Combinatorics
TI - A note on the complexity of real algebraic hypersurfaces
VL - 27
ER -
TY - CHAP
AB - We study the topology of the Megaparsec Cosmic Web in terms of the scale-dependent Betti numbers, which formalize the topological information content of the cosmic mass distribution. While the Betti numbers do not fully quantify topology, they extend the information beyond conventional cosmological studies of topology in terms of genus and Euler characteristic. The richer information content of Betti numbers goes along the availability of fast algorithms to compute them. For continuous density fields, we determine the scale-dependence of Betti numbers by invoking the cosmologically familiar filtration of sublevel or superlevel sets defined by density thresholds. For the discrete galaxy distribution, however, the analysis is based on the alpha shapes of the particles. These simplicial complexes constitute an ordered sequence of nested subsets of the Delaunay tessellation, a filtration defined by the scale parameter, α. As they are homotopy equivalent to the sublevel sets of the distance field, they are an excellent tool for assessing the topological structure of a discrete point distribution. In order to develop an intuitive understanding for the behavior of Betti numbers as a function of α, and their relation to the morphological patterns in the Cosmic Web, we first study them within the context of simple heuristic Voronoi clustering models. These can be tuned to consist of specific morphological elements of the Cosmic Web, i.e. clusters, filaments, or sheets. To elucidate the relative prominence of the various Betti numbers in different stages of morphological evolution, we introduce the concept of alpha tracks. Subsequently, we address the topology of structures emerging in the standard LCDM scenario and in cosmological scenarios with alternative dark energy content. The evolution of the Betti numbers is shown to reflect the hierarchical evolution of the Cosmic Web. We also demonstrate that the scale-dependence of the Betti numbers yields a promising measure of cosmological parameters, with a potential to help in determining the nature of dark energy and to probe primordial non-Gaussianities. We also discuss the expected Betti numbers as a function of the density threshold for superlevel sets of a Gaussian random field. Finally, we introduce the concept of persistent homology. It measures scale levels of the mass distribution and allows us to separate small from large scale features. Within the context of the hierarchical cosmic structure formation, persistence provides a natural formalism for a multiscale topology study of the Cosmic Web.
AU - Van De Weygaert, Rien
AU - Vegter, Gert
AU - Edelsbrunner, Herbert
AU - Jones, Bernard
AU - Pranav, Pratyush
AU - Park, Changbom
AU - Hellwing, Wojciech
AU - Eldering, Bob
AU - Kruithof, Nico
AU - Bos, Patrick
AU - Hidding, Johan
AU - Feldbrugge, Job
AU - Ten Have, Eline
AU - Van Engelen, Matti
AU - Caroli, Manuel
AU - Teillaud, Monique
ED - Gavrilova, Marina
ED - Tan, Kenneth
ED - Mostafavi, Mir
ID - 3335
T2 - Transactions on Computational Science XIV
TI - Alpha, Betti and the Megaparsec Universe: On the topology of the Cosmic Web
VL - 6970
ER -
TY - GEN
AB - We consider 2-player games played on a finite state space for an infinite number of rounds. The games are concurrent: in each round, the two players (player 1 and player 2) choose their moves inde- pendently and simultaneously; the current state and the two moves determine the successor state. We study concurrent games with ω-regular winning conditions specified as parity objectives. We consider the qualitative analysis problems: the computation of the almost-sure and limit-sure winning set of states, where player 1 can ensure to win with probability 1 and with probability arbitrarily close to 1, respec- tively. In general the almost-sure and limit-sure winning strategies require both infinite-memory as well as infinite-precision (to describe probabilities). We study the bounded-rationality problem for qualitative analysis of concurrent parity games, where the strategy set for player 1 is restricted to bounded-resource strategies. In terms of precision, strategies can be deterministic, uniform, finite-precision or infinite- precision; and in terms of memory, strategies can be memoryless, finite-memory or infinite-memory. We present a precise and complete characterization of the qualitative winning sets for all combinations of classes of strategies. In particular, we show that uniform memoryless strategies are as powerful as finite-precision infinite-memory strategies, and infinite-precision memoryless strategies are as power- ful as infinite-precision finite-memory strategies. We show that the winning sets can be computed in O(n2d+3) time, where n is the size of the game structure and 2d is the number of priorities (or colors), and our algorithms are symbolic. The membership problem of whether a state belongs to a winning set can be decided in NP ∩ coNP. While this complexity is the same as for the simpler class of turn-based parity games, where in each state only one of the two players has a choice of moves, our algorithms, that are obtained by characterization of the winning sets as μ-calculus formulas, are considerably more involved than those for turn-based games.
AU - Chatterjee, Krishnendu
ID - 3338
T2 - arXiv
TI - Bounded rationality in concurrent parity games
ER -
TY - GEN
AB - Turn-based stochastic games and its important subclass Markov decision processes (MDPs) provide models for systems with both probabilistic and nondeterministic behaviors. We consider turn-based stochastic games with two classical quantitative objectives: discounted-sum and long-run average objectives. The game models and the quantitative objectives are widely used in probabilistic verification, planning, optimal inventory control, network protocol and performance analysis. Games and MDPs that model realistic systems often have very large state spaces, and probabilistic abstraction techniques are necessary to handle the state-space explosion. The commonly used full-abstraction techniques do not yield space-savings for systems that have many states with similar value, but does not necessarily have similar transition structure. A semi-abstraction technique, namely Magnifying-lens abstractions (MLA), that clusters states based on value only, disregarding differences in their transition relation was proposed for qualitative objectives (reachability and safety objectives). In this paper we extend the MLA technique to solve stochastic games with discounted-sum and long-run average objectives. We present the MLA technique based abstraction-refinement algorithm for stochastic games and MDPs with discounted-sum objectives. For long-run average objectives, our solution works for all MDPs and a sub-class of stochastic games where every state has the same value.
AU - Chatterjee, Krishnendu
AU - De Alfaro, Luca
AU - Pritam, Roy
ID - 3339
T2 - arXiv
TI - Magnifying lens abstraction for stochastic games with discounted and long-run average objectives
ER -
TY - CONF
AB - We consider Markov decision processes (MDPs) with ω-regular specifications given as parity objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. The algorithms for the computation of the almost-sure winning set for parity objectives iteratively use the solutions for the almost-sure winning set for Büchi objectives (a special case of parity objectives). 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(nm) 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 often have constant out-degree, and then our symbolic algorithm takes O(nn) 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(nK) 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 - Nisarg, Shah
ED - Gopalakrishnan, Ganesh
ED - Qadeer, Shaz
ID - 3342
TI - Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives
VL - 6806
ER -
TY - CONF
AB - We present faster and dynamic algorithms for the following problems arising in probabilistic verification: Computation of the maximal end-component (mec) decomposition of Markov decision processes (MDPs), and of the almost sure winning set for reachability and parity objectives in MDPs. We achieve the following running time for static algorithms in MDPs with graphs of n vertices and m edges: (1) O(m · min{ √m, n2/3 }) for the mec decomposition, improving the longstanding O(m·n) bound; (2) O(m·n2/3) for reachability objectives, improving the previous O(m · √m) bound for m > n4/3; and (3) O(m · min{ √m, n2/3 } · log(d)) for parity objectives with d priorities, improving the previous O(m · √m · d) bound. We also give incremental and decremental algorithms in linear time for mec decomposition and reachability objectives and O(m · log d) time for parity ob jectives.
AU - Chatterjee, Krishnendu
AU - Henzinger, Monika
ID - 3343
TI - Faster and dynamic algorithms for maximal end component decomposition and related graph problems in probabilistic verification
ER -
TY - CONF
AB - We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode ω-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition re- quires that the resource level never drops below 0, and the mean-payoff condi- tion requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
ID - 3345
TI - Energy and mean-payoff parity Markov Decision Processes
VL - 6907
ER -
TY - CONF
AB - We study Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) functions. We consider two different objectives, namely, expectation and satisfaction objectives. Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected limit-average value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector. We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and that finite-memory randomized strategies are sufficient. Under the satisfaction objective, in contrast to the single-objective case, infinite memory is necessary for strategies, and that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon>;0. We further prove that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>;0. Our results also reveal flaws in previous work for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results.
AU - Brázdil, Tomáš
AU - Brožek, Václav
AU - Chatterjee, Krishnendu
AU - Forejt, Vojtěch
AU - Kučera, Antonín
ID - 3346
TI - Two views on multiple mean payoff objectives in Markov Decision Processes
ER -
TY - CONF
AB - The class of omega-regular languages provides a robust specification language in verification. Every omega-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens "eventually". Finitary liveness was proposed by Alur and Henzinger as a stronger formulation of liveness. It requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider automata with finitary acceptance conditions defined by finitary Buchi, parity and Streett languages. We study languages expressible by such automata: we give their topological complexity and present a regular-expression characterization. We compare the expressive power of finitary automata and give optimal algorithms for classical decisions questions. We show that the finitary languages are Sigma 2-complete; we present a complete picture of the expressive power of various classes of automata with finitary and infinitary acceptance conditions; we show that the languages defined by finitary parity automata exactly characterize the star-free fragment of omega B-regular languages; and we show that emptiness is NLOGSPACE-complete and universality as well as language inclusion are PSPACE-complete for finitary parity and Streett automata.
AU - Chatterjee, Krishnendu
AU - Fijalkow, Nathanaël
ID - 3347
TI - Finitary languages
VL - 6638
ER -
TY - CONF
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 linear (in the number of clocks) number of memory bits. Precisely, we show that for safety objectives, a memory of size (3 · |C|+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 bound. We also settle the open question of whether winning region controller strategies require memory for safety objectives by showing with an example the necessity of memory for region strategies to win for safety objectives.
AU - Chatterjee, Krishnendu
AU - Prabhu, Vinayak
ID - 3348
TI - Synthesis of memory efficient real time controllers for safety objectives
ER -
TY - CONF
AB - Games on graphs provide a natural model for reactive non-terminating systems. In such games, the interaction of two players on an arena results in an infinite path that describes a run of the system. Different settings are used to model various open systems in computer science, as for instance turn-based or concurrent moves, and deterministic or stochastic transitions. In this paper, we are interested in turn-based games, and specifically in deterministic parity games and stochastic reachability games (also known as simple stochastic games). We present a simple, direct and efficient reduction from deterministic parity games to simple stochastic games: it yields an arena whose size is linear up to a logarithmic factor in size of the original arena.
AU - Chatterjee, Krishnendu
AU - Fijalkow, Nathanaël
ID - 3349
TI - A reduction from parity games to simple stochastic games
VL - 54
ER -
TY - CONF
AB - In two-player games on graph, the players construct an infinite path through the game graph and get a reward computed by a payoff function over infinite paths. Over weighted graphs, the typical and most studied payoff functions compute the limit-average or the discounted sum of the rewards along the path. Besides their simple definition, these two payoff functions enjoy the property that memoryless optimal strategies always exist. In an attempt to construct other simple payoff functions, we define a class of payoff functions which compute an (infinite) weighted average of the rewards. This new class contains both the limit-average and the discounted sum functions, and we show that they are the only members of this class which induce memoryless optimal strategies, showing that there is essentially no other simple payoff functions.
AU - Chatterjee, Krishnendu
AU - Doyen, Laurent
AU - Singh, Rohit
ED - Owe, Olaf
ED - Steffen, Martin
ED - Telle, Jan Arne
ID - 3351
TI - On memoryless quantitative objectives
VL - 6914
ER -
TY - JOUR
AB - Compositional theories are crucial when designing large and complex systems from smaller components. In this work we propose such a theory for synchronous concurrent systems. Our approach follows so-called interface theories, which use game-theoretic interpretations of composition and refinement. These are appropriate for systems with distinct inputs and outputs, and explicit conditions on inputs that must be enforced during composition. Our interfaces model systems that execute in an infinite sequence of synchronous rounds. At each round, a contract must be satisfied. The contract is simply a relation specifying the set of valid input/output pairs. Interfaces can be composed by parallel, serial or feedback composition. A refinement relation between interfaces is defined, and shown to have two main properties: (1) it is preserved by composition, and (2) it is equivalent to substitutability, namely, the ability to replace an interface by another one in any context. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.
AU - Tripakis, Stavros
AU - Lickly, Ben
AU - Henzinger, Thomas A
AU - Lee, Edward
ID - 3353
IS - 4
JF - ACM Transactions on Programming Languages and Systems (TOPLAS)
TI - A theory of synchronous relational interfaces
VL - 33
ER -
TY - CONF
AB - Byzantine Fault Tolerant (BFT) protocols aim to improve the reliability of distributed systems. They enable systems to tolerate arbitrary failures in a bounded number of nodes. BFT protocols are usually proven correct for certain safety and liveness properties. However, recent studies have shown that the performance of state-of-the-art BFT protocols decreases drastically in the presence of even a single malicious node. This motivates a formal quantitative analysis of BFT protocols to investigate their performance characteristics under different scenarios. We present HyPerf, a new hybrid methodology based on model checking and simulation techniques for evaluating the performance of BFT protocols. We build a transition system corresponding to a BFT protocol and systematically explore the set of behaviors allowed by the protocol. We associate certain timing information with different operations in the protocol, like cryptographic operations and message transmission. After an elaborate state exploration, we use the time information to evaluate the performance characteristics of the protocol using simulation techniques. We integrate our framework in Mace, a tool for building and verifying distributed systems. We evaluate the performance of PBFT using our framework. We describe two different use-cases of our methodology. For the benign operation of the protocol, we use the time information as random variables to compute the probability distribution of the execution times. In the presence of faults, we estimate the worst-case performance of the protocol for various attacks that can be employed by malicious nodes. Our results show the importance of hybrid techniques in systematically analyzing the performance of large-scale systems.
AU - Halalai, Raluca
AU - Henzinger, Thomas A
AU - Singh, Vasu
ID - 3355
TI - Quantitative evaluation of BFT protocols
ER -
TY - CONF
AB - There is recently a significant effort to add quantitative objectives to formal verification and synthesis. We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications. In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is a numeric variable of the system, c is a constant rational number, and Sum(v) and Avg(v) denote the accumulated sum and average of the values of v from the beginning of the computation up to the current point of time. We also allow the path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring to the average value along an entire computation. We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with "controlled-accumulation", allowing, for example, to specify constraints on the average waiting time between a request and a grant. On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.
AU - Boker, Udi
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Kupferman, Orna
ID - 3356
TI - Temporal specifications with accumulative values
ER -
TY - CONF
AB - The static scheduling problem often arises as a fundamental problem in real-time systems and grid computing. We consider the problem of statically scheduling a large job expressed as a task graph on a large number of computing nodes, such as a data center. This paper solves the large-scale static scheduling problem using abstraction refinement, a technique commonly used in formal verification to efficiently solve computationally hard problems. A scheduler based on abstraction refinement first attempts to solve the scheduling problem with abstract representations of the job and the computing resources. As abstract representations are generally small, the scheduling can be done reasonably fast. If the obtained schedule does not meet specified quality conditions (like data center utilization or schedule makespan) then the scheduler refines the job and data center abstractions and, again solves the scheduling problem. We develop different schedulers based on abstraction refinement. We implemented these schedulers and used them to schedule task graphs from various computing domains on simulated data centers with realistic topologies. We compared the speed of scheduling and the quality of the produced schedules with our abstraction refinement schedulers against a baseline scheduler that does not use any abstraction. We conclude that abstraction refinement techniques give a significant speed-up compared to traditional static scheduling heuristics, at a reasonable cost in the quality of the produced schedules. We further used our static schedulers in an actual system that we deployed on Amazon EC2 and compared it against the Hadoop dynamic scheduler for large MapReduce jobs. Our experiments indicate that there is great potential for static scheduling techniques.
AU - Henzinger, Thomas A
AU - Singh, Vasu
AU - Wies, Thomas
AU - Zufferey, Damien
ID - 3358
TI - Scheduling large jobs by abstraction refinement
ER -
TY - CONF
AB - A discounted-sum automaton (NDA) is a nondeterministic finite automaton with edge weights, which values a run by the discounted sum of visited edge weights. More precisely, the weight in the i-th position of the run is divided by lambda^i, where the discount factor lambda is a fixed rational number greater than 1. Discounted summation is a common and useful measuring scheme, especially for infinite sequences, which reflects the assumption that earlier weights are more important than later weights. Determinizing automata is often essential, for example, in formal verification, where there are polynomial algorithms for comparing two deterministic NDAs, while the equivalence problem for NDAs is not known to be decidable. Unfortunately, however, discounted-sum automata are, in general, not determinizable: it is currently known that for every rational discount factor 1 < lambda < 2, there is an NDA with lambda (denoted lambda-NDA) that cannot be determinized. We provide positive news, showing that every NDA with an integral factor is determinizable. We also complete the picture by proving that the integers characterize exactly the discount factors that guarantee determinizability: we show that for every non-integral rational factor lambda, there is a nondeterminizable lambda-NDA. Finally, we prove that the class of NDAs with integral discount factors enjoys closure under the algebraic operations min, max, addition, and subtraction, which is not the case for general NDAs nor for deterministic NDAs. This shows that for integral discount factors, the class of NDAs forms an attractive specification formalism in quantitative formal verification. All our results hold equally for automata over finite words and for automata over infinite words.
AU - Boker, Udi
AU - Henzinger, Thomas A
ID - 3360
TI - Determinizing discounted-sum automata
VL - 12
ER -
TY - CONF
AB - In this paper, we investigate the computational complexity of quantitative information flow (QIF) problems. Information-theoretic quantitative relaxations of noninterference (based on Shannon entropy)have been introduced to enable more fine-grained reasoning about programs in situations where limited information flow is acceptable. The QIF bounding problem asks whether the information flow in a given program is bounded by a constant $d$. Our first result is that the QIF bounding problem is PSPACE-complete. The QIF memoryless synthesis problem asks whether it is possible to resolve nondeterministic choices in a given partial program in such a way that in the resulting deterministic program, the quantitative information flow is bounded by a given constant $d$. Our second result is that the QIF memoryless synthesis problem is also EXPTIME-complete. The QIF memoryless synthesis problem generalizes to QIF general synthesis problem which does not impose the memoryless requirement (that is, by allowing the synthesized program to have more variables then the original partial program). Our third result is that the QIF general synthesis problem is EXPTIME-hard.
AU - Cerny, Pavol
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
ID - 3361
TI - The complexity of quantitative information flow problems
ER -
TY - CONF
AB - State-transition systems communicating by shared variables have been the underlying model of choice for applications of model checking. Such formalisms, however, have difficulty with modeling process creation or death and communication reconfigurability. Here, we introduce “dynamic reactive modules” (DRM), a state-transition modeling formalism that supports dynamic reconfiguration and creation/death of processes. The resulting formalism supports two types of variables, data variables and reference variables. Reference variables enable changing the connectivity between processes and referring to instances of processes. We show how this new formalism supports parallel composition and refinement through trace containment. DRM provide a natural language for modeling (and ultimately reasoning about) biological systems and multiple threads communicating through shared variables.
AU - Fisher, Jasmin
AU - Henzinger, Thomas A
AU - Nickovic, Dejan
AU - Piterman, Nir
AU - Singh, Anmol
AU - Vardi, Moshe
ID - 3362
TI - Dynamic reactive modules
VL - 6901
ER -
TY - GEN
AB - We consider probabilistic automata on infinite words with acceptance defined by safety, reachability, Büchi, coBüchi, and limit-average conditions. We consider quantitative and qualitative decision problems. We present extensions and adaptations of proofs for probabilistic finite automata and present a complete characterization of the decidability and undecidability frontier of the quantitative and qualitative decision problems for probabilistic automata on infinite words.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Tracol, Mathieu
ID - 3363
TI - The decidability frontier for probabilistic automata on infinite words
ER -
TY - JOUR
AB - Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete-state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive. We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.
AU - Didier, Frédéric
AU - Henzinger, Thomas A
AU - Mateescu, Maria
AU - Wolf, Verena
ID - 3364
IS - 21
JF - Theoretical Computer Science
TI - Approximation of event probabilities in noisy cellular processes
VL - 412
ER -
TY - CONF
AB - We present the tool Quasy, a quantitative synthesis tool. Quasy takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. The user can choose between a system that satisfies and optimizes the specifications (a) under all possible environment behaviors or (b) under the most-likely environment behaviors given as a probability distribution on the possible input sequences. Quasy solves these two quantitative synthesis problems by reduction to instances of 2-player games and Markov Decision Processes (MDPs) with quantitative winning objectives. Quasy can also be seen as a game solver for quantitative games. Most notable, it can solve lexicographic mean-payoff games with 2 players, MDPs with mean-payoff objectives, and ergodic MDPs with mean-payoff parity objectives.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Jobstmann, Barbara
AU - Singh, Rohit
ID - 3365
TI - QUASY: quantitative synthesis tool
VL - 6605
ER -
TY - CONF
AB - We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized "specification free", in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures.
AU - Cerny, Pavol
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Radhakrishna, Arjun
AU - Singh, Rohit
ED - Gopalakrishnan, Ganesh
ED - Qadeer, Shaz
ID - 3366
TI - Quantitative synthesis for concurrent programs
VL - 6806
ER -
TY - JOUR
AB - Tissue surface tension (TST) is an important mechanical property influencing cell sorting and tissue envelopment. The study by Manning et al. (1) reported on a mathematical model describing TST on the basis of the balance between adhesive and tensile properties of the constituent cells. The model predicts that, in high-adhesion cell aggregates, surface cells will be stretched to maintain the same area of cell–cell contact as interior bulk cells, resulting in an elongated and flattened cell shape. The authors (1) observed flat and elongated cells at the surface of high-adhesion zebrafish germ-layer explants, which they argue are undifferentiated stretched germ-layer progenitor cells, and they use this observation as a validation of their model.
AU - Krens, Gabriel
AU - Möllmert, Stephanie
AU - Heisenberg, Carl-Philipp J
ID - 3368
IS - 3
JF - PNAS
TI - Enveloping cell layer differentiation at the surface of zebrafish germ layer tissue explants
VL - 108
ER -
TY - JOUR
AB - Supertree methods are widely applied and give rise to new conclusions about phylogenies (e.g., Bininda-Emonds et al. 2007). Although several desiderata for supertree methods exist (Wilkinson, Thorley, et al. 2004), only few of them have been studied in greater detail, examples include shape bias (Wilkinson et al. 2005) or pareto properties (Wilkinson et al. 2007). Here I look more closely at two matrix representation methods, matrix representation with compatibility (MRC) and matrix representation with parsimony (MRP). Different null models of random data are studied and the resulting tree shapes are investigated. Thereby I consider unrooted trees and a bias in tree shape is determined by a tree balance measure. The measure for unrooted trees is a modification of a tree balance measure for rooted trees. I observe that depending on the underlying null model of random data, the methods may resolve conflict in favor of more balanced tree shapes. The analyses refer only to trees with the same taxon set, also known as the consensus setting (e.g., Wilkinson et al. 2007), but I will be able to draw conclusions on how to deal with missing data.
AU - Kupczok, Anne
ID - 3370
IS - 2
JF - Systematic Biology
TI - Consequences of different null models on the tree shape bias of supertree methods
VL - 60
ER -
TY - JOUR
AB - The Minisymposium “Cell Migration and Motility” was attended by approximately 500 visitors and covered a broad range of questions in the field using diverse model systems. Topics comprised actin dynamics, cell polarity, force transduction, signal transduction, bar- rier transmigration, and chemotactic guidance.
AU - Sixt, Michael K
AU - Parent, Carole
ID - 3371
IS - 6
JF - Molecular Biology and Evolution
TI - Cells on the move in Philadelphia
VL - 22
ER -
TY - JOUR
AB - Nowak et al.1 argue that inclusive fitness theory has been of little value in explaining the natural world, and that it has led to negligible progress in explaining the evolution of eusociality. However, we believe that their arguments are based upon a misunderstanding of evolutionary theory and a misrepresentation of the empirical literature. We will focus our comments on three general issues.
AU - Abbot, Patrick
AU - Abe, Jun
AU - Alcock, John
AU - Alizon, Samuel
AU - Alpedrinha, Joao
AU - Andersson, Malte
AU - Andre, Jean
AU - Van Baalen, Minus
AU - Balloux, Francois
AU - Balshine, Sigal
AU - Barton, Nicholas H
AU - Beukeboom, Leo
AU - Biernaskie, Jay
AU - Bilde, Trine
AU - Borgia, Gerald
AU - Breed, Michael
AU - Brown, Sam
AU - Bshary, Redouan
AU - Buckling, Angus
AU - Burley, Nancy
AU - Burton Chellew, Max
AU - Cant, Michael
AU - Chapuisat, Michel
AU - Charnov, Eric
AU - Clutton Brock, Tim
AU - Cockburn, Andrew
AU - Cole, Blaine
AU - Colegrave, Nick
AU - Cosmides, Leda
AU - Couzin, Iain
AU - Coyne, Jerry
AU - Creel, Scott
AU - Crespi, Bernard
AU - Curry, Robert
AU - Dall, Sasha
AU - Day, Troy
AU - Dickinson, Janis
AU - Dugatkin, Lee
AU - El Mouden, Claire
AU - Emlen, Stephen
AU - Evans, Jay
AU - Ferriere, Regis
AU - Field, Jeremy
AU - Foitzik, Susanne
AU - Foster, Kevin
AU - Foster, William
AU - Fox, Charles
AU - Gadau, Juergen
AU - Gandon, Sylvain
AU - Gardner, Andy
AU - Gardner, Michael
AU - Getty, Thomas
AU - Goodisman, Michael
AU - Grafen, Alan
AU - Grosberg, Rick
AU - Grozinger, Christina
AU - Gouyon, Pierre
AU - Gwynne, Darryl
AU - Harvey, Paul
AU - Hatchwell, Ben
AU - Heinze, Jürgen
AU - Helantera, Heikki
AU - Helms, Ken
AU - Hill, Kim
AU - Jiricny, Natalie
AU - Johnstone, Rufus
AU - Kacelnik, Alex
AU - Kiers, E Toby
AU - Kokko, Hanna
AU - Komdeur, Jan
AU - Korb, Judith
AU - Kronauer, Daniel
AU - Kümmerli, Rolf
AU - Lehmann, Laurent
AU - Linksvayer, Timothy
AU - Lion, Sébastien
AU - Lyon, Bruce
AU - Marshall, James
AU - Mcelreath, Richard
AU - Michalakis, Yannis
AU - Michod, Richard
AU - Mock, Douglas
AU - Monnin, Thibaud
AU - Montgomerie, Robert
AU - Moore, Allen
AU - Mueller, Ulrich
AU - Noë, Ronald
AU - Okasha, Samir
AU - Pamilo, Pekka
AU - Parker, Geoff
AU - Pedersen, Jes
AU - Pen, Ido
AU - Pfennig, David
AU - Queller, David
AU - Rankin, Daniel
AU - Reece, Sarah
AU - Reeve, Hudson
AU - Reuter, Max
AU - Roberts, Gilbert
AU - Robson, Simon
AU - Roze, Denis
AU - Rousset, Francois
AU - Rueppell, Olav
AU - Sachs, Joel
AU - Santorelli, Lorenzo
AU - Schmid Hempel, Paul
AU - Schwarz, Michael
AU - Scott Phillips, Tom
AU - Shellmann Sherman, Janet
AU - Sherman, Paul
AU - Shuker, David
AU - Smith, Jeff
AU - Spagna, Joseph
AU - Strassmann, Beverly
AU - Suarez, Andrew
AU - Sundström, Liselotte
AU - Taborsky, Michael
AU - Taylor, Peter
AU - Thompson, Graham
AU - Tooby, John
AU - Tsutsui, Neil
AU - Tsuji, Kazuki
AU - Turillazzi, Stefano
AU - Úbeda, Francisco
AU - Vargo, Edward
AU - Voelkl, Bernard
AU - Wenseleers, Tom
AU - West, Stuart
AU - West Eberhard, Mary
AU - Westneat, David
AU - Wiernasz, Diane
AU - Wild, Geoff
AU - Wrangham, Richard
AU - Young, Andrew
AU - Zeh, David
AU - Zeh, Jeanne
AU - Zink, Andrew
ID - 3372
IS - 7339
JF - Nature
TI - Inclusive fitness theory and eusociality
VL - 471
ER -
TY - JOUR
AB - The use of optical traps to measure or apply forces on the molecular level requires a precise knowledge of the trapping force field. Close to the trap center, this field is typically approximated as linear in the displacement of the trapped microsphere. However, applications demanding high forces at low laser intensities can probe the light-microsphere interaction beyond the linear regime. Here, we measured the full nonlinear force and displacement response of an optical trap in two dimensions using a dual-beam optical trap setup with back-focal-plane photodetection. We observed a substantial stiffening of the trap beyond the linear regime that depends on microsphere size, in agreement with Mie theory calculations. Surprisingly, we found that the linear detection range for forces exceeds the one for displacement by far. Our approach allows for a complete calibration of an optical trap.
AU - Jahnel, Marcus
AU - Behrndt, Martin
AU - Jannasch, Anita
AU - Schaeffer, Erik
AU - Grill, Stephan
ID - 3373
IS - 7
JF - Optics Letters
TI - Measuring the complete force field of an optical trap
VL - 36
ER -
TY - JOUR
AB - Genetic regulatory networks enable cells to respond to changes in internal and external conditions by dynamically coordinating their gene expression profiles. Our ability to make quantitative measurements in these biochemical circuits has deepened our understanding of what kinds of computations genetic regulatory networks can perform, and with what reliability. These advances have motivated researchers to look for connections between the architecture and function of genetic regulatory networks. Transmitting information between a network's inputs and outputs has been proposed as one such possible measure of function, relevant in certain biological contexts. Here we summarize recent developments in the application of information theory to gene regulatory networks. We first review basic concepts in information theory necessary for understanding recent work. We then discuss the functional complexity of gene regulation, which arises from the molecular nature of the regulatory interactions. We end by reviewing some experiments that support the view that genetic networks responsible for early development of multicellular organisms might be maximizing transmitted 'positional information'.
AU - Tkacik, Gasper
AU - Walczak, Aleksandra
ID - 3374
IS - 15
JF - Journal of Physics: Condensed Matter
TI - Information transmission in genetic regulatory networks a review
VL - 23
ER -
TY - JOUR
AB - By exploiting an analogy between population genetics and statistical mechanics, we study the evolution of a polygenic trait under stabilizing selection, mutation and genetic drift. This requires us to track only four macroscopic variables, instead of the distribution of all the allele frequencies that influence the trait. These macroscopic variables are the expectations of: the trait mean and its square, the genetic variance, and of a measure of heterozygosity, and are derived from a generating function that is in turn derived by maximizing an entropy measure. These four macroscopics are enough to accurately describe the dynamics of the trait mean and of its genetic variance (and in principle of any other quantity). Unlike previous approaches that were based on an infinite series of moments or cumulants, which had to be truncated arbitrarily, our calculations provide a well-defined approximation procedure. We apply the framework to abrupt and gradual changes in the optimum, as well as to changes in the strength of stabilizing selection. Our approximations are surprisingly accurate, even for systems with as few as five loci. We find that when the effects of drift are included, the expected genetic variance is hardly altered by directional selection, even though it fluctuates in any particular instance. We also find hysteresis, showing that even after averaging over the microscopic variables, the macroscopic trajectories retain a memory of the underlying genetic states.
AU - de Vladar, Harold
AU - Barton, Nicholas H
ID - 3375
IS - 58
JF - Journal of the Royal Society Interface
TI - The statistical mechanics of a polygenic character under stabilizing selection mutation and drift
VL - 8
ER -
TY - JOUR
AB - Regulatory conflicts occur when two signals that individually trigger opposite cellular responses are present simultaneously. Here, we investigate regulatory conflicts in the bacterial response to antibiotic combinations. We use an Escherichia coli promoter-GFP library to study the transcriptional response of many promoters to either additive or antagonistic drug pairs at fine two-dimensional (2D) resolution of drug concentration. Surprisingly, we find that this data set can be characterized as a linear sum of only two principal components. Component one, accounting for over 70% of the response, represents the response to growth inhibition by the drugs. Component two describes how regulatory conflicts are resolved. For the additive drug pair, conflicts are resolved by linearly interpolating the single drug responses, while for the antagonistic drug pair, the growth-limiting drug dominates the response. Importantly, for a given drug pair, the same conflict resolution strategy applies to almost all genes. These results provide a recipe for predicting gene expression responses to antibiotic combinations.
AU - Bollenbach, Mark Tobias
AU - Kishony, Roy
ID - 3376
IS - 4
JF - Molecular Cell
TI - Resolution of gene regulatory conflicts caused by combinations of antibiotics
VL - 42
ER -
TY - JOUR
AB - By definition, transverse intersections are stable under in- finitesimal perturbations. Using persistent homology, we ex- tend this notion to sizeable perturbations. Specifically, we assign to each homology class of the intersection its robust- ness, the magnitude of a perturbation necessary to kill it, and prove that robustness is stable. Among the applications of this result is a stable notion of robustness for fixed points of continuous mappings and a statement of stability for con- tours of smooth mappings.
AU - Edelsbrunner, Herbert
AU - Morozov, Dmitriy
AU - Patel, Amit
ID - 3377
IS - 3
JF - Foundations of Computational Mathematics
TI - Quantifying transversality by measuring the robustness of intersections
VL - 11
ER -
TY - JOUR
AB - The process of gastrulation is highly conserved across vertebrates on both the genetic and morphological levels, despite great variety in embryonic shape and speed of development. This mechanism spatially separates the germ layers and establishes the organizational foundation for future development. Mesodermal identity is specified in a superficial layer of cells, the epiblast, where cells maintain an epithelioid morphology. These cells involute to join the deeper hypoblast layer where they adopt a migratory, mesenchymal morphology. Expression of a cascade of related transcription factors orchestrates the parallel genetic transition from primitive to mature mesoderm. Although the early and late stages of this process are increasingly well understood, the transition between them has remained largely mysterious. We present here the first high resolution in vivo observations of the blebby transitional morphology of involuting mesodermal cells in a vertebrate embryo. We further demonstrate that the zebrafish spadetail mutation creates a reversible block in the maturation program, stalling cells in the transition state. This mutation creates an ideal system for dissecting the specific properties of cells undergoing the morphological transition of maturing mesoderm, as we demonstrate with a direct measurement of cell–cell adhesion.
AU - Row, Richard
AU - Maître, Jean-Léon
AU - Martin, Benjamin
AU - Stockinger, Petra
AU - Heisenberg, Carl-Philipp J
AU - Kimelman, David
ID - 3379
IS - 1
JF - Developmental Biology
TI - Completion of the epithelial to mesenchymal transition in zebrafish mesoderm requires Spadetail
VL - 354
ER -
TY - JOUR
AB - Linkage between markers and genes that affect a phenotype of interest may be determined by examining differences in marker allele frequency in the extreme progeny of a cross between two inbred lines. This strategy is usually employed when pooling is used to reduce genotyping costs. When the cross progeny are asexual, the extreme progeny may be selected by multiple generations of asexual reproduction and selection. We analyse this method of measuring phenotype in asexual progeny and examine the changes in marker allele frequency due to selection over many generations. Stochasticity in marker frequency in the selected population arises due to the finite initial population size. We derive the distribution of marker frequency as a result of selection at a single major locus, and show that in order to avoid spurious changes in marker allele frequency in the selected population, the initial population size should be in the low to mid hundreds.
AU - Logeswaran, Sayanthan
AU - Barton, Nicholas H
ID - 3380
IS - 3
JF - Genetical Research
TI - Mapping Mendelian traits in asexual progeny using changes in marker allele frequency
VL - 93
ER -
TY - JOUR
AB - In this survey, we compare several languages for specifying Markovian population models such as queuing networks and chemical reaction networks. All these languages — matrix descriptions, stochastic Petri nets, stoichiometric equations, stochastic process algebras, and guarded command models — describe continuous-time Markov chains, but they differ according to important properties, such as compositionality, expressiveness and succinctness, executability, and ease of use. Moreover, they provide different support for checking the well-formedness of a model and for analyzing a model.
AU - Henzinger, Thomas A
AU - Jobstmann, Barbara
AU - Wolf, Verena
ID - 3381
IS - 4
JF - IJFCS: International Journal of Foundations of Computer Science
TI - Formalisms for specifying Markovian population models
VL - 22
ER -
TY - JOUR
AB - Here we introduce a database of calibrated natural images publicly available through an easy-to-use web interface. Using a Nikon D70 digital SLR camera, we acquired about six-megapixel images of Okavango Delta of Botswana, a tropical savanna habitat similar to where the human eye is thought to have evolved. Some sequences of images were captured unsystematically while following a baboon troop, while others were designed to vary a single parameter such as aperture, object distance, time of day or position on the horizon. Images are available in the raw RGB format and in grayscale. Images are also available in units relevant to the physiology of human cone photoreceptors, where pixel values represent the expected number of photoisomerizations per second for cones sensitive to long (L), medium (M) and short (S) wavelengths. This database is distributed under a Creative Commons Attribution-Noncommercial Unported license to facilitate research in computer vision, psychophysics of perception, and visual neuroscience.
AU - Tkacik, Gasper
AU - Garrigan, Patrick
AU - Ratliff, Charles
AU - Milcinski, Grega
AU - Klein, Jennifer
AU - Seyfarth, Lucia
AU - Sterling, Peter
AU - Brainard, David
AU - Balasubramanian, Vijay
ID - 3384
IS - 6
JF - PLoS One
TI - Natural images from the birthplace of the human eye
VL - 6
ER -
TY - JOUR
AB - Background: Supertree methods combine overlapping input trees into a larger supertree. Here, I consider split-based supertree methods that first extract the split information of the input trees and subsequently combine this split information into a phylogeny. Well known split-based supertree methods are matrix representation with parsimony and matrix representation with compatibility. Combining input trees on the same taxon set, as in the consensus setting, is a well-studied task and it is thus desirable to generalize consensus methods to supertree methods. Results: Here, three variants of majority-rule (MR) supertrees that generalize majority-rule consensus trees are investigated. I provide simple formulas for computing the respective score for bifurcating input- and supertrees. These score computations, together with a heuristic tree search minmizing the scores, were implemented in the python program PluMiST (Plus- and Minus SuperTrees) available from http://www.cibiv.at/software/ plumist. The different MR methods were tested by simulation and on real data sets. The search heuristic was successful in combining compatible input trees. When combining incompatible input trees, especially one variant, MR(-) supertrees, performed well. Conclusions: The presented framework allows for an efficient score computation of three majority-rule supertree variants and input trees. I combined the score computation with a heuristic search over the supertree space. The implementation was tested by simulation and on real data sets and showed promising results. Especially the MR(-) variant seems to be a reasonable score for supertree reconstruction. Generalizing these computations to multifurcating trees is an open problem, which may be tackled using this framework.
AU - Kupczok, Anne
ID - 3387
IS - 205
JF - BMC Evolutionary Biology
TI - Split based computation of majority rule supertrees
VL - 11
ER -
TY - JOUR
AB - Background: Fragmentation of terrestrial ecosystems has had detrimental effects on metapopulations of habitat specialists. Maculinea butterflies have been particularly affected because of their specialized lifecycles, requiring both specific food-plants and host-ants. However, the interaction between dispersal, effective population size, and long-term genetic erosion of these endangered butterflies remains unknown. Using non-destructive sampling, we investigated the genetic diversity of the last extant population of M. arion in Denmark, which experienced critically low numbers in the 1980s. Results: Using nine microsatellite markers, we show that the population is genetically impoverished compared to nearby populations in Sweden, but less so than monitoring programs suggested. Ten additional short repeat microsatellites were used to reconstruct changes in genetic diversity and population structure over the last 77 years from museum specimens. We also tested amplification efficiency in such historical samples as a function of repeat length and sample age. Low population numbers in the 1980s did not affect genetic diversity, but considerable turnover of alleles has characterized this population throughout the time-span of our analysis. Conclusions: Our results suggest that M. arion is less sensitive to genetic erosion via population bottlenecks than previously thought, and that managing clusters of high quality habitat may be key for long-term conservation.
AU - Ugelvig, Line V
AU - Nielsen, Per
AU - Boomsma, Jacobus
AU - Nash, David
ID - 3388
IS - 201
JF - BMC Evolutionary Biology
TI - Reconstructing eight decades of genetic variation in an isolated Danish population of the large blue butterfly Maculinea arion
VL - 11
ER -
TY - JOUR
AB - What determines the genetic contribution that an individual makes to future generations? With biparental reproduction, each individual leaves a 'pedigree' of descendants, determined by the biparental relationships in the population. The pedigree of an individual constrains the lines of descent of each of its genes. An individual's reproductive value is the expected number of copies of each of its genes that is passed on to distant generations conditional on its pedigree. For the simplest model of biparental reproduction analogous to the Wright-Fisher model, an individual's reproductive value is determined within ~10 generations, independent of population size. Partial selfing and subdivision do not greatly slow this convergence. Our central result is that the probability that a gene will survive is proportional to the reproductive value of the individual that carries it, and that conditional on survival, after a few tens of generations, the distribution of the number of surviving copies is the same for all individuals, whatever their reproductive value. These results can be generalized to the joint distribution of surviving blocks of ancestral genome. Selection on unlinked loci in the genetic background may greatly increase the variance in reproductive value, but the above results nevertheless still hold. The almost linear relationship between survival probability and reproductive value also holds for weakly favored alleles. Thus, the influence of the complex pedigree of descendants on an individual's genetic contribution to the population can be summarized through a single number: its reproductive value.
AU - Barton, Nicholas H
AU - Etheridge, Alison
ID - 3390
IS - 4
JF - Genetics
TI - The relation between reproductive value and genetic contribution
VL - 188
ER -
TY - JOUR
AB - Evolutionary biology shares many concepts with statistical physics: both deal with populations, whether of molecules or organisms, and both seek to simplify evolution in very many dimensions. Often, methodologies have undergone parallel and independent development, as with stochastic methods in population genetics. Here, we discuss aspects of population genetics that have embraced methods from physics: non-equilibrium statistical mechanics, travelling waves and Monte-Carlo methods, among others, have been used to study polygenic evolution, rates of adaptation and range expansions. These applications indicate that evolutionary biology can further benefit from interactions with other areas of statistical physics; for example, by following the distribution of paths taken by a population through time
AU - de Vladar, Harold
AU - Barton, Nicholas H
ID - 3391
IS - 8
JF - Trends in Ecology and Evolution
TI - The contribution of statistical physics to evolutionary biology
VL - 26
ER -
TY - JOUR
AB - Unlike unconditionally advantageous “Fisherian” variants that tend to spread throughout a species range once introduced anywhere, “bistable” variants, such as chromosome translocations, have two alternative stable frequencies, absence and (near) fixation. Analogous to populations with Allee effects, bistable variants tend to increase locally only once they become sufficiently common, and their spread depends on their rate of increase averaged over all frequencies. Several proposed manipulations of insect populations, such as using Wolbachia or “engineered underdominance” to suppress vector-borne diseases, produce bistable rather than Fisherian dynamics. We synthesize and extend theoretical analyses concerning three features of their spatial behavior: rate of spread, conditions to initiate spread from a localized introduction, and wave stopping caused by variation in population densities or dispersal rates. Unlike Fisherian variants, bistable variants tend to spread spatially only for particular parameter combinations and initial conditions. Wave initiation requires introduction over an extended region, while subsequent spatial spread is slower than for Fisherian waves and can easily be halted by local spatial inhomogeneities. We present several new results, including robust sufficient conditions to initiate (and stop) spread, using a one-parameter cubic approximation applicable to several models. The results have both basic and applied implications.
AU - Barton, Nicholas H
AU - Turelli, Michael
ID - 3393
IS - 3
JF - American Naturalist
TI - Spatial waves of advance with bistable dynamics: Cytoplasmic and genetic analogues of Allee effects
VL - 178
ER -
TY - JOUR
AB - Random genetic drift shifts clines in space, alters their width, and distorts their shape. Such random fluctuations complicate inferences from cline width and position. Notably, the effect of genetic drift on the expected shape of the cline is opposite to the naive (but quite common) misinterpretation of classic results on the expected cline. While random drift on average broadens the overall cline in expected allele frequency, it narrows the width of any particular cline. The opposing effects arise because locally, drift drives alleles to fixation—but fluctuations in position widen the expected cline. The effect of genetic drift can be predicted from standardized variance in allele frequencies, averaged across the habitat: 〈F〉. A cline maintained by spatially varying selection (step change) is expected to be narrower by a factor of relative to the cline in the absence of drift. The expected cline is broader by the inverse of this factor. In a tension zone maintained by underdominance, the expected cline width is narrower by about 1 – 〈F〉relative to the width in the absence of drift. Individual clines can differ substantially from the expectation, and we give quantitative predictions for the variance in cline position and width. The predictions apply to clines in almost one-dimensional circumstances such as hybrid zones in rivers, deep valleys, or along a coast line and give a guide to what patterns to expect in two dimensions.
AU - Polechova, Jitka
AU - Barton, Nicholas H
ID - 3394
IS - 1
JF - Genetics
TI - Genetic drift widens the expected cline but narrows the expected cline width
VL - 189
ER -
TY - JOUR
AB - Facial branchiomotor neurons (FBMNs) in zebrafish and mouse embryonic hindbrain undergo a characteristic tangential migration from rhombomere (r) 4, where they are born, to r6/7. Cohesion among neuroepithelial cells (NCs) has been suggested to function in FBMN migration by inhibiting FBMNs positioned in the basal neuroepithelium such that they move apically between NCs towards the midline of the neuroepithelium instead of tangentially along the basal side of the neuroepithelium towards r6/7. However, direct experimental evaluation of this hypothesis is still lacking. Here, we have used a combination of biophysical cell adhesion measurements and high-resolution time-lapse microscopy to determine the role of NC cohesion in FBMN migration. We show that reducing NC cohesion by interfering with Cadherin 2 (Cdh2) activity results in FBMNs positioned at the basal side of the neuroepithelium moving apically towards the neural tube midline instead of tangentially towards r6/7. In embryos with strongly reduced NC cohesion, ectopic apical FBMN movement frequently results in fusion of the bilateral FBMN clusters over the apical midline of the neural tube. By contrast, reducing cohesion among FBMNs by interfering with Contactin 2 (Cntn2) expression in these cells has little effect on apical FBMN movement, but reduces the fusion of the bilateral FBMN clusters in embryos with strongly diminished NC cohesion. These data provide direct experimental evidence that NC cohesion functions in tangential FBMN migration by restricting their apical movement.
AU - Stockinger, Petra
AU - Heisenberg, Carl-Philipp J
AU - Maître, Jean-Léon
ID - 3396
IS - 21
JF - Development
TI - Defective neuroepithelial cell cohesion affects tangential branchiomotor neuron migration in the zebrafish neural tube
VL - 138
ER -
TY - JOUR
AB - Recent advances in microscopy techniques and biophysical measurements have provided novel insight into the molecular, cellular and biophysical basis of cell adhesion. However, comparably little is known about a core element of cell–cell adhesion—the energy of adhesion at the cell–cell contact. In this review, we discuss approaches to understand the nature and regulation of adhesion energy, and propose strategies to determine adhesion energy between cells in vitro and in vivo.
AU - Maître, Jean-Léon
AU - Heisenberg, Carl-Philipp J
ID - 3397
IS - 5
JF - Current Opinion in Cell Biology
TI - The role of adhesion energy in controlling cell-cell contacts
VL - 23
ER -
TY - JOUR
AB - Context-dependent adjustment of mating tactics can drastically increase the mating success of behaviourally flexible animals. We used the ant Cardiocondyla obscurior as a model system to study adaptive adjustment of male mating tactics. This species shows a male diphenism of wingless fighter males and peaceful winged males. Whereas the wingless males stay and exclusively mate in the maternal colony, the mating behaviour of winged males is plastic. They copulate with female sexuals in their natal nests early in life but later disperse in search for sexuals outside. In this study, we observed the nest-leaving behaviour of winged males under different conditions and found that they adaptively adjust the timing of their dispersal to the availability of mating partners, as well as the presence, and even the type of competitors in their natal nests. In colonies with virgin female queens winged males stayed longest when they were the only male in the nest. They left earlier when mating partners were not available or when other males were present. In the presence of wingless, locally mating fighter males, winged males dispersed earlier than in the presence of docile, winged competitors. This suggests that C. obscurior males are capable of estimating their local breeding chances and adaptively adjust their dispersal behaviour in both an opportunistic and a risk-sensitive way, thus showing hitherto unknown behavioural plasticity in social insect males.
AU - Cremer, Sylvia
AU - Schrempf, Alexandra
AU - Heinze, Jürgen
ID - 3399
IS - 3
JF - PLoS One
TI - Competition and opportunity shape the reproductive tactics of males in the ant Cardiocondyla obscurior
VL - 6
ER -
TY - JOUR
AB - Glutamate is the major excitatory neurotransmitter in the mammalian central nervous system and gates non-selective cation channels. The origins of glutamate receptors are not well understood as they differ structurally and functionally from simple bacterial ligand-gated ion channels. Here we report the discovery of an ionotropic glutamate receptor that combines the typical eukaryotic domain architecture with the 'TXVGYG' signature sequence of the selectivity filter found in K+ channels. This receptor exhibits functional properties intermediate between bacterial and eukaryotic glutamate-gated ion channels, suggesting a link in the evolution of ionotropic glutamate receptors.
AU - Janovjak, Harald L
AU - Sandoz, Guillaume
AU - Isacoff, Ehud
ID - 3405
IS - 232
JF - Nature Communications
TI - Modern ionotropic glutamate receptor with a K+ selectivity signature sequence
VL - 2
ER -
TY - JOUR
AB - Cell migration on two-dimensional (2D) substrates follows entirely different rules than cell migration in three-dimensional (3D) environments. This is especially relevant for leukocytes that are able to migrate in the absence of adhesion receptors within the confined geometry of artificial 3D extracellular matrix scaffolds and within the interstitial space in vivo. Here, we describe in detail a simple and economical protocol to visualize dendritic cell migration in 3D collagen scaffolds along chemotactic gradients. This method can be adapted to other cell types and may serve as a physiologically relevant paradigm for the directed locomotion of most amoeboid cells.
AU - Sixt, Michael K
AU - Lämmermann, Tim
ID - 3505
JF - Cell Migration
TI - In vitro analysis of chemotactic leukocyte migration in 3D environments
VL - 769
ER -
TY - THES
AB - Chemokines organize immune cell trafficking by inducing either directed (tactic) or random (kinetic) migration and by activating integrins in order to support surface adhesion (haptic). Beyond that the same chemokines can establish clearly defined functional areas in secondary lymphoid organs. Until now it is unclear how chemokines can fulfill such diverse functions. One decisive prerequisite to explain these capacities is to know how chemokines are presented in tissue. In theory chemokines could occur either soluble or immobilized, and could be distributed either homogenously or as a concentration gradient. To dissect if and how the presenting mode of chemokines influences immune cells, I tested the response of dendritic cells (DCs) to differentially displayed chemokines. DCs are antigen presenting cells that reside in the periphery and migrate into draining lymph nodes (LNs) once exposed to inflammatory stimuli to activate naïve T cells. DCs are guided to and within the LN by the chemokine receptor CCR7, which has two ligands, the chemokines CCL19 and CCL21. Both CCR7 ligands are expressed by fibroblastic reticular cells in the LN, but differ in their ability to bind to heparan sulfate residues. CCL21 has a highly charged C-terminal extension, which mediates binding to anionic surfaces, whereas CCL19 is lacking such residues and likely distributes as a soluble molecule. This study shows that surface-bound CCL21 causes random, haptokinetic DC motility, which is confined to the chemokine coated area by insideout activation of β2 integrins that mediate cell binding to the surface. CCL19 on the other hand forms concentration gradients which trigger directional, chemotactic movement, but no surface adhesion. In addition DCs can actively manipulate this system by recruiting and activating serine proteases on their surfaces, which create - by proteolytically removing the adhesive C-terminus - a solubilized variant of CCL21 that functionally resembles CCL19. By generating a CCL21 concentration gradient DCs establish a positive feedback loop to recruit further DCs from the periphery to the CCL21 coated region. In addition DCs can sense chemotactic gradients as well as immobilized haptokinetic fields at the same time and integrate these signals. The result is chemotactically biased haptokinesis - directional migration confined to a chemokine coated track or area - which could explain the dynamic but spatially tightly controlled swarming leukocyte locomotion patterns that have been observed in lymphatic organs by intravital microscopists. The finding that DCs can approach soluble cues in a non-adhesive manner while they attach to surfaces coated with immobilized cues raises the question how these cells transmit intracellular forces to the environment, especially in the non-adherent migration mode. In order to migrate, cells have to generate and transmit force to the extracellular substrate. Force transmission is the prerequisite to procure an expansion of the leading edge and a forward motion of the whole cell body. In the current conceptions actin polymerization at the leading edge is coupled to extracellular ligands via the integrin family of transmembrane receptors, which allows the transmission of intracellular force. Against the paradigm of force transmission during migration, leukocytes, like DCs, are able to migrate in threedimensional environments without using integrin transmembrane receptors (Lämmermann et al., 2008). This reflects the biological function of leukocytes, as they can invade almost all tissues, whereby their migration has to be independent from the extracellular environment. How the cells can achieve this is unclear. For this study I examined DC migration in a defined threedimensional environment and highlighted actin-dynamics with the probe Lifeact-GFP. The result was that chemotactic DCs can switch between integrin-dependent and integrin- independent locomotion and can thereby adapt to the adhesive properties of their environment. If the cells are able to couple their actin cytoskeleton to the substrate, actin polymerization is entirely converted into protrusion. Without coupling the actin cortex undergoes slippage and retrograde actin flow can be observed. But retrograde actin flow can be completely compensated by higher actin polymerization rate keeping the migration velocity and the shape of the cells unaltered. Mesenchymal cells like fibroblast cannot balance the loss of adhesive interaction, cannot protrude into open space and, therefore, strictly depend on integrinmediated force coupling. This leukocyte specific phenomenon of “adaptive force transmission” endows these cells with the unique ability to transit and invade almost every type of tissue.
AU - Schumann, Kathrin
ID - 3275
TI - The role of chemotactic gradients in dendritic cell migration
ER -
TY - JOUR
AB - We report the switching behavior of the full bacterial flagellum system that includes the filament and the motor in wild-type Escherichia coli cells. In sorting the motor behavior by the clockwise bias, we find that the distributions of the clockwise (CW) and counterclockwise (CCW) intervals are either exponential or nonexponential with long tails. At low bias, CW intervals are exponentially distributed and CCW intervals exhibit long tails. At intermediate CW bias (0.5) both CW and CCW intervals are mainly exponentially distributed. A simple model suggests that these two distinct switching behaviors are governed by the presence of signaling noise within the chemotaxis network. Low noise yields exponentially distributed intervals, whereas large noise yields nonexponential behavior with long tails. These drastically different motor statistics may play a role in optimizing bacterial behavior for a wide range of environmental conditions.
AU - Park, Heungwon
AU - Oikonomou, Panos
AU - Guet, Calin C
AU - Cluzel, Philippe
ID - 6496
IS - 10
JF - Biophysical Journal
SN - 0006-3495
TI - Noise underlies switching behavior of the bacterial flagellum
VL - 101
ER -
TY - JOUR
AB - Imprinted genes are expressed primarily or exclusively from either the maternal or paternal allele, a phenomenon that occurs in flowering plants and mammals. Flowering plant imprinted gene expression has been described primarily in endosperm, a terminal nutritive tissue consumed by the embryo during seed development or after germination. Imprinted expression in Arabidopsis thaliana endosperm is orchestrated by differences in cytosine DNA methylation between the paternal and maternal genomes as well as by Polycomb group proteins. Currently, only 11 imprinted A. thaliana genes are known. Here, we use extensive sequencing of cDNA libraries to identify 9 paternally expressed and 34 maternally expressed imprinted genes in A. thaliana endosperm that are regulated by the DNA-demethylating glycosylase DEMETER, the DNA methyltransferase MET1, and/or the core Polycomb group protein FIE. These genes encode transcription factors, proteins involved in hormone signaling, components of the ubiquitin protein degradation pathway, regulators of histone and DNA methylation, and small RNA pathway proteins. We also identify maternally expressed genes that may be regulated by unknown mechanisms or deposited from maternal tissues. We did not detect any imprinted genes in the embryo. Our results show that imprinted gene expression is an extensive mechanistically complex phenomenon that likely affects multiple aspects of seed development.
AU - Hsieh, Tzung-Fu
AU - Shin, Juhyun
AU - Uzawa, Rie
AU - Silva, Pedro
AU - Cohen, Stephanie
AU - Bauer, Matthew J.
AU - Hashimoto, Meryl
AU - Kirkbride, Ryan C.
AU - Harada, John J.
AU - ZILBERMAN, Daniel
AU - Fischer, Robert L.
ID - 9483
IS - 5
JF - Proceedings of the National Academy of Sciences
SN - 0027-8424
TI - Regulation of imprinted gene expression in Arabidopsis endosperm
VL - 108
ER -
TY - GEN
AB - Little is known about chromatin remodeling events immediately after fertilization. A recent report by Autran et al. (2011) in Cell now shows that chromatin regulatory pathways that silence transposable elements are responsible for global delayed activation of gene expression in the early Arabidopsis embryo.
AU - ZILBERMAN, Daniel
ID - 9522
IS - 6
SN - 1534-5807
T2 - Developmental Cell
TI - Balancing parental contributions in plant embryonic gene activation
VL - 20
ER -
TY - JOUR
AB - We study the average order of the divisor function, as it ranges over the values of binary quartic forms that are reducible over ℚ.
AU - De La Bretèche, Régis
AU - Browning, Timothy D
ID - 232
IS - 646
JF - Journal fur die Reine und Angewandte Mathematik
TI - Le problème des diviseurs pour des formes binaires de degré 4
ER -
TY - CONF
AU - Frank, Rupert L
AU - Lieb, Élliott H
AU - Robert Seiringer
ID - 2322
TI - Equivalence of Sobolev inequalities and Lieb-Thirring inequalities
ER -
TY - CONF
AB - Since the first experimental realization of Bose-Einstein condensation in cold atomic gases in 1995 there has been a surge of activity in this field. Ingenious experiments have allowed us to probe matter close to zero temperature and reveal some of the fascinating effects quantum mechanics has bestowed on nature. It is a challenge for mathematical physicists to understand these various phenomena from first principles, that is, starting from the underlying many-body Schrödinger equation. Recent progress in this direction concerns mainly equilibrium properties of dilute, cold quantum gases. We shall explain some of the results in this article, and describe the mathematics involved in understanding these phenomena. Topics include the ground state energy and the free energy at positive temperature, the effect of interparticle interaction on the critical temperature for Bose-Einstein condensation, as well as the occurrence of superfluidity and quantized vortices in rapidly rotating gases.
AU - Robert Seiringer
ID - 2323
TI - Hot topics on cold gases
ER -
TY - CHAP
AB - We determine the sharp constant in the Hardy inequality for fractional Sobolev spaces on half-spaces. Our proof relies on a nonlinear and nonlocal version of the ground state representation.
AU - Frank, Rupert L
AU - Robert Seiringer
ID - 2324
T2 - Around the Research of Vladimir Maz'ya I
TI - Sharp fractional Hardy inequalities in half-spaces
VL - 11
ER -
TY - JOUR
AB - We study the eigenvalues of Schrödinger type operators T + λV and their asymptotic behavior in the small coupling limit λ → 0, in the case where the symbol of the kinetic energy, T (p), strongly degenerates on a non-trivial manifold of codimension one.
AU - Hainzl, Christian
AU - Robert Seiringer
ID - 2389
IS - 3
JF - Mathematische Nachrichten
TI - Asymptotic behavior of eigenvalues of Schrödinger type operators with degenerate kinetic energy
VL - 283
ER -
TY - JOUR
AB - The binding of polarons, or its absence, is an old and subtle topic. Here we prove two things rigorously. First, the transition from many-body collapse to the existence of a thermodynamic limit for N polarons occurs precisely at U=2α, where U is the electronic Coulomb repulsion and α is the polaron coupling constant. Second, if U is large enough, there is no multipolaron binding of any kind. Considering the known fact that there is binding for some U>2α, these conclusions are not obvious and their proof has been an open problem for some time.
AU - Frank, Rupert L
AU - Lieb, Élliott H
AU - Robert Seiringer
AU - Thomas, Lawrence E
ID - 2392
IS - 21
JF - Physical Review Letters
TI - Bipolaron and N-polaron binding energies
VL - 104
ER -
TY - JOUR
AB - Background: The availability of many gene alignments with overlapping taxon sets raises the question of which strategy is the best to infer species phylogenies from multiple gene information. Methods and programs abound that use the gene alignment in different ways to reconstruct the species tree. In particular, different methods combine the original data at different points along the way from the underlying sequences to the final tree. Accordingly, they are classified into superalignment, supertree and medium-level approaches. Here, we present a simulation study to compare different methods from each of these three approaches.
Results: We observe that superalignment methods usually outperform the other approaches over a wide range of parameters including sparse data and gene-specific evolutionary parameters. In the presence of high incongruency among gene trees, however, other combination methods show better performance than the superalignment approach. Surprisingly, some supertree and medium-level methods exhibit, on average, worse results than a single gene phylogeny with complete taxon information.
Conclusions: For some methods, using the reconstructed gene tree as an estimation of the species tree is superior to the combination of incomplete information. Superalignment usually performs best since it is less susceptible to stochastic error. Supertree methods can outperform superalignment in the presence of gene-tree conflict.
AU - Kupczok, Anne
AU - Schmidt, Heiko
AU - Von Haeseler, Arndt
ID - 2409
IS - 1
JF - Algorithms for Molecular Biology
TI - Accuracy of phylogeny reconstruction methods combining overlapping gene data sets
VL - 5
ER -
TY - JOUR
AB - In a new study published in this issue of Developmental Cell, Krouk et al. reveal a surprising mechanism by which plant root systems adapt their architecture for soil exploitation. The dual transporter NRT1.1 uses both nitrate and the plant hormone auxin as substrates, enabling soil nitrate availability to regulate auxin-driven lateral root development.
AU - Beeckman, Tom
AU - Friml, Jirí
ID - 2442
IS - 6
JF - Developmental Cell
TI - Nitrate Contra Auxin: Nutrient Sensing by roots
VL - 18
ER -
TY - JOUR
AB - We consider N × N Hermitian random matrices with independent identically distributed entries (Wigner matrices). The matrices are normalized so that the average spacing between consecutive eigenvalues is of order 1/ N. Under suitable assumptions on the distribution of the single matrix element, we first prove that, away from the spectral edges, the empirical density of eigenvalues concentrates around the Wigner semicircle law on energy scales η ≫ N -1. This result establishes the semicircle law on the optimal scale and it removes a logarithmic factor from our previous result [6]. We then show a Wegner estimate, i.e., that the averaged density of states is bounded. Finally, we prove that the eigenvalues of a Wigner matrix repel each other, in agreement with the universality conjecture.
AU - László Erdös
AU - Schlein, Benjamin
AU - Yau, Horng-Tzer
ID - 2701
IS - 3
JF - International Mathematics Research Notices
TI - Wegner estimate and level repulsion for Wigner random matrices
ER -
TY - CONF
AB - Efficient zero-knowledge proofs of knowledge for group homomorphisms are essential for numerous systems in applied cryptography. Especially, Σ-protocols for proving knowledge of discrete logarithms in known and hidden order groups are of prime importance. Yet, while these proofs can be performed very efficiently within groups of known order, for hidden order groups the respective proofs are far less efficient.
This paper shows strong evidence that this efficiency gap cannot be bridged. Namely, while there are efficient protocols allowing a prover to cheat only with negligibly small probability in the case of known order groups, we provide strong evidence that for hidden order groups this probability is bounded below by 1/2 for all efficient Σ-protocols not using common reference strings or the like.
We prove our results for a comprehensive class of Σ-protocols in the generic group model, and further strengthen them by investigating certain instantiations in the plain model.
AU - Bangerter, Endre
AU - Camenisch, Jan
AU - Stephan Krenn
ED - Micciancio, Daniele
ID - 2978
TI - Efficiency Limitations for Σ-Protocols for Group Homomorphisms
VL - 5978
ER -
TY - CONF
AB - Zero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone.
We contribute to overcoming these challenges as follows: We present a comprehensive specification language and a compiler for ZK-PoK protocols based on Σ-protocols. The compiler allows the fully automatic translation of an abstract description of a proof goal into an executable implementation. Moreover, the compiler overcomes various restrictions of previous approaches, e.g., it supports the important class of exponentiation homomorphisms with hidden-order co-domain, needed for privacy-preserving applications such as DAA. Finally, our compiler is certifying, in the sense that it automatically produces a formal proof of the soundness of the compiled protocol for a large class of protocols using the Isabelle/HOL theorem prover.
AU - Almeida, José Bacelar
AU - Bangerter, Endre
AU - Barbosa, Manuel
AU - Stephan Krenn
AU - Sadeghi, Ahmad-Reza
AU - Schneider, Thomas
ED - Gritzalis, Dimitris
ED - Preneel, Bart
ED - Theoharidou, Marianthi
ID - 2979
TI - A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols
VL - 6345
ER -
TY - JOUR
AB - The epitaxial growth of germanium on silicon leads to the self-assembly of SiGe nanocrystals by a process that allows the size, composition and position of the nanocrystals to be controlled. This level of control, combined with an inherent compatibility with silicon technology, could prove useful in nanoelectronic applications. Here, we report the confinement of holes in quantum-dot devices made by directly contacting individual SiGe nanocrystals with aluminium electrodes, and the production of hybrid superconductor- semiconductor devices, such as resonant supercurrent transistors, when the quantum dot is strongly coupled to the electrodes. Charge transport measurements on weakly coupled quantum dots reveal discrete energy spectra, with the confined hole states displaying anisotropic gyromagnetic factors and strong spin-orbit coupling with pronounced dependences on gate voltage and magnetic field.
AU - Georgios Katsaros
AU - Spathis, Panayotis N
AU - Stoffel, Mathieu
AU - Fournel, Frank
AU - Mongillo, Massimo
AU - Bouchiat, Vincent
AU - Lefloch, François
AU - Rastelli, Armando
AU - Schmidt, Oliver G
AU - De Franceschi, Silvano
ID - 1752
IS - 6
JF - Nature Nanotechnology
TI - Hybrid superconductor-semiconductor devices made from self-assembled SiGe nanocrystals on silicon
VL - 5
ER -
TY - JOUR
AB - We investigate electronic transport in n-i-n GaN nanowires with and without AlN double barriers. The nanowires are grown by catalyst-free, plasma-assisted molecular beam epitaxy enabling abrupt GaN/AlN interfaces as well as longitudinal n-type doping modulation. At low temperature, transport in n-i-n GaN nanowires is dominated by the Coulomb blockade effect. Carriers are confined in the undoped middle region, forming single or multiple islands with a characteristic length of ∼100 nm. The incorporation of two AlN tunnel barriers causes confinement to occur within the GaN dot in between. In the case of a 6 nm thick dot and 2 nm thick barriers, we observe characteristic signatures of Coulomb-blockaded transport in single quantum dots with discrete energy states. For thinner dots and barriers, Coulomb-blockade effects do not play a significant role while the onset of resonant tunneling via the confined quantum levels is accompanied by a negative differential resistance surviving up to ∼150 K.
AU - Songmuang, Rudeeson
AU - Georgios Katsaros
AU - Monroy, Eva
AU - Spathis, Panayotis N
AU - Bougerol, Catherine
AU - Mongillo, Massimo
AU - De Franceschi, Silvano
ID - 1753
IS - 9
JF - Nano Letters
TI - Quantum transport in GaN/AlN double-barrier heterostructure nanowires
VL - 10
ER -
TY - JOUR
AB - The quantum properties of electromagnetic, mechanical or other harmonic oscillators can be revealed by investigating their strong coherent coupling to a single quantum two level system in an approach known as cavity quantum electrodynamics (QED). At temperatures much lower than the characteristic energy level spacing the observation of vacuum Rabi oscillations or mode splittings with one or a few quanta asserts the quantum nature of the oscillator. Here, we study how the classical response of a cavity QED system emerges from the quantum one when its thermal occupation-or effective temperature-is raised gradually over 5 orders of magnitude. In this way we explore in detail the continuous quantum-to-classical crossover and demonstrate how to extract effective cavity field temperatures from both spectroscopic and time-resolved vacuum Rabi measurements.
AU - Johannes Fink
AU - Steffen, L. Kraig
AU - Studer, Peter
AU - Bishop, Lev S
AU - Baur, Matthias P
AU - Bianchetti, R
AU - Bozyigit, Deniz
AU - Lang, C
AU - Filipp, Stefan
AU - Leek, Peter J
AU - Wallraff, Andreas
ID - 1773
IS - 16
JF - Physical Review Letters
TI - Quantum-to-classical transition in cavity quantum electrodynamics
VL - 105
ER -