@inproceedings{6887,
abstract = {The fundamental model-checking problem, given as input a model and a specification, asks for the algorithmic verification of whether the model satisfies the specification. Two classical models for reactive systems are graphs and Markov decision processes (MDPs). A basic specification formalism in the verification of reactive systems is the strong fairness (aka Streett) objective, where given different types of requests and corresponding grants, the requirement is that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All omega-regular objectives can be expressed as Streett objectives and hence they are canonical in verification. Consider graphs/MDPs with n vertices, m edges, and a Streett objectives with k pairs, and let b denote the size of the description of the Streett objective for the sets of requests and grants. The current best-known algorithm for the problem requires time O(min(n^2, m sqrt{m log n}) + b log n). In this work we present randomized near-linear time algorithms, with expected running time O~(m + b), where the O~ notation hides poly-log factors. Our randomized algorithms are near-linear in the size of the input, and hence optimal up to poly-log factors. },
author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika and Svozil, Alexander},
booktitle = {Leibniz International Proceedings in Informatics},
location = {Amsterdam, Netherlands},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{Near-linear time algorithms for Streett objectives in graphs and MDPs}},
doi = {10.4230/LIPICS.CONCUR.2019.7},
volume = {140},
year = {2019},
}
@article{6940,
abstract = {We study the effect of a linear tunneling coupling between two-dimensional systems, each separately
exhibiting the topological Berezinskii-Kosterlitz-Thouless (BKT) transition. In the uncoupled limit, there
are two phases: one where the one-body correlation functions are algebraically decaying and the other with
exponential decay. When the linear coupling is turned on, a third BKT-paired phase emerges, in which one-body correlations are exponentially decaying, while two-body correlation functions exhibit power-law
decay. We perform numerical simulations in the paradigmatic case of two coupled XY models at finite
temperature, finding evidences that for any finite value of the interlayer coupling, the BKT-paired phase is
present. We provide a picture of the phase diagram using a renormalization group approach.},
author = {Bighin, Giacomo and Defenu, Nicolò and Nándori, István and Salasnich, Luca and Trombettoni, Andrea},
issn = {1079-7114},
journal = {Physical Review Letters},
number = {10},
publisher = {American Physical Society (APS)},
title = {{Berezinskii-Kosterlitz-Thouless paired phase in coupled XY models}},
doi = {10.1103/physrevlett.123.100601},
volume = {123},
year = {2019},
}
@article{6508,
author = {Shamipour, Shayan and Kardos, Roland and Xue, Shi-lei and Hof, Björn and Hannezo, Edouard B and Heisenberg, Carl-Philipp J},
issn = {10974172},
journal = {Cell},
number = {6},
pages = {1463--1479.e18},
publisher = {Elsevier},
title = {{Bulk actin dynamics drive phase segregation in zebrafish oocytes}},
doi = {10.1016/j.cell.2019.04.030},
volume = {177},
year = {2019},
}
@inproceedings{6647,
abstract = {The Tverberg theorem is one of the cornerstones of discrete geometry. It states that, given a set X of at least (d+1)(r-1)+1 points in R^d, one can find a partition X=X_1 cup ... cup X_r of X, such that the convex hulls of the X_i, i=1,...,r, all share a common point. In this paper, we prove a strengthening of this theorem that guarantees a partition which, in addition to the above, has the property that the boundaries of full-dimensional convex hulls have pairwise nonempty intersections. Possible generalizations and algorithmic aspects are also discussed. As a concrete application, we show that any n points in the plane in general position span floor[n/3] vertex-disjoint triangles that are pairwise crossing, meaning that their boundaries have pairwise nonempty intersections; this number is clearly best possible. A previous result of Alvarez-Rebollar et al. guarantees floor[n/6] pairwise crossing triangles. Our result generalizes to a result about simplices in R^d,d >=2.},
author = {Fulek, Radoslav and Gärtner, Bernd and Kupavskii, Andrey and Valtr, Pavel and Wagner, Uli},
booktitle = {35th International Symposium on Computational Geometry},
isbn = {9783959771047},
issn = {1868-8969},
location = {Portland, OR, United States},
pages = {38:1--38:13},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
title = {{The crossing Tverberg theorem}},
doi = {10.4230/LIPICS.SOCG.2019.38},
volume = {129},
year = {2019},
}
@phdthesis{6894,
abstract = {Hybrid automata combine finite automata and dynamical systems, and model the interaction of digital with physical systems. Formal analysis that can guarantee the safety of all behaviors or rigorously witness failures, while unsolvable in general, has been tackled algorithmically using, e.g., abstraction, bounded model-checking, assisted theorem proving.
Nevertheless, very few methods have addressed the time-unbounded reachability analysis of hybrid automata and, for current sound and automatic tools, scalability remains critical. We develop methods for the polyhedral abstraction of hybrid automata, which construct coarse overapproximations and tightens them incrementally, in a CEGAR fashion. We use template polyhedra, i.e., polyhedra whose facets are normal to a given set of directions.
While, previously, directions were given by the user, we introduce (1) the first method
for computing template directions from spurious counterexamples, so as to generalize and
eliminate them. The method applies naturally to convex hybrid automata, i.e., hybrid
automata with (possibly non-linear) convex constraints on derivatives only, while for linear
ODE requires further abstraction. Specifically, we introduce (2) the conic abstractions,
which, partitioning the state space into appropriate (possibly non-uniform) cones, divide
curvy trajectories into relatively straight sections, suitable for polyhedral abstractions.
Finally, we introduce (3) space-time interpolation, which, combining interval arithmetic
and template refinement, computes appropriate (possibly non-uniform) time partitioning
and template directions along spurious trajectories, so as to eliminate them.
We obtain sound and automatic methods for the reachability analysis over dense
and unbounded time of convex hybrid automata and hybrid automata with linear ODE.
We build prototype tools and compare—favorably—our methods against the respective
state-of-the-art tools, on several benchmarks.},
author = {Giacobbe, Mirco},
issn = {2663-337X},
pages = {132},
publisher = {IST Austria},
title = {{Automatic time-unbounded reachability analysis of hybrid systems}},
doi = {10.15479/AT:ISTA:6894},
year = {2019},
}
@article{7227,
abstract = {Gastrulation entails specification and formation of three embryonic germ layers—ectoderm, mesoderm and endoderm—thereby establishing the basis for the future body plan. In zebrafish embryos, germ layer specification occurs during blastula and early gastrula stages (Ho & Kimmel, 1993), a period when the main morphogenetic movements underlying gastrulation are initiated. Hence, the signals driving progenitor cell fate specification, such as Nodal ligands from the TGF-β family, also play key roles in regulating germ layer progenitor cell segregation (Carmany-Rampey & Schier, 2001; David & Rosa, 2001; Feldman et al., 2000; Gritsman et al., 1999; Keller et al., 2008). In this review, we summarize and discuss the main signaling pathways involved in germ layer progenitor cell fate specification and segregation, specifically focusing on recent advances in understanding the interplay between mesoderm and endoderm specification and the internalization movements at the onset of zebrafish gastrulation.},
author = {Nunes Pinheiro, Diana C and Heisenberg, Carl-Philipp J},
issn = {00702153},
journal = {Current Topics in Developmental Biology},
publisher = {Elsevier},
title = {{Zebrafish gastrulation: Putting fate in motion}},
doi = {10.1016/bs.ctdb.2019.10.009},
year = {2019},
}
@article{73,
abstract = {We consider the space of probability measures on a discrete set X, endowed with a dynamical optimal transport metric. Given two probability measures supported in a subset Y⊆X, it is natural to ask whether they can be connected by a constant speed geodesic with support in Y at all times. Our main result answers this question affirmatively, under a suitable geometric condition on Y introduced in this paper. The proof relies on an extension result for subsolutions to discrete Hamilton-Jacobi equations, which is of independent interest.},
author = {Erbar, Matthias and Maas, Jan and Wirth, Melchior},
issn = {09442669},
journal = {Calculus of Variations and Partial Differential Equations},
number = {1},
publisher = {Springer},
title = {{On the geometry of geodesics in discrete optimal transport}},
doi = {10.1007/s00526-018-1456-1},
volume = {58},
year = {2019},
}
@article{80,
abstract = {We consider an interacting, dilute Bose gas trapped in a harmonic potential at a positive temperature. The system is analyzed in a combination of a thermodynamic and a Gross–Pitaevskii (GP) limit where the trap frequency ω, the temperature T, and the particle number N are related by N∼ (T/ ω) 3→ ∞ while the scattering length is so small that the interaction energy per particle around the center of the trap is of the same order of magnitude as the spectral gap in the trap. We prove that the difference between the canonical free energy of the interacting gas and the one of the noninteracting system can be obtained by minimizing the GP energy functional. We also prove Bose–Einstein condensation in the following sense: The one-particle density matrix of any approximate minimizer of the canonical free energy functional is to leading order given by that of the noninteracting gas but with the free condensate wavefunction replaced by the GP minimizer.},
author = {Deuchert, Andreas and Seiringer, Robert and Yngvason, Jakob},
journal = {Communications in Mathematical Physics},
number = {2},
pages = {723--776},
publisher = {Springer},
title = {{Bose–Einstein condensation in a dilute, trapped gas at positive temperature}},
doi = {10.1007/s00220-018-3239-0},
volume = {368},
year = {2019},
}
@inproceedings{7183,
abstract = {A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2).},
author = {Brázdil, Tomás and Chatterjee, Krishnendu and Kucera, Antonín and Novotný, Petr and Velan, Dominik},
booktitle = {International Symposium on Automated Technology for Verification and Analysis},
isbn = {9783030317836},
issn = {16113349},
location = {Taipei, Taiwan},
pages = {462--478},
publisher = {Springer Nature},
title = {{Deciding fast termination for probabilistic VASS with nondeterminism}},
doi = {10.1007/978-3-030-31784-3_27},
volume = {11781},
year = {2019},
}
@article{7001,
author = {Schwayer, Cornelia and Shamipour, Shayan and Pranjic-Ferscha, Kornelija and Schauer, Alexandra and Balda, M and Tada, M and Matter, K and Heisenberg, Carl-Philipp J},
issn = {1097-4172},
journal = {Cell},
number = {4},
pages = {937--952.e18},
publisher = {Cell Press},
title = {{Mechanosensation of tight junctions depends on ZO-1 phase separation and flow}},
doi = {10.1016/j.cell.2019.10.006},
volume = {179},
year = {2019},
}
@article{7210,
abstract = {The rate of biological evolution depends on the fixation probability and on the fixation time of new mutants. Intensive research has focused on identifying population structures that augment the fixation probability of advantageous mutants. But these amplifiers of natural selection typically increase fixation time. Here we study population structures that achieve a tradeoff between fixation probability and time. First, we show that no amplifiers can have an asymptotically lower absorption time than the well-mixed population. Then we design population structures that substantially augment the fixation probability with just a minor increase in fixation time. Finally, we show that those structures enable higher effective rate of evolution than the well-mixed population provided that the rate of generating advantageous mutants is relatively low. Our work sheds light on how population structure affects the rate of evolution. Moreover, our structures could be useful for lab-based, medical, or industrial applications of evolutionary optimization.},
author = {Tkadlec, Josef and Pavlogiannis, Andreas and Chatterjee, Krishnendu and Nowak, Martin A.},
issn = {2399-3642},
journal = {Communications Biology},
publisher = {Springer Nature},
title = {{Population structure determines the tradeoff between fixation probability and fixation time}},
doi = {10.1038/s42003-019-0373-y},
volume = {2},
year = {2019},
}
@misc{6060,
author = {Vicoso, Beatriz},
publisher = {IST Austria},
title = {{Supplementary data for "Sex-biased gene expression and dosage compensation on the Artemia franciscana Z-chromosome" (Huylman, Toups et al., 2019). }},
doi = {10.15479/AT:ISTA:6060},
year = {2019},
}
@article{7436,
abstract = {For an ordinary K3 surface over an algebraically closed field of positive characteristic we show that every automorphism lifts to characteristic zero. Moreover, we show that the Fourier-Mukai partners of an ordinary K3 surface are in one-to-one correspondence with the Fourier-Mukai partners of the geometric generic fiber of its canonical lift. We also prove that the explicit counting formula for Fourier-Mukai partners of the K3 surfaces with Picard rank two and with discriminant equal to minus of a prime number, in terms of the class number of the prime, holds over a field of positive characteristic as well. We show that the image of the derived autoequivalence group of a K3 surface of finite height in the group of isometries of its crystalline cohomology has index at least two. Moreover, we provide a conditional upper bound on the kernel of this natural cohomological descent map. Further, we give an extended remark in the appendix on the possibility of an F-crystal structure on the crystalline cohomology of a K3 surface over an algebraically closed field of positive characteristic and show that the naive F-crystal structure fails in being compatible with inner product. },
author = {Srivastava, Tanya K},
issn = {14310643},
journal = {Documenta Mathematica},
pages = {1135--1177},
publisher = {Deutsche Mathematiker-Vereinigung},
title = {{On derived equivalences of k3 surfaces in positive characteristic}},
doi = {10.25537/dm.2019v24.1135-1177},
volume = {24},
year = {2019},
}
@article{7417,
abstract = {Previously, we reported that the allelic de-etiolated by zinc (dez) and trichome birefringence (tbr) mutants exhibit photomorphogenic development in the dark, which is enhanced by high Zn. TRICHOME BIREFRINGENCE-LIKE proteins had been implicated in transferring acetyl groups to various hemicelluloses. Pectin O-acetylation levels were lower in dark-grown dez seedlings than in the wild type. We observed Zn-enhanced photomorphogenesis in the dark also in the reduced wall acetylation 2 (rwa2-3) mutant, which exhibits lowered O-acetylation levels of cell wall macromolecules including pectins and xyloglucans, supporting a role for cell wall macromolecule O-acetylation in the photomorphogenic phenotypes of rwa2-3 and dez. Application of very short oligogalacturonides (vsOGs) restored skotomorphogenesis in dark-grown dez and rwa2-3. Here we demonstrate that in dez, O-acetylation of non-pectin cell wall components, notably of xyloglucan, is enhanced. Our results highlight the complexity of cell wall homeostasis and indicate against an influence of xyloglucan O-acetylation on light-dependent seedling development.},
author = {Sinclair, Scott A and Gille, S. and Pauly, M. and Krämer, U.},
issn = {1559-2324},
journal = {Plant Signaling & Behavior},
publisher = {Informa UK Limited},
title = {{Regulation of acetylation of plant cell wall components is complex and responds to external stimuli}},
doi = {10.1080/15592324.2019.1687185},
year = {2019},
}
@article{7412,
abstract = {We develop a framework for the rigorous analysis of focused stochastic local search algorithms. These algorithms search a state space by repeatedly selecting some constraint that is violated in the current state and moving to a random nearby state that addresses the violation, while (we hope) not introducing many new violations. An important class of focused local search algorithms with provable performance guarantees has recently arisen from algorithmizations of the Lovász local lemma (LLL), a nonconstructive tool for proving the existence of satisfying states by introducing a background measure on the state space. While powerful, the state transitions of algorithms in this class must be, in a precise sense, perfectly compatible with the background measure. In many applications this is a very restrictive requirement, and one needs to step outside the class. Here we introduce the notion of measure distortion and develop a framework for analyzing arbitrary focused stochastic local search algorithms, recovering LLL algorithmizations as the special case of no distortion. Our framework takes as input an arbitrary algorithm of such type and an arbitrary probability measure and shows how to use the measure as a yardstick of algorithmic progress, even for algorithms designed independently of the measure.},
author = {Achlioptas, Dimitris and Iliopoulos, Fotis and Kolmogorov, Vladimir},
issn = {1095-7111},
journal = {SIAM Journal on Computing},
number = {5},
pages = {1583--1602},
publisher = {SIAM},
title = {{A local lemma for focused stochastical algorithms}},
doi = {10.1137/16m109332x},
volume = {48},
year = {2019},
}
@article{7397,
abstract = {Polymer additives can substantially reduce the drag of turbulent flows and the upperlimit, the so called “maximum drag reduction” (MDR) asymptote is universal, i.e. inde-pendent of the type of polymer and solvent used. Until recently, the consensus was that,in this limit, flows are in a marginal state where only a minimal level of turbulence activ-ity persists. Observations in direct numerical simulations using minimal sized channelsappeared to support this view and reported long “hibernation” periods where turbu-lence is marginalized. In simulations of pipe flow we find that, indeed, with increasingWeissenberg number (Wi), turbulence expresses long periods of hibernation if the domainsize is small. However, with increasing pipe length, the temporal hibernation continuouslyalters to spatio-temporal intermittency and here the flow consists of turbulent puffs sur-rounded by laminar flow. Moreover, upon an increase in Wi, the flow fully relaminarises,in agreement with recent experiments. At even larger Wi, a different instability is en-countered causing a drag increase towards MDR. Our findings hence link earlier minimalflow unit simulations with recent experiments and confirm that the addition of polymersinitially suppresses Newtonian turbulence and leads to a reverse transition. The MDRstate on the other hand results from a separate instability and the underlying dynamicscorresponds to the recently proposed state of elasto-inertial-turbulence (EIT).},
author = {Lopez Alonso, Jose M and Choueiri, George H and Hof, Björn},
issn = {0022-1120},
journal = {Journal of Fluid Mechanics},
pages = {699--719},
publisher = {CUP},
title = {{Dynamics of viscoelastic pipe flow at low Reynolds numbers in the maximum drag reduction limit}},
doi = {10.1017/jfm.2019.486},
volume = {874},
year = {2019},
}
@article{7405,
abstract = {Biophysical modeling of neuronal networks helps to integrate and interpret rapidly growing and disparate experimental datasets at multiple scales. The NetPyNE tool (www.netpyne.org) provides both programmatic and graphical interfaces to develop data-driven multiscale network models in NEURON. NetPyNE clearly separates model parameters from implementation code. Users provide specifications at a high level via a standardized declarative language, for example connectivity rules, to create millions of cell-to-cell connections. NetPyNE then enables users to generate the NEURON network, run efficiently parallelized simulations, optimize and explore network parameters through automated batch runs, and use built-in functions for visualization and analysis – connectivity matrices, voltage traces, spike raster plots, local field potentials, and information theoretic measures. NetPyNE also facilitates model sharing by exporting and importing standardized formats (NeuroML and SONATA). NetPyNE is already being used to teach computational neuroscience students and by modelers to investigate brain regions and phenomena.},
author = {Dura-Bernal, Salvador and Suter, Benjamin and Gleeson, Padraig and Cantarelli, Matteo and Quintana, Adrian and Rodriguez, Facundo and Kedziora, David J and Chadderdon, George L and Kerr, Cliff C and Neymotin, Samuel A and McDougal, Robert A and Hines, Michael and Shepherd, Gordon MG and Lytton, William W},
issn = {2050-084X},
journal = {eLife},
publisher = {eLife Sciences Publications},
title = {{NetPyNE, a tool for data-driven multiscale modeling of brain circuits}},
doi = {10.7554/elife.44494},
volume = {8},
year = {2019},
}
@article{7400,
abstract = {Suppressed recombination allows divergence between homologous sex chromosomes and the functionality of their genes. Here, we reveal patterns of the earliest stages of sex-chromosome evolution in the diploid dioecious herb Mercurialis annua on the basis of cytological analysis, de novo genome assembly and annotation, genetic mapping, exome resequencing of natural populations, and transcriptome analysis. The genome assembly contained 34,105 expressed genes, of which 10,076 were assigned to linkage groups. Genetic mapping and exome resequencing of individuals across the species range both identified the largest linkage group, LG1, as the sex chromosome. Although the sex chromosomes of M. annua are karyotypically homomorphic, we estimate that about one-third of the Y chromosome, containing 568 transcripts and spanning 22.3 cM in the corresponding female map, has ceased recombining. Nevertheless, we found limited evidence for Y-chromosome degeneration in terms of gene loss and pseudogenization, and most X- and Y-linked genes appear to have diverged in the period subsequent to speciation between M. annua and its sister species M. huetii, which shares the same sex-determining region. Taken together, our results suggest that the M. annua Y chromosome has at least two evolutionary strata: a small old stratum shared with M. huetii, and a more recent larger stratum that is probably unique to M. annua and that stopped recombining ∼1 MYA. Patterns of gene expression within the nonrecombining region are consistent with the idea that sexually antagonistic selection may have played a role in favoring suppressed recombination.},
author = {Veltsos, Paris and Ridout, Kate E. and Toups, Melissa A and González-Martínez, Santiago C. and Muyle, Aline and Emery, Olivier and Rastas, Pasi and Hudzieczek, Vojtech and Hobza, Roman and Vyskot, Boris and Marais, Gabriel A. B. and Filatov, Dmitry A. and Pannell, John R.},
issn = {1943-2631},
journal = {Genetics},
number = {3},
pages = {815--835},
publisher = {Genetics Society of America},
title = {{Early sex-chromosome evolution in the diploid dioecious plant Mercurialis annua}},
doi = {10.1534/genetics.119.302045},
volume = {212},
year = {2019},
}
@article{6818,
abstract = {Indigoidine is a blue natural pigment, which can be efficiently synthetized in E. coli. In addition to its antioxidant and antimicrobial activities indigoidine due to its stability and deep blue color can find an application as an industrial, environmentally friendly dye. Moreover, similarly to its counterpart regular indigo dye, due to its molecular structure, indigoidine is an organic semiconductor. Fully conjugated aromatic moiety and intermolecular hydrogen bonding of indigoidine result in an unusually narrow bandgap for such a small molecule. This, in its turn, result is tight molecular packing in the solid state and opens a path for a wide range of application in organic and bio-electronics, such as electrochemical and field effect transistors, organic solar cells, light and bio-sensors etc.},
author = {Yumusak, Cigdem and Prochazkova, Anna Jancik and Apaydin, Dogukan H and Seelajaroen, Hathaichanok and Sariciftci, Niyazi Serdar and Weiter, Martin and Krajcovic, Jozef and Qin, Yong and Zhang, Wei and Zhan, Jixun and Kovalenko, Alexander},
issn = {0143-7208},
journal = {Dyes and Pigments},
publisher = {Elsevier},
title = {{Indigoidine - Biosynthesized organic semiconductor}},
doi = {10.1016/j.dyepig.2019.107768},
volume = {171},
year = {2019},
}
@inproceedings{6565,
abstract = {In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example.},
author = {Kundu, Atreyee and Garcia Soto, Miriam and Prabhakar, Pavithra},
booktitle = {5th Indian Control Conference Proceedings},
isbn = {978-153866246-5},
location = {Delhi, India},
publisher = {IEEE},
title = {{Formal synthesis of stabilizing controllers for periodically controlled linear switched systems}},
doi = {10.1109/INDIANCC.2019.8715598},
year = {2019},
}