TY - JOUR
AB - D-cycloserine ameliorates breathing abnormalities and survival rate in a mouse model of Rett syndrome.
AU - Novarino, Gaia
ID - 715
IS - 405
JF - Science Translational Medicine
SN - 19466234
TI - More excitation for Rett syndrome
VL - 9
ER -
TY - JOUR
AB - Two-player games on graphs are central in many problems in formal verification and program analysis, such as synthesis and verification of open systems. In this work, we consider solving recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion.While pushdown games have been studied before with qualitative objectives-such as reachability and ?-regular objectives- in this work, we study for the first time such games with the most well-studied quantitative objective, the mean-payoff objective. In pushdown games, two types of strategies are relevant: (1) global strategies, which depend on the entire global history; and (2) modular strategies, which have only local memory and thus do not depend on the context of invocation but rather only on the history of the current invocation of the module. Our main results are as follows: (1) One-player pushdown games with mean-payoff objectives under global strategies are decidable in polynomial time. (2) Two-player pushdown games with mean-payoff objectives under global strategies are undecidable. (3) One-player pushdown games with mean-payoff objectives under modular strategies are NP-hard. (4) Two-player pushdown games with mean-payoff objectives under modular strategies can be solved in NP (i.e., both one-player and two-player pushdown games with mean-payoff objectives under modular strategies are NP-complete). We also establish the optimal strategy complexity by showing that global strategies for mean-payoff objectives require infinite memory even in one-player pushdown games and memoryless modular strategies are sufficient in two-player pushdown games. Finally, we also show that all the problems have the same complexity if the stack boundedness condition is added, where along with the mean-payoff objective the player must also ensure that the stack height is bounded.
AU - Chatterjee, Krishnendu
AU - Velner, Yaron
ID - 716
IS - 5
JF - Journal of the ACM
SN - 00045411
TI - The complexity of mean-payoff pushdown games
VL - 64
ER -
TY - DATA
AB - The de novo genome assemblies generated for this study, and the associated metadata.
AU - Fraisse, Christelle
ID - 7163
TI - Supplementary Files for "The deep conservation of the Lepidoptera Z chromosome suggests a non canonical origin of the W"
ER -
TY - JOUR
AB - We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard.
AU - Chatterjee, Krishnendu
AU - Velner, Yaron
ID - 717
JF - Journal of Computer and System Sciences
TI - Hyperplane separation technique for multidimensional mean-payoff games
VL - 88
ER -
TY - JOUR
AB - Mapping every simplex in the Delaunay mosaic of a discrete point set to the radius of the smallest empty circumsphere gives a generalized discrete Morse function. Choosing the points from a Poisson point process in ℝ n , we study the expected number of simplices in the Delaunay mosaic as well as the expected number of critical simplices and nonsingular intervals in the corresponding generalized discrete gradient. Observing connections with other probabilistic models, we obtain precise expressions for the expected numbers in low dimensions. In particular, we obtain the expected numbers of simplices in the Poisson–Delaunay mosaic in dimensions n ≤ 4.
AU - Edelsbrunner, Herbert
AU - Nikitenko, Anton
AU - Reitzner, Matthias
ID - 718
IS - 3
JF - Advances in Applied Probability
SN - 00018678
TI - Expected sizes of poisson Delaunay mosaics and their discrete Morse functions
VL - 49
ER -
TY - JOUR
AB - The ubiquity of computation in modern machines and devices imposes a need to assert the correctness of their behavior. Especially in the case of safety-critical systems, their designers need to take measures that enforce their safe operation. Formal methods has emerged as a research field that addresses this challenge: by rigorously proving that all system executions adhere to their specifications, the correctness of an implementation under concern can be assured. To achieve this goal, a plethora of techniques are nowadays available, all of which are optimized for different system types and application domains.
AU - Chatterjee, Krishnendu
AU - Ehlers, Rüdiger
ID - 719
IS - 6
JF - Acta Informatica
SN - 00015903
TI - Special issue: Synthesis and SYNT 2014
VL - 54
ER -
TY - JOUR
AB - Advances in multi-unit recordings pave the way for statistical modeling of activity patterns in large neural populations. Recent studies have shown that the summed activity of all neurons strongly shapes the population response. A separate recent finding has been that neural populations also exhibit criticality, an anomalously large dynamic range for the probabilities of different population activity patterns. Motivated by these two observations, we introduce a class of probabilistic models which takes into account the prior knowledge that the neural population could be globally coupled and close to critical. These models consist of an energy function which parametrizes interactions between small groups of neurons, and an arbitrary positive, strictly increasing, and twice differentiable function which maps the energy of a population pattern to its probability. We show that: 1) augmenting a pairwise Ising model with a nonlinearity yields an accurate description of the activity of retinal ganglion cells which outperforms previous models based on the summed activity of neurons; 2) prior knowledge that the population is critical translates to prior expectations about the shape of the nonlinearity; 3) the nonlinearity admits an interpretation in terms of a continuous latent variable globally coupling the system whose distribution we can infer from data. Our method is independent of the underlying system’s state space; hence, it can be applied to other systems such as natural scenes or amino acid sequences of proteins which are also known to exhibit criticality.
AU - Humplik, Jan
AU - Tkacik, Gasper
ID - 720
IS - 9
JF - PLoS Computational Biology
SN - 1553734X
TI - Probabilistic models for neural populations that naturally capture global coupling and criticality
VL - 13
ER -
TY - JOUR
AB - Let S be a positivity-preserving symmetric linear operator acting on bounded functions. The nonlinear equation -1/m=z+Sm with a parameter z in the complex upper half-plane ℍ has a unique solution m with values in ℍ. We show that the z-dependence of this solution can be represented as the Stieltjes transforms of a family of probability measures v on ℝ. Under suitable conditions on S, we show that v has a real analytic density apart from finitely many algebraic singularities of degree at most 3. Our motivation comes from large random matrices. The solution m determines the density of eigenvalues of two prominent matrix ensembles: (i) matrices with centered independent entries whose variances are given by S and (ii) matrices with correlated entries with a translation-invariant correlation structure. Our analysis shows that the limiting eigenvalue density has only square root singularities or cubic root cusps; no other singularities occur.
AU - Ajanki, Oskari H
AU - Krüger, Torben H
AU - Erdös, László
ID - 721
IS - 9
JF - Communications on Pure and Applied Mathematics
SN - 00103640
TI - Singularities of solutions to quadratic vector equations on the complex upper half plane
VL - 70
ER -
TY - JOUR
AB - Plants are sessile organisms rooted in one place. The soil resources that plants require are often distributed in a highly heterogeneous pattern. To aid foraging, plants have evolved roots whose growth and development are highly responsive to soil signals. As a result, 3D root architecture is shaped by myriad environmental signals to ensure resource capture is optimised and unfavourable environments are avoided. The first signals sensed by newly germinating seeds — gravity and light — direct root growth into the soil to aid seedling establishment. Heterogeneous soil resources, such as water, nitrogen and phosphate, also act as signals that shape 3D root growth to optimise uptake. Root architecture is also modified through biotic interactions that include soil fungi and neighbouring plants. This developmental plasticity results in a ‘custom-made’ 3D root system that is best adapted to forage for resources in each soil environment that a plant colonises.
AU - Morris, Emily
AU - Griffiths, Marcus
AU - Golebiowska, Agata
AU - Mairhofer, Stefan
AU - Burr Hersey, Jasmine
AU - Goh, Tatsuaki
AU - Von Wangenheim, Daniel
AU - Atkinson, Brian
AU - Sturrock, Craig
AU - Lynch, Jonathan
AU - Vissenberg, Kris
AU - Ritz, Karl
AU - Wells, Darren
AU - Mooney, Sacha
AU - Bennett, Malcolm
ID - 722
IS - 17
JF - Current Biology
SN - 09609822
TI - Shaping 3D root system architecture
VL - 27
ER -
TY - JOUR
AB - We investigate the stationary and dynamical behavior of an Anderson localized chain coupled to a single central bound state. Although this coupling partially dilutes the Anderson localized peaks towards nearly resonant sites, the most weight of the original peaks remains unchanged. This leads to multifractal wave functions with a frozen spectrum of fractal dimensions, which is characteristic for localized phases in models with power-law hopping. Using a perturbative approach we identify two different dynamical regimes. At weak couplings to the central site, the transport of particles and information is logarithmic in time, a feature usually attributed to many-body localization. We connect such transport to the persistence of the Poisson statistics of level spacings in parts of the spectrum. In contrast, at stronger couplings the level repulsion is established in the entire spectrum, the problem can be mapped to the Fano resonance, and the transport is ballistic.
AU - Hetterich, Daniel
AU - Serbyn, Maksym
AU - Domínguez, Fernando
AU - Pollmann, Frank
AU - Trauzettel, Björn
ID - 724
IS - 10
JF - Physical Review B
SN - 24699950
TI - Noninteracting central site model localization and logarithmic entanglement growth
VL - 96
ER -
TY - JOUR
AB - Individual computations and social interactions underlying collective behavior in groups of animals are of great ethological, behavioral, and theoretical interest. While complex individual behaviors have successfully been parsed into small dictionaries of stereotyped behavioral modes, studies of collective behavior largely ignored these findings; instead, their focus was on inferring single, mode-independent social interaction rules that reproduced macroscopic and often qualitative features of group behavior. Here, we bring these two approaches together to predict individual swimming patterns of adult zebrafish in a group. We show that fish alternate between an “active” mode, in which they are sensitive to the swimming patterns of conspecifics, and a “passive” mode, where they ignore them. Using a model that accounts for these two modes explicitly, we predict behaviors of individual fish with high accuracy, outperforming previous approaches that assumed a single continuous computation by individuals and simple metric or topological weighing of neighbors’ behavior. At the group level, switching between active and passive modes is uncorrelated among fish, but correlated directional swimming behavior still emerges. Our quantitative approach for studying complex, multi-modal individual behavior jointly with emergent group behavior is readily extensible to additional behavioral modes and their neural correlates as well as to other species.
AU - Harpaz, Roy
AU - Tkacik, Gasper
AU - Schneidman, Elad
ID - 725
IS - 38
JF - PNAS
SN - 00278424
TI - Discrete modes of social information processing predict individual behavior of fish in a group
VL - 114
ER -
TY - JOUR
AB - The morphogenesis of branched organs remains a subject of abiding interest. Although much is known about the underlying signaling pathways, it remains unclear how macroscopic features of branched organs, including their size, network topology, and spatial patterning, are encoded. Here, we show that, in mouse mammary gland, kidney, and human prostate, these features can be explained quantitatively within a single unifying framework of branching and annihilating random walks. Based on quantitative analyses of large-scale organ reconstructions and proliferation kinetics measurements, we propose that morphogenesis follows from the proliferative activity of equipotent tips that stochastically branch and randomly explore their environment but compete neutrally for space, becoming proliferatively inactive when in proximity with neighboring ducts. These results show that complex branched epithelial structures develop as a self-organized process, reliant upon a strikingly simple but generic rule, without recourse to a rigid and deterministic sequence of genetically programmed events.
AU - Hannezo, Edouard B
AU - Scheele, Colinda
AU - Moad, Mohammad
AU - Drogo, Nicholas
AU - Heer, Rakesh
AU - Sampogna, Rosemary
AU - Van Rheenen, Jacco
AU - Simons, Benjamin
ID - 726
IS - 1
JF - Cell
SN - 00928674
TI - A unifying theory of branching morphogenesis
VL - 171
ER -
TY - JOUR
AB - Actin filaments polymerizing against membranes power endocytosis, vesicular traffic, and cell motility. In vitro reconstitution studies suggest that the structure and the dynamics of actin networks respond to mechanical forces. We demonstrate that lamellipodial actin of migrating cells responds to mechanical load when membrane tension is modulated. In a steady state, migrating cell filaments assume the canonical dendritic geometry, defined by Arp2/3-generated 70° branch points. Increased tension triggers a dense network with a broadened range of angles, whereas decreased tension causes a shift to a sparse configuration dominated by filaments growing perpendicularly to the plasma membrane. We show that these responses emerge from the geometry of branched actin: when load per filament decreases, elongation speed increases and perpendicular filaments gradually outcompete others because they polymerize the shortest distance to the membrane, where they are protected from capping. This network-intrinsic geometrical adaptation mechanism tunes protrusive force in response to mechanical load.
AU - Mueller, Jan
AU - Szep, Gregory
AU - Nemethova, Maria
AU - De Vries, Ingrid
AU - Lieber, Arnon
AU - Winkler, Christoph
AU - Kruse, Karsten
AU - Small, John
AU - Schmeiser, Christian
AU - Keren, Kinneret
AU - Hauschild, Robert
AU - Sixt, Michael K
ID - 727
IS - 1
JF - Cell
SN - 00928674
TI - Load adaptation of lamellipodial actin networks
VL - 171
ER -
TY - JOUR
AB - During animal development, cell-fate-specific changes in gene expression can modify the material properties of a tissue and drive tissue morphogenesis. While mechanistic insights into the genetic control of tissue-shaping events are beginning to emerge, how tissue morphogenesis and mechanics can reciprocally impact cell-fate specification remains relatively unexplored. Here we review recent findings reporting how multicellular morphogenetic events and their underlying mechanical forces can feed back into gene regulatory pathways to specify cell fate. We further discuss emerging techniques that allow for the direct measurement and manipulation of mechanical signals in vivo, offering unprecedented access to study mechanotransduction during development. Examination of the mechanical control of cell fate during tissue morphogenesis will pave the way to an integrated understanding of the design principles that underlie robust tissue patterning in embryonic development.
AU - Chan, Chii
AU - Heisenberg, Carl-Philipp J
AU - Hiiragi, Takashi
ID - 728
IS - 18
JF - Current Biology
SN - 09609822
TI - Coordination of morphogenesis and cell fate specification in development
VL - 27
ER -
TY - JOUR
AB - The cellular mechanisms allowing tissues to efficiently regenerate are not fully understood. In this issue of Developmental Cell, Cao et al. (2017)) discover that during zebrafish heart regeneration, epicardial cells at the leading edge of regenerating tissue undergo endoreplication, possibly due to increased tissue tension, thereby boosting their regenerative capacity.
AU - Spiro, Zoltan P
AU - Heisenberg, Carl-Philipp J
ID - 729
IS - 6
JF - Developmental Cell
SN - 15345807
TI - Regeneration tensed up polyploidy takes the lead
VL - 42
ER -
TY - JOUR
AB - Neural responses are highly structured, with population activity restricted to a small subset of the astronomical range of possible activity patterns. Characterizing these statistical regularities is important for understanding circuit computation, but challenging in practice. Here we review recent approaches based on the maximum entropy principle used for quantifying collective behavior in neural activity. We highlight recent models that capture population-level statistics of neural data, yielding insights into the organization of the neural code and its biological substrate. Furthermore, the MaxEnt framework provides a general recipe for constructing surrogate ensembles that preserve aspects of the data, but are otherwise maximally unstructured. This idea can be used to generate a hierarchy of controls against which rigorous statistical tests are possible.
AU - Savin, Cristina
AU - Tkacik, Gasper
ID - 730
JF - Current Opinion in Neurobiology
SN - 09594388
TI - Maximum entropy models as a tool for building precise neural controls
VL - 46
ER -
TY - JOUR
AB - Genetic variations in the oxytocin receptor gene affect patients with ASD and ADHD differently.
AU - Novarino, Gaia
ID - 731
IS - 411
JF - Science Translational Medicine
SN - 19466234
TI - The science of love in ASD and ADHD
VL - 9
ER -
TY - JOUR
AB - Background: Social insects form densely crowded societies in environments with high pathogen loads, but have evolved collective defences that mitigate the impact of disease. However, colony-founding queens lack this protection and suffer high rates of mortality. The impact of pathogens may be exacerbated in species where queens found colonies together, as healthy individuals may contract pathogens from infectious co-founders. Therefore, we tested whether ant queens avoid founding colonies with pathogen-exposed conspecifics and how they might limit disease transmission from infectious individuals. Results: Using Lasius Niger queens and a naturally infecting fungal pathogen Metarhizium brunneum, we observed that queens were equally likely to found colonies with another pathogen-exposed or sham-treated queen. However, when one queen died, the surviving individual performed biting, burial and removal of the corpse. These undertaking behaviours were performed prophylactically, i.e. targeted equally towards non-infected and infected corpses, as well as carried out before infected corpses became infectious. Biting and burial reduced the risk of the queens contracting and dying from disease from an infectious corpse of a dead co-foundress. Conclusions: We show that co-founding ant queens express undertaking behaviours that, in mature colonies, are performed exclusively by workers. Such infection avoidance behaviours act before the queens can contract the disease and will therefore improve the overall chance of colony founding success in ant queens.
AU - Pull, Christopher
AU - Cremer, Sylvia
ID - 732
IS - 1
JF - BMC Evolutionary Biology
SN - 14712148
TI - Co-founding ant queens prevent disease by performing prophylactic undertaking behaviour
VL - 17
ER -
TY - JOUR
AB - Let A and B be two N by N deterministic Hermitian matrices and let U be an N by N Haar distributed unitary matrix. It is well known that the spectral distribution of the sum H = A + UBU∗ converges weakly to the free additive convolution of the spectral distributions of A and B, as N tends to infinity. We establish the optimal convergence rate in the bulk of the spectrum.
AU - Bao, Zhigang
AU - Erdös, László
AU - Schnelli, Kevin
ID - 733
JF - Advances in Mathematics
TI - Convergence rate for spectral distribution of addition of random matrices
VL - 319
ER -
TY - JOUR
AB - Social insect societies are long-standing models for understanding social behaviour and evolution. Unlike other advanced biological societies (such as the multicellular body), the component parts of social insect societies can be easily deconstructed and manipulated. Recent methodological and theoretical innovations have exploited this trait to address an expanded range of biological questions. We illustrate the broadening range of biological insight coming from social insect biology with four examples. These new frontiers promote open-minded, interdisciplinary exploration of one of the richest and most complex of biological phenomena: sociality.
AU - Kennedy, Patrick
AU - Baron, Gemma
AU - Qiu, Bitao
AU - Freitak, Dalial
AU - Helantera, Heikki
AU - Hunt, Edmund
AU - Manfredini, Fabio
AU - O'Shea Wheller, Thomas
AU - Patalano, Solenn
AU - Pull, Christopher
AU - Sasaki, Takao
AU - Taylor, Daisy
AU - Wyatt, Christopher
AU - Sumner, Seirian
ID - 734
IS - 11
JF - Trends in Ecology and Evolution
SN - 01695347
TI - Deconstructing superorganisms and societies to address big questions in biology
VL - 32
ER -
TY - JOUR
AB - Cell-cell contact formation constitutes an essential step in evolution, leading to the differentiation of specialized cell types. However, remarkably little is known about whether and how the interplay between contact formation and fate specification affects development. Here, we identify a positive feedback loop between cell-cell contact duration, morphogen signaling, and mesendoderm cell-fate specification during zebrafish gastrulation. We show that long-lasting cell-cell contacts enhance the competence of prechordal plate (ppl) progenitor cells to respond to Nodal signaling, required for ppl cell-fate specification. We further show that Nodal signaling promotes ppl cell-cell contact duration, generating a positive feedback loop between ppl cell-cell contact duration and cell-fate specification. Finally, by combining mathematical modeling and experimentation, we show that this feedback determines whether anterior axial mesendoderm cells become ppl or, instead, turn into endoderm. Thus, the interdependent activities of cell-cell signaling and contact formation control fate diversification within the developing embryo.
AU - Barone, Vanessa
AU - Lang, Moritz
AU - Krens, Gabriel
AU - Pradhan, Saurabh
AU - Shamipour, Shayan
AU - Sako, Keisuke
AU - Sikora, Mateusz K
AU - Guet, Calin C
AU - Heisenberg, Carl-Philipp J
ID - 735
IS - 2
JF - Developmental Cell
SN - 15345807
TI - An effective feedback loop between cell-cell contact duration and morphogen signaling determines cell fate
VL - 43
ER -
TY - JOUR
AB - The neurotransmitter receptor subtype, number, density, and distribution relative to the location of transmitter release sites are key determinants of signal transmission. AMPA-type ionotropic glutamate receptors (AMPARs) containing GluA3 and GluA4 subunits are prominently expressed in subsets of neurons capable of firing action potentials at high frequencies, such as auditory relay neurons. The auditory nerve (AN) forms glutamatergic synapses on two types of relay neurons, bushy cells (BCs) and fusiform cells (FCs) of the cochlear nucleus. AN-BC and AN-FC synapses have distinct kinetics; thus, we investigated whether the number, density, and localization of GluA3 and GluA4 subunits in these synapses are differentially organized using quantitative freeze-fracture replica immunogold labeling. We identify a positive correlation between the number of AMPARs and the size of AN-BC and AN-FC synapses. Both types of AN synapses have similar numbers of AMPARs; however, the AN-BC have a higher density of AMPARs than AN-FC synapses, because the AN-BC synapses are smaller. A higher number and density of GluA3 subunits are observed at AN-BC synapses, whereas a higher number and density of GluA4 subunits are observed at AN-FC synapses. The intrasynaptic distribution of immunogold labeling revealed that AMPAR subunits, particularly GluA3, are concentrated at the center of the AN-BC synapses. The central distribution of AMPARs is absent in GluA3-knockout mice, and gold particles are evenly distributed along the postsynaptic density. GluA4 gold labeling was homogenously distributed along both synapse types. Thus, GluA3 and GluA4 subunits are distributed at AN synapses in a target-cell-dependent manner.
AU - Rubio, María
AU - Matsui, Ko
AU - Fukazawa, Yugo
AU - Kamasawa, Naomi
AU - Harada, Harumi
AU - Itakura, Makoto
AU - Molnár, Elek
AU - Abe, Manabu
AU - Sakimura, Kenji
AU - Shigemoto, Ryuichi
ID - 736
IS - 8
JF - Brain Structure and Function
SN - 18632653
TI - The number and distribution of AMPA receptor channels containing fast kinetic GluA3 and GluA4 subunits at auditory nerve synapses depend on the target cells
VL - 222
ER -
TY - JOUR
AB - Inflammation, which is a highly regulated host response against danger signals, may be harmful if it is excessive and deregulated. Ideally, anti-inflammatory therapy should autonomously commence as soon as possible after the onset of inflammation, should be controllable by a physician, and should not systemically block beneficial immune response in the long term. We describe a genetically encoded anti-inflammatory mammalian cell device based on a modular engineered genetic circuit comprising a sensor, an amplifier, a “thresholder” to restrict activation of a positive-feedback loop, a combination of advanced clinically used biopharmaceutical proteins, and orthogonal regulatory elements that linked modules into the functional device. This genetic circuit was autonomously activated by inflammatory signals, including endogenous cecal ligation and puncture (CLP)-induced inflammation in mice and serum from a systemic juvenile idiopathic arthritis (sIJA) patient, and could be reset externally by a chemical signal. The microencapsulated anti-inflammatory device significantly reduced the pathology in dextran sodium sulfate (DSS)-induced acute murine colitis, demonstrating a synthetic immunological approach for autonomous anti-inflammatory therapy.
AU - Smole, Anže
AU - Lainšček, Duško
AU - Bezeljak, Urban
AU - Horvat, Simon
AU - Jerala, Roman
ID - 7360
IS - 1
JF - Molecular Therapy
SN - 1525-0016
TI - A synthetic mammalian therapeutic gene circuit for sensing and suppressing inflammation
VL - 25
ER -
TY - JOUR
AB - We generalize Brazas’ topology on the fundamental group to the whole universal path space X˜ i.e., to the set of homotopy classes of all based paths. We develop basic properties of the new notion and provide a complete comparison of the obtained topology with the established topologies, in particular with the Lasso topology and the CO topology, i.e., the topology that is induced by the compact-open topology. It turns out that the new topology is the finest topology contained in the CO topology, for which the action of the fundamental group on the universal path space is a continuous group action.
AU - Virk, Ziga
AU - Zastrow, Andreas
ID - 737
JF - Topology and its Applications
SN - 01668641
TI - A new topology on the universal path space
VL - 231
ER -
TY - JOUR
AB - We study the norm approximation to the Schrödinger dynamics of N bosons in with an interaction potential of the form . Assuming that in the initial state the particles outside of the condensate form a quasi-free state with finite kinetic energy, we show that in the large N limit, the fluctuations around the condensate can be effectively described using Bogoliubov approximation for all . The range of β is expected to be optimal for this large class of initial states.
AU - Nam, Phan
AU - Napiórkowski, Marcin M
ID - 739
IS - 5
JF - Journal de Mathématiques Pures et Appliquées
SN - 00217824
TI - A note on the validity of Bogoliubov correction to mean field dynamics
VL - 108
ER -
TY - JOUR
AB - Developments in bioengineering and molecular biology have introduced a palette of genetically encoded probes for identification of specific cell populations in electron microscopy. These probes can be targeted to distinct cellular compartments, rendering them electron dense through a subsequent chemical reaction. These electron densities strongly increase the local contrast in samples prepared for electron microscopy, allowing three major advances in ultrastructural mapping of circuits: genetic identification of circuit components, targeted imaging of regions of interest and automated analysis of the tagged circuits. Together, the gains from these advances can decrease the time required for the analysis of targeted circuit motifs by over two orders of magnitude. These genetic encoded tags for electron microscopy promise to simplify the analysis of circuit motifs and become a central tool for structure‐function studies of synaptic connections in the brain. We review the current state‐of‐the‐art with an emphasis on connectomics, the quantitative analysis of neuronal structures and motifs.
AU - Shigemoto, Ryuichi
AU - Jösch, Maximilian A
ID - 740
IS - 6
JF - WIREs Developmental Biology
SN - 17597684
TI - The genetic encoded toolbox for electron microscopy and connectomics
VL - 6
ER -
TY - JOUR
AB - We prove that a system of N fermions interacting with an additional particle via point interactions is stable if the ratio of the mass of the additional particle to the one of the fermions is larger than some critical m*. The value of m* is independent of N and turns out to be less than 1. This fact has important implications for the stability of the unitary Fermi gas. We also characterize the domain of the Hamiltonian of this model, and establish the validity of the Tan relations for all wave functions in the domain.
AU - Moser, Thomas
AU - Seiringer, Robert
ID - 741
IS - 1
JF - Communications in Mathematical Physics
SN - 00103616
TI - Stability of a fermionic N+1 particle system with point interactions
VL - 356
ER -
TY - JOUR
AB - This special issue of the Journal on Formal Methods in System Design is dedicated to Prof. Helmut Veith, who unexpectedly passed away in March 2016. Helmut Veith was a brilliant researcher, inspiring collaborator, passionate mentor, generous friend, and valued member of the formal methods community. Helmut was not only known for his numerous and influential contributions in the field of automated verification (most prominently his work on Counterexample-Guided Abstraction Refinement [1,2]), but also for his untiring and passionate efforts for the logic community: he co-organized the Vienna Summer of Logic (an event comprising twelve conferences and numerous workshops which attracted thousands of researchers from all over the world), he initiated the Vienna Center for Logic and Algorithms (which promotes international collaboration on logic and algorithms and organizes outreach events such as the LogicLounge), and he coordinated the Doctoral Program on Logical Methods in Computer Science at TU Wien (currently educating more than 40 doctoral students) and a National Research Network on Rigorous Systems Engineering (uniting fifteen researchers in Austria to address the challenge of building reliable and safe computer
systems). With his enthusiasm and commitment, Helmut completely reshaped the Austrian research landscape in the field of logic and verification in his few years as a full professor at TU Wien.
AU - Gottlob, Georg
AU - Henzinger, Thomas A
AU - Weißenbacher, Georg
ID - 743
IS - 2
JF - Formal Methods in System Design
TI - Preface of the special issue in memoriam Helmut Veith
VL - 51
ER -
TY - JOUR
AB - In evolutionary game theory interactions between individuals are often assumed obligatory. However, in many real-life situations, individuals can decide to opt out of an interaction depending on the information they have about the opponent. We consider a simple evolutionary game theoretic model to study such a scenario, where at each encounter between two individuals the type of the opponent (cooperator/defector) is known with some probability, and where each individual either accepts or opts out of the interaction. If the type of the opponent is unknown, a trustful individual accepts the interaction, whereas a suspicious individual opts out of the interaction. If either of the two individuals opt out both individuals remain without an interaction. We show that in the prisoners dilemma optional interactions along with suspicious behaviour facilitates the emergence of trustful cooperation.
AU - Priklopil, Tadeas
AU - Chatterjee, Krishnendu
AU - Nowak, Martin
ID - 744
JF - Journal of Theoretical Biology
SN - 00225193
TI - Optional interactions and suspicious behaviour facilitates trustful cooperation in prisoners dilemma
VL - 433
ER -
TY - JOUR
AB - Fluid flows in nature and applications are frequently subject to periodic velocity modulations. Surprisingly, even for the generic case of flow through a straight pipe, there is little consensus regarding the influence of pulsation on the transition threshold to turbulence: while most studies predict a monotonically increasing threshold with pulsation frequency (i.e. Womersley number, ), others observe a decreasing threshold for identical parameters and only observe an increasing threshold at low . In the present study we apply recent advances in the understanding of transition in steady shear flows to pulsating pipe flow. For moderate pulsation amplitudes we find that the first instability encountered is subcritical (i.e. requiring finite amplitude disturbances) and gives rise to localized patches of turbulence ('puffs') analogous to steady pipe flow. By monitoring the impact of pulsation on the lifetime of turbulence we map the onset of turbulence in parameter space. Transition in pulsatile flow can be separated into three regimes. At small Womersley numbers the dynamics is dominated by the decay turbulence suffers during the slower part of the cycle and hence transition is delayed significantly. As shown in this regime thresholds closely agree with estimates based on a quasi-steady flow assumption only taking puff decay rates into account. The transition point predicted in the zero limit equals to the critical point for steady pipe flow offset by the oscillation Reynolds number (i.e. the dimensionless oscillation amplitude). In the high frequency limit on the other hand, puff lifetimes are identical to those in steady pipe flow and hence the transition threshold appears to be unaffected by flow pulsation. In the intermediate frequency regime the transition threshold sharply drops (with increasing ) from the decay dominated (quasi-steady) threshold to the steady pipe flow level.
AU - Xu, Duo
AU - Warnecke, Sascha
AU - Song, Baofang
AU - Ma, Xingyu
AU - Hof, Björn
ID - 745
JF - Journal of Fluid Mechanics
SN - 00221120
TI - Transition to turbulence in pulsating pipe flow
VL - 831
ER -
TY - JOUR
AB - Metabotropic glutamate receptor subtype 5 (mGluR5) is crucially implicated in the pathophysiology of Fragile X Syndrome (FXS); however, its dysfunction at the sub-cellular level, and related synaptic and cognitive phenotypes are unexplored. Here, we probed the consequences of mGluR5/Homer scaffold disruption for mGluR5 cell-surface mobility, synaptic N-methyl-D-Aspartate receptor (NMDAR) function, and behavioral phenotypes in the second-generation Fmr1 knockout (KO) mouse. Using single-molecule tracking, we found that mGluR5 was significantly more mobile at synapses in hippocampal Fmr1 KO neurons, causing an increased synaptic surface co-clustering of mGluR5 and NMDAR. This correlated with a reduced amplitude of synaptic NMDAR currents, a lack of their mGluR5-Activated long-Term depression, and NMDAR/hippocampus dependent cognitive deficits. These synaptic and behavioral phenomena were reversed by knocking down Homer1a in Fmr1 KO mice. Our study provides a mechanistic link between changes of mGluR5 dynamics and pathological phenotypes of FXS, unveiling novel targets for mGluR5-based therapeutics.
AU - Aloisi, Elisabetta
AU - Le Corf, Katy
AU - Dupuis, Julien
AU - Zhang, Pei
AU - Ginger, Melanie
AU - Labrousse, Virginie
AU - Spatuzza, Michela
AU - Georg Haberl, Matthias
AU - Costa, Lara
AU - Shigemoto, Ryuichi
AU - Tappe Theodor, Anke
AU - Drago, Fillippo
AU - Vincenzo Piazza, Pier
AU - Mulle, Christophe
AU - Groc, Laurent
AU - Ciranna, Lucia
AU - Catania, Maria
AU - Frick, Andreas
ID - 746
IS - 1
JF - Nature Communications
SN - 20411723
TI - Altered surface mGluR5 dynamics provoke synaptic NMDAR dysfunction and cognitive defects in Fmr1 knockout mice
VL - 8
ER -
TY - JOUR
AB - Bradykinin (BK), a component of the kallikrein-kininogen-kinin system exerts multiple effects via B1 and B2 receptor activation. In the cardiovascular system, bradykinin has cardioprotective and vasodilator properties. We investigated the effect of BK on cardiac-projecting neurons of nucleus ambiguus, a key site for the parasympathetic cardiac regulation. BK produced a dose-dependent increase in cytosolic Ca2+ concentration. Pretreatment with HOE140, a B2 receptor antagonist, but not with R715, a B1 receptor antagonist, abolished the response to BK. A selective B2 receptor agonist, but not a B1 receptor agonist, elicited an increase in cytosolic Ca2+ similarly to BK. Inhibition of N-type voltage-gated Ca2+ channels with ω-conotoxin GVIA had no effect on the Ca2+ signal produced by BK, while pretreatment with ω-conotoxin MVIIC, a blocker of P/Q-type of Ca2+ channels, significantly diminished the effect of BK. Pretreatment with xestospongin C and 2-aminoethoxydiphenyl borate, antagonists of inositol 1,4,5-trisphosphate receptors, abolished the response to BK. Inhibition of ryanodine receptors reduced the BK-induced Ca2+ increase, while disruption of lysosomal Ca2+ stores with bafilomycin A1 did not affect the response. BK produced a dose-dependent depolarization of nucleus ambiguus neurons, which was prevented by the B2 receptor antagonist. In vivo studies indicate that microinjection of BK into nucleus ambiguus elicited bradycardia in conscious rats via B2 receptors. In summary, in cardiac vagal neurons of nucleus ambiguus, BK activates B2 receptors promoting Ca2+ influx and Ca2+ release from endoplasmic reticulum, and membrane depolarization; these effects are translated in vivo by bradycardia.
AU - Brǎiloiu, Eugen
AU - Mcguire, Matthew
AU - Shuler, Shadaria
AU - Deliu, Elena
AU - Barr, Jeffrey
AU - Abood, Mary
AU - Brailoiu, Gabriela
ID - 747
JF - Neuroscience
SN - 03064522
TI - Modulation of cardiac vagal tone by bradykinin acting on nucleus ambiguus
VL - 365
ER -
TY - JOUR
AB - Synaptotagmin 7 (Syt7) is thought to be a Ca2+ sensor that mediates asynchronous transmitter release and facilitation at synapses. However, Syt7 is strongly expressed in fast-spiking, parvalbumin-expressing GABAergic interneurons, and the output synapses of these neurons produce only minimal asynchronous release and show depression rather than facilitation. To resolve this apparent contradiction, we examined the effects of genetic elimination of Syt7 on synaptic transmission at the GABAergic basket cell (BC)-Purkinje cell (PC) synapse in cerebellum. Our results indicate that at the BC-PC synapse, Syt7 contributes to asynchronous release, pool replenishment, and facilitation. In combination, these three effects ensure efficient transmitter release during high-frequency activity and guarantee frequency independence of inhibition. Our results identify a distinct function of Syt7: ensuring the efficiency of high-frequency inhibitory synaptic transmission
AU - Chen, Chong
AU - Satterfield, Rachel
AU - Young, Samuel
AU - Jonas, Peter M
ID - 749
IS - 8
JF - Cell Reports
SN - 22111247
TI - Triple function of Synaptotagmin 7 ensures efficiency of high-frequency transmission at central GABAergic synapses
VL - 21
ER -
TY - CONF
AB - Modern communication technologies allow first responders to contact thousands of potential volunteers simultaneously for support during a crisis or disaster event. However, such volunteer efforts must be well coordinated and monitored, in order to offer an effective relief to the professionals. In this paper we extend earlier work on optimally assigning volunteers to selected landmark locations. In particular, we emphasize the aspect that obtaining good assignments requires not only advanced computational tools, but also a realistic measure of distance between volunteers and landmarks. Specifically, we propose the use of the Open Street Map (OSM) driving distance instead of he previously used flight distance. We find the OSM driving distance to be better aligned with the interests of volunteers and first responders. Furthermore, we show that relying on the flying distance leads to a substantial underestimation of the number of required volunteers, causing negative side effects in case of an actual crisis situation.
AU - Pielorz, Jasmin
AU - Prandtstetter, Matthias
AU - Straub, Markus
AU - Lampert, Christoph
ID - 750
SN - 978-153862714-3
T2 - 2017 IEEE International Conference on Big Data
TI - Optimal geospatial volunteer allocation needs realistic distances
ER -
TY - JOUR
AB - The basement membrane (BM) is a thin layer of extracellular matrix (ECM) beneath nearly all epithelial cell types that is critical for cellular and tissue function. It is composed of numerous components conserved among all bilaterians [1]; however, it is unknown how all of these components are generated and subsequently constructed to form a fully mature BM in the living animal. Although BM formation is thought to simply involve a process of self-assembly [2], this concept suffers from a number of logistical issues when considering its construction in vivo. First, incorporation of BM components appears to be hierarchical [3-5], yet it is unclear whether their production during embryogenesis must also be regulated in a temporal fashion. Second, many BM proteins are produced not only by the cells residing on the BM but also by surrounding cell types [6-9], and it is unclear how large, possibly insoluble protein complexes [10] are delivered into the matrix. Here we exploit our ability to live image and genetically dissect de novo BM formation during Drosophila development. This reveals that there is a temporal hierarchy of BM protein production that is essential for proper component incorporation. Furthermore, we show that BM components require secretion by migrating macrophages (hemocytes) during their developmental dispersal, which is critical for embryogenesis. Indeed, hemocyte migration is essential to deliver a subset of ECM components evenly throughout the embryo. This reveals that de novo BM construction requires a combination of both production and distribution logistics allowing for the timely delivery of core components.
AU - Matsubayashi, Yutaka
AU - Louani, Adam
AU - Dragu, Anca
AU - Sanchez Sanchez, Besaiz
AU - Serna Morales, Eduardo
AU - Yolland, Lawrence
AU - György, Attila
AU - Vizcay, Gema
AU - Fleck, Roland
AU - Heddleston, John
AU - Chew, Teng
AU - Siekhaus, Daria E
AU - Stramer, Brian
ID - 751
IS - 22
JF - Current Biology
SN - 09609822
TI - A moving source of matrix components is essential for De Novo basement membrane formation
VL - 27
ER -
TY - CONF
AB - Consider the following random process: we are given n queues, into which elements of increasing labels are inserted uniformly at random. To remove an element, we pick two queues at random, and remove the element of lower label (higher priority) among the two. The cost of a removal is the rank of the label removed, among labels still present in any of the queues, that is, the distance from the optimal choice at each step. Variants of this strategy are prevalent in state-of-the-art concurrent priority queue implementations. Nonetheless, it is not known whether such implementations provide any rank guarantees, even in a sequential model. We answer this question, showing that this strategy provides surprisingly strong guarantees: Although the single-choice process, where we always insert and remove from a single randomly chosen queue, has degrading cost, going to infinity as we increase the number of steps, in the two choice process, the expected rank of a removed element is O(n) while the expected worst-case cost is O(n log n). These bounds are tight, and hold irrespective of the number of steps for which we run the process. The argument is based on a new technical connection between "heavily loaded" balls-into-bins processes and priority scheduling. Our analytic results inspire a new concurrent priority queue implementation, which improves upon the state of the art in terms of practical performance.
AU - Alistarh, Dan-Adrian
AU - Kopinsky, Justin
AU - Li, Jerry
AU - Nadiradze, Giorgi
ID - 791
SN - 978-145034992-5
T2 - Proceedings of the ACM Symposium on Principles of Distributed Computing
TI - The power of choice in priority scheduling
VL - Part F129314
ER -
TY - JOUR
AB - The chaotic dynamics of low-dimensional systems, such as Lorenz or Rössler flows, is guided by the infinity of periodic orbits embedded in their strange attractors. Whether this is also the case for the infinite-dimensional dynamics of Navier–Stokes equations has long been speculated, and is a topic of ongoing study. Periodic and relative periodic solutions have been shown to be involved in transitions to turbulence. Their relevance to turbulent dynamics – specifically, whether periodic orbits play the same role in high-dimensional nonlinear systems like the Navier–Stokes equations as they do in lower-dimensional systems – is the focus of the present investigation. We perform here a detailed study of pipe flow relative periodic orbits with energies and mean dissipations close to turbulent values. We outline several approaches to reduction of the translational symmetry of the system. We study pipe flow in a minimal computational cell at Re=2500, and report a library of invariant solutions found with the aid of the method of slices. Detailed study of the unstable manifolds of a sample of these solutions is consistent with the picture that relative periodic orbits are embedded in the chaotic saddle and that they guide the turbulent dynamics.
AU - Budanur, Nazmi B
AU - Short, Kimberly
AU - Farazmand, Mohammad
AU - Willis, Ashley
AU - Cvitanović, Predrag
ID - 792
JF - Journal of Fluid Mechanics
SN - 00221120
TI - Relative periodic orbits form the backbone of turbulent pipe flow
VL - 833
ER -
TY - JOUR
AB - Let P be a finite point set in the plane. A cordinary triangle in P is a subset of P consisting of three non-collinear points such that each of the three lines determined by the three points contains at most c points of P . Motivated by a question of Erdös, and answering a question of de Zeeuw, we prove that there exists a constant c > 0such that P contains a c-ordinary triangle, provided that P is not contained in the union of two lines. Furthermore, the number of c-ordinary triangles in P is Ω(| P |).
AU - Fulek, Radoslav
AU - Mojarrad, Hossein
AU - Naszódi, Márton
AU - Solymosi, József
AU - Stich, Sebastian
AU - Szedlák, May
ID - 793
JF - Computational Geometry: Theory and Applications
SN - 09257721
TI - On the existence of ordinary triangles
VL - 66
ER -
TY - JOUR
AB - We show that c-planarity is solvable in quadratic time for flat clustered graphs with three clusters if the combinatorial embedding of the underlying graph is fixed. In simpler graph-theoretical terms our result can be viewed as follows. Given a graph G with the vertex set partitioned into three parts embedded on a 2-sphere, our algorithm decides if we can augment G by adding edges without creating an edge-crossing so that in the resulting spherical graph the vertices of each part induce a connected sub-graph. We proceed by a reduction to the problem of testing the existence of a perfect matching in planar bipartite graphs. We formulate our result in a slightly more general setting of cyclic clustered graphs, i.e., the simple graph obtained by contracting each cluster, where we disregard loops and multi-edges, is a cycle.
AU - Fulek, Radoslav
ID - 794
JF - Computational Geometry: Theory and Applications
TI - C-planarity of embedded cyclic c-graphs
VL - 66
ER -
TY - JOUR
AB - We introduce a common generalization of the strong Hanani–Tutte theorem and the weak Hanani–Tutte theorem: if a graph G has a drawing D in the plane where every pair of independent edges crosses an even number of times, then G has a planar drawing preserving the rotation of each vertex whose incident edges cross each other evenly in D. The theorem is implicit in the proof of the strong Hanani–Tutte theorem by Pelsmajer, Schaefer and Štefankovič. We give a new, somewhat simpler proof.
AU - Fulek, Radoslav
AU - Kynčl, Jan
AU - Pálvölgyi, Dömötör
ID - 795
IS - 3
JF - Electronic Journal of Combinatorics
SN - 10778926
TI - Unified Hanani Tutte theorem
VL - 24
ER -
TY - JOUR
AB - We investigate transient behaviors induced by magnetic fields on the dynamics of the flow of a ferrofluid in the gap between two concentric, independently rotating cylinders. Without applying any magnetic fields, we uncover emergence of flow states constituted by a combination of a localized spiral state (SPIl) in the top and bottom of the annulus and different multi-cell flow states (SPI2v, SPI3v) with toroidally closed vortices in the interior of the bulk (SPIl+2v = SPIl + SPI2v and SPIl+3v = SPIl + SPI3v). However, when a magnetic field is presented, we observe the transient behaviors between multi-cell states passing through two critical thresholds in a strength of an axial (transverse) magnetic field. Before the first critical threshold of a magnetic field strength, multi-stable states with different number of cells could be observed. After the first critical threshold, we find the transient behavior between the three- and two-cell flow states. For more strength of magnetic field or after the second critical threshold, we discover that multi-cell states are disappeared and a localized spiral state remains to be stimulated. The studied transient behavior could be understood by the investigation of various quantities including a modal kinetic energy, a mode amplitude of the radial velocity, wavenumber, angular momentum, and torque. In addition, the emergence of new flow states and the transient behavior between their states in ferrofluidic flows indicate that richer and potentially controllable dynamics through magnetic fields could be possible in ferrofluic flow.
AU - Altmeyer, Sebastian
AU - Do, Younghae
AU - Ryu, Soorok
ID - 463
IS - 11
JF - Chaos
SN - 10541500
TI - Transient behavior between multi-cell flow states in ferrofluidic Taylor-Couette flow
VL - 27
ER -
TY - JOUR
AB - The computation of the winning set for parity objectives and for Streett objectives in graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We show how to compute the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs in time O(n2+nklogn). For both problems this gives faster algorithms for dense graphs and represents the first improvement in asymptotic running time in 15 years.
AU - Chatterjee, Krishnendu
AU - Henzinger, Monika
AU - Loitzenbauer, Veronika
ID - 464
IS - 3
JF - Logical Methods in Computer Science
SN - 18605974
TI - Improved algorithms for parity and Streett objectives
VL - 13
ER -
TY - JOUR
AB - The edit distance between two words w 1 , w 2 is the minimal number of word operations (letter insertions, deletions, and substitutions) necessary to transform w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the edit distance from L 1 to L 2 is the minimal number k such that for every word from L 1 there exists a word in L 2 with edit distance at most k . We study the edit distance computation problem between pushdown automata and their subclasses. The problem of computing edit distance to a pushdown automaton is undecidable, and in practice, the interesting question is to compute the edit distance from a pushdown automaton (the implementation, a standard model for programs with recursion) to a regular language (the specification). In this work, we present a complete picture of decidability and complexity for the following problems: (1) deciding whether, for a given threshold k , the edit distance from a pushdown automaton to a finite automaton is at most k , and (2) deciding whether the edit distance from a pushdown automaton to a finite automaton is finite.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Ibsen-Jensen, Rasmus
AU - Otop, Jan
ID - 465
IS - 3
JF - Logical Methods in Computer Science
SN - 18605974
TI - Edit distance for pushdown automata
VL - 13
ER -
TY - JOUR
AB - We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto-curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem.
AU - Chatterjee, Krishnendu
AU - Křetínská, Zuzana
AU - Kretinsky, Jan
ID - 466
IS - 2
JF - Logical Methods in Computer Science
SN - 18605974
TI - Unifying two views on multiple mean-payoff objectives in Markov decision processes
VL - 13
ER -
TY - JOUR
AB - Recently there has been a significant effort to handle quantitative properties in formal verification and synthesis. While weighted automata over finite and infinite words provide a natural and flexible framework to express quantitative properties, perhaps surprisingly, some basic system properties such as average response time cannot be expressed using weighted automata or in any other known decidable formalism. In this work, we introduce nested weighted automata as a natural extension of weighted automata, which makes it possible to express important quantitative properties such as average response time. In nested weighted automata, a master automaton spins off and collects results from weighted slave automata, each of which computes a quantity along a finite portion of an infinite word. Nested weighted automata can be viewed as the quantitative analogue of monitor automata, which are used in runtime verification. We establish an almost-complete decidability picture for the basic decision problems about nested weighted automata and illustrate their applicability in several domains. In particular, nested weighted automata can be used to decide average response time properties.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 467
IS - 4
JF - ACM Transactions on Computational Logic (TOCL)
SN - 15293785
TI - Nested weighted automata
VL - 18
ER -
TY - JOUR
AB - This paper presents a method for simulating water surface waves as a displacement field on a 2D domain. Our method relies on Lagrangian particles that carry packets of water wave energy; each packet carries information about an entire group of wave trains, as opposed to only a single wave crest. Our approach is unconditionally stable and can simulate high resolution geometric details. This approach also presents a straightforward interface for artistic control, because it is essentially a particle system with intuitive parameters like wavelength and amplitude. Our implementation parallelizes well and runs in real time for moderately challenging scenarios.
AU - Jeschke, Stefan
AU - Wojtan, Christopher J
ID - 470
IS - 4
JF - ACM Transactions on Graphics
SN - 07300301
TI - Water wave packets
VL - 36
ER -
TY - JOUR
AB - We present a new algorithm for the statistical model checking of Markov chains with respect to unbounded temporal properties, including full linear temporal logic. The main idea is that we monitor each simulation run on the fly, in order to detect quickly if a bottom strongly connected component is entered with high probability, in which case the simulation run can be terminated early. As a result, our simulation runs are often much shorter than required by termination bounds that are computed a priori for a desired level of confidence on a large state space. In comparison to previous algorithms for statistical model checking our method is not only faster in many cases but also requires less information about the system, namely, only the minimum transition probability that occurs in the Markov chain. In addition, our method can be generalised to unbounded quantitative properties such as mean-payoff bounds.
AU - Daca, Przemyslaw
AU - Henzinger, Thomas A
AU - Kretinsky, Jan
AU - Petrov, Tatjana
ID - 471
IS - 2
JF - ACM Transactions on Computational Logic (TOCL)
SN - 15293785
TI - Faster statistical model checking for unbounded temporal properties
VL - 18
ER -
TY - JOUR
AB - We introduce planar matchings on directed pseudo-line arrangements, which yield a planar set of pseudo-line segments such that only matching-partners are adjacent. By translating the planar matching problem into a corresponding stable roommates problem we show that such matchings always exist. Using our new framework, we establish, for the first time, a complete, rigorous definition of weighted straight skeletons, which are based on a so-called wavefront propagation process. We present a generalized and unified approach to treat structural changes in the wavefront that focuses on the restoration of weak planarity by finding planar matchings.
AU - Biedl, Therese
AU - Huber, Stefan
AU - Palfrader, Peter
ID - 481
IS - 3-4
JF - International Journal of Computational Geometry and Applications
TI - Planar matchings for weighted straight skeletons
VL - 26
ER -
TY - JOUR
AB - We prove the universality for the eigenvalue gap statistics in the bulk of the spectrum for band matrices, in the regime where the band width is comparable with the dimension of the matrix, W ~ N. All previous results concerning universality of non-Gaussian random matrices are for mean-field models. By relying on a new mean-field reduction technique, we deduce universality from quantum unique ergodicity for band matrices.
AU - Bourgade, Paul
AU - Erdös, László
AU - Yau, Horng
AU - Yin, Jun
ID - 483
IS - 3
JF - Advances in Theoretical and Mathematical Physics
SN - 10950761
TI - Universality for a class of random band matrices
VL - 21
ER -
TY - JOUR
AB - We consider the dynamics of a large quantum system of N identical bosons in 3D interacting via a two-body potential of the form N3β-1w(Nβ(x - y)). For fixed 0 = β < 1/3 and large N, we obtain a norm approximation to the many-body evolution in the Nparticle Hilbert space. The leading order behaviour of the dynamics is determined by Hartree theory while the second order is given by Bogoliubov theory.
AU - Nam, Phan
AU - Napiórkowski, Marcin M
ID - 484
IS - 3
JF - Advances in Theoretical and Mathematical Physics
SN - 10950761
TI - Bogoliubov correction to the mean-field dynamics of interacting bosons
VL - 21
ER -