TY - CONF
AB - Automata with monitor counters, where the transitions do not depend on counter values, and nested weighted automata are two expressive automata-theoretic frameworks for quantitative properties. For a well-studied and wide class of quantitative functions, we establish that automata with monitor counters and nested weighted automata are equivalent. We study for the first time such quantitative automata under probabilistic semantics. We show that several problems that are undecidable for the classical questions of emptiness and universality become decidable under the probabilistic semantics. We present a complete picture of decidability for such automata, and even an almost-complete picture of computational complexity, for the probabilistic questions we consider. © 2016 ACM.
AU - Chatterjee, Krishnendu
AU - Henzinger, Thomas A
AU - Otop, Jan
ID - 1138
T2 - Proceedings of the 31st Annual ACM/IEEE Symposium
TI - Quantitative automata under probabilistic semantics
ER -
TY - JOUR
AB - Microtubules switch stochastically between phases of growth and shrinkage. The molecular mechanism responsible for the end of a growth phase, an event called catastrophe, is still not understood. The probability for a catastrophe to occur increases with microtubule age, putting constraints on the possible molecular mechanism of catastrophe induction. Here we used microfluidics-Assisted fast tubulin washout experiments to induce microtubule depolymerization in a controlled manner at different times after the start of growth. We found that aging can also be observed in this assay, providing valuable new constraints against which theoretical models of catastrophe induction can be tested. We found that the data can be quantitatively well explained by a simple kinetic threshold model that assumes an age-dependent broadening of the protective cap at the microtubule end as a result of an evolving tapered end structure; this leads to a decrease of the cap density and its stability. This analysis suggests an intuitive picture of the role of morphological changes of the protective cap for the age dependence of microtubule stability.
AU - Düllberg, Christian F
AU - Cade, Nicholas
AU - Surrey, Thomas
ID - 1139
IS - 22
JF - Molecular Biology and Evolution
TI - Microtubule aging probed by microfluidics assisted tubulin washout
VL - 27
ER -
TY - CONF
AB - Given a model of a system and an objective, the model-checking question asks whether the model satisfies the objective. We study polynomial-time problems in two classical models, graphs and Markov Decision Processes (MDPs), with respect to several fundamental -regular objectives, e.g., Rabin and Streett objectives. For many of these problems the best-known upper bounds are quadratic or cubic, yet no super-linear lower bounds are known. In this work our contributions are two-fold: First, we present several improved algorithms, and second, we present the first conditional super-linear lower bounds based on widely believed assumptions about the complexity of CNF-SAT and combinatorial Boolean matrix multiplication. A separation result for two models with respect to an objective means a conditional lower bound for one model that is strictly higher than the existing upper bound for the other model, and similarly for two objectives with respect to a model. Our results establish the following separation results: (1) A separation of models (graphs and MDPs) for disjunctive queries of reachability and Büchi objectives. (2) Two kinds of separations of objectives, both for graphs and MDPs, namely, (2a) the separation of dual objectives such as Streett/Rabin objectives, and (2b) the separation of conjunction and disjunction of multiple objectives of the same type such as safety, Büchi, and coBüchi. In summary, our results establish the first model and objective separation results for graphs and MDPs for various classical -regular objectives. Quite strikingly, we establish conditional lower bounds for the disjunction of objectives that are strictly higher than the existing upper bounds for the conjunction of the same objectives. © 2016 ACM.
AU - Chatterjee, Krishnendu
AU - Dvoák, Wolfgang
AU - Henzinger, Monika
AU - Loitzenbauer, Veronika
ID - 1140
T2 - Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
TI - Model and objective separation with conditional lower bounds disjunction is harder than conjunction
ER -
TY - JOUR
AB - In this paper we introduce the Multiobjective Optimization Hierarchic Genetic Strategy with maturing (MO-mHGS), a meta-algorithm that performs evolutionary optimization in a hierarchy of populations. The maturing mechanism improves growth and reduces redundancy. The performance of MO-mHGS with selected state-of-the-art multiobjective evolutionary algorithms as internal algorithms is analysed on benchmark problems and their modifications for which single fitness evaluation time depends on the solution accuracy. We compare the proposed algorithm with the Island Model Genetic Algorithm as well as with single-deme methods, and discuss the impact of internal algorithms on the MO-mHGS meta-algorithm. © 2016 Elsevier B.V.
AU - Łazarz, Radosław
AU - Idzik, Michał
AU - Gądek, Konrad
AU - Gajda-Zagorska, Ewa P
ID - 1141
IS - 1
JF - Journal of Computational Science
TI - Hierarchic genetic strategy with maturing as a generic tool for multiobjective optimization
VL - 17
ER -
TY - JOUR
AB - Hemolysis drives susceptibility to bacterial infections and predicts poor outcome from sepsis. These detrimental effects are commonly considered to be a consequence of heme-iron serving as a nutrient for bacteria. We employed a Gram-negative sepsis model and found that elevated heme levels impaired the control of bacterial proliferation independently of heme-iron acquisition by pathogens. Heme strongly inhibited phagocytosis and the migration of human and mouse phagocytes by disrupting actin cytoskeletal dynamics via activation of the GTP-binding Rho family protein Cdc42 by the guanine nucleotide exchange factor DOCK8. A chemical screening approach revealed that quinine effectively prevented heme effects on the cytoskeleton, restored phagocytosis and improved survival in sepsis. These mechanistic insights provide potential therapeutic targets for patients with sepsis or hemolytic disorders.
AU - Martins, Rui
AU - Maier, Julia
AU - Gorki, Anna
AU - Huber, Kilian
AU - Sharif, Omar
AU - Starkl, Philipp
AU - Saluzzo, Simona
AU - Quattrone, Federica
AU - Gawish, Riem
AU - Lakovits, Karin
AU - Aichinger, Michael
AU - Radic Sarikas, Branka
AU - Lardeau, Charles
AU - Hladik, Anastasiya
AU - Korosec, Ana
AU - Brown, Markus
AU - Vaahtomeri, Kari
AU - Duggan, Michelle
AU - Kerjaschki, Dontscho
AU - Esterbauer, Harald
AU - Colinge, Jacques
AU - Eisenbarth, Stephanie
AU - Decker, Thomas
AU - Bennett, Keiryn
AU - Kubicek, Stefan
AU - Sixt, Michael K
AU - Superti Furga, Giulio
AU - Knapp, Sylvia
ID - 1142
IS - 12
JF - Nature Immunology
TI - Heme drives hemolysis-induced susceptibility to infection via disruption of phagocyte functions
VL - 17
ER -
TY - JOUR
AB - We study the ground state of a dilute Bose gas in a scaling limit where the Gross-Pitaevskii functional emerges. This is a repulsive nonlinear Schrödinger functional whose quartic term is proportional to the scattering length of the interparticle interaction potential. We propose a new derivation of this limit problem, with a method that bypasses some of the technical difficulties that previous derivations had to face. The new method is based on a combination of Dyson\'s lemma, the quantum de Finetti theorem and a second moment estimate for ground states of the effective Dyson Hamiltonian. It applies equally well to the case where magnetic fields or rotation are present.
AU - Nam, Phan
AU - Rougerie, Nicolas
AU - Seiringer, Robert
ID - 1143
IS - 2
JF - Analysis and PDE
TI - Ground states of large bosonic systems: The gross Pitaevskii limit revisited
VL - 9
ER -
TY - JOUR
AB - Auxin directs plant ontogenesis via differential accumulation within tissues depending largely on the activity of PIN proteins that mediate auxin efflux from cells and its directional cell-to-cell transport. Regardless of the developmental importance of PINs, the structure of these transporters is poorly characterized. Here, we present experimental data concerning protein topology of plasma membrane-localized PINs. Utilizing approaches based on pH-dependent quenching of fluorescent reporters combined with immunolocalization techniques, we mapped the membrane topology of PINs and further cross-validated our results using available topology modeling software. We delineated the topology of PIN1 with two transmembrane (TM) bundles of five α-helices linked by a large intracellular loop and a C-terminus positioned outside the cytoplasm. Using constraints derived from our experimental data, we also provide an updated position of helical regions generating a verisimilitude model of PIN1. Since the canonical long PINs show a high degree of conservation in TM domains and auxin transport capacity has been demonstrated for Arabidopsis representatives of this group, this empirically enhanced topological model of PIN1 will be an important starting point for further studies on PIN structure–function relationships. In addition, we have established protocols that can be used to probe the topology of other plasma membrane proteins in plants. © 2016 The Authors
AU - Nodzyński, Tomasz
AU - Vanneste, Steffen
AU - Zwiewka, Marta
AU - Pernisová, Markéta
AU - Hejátko, Jan
AU - Friml, Jirí
ID - 1145
IS - 11
JF - Molecular Plant
TI - Enquiry into the topology of plasma membrane localized PIN auxin transport components
VL - 9
ER -
TY - JOUR
AB - Apical dominance is one of the fundamental developmental phenomena in plant biology, which determines the overall architecture of aerial plant parts. Here we show apex decapitation activated competition for dominance in adjacent upper and lower axillary buds. A two-nodal-bud pea (Pisum sativum L.) was used as a model system to monitor and assess auxin flow, auxin transport channels, and dormancy and initiation status of axillary buds. Auxin flow was manipulated by lateral stem wounds or chemically by auxin efflux inhibitors 2,3,5-triiodobenzoic acid (TIBA), 1-N-naphtylphtalamic acid (NPA), or protein synthesis inhibitor cycloheximide (CHX) treatments, which served to interfere with axillary bud competition. Redirecting auxin flow to different points influenced which bud formed the outgrowing and dominant shoot. The obtained results proved that competition between upper and lower axillary buds as secondary auxin sources is based on the same auxin canalization principle that operates between the shoot apex and axillary bud. © The Author(s) 2016.
AU - Balla, Jozef
AU - Medved'Ová, Zuzana
AU - Kalousek, Petr
AU - Matiješčuková, Natálie
AU - Friml, Jirí
AU - Reinöhl, Vilém
AU - Procházka, Stanislav
ID - 1147
JF - Scientific Reports
TI - Auxin flow mediated competition between axillary buds to restore apical dominance
VL - 6
ER -
TY - JOUR
AB - Continuous-time Markov chain (CTMC) models have become a central tool for understanding the dynamics of complex reaction networks and the importance of stochasticity in the underlying biochemical processes. When such models are employed to answer questions in applications, in order to ensure that the model provides a sufficiently accurate representation of the real system, it is of vital importance that the model parameters are inferred from real measured data. This, however, is often a formidable task and all of the existing methods fail in one case or the other, usually because the underlying CTMC model is high-dimensional and computationally difficult to analyze. The parameter inference methods that tend to scale best in the dimension of the CTMC are based on so-called moment closure approximations. However, there exists a large number of different moment closure approximations and it is typically hard to say a priori which of the approximations is the most suitable for the inference procedure. Here, we propose a moment-based parameter inference method that automatically chooses the most appropriate moment closure method. Accordingly, contrary to existing methods, the user is not required to be experienced in moment closure techniques. In addition to that, our method adaptively changes the approximation during the parameter inference to ensure that always the best approximation is used, even in cases where different approximations are best in different regions of the parameter space. © 2016 Elsevier Ireland Ltd
AU - Schilling, Christian
AU - Bogomolov, Sergiy
AU - Henzinger, Thomas A
AU - Podelski, Andreas
AU - Ruess, Jakob
ID - 1148
JF - Biosystems
TI - Adaptive moment closure for parameter inference of biochemical reaction networks
VL - 149
ER -
TY - JOUR
AB - We study the usefulness of two most prominent publicly available rigorous ODE integrators: one provided by the CAPD group (capd.ii.uj.edu.pl), the other based on the COSY Infinity project (cosyinfinity.org). Both integrators are capable of handling entire sets of initial conditions and provide tight rigorous outer enclosures of the images under a time-T map. We conduct extensive benchmark computations using the well-known Lorenz system, and compare the computation time against the final accuracy achieved. We also discuss the effect of a few technical parameters, such as the order of the numerical integration method, the value of T, and the phase space resolution. We conclude that COSY may provide more precise results due to its ability of avoiding the variable dependency problem. However, the overall cost of computations conducted using CAPD is typically lower, especially when intervals of parameters are involved. Moreover, access to COSY is limited (registration required) and the rigorous ODE integrators are not publicly available, while CAPD is an open source free software project. Therefore, we recommend the latter integrator for this kind of computations. Nevertheless, proper choice of the various integration parameters turns out to be of even greater importance than the choice of the integrator itself. © 2016 IMACS. Published by Elsevier B.V. All rights reserved.
AU - Miyaji, Tomoyuki
AU - Pilarczyk, Pawel
AU - Gameiro, Marcio
AU - Kokubu, Hiroshi
AU - Mischaikow, Konstantin
ID - 1149
JF - Applied Numerical Mathematics
TI - A study of rigorous ODE integrators for multi scale set oriented computations
VL - 107
ER -
TY - JOUR
AB - When neutrophils infiltrate a site of inflammation, they have to stop at the right place to exert their effector function. In this issue of Developmental Cell, Wang et al. (2016) show that neutrophils sense reactive oxygen species via the TRPM2 channel to arrest migration at their target site. © 2016 Elsevier Inc.
AU - Renkawitz, Jörg
AU - Sixt, Michael K
ID - 1150
IS - 5
JF - Developmental Cell
TI - A Radical Break Restraining Neutrophil Migration
VL - 38
ER -
TY - JOUR
AB - Tissue patterning in multicellular organisms is the output of precise spatio–temporal regulation of gene expression coupled with changes in hormone dynamics. In plants, the hormone auxin regulates growth and development at every stage of a plant’s life cycle. Auxin signaling occurs through binding of the auxin molecule to a TIR1/AFB F-box ubiquitin ligase, allowing interaction with Aux/IAA transcriptional repressor proteins. These are subsequently ubiquitinated and degraded via the 26S proteasome, leading to derepression of auxin response factors (ARFs). How auxin is able to elicit such a diverse range of developmental responses through a single signaling module has not yet been resolved. Here we present an alternative auxin-sensing mechanism in which the ARF ARF3/ETTIN controls gene expression through interactions with process-specific transcription factors. This noncanonical hormonesensing mechanism exhibits strong preference for the naturally occurring auxin indole 3-acetic acid (IAA) and is important for coordinating growth and patterning in diverse developmental contexts such as gynoecium morphogenesis, lateral root emergence, ovule development, and primary branch formation. Disrupting this IAA-sensing ability induces morphological aberrations with consequences for plant fitness. Therefore, our findings introduce a novel transcription factor-based mechanism of hormone perception in plants. © 2016 Simonini et al.
AU - Simonini, Sara
AU - Deb, Joyita
AU - Moubayidin, Laila
AU - Stephenson, Pauline
AU - Valluru, Manoj
AU - Freire Rios, Alejandra
AU - Sorefan, Karim
AU - Weijers, Dolf
AU - Friml, Jirí
AU - Östergaard, Lars
ID - 1151
IS - 20
JF - Genes and Development
TI - A noncanonical auxin sensing mechanism is required for organ morphogenesis in arabidopsis
VL - 30
ER -
TY - JOUR
AB - Differential cell growth enables flexible organ bending in the presence of environmental signals such as light or gravity. A prominent example of the developmental processes based on differential cell growth is the formation of the apical hook that protects the fragile shoot apical meristem when it breaks through the soil during germination. Here, we combined in silico and in vivo approaches to identify a minimal mechanism producing auxin gradient-guided differential growth during the establishment of the apical hook in the model plant Arabidopsis thaliana. Computer simulation models based on experimental data demonstrate that asymmetric expression of the PIN-FORMED auxin efflux carrier at the concave (inner) versus convex (outer) side of the hook suffices to establish an auxin maximum in the epidermis at the concave side of the apical hook. Furthermore, we propose a mechanism that translates this maximum into differential growth, and thus curvature, of the apical hook. Through a combination of experimental and in silico computational approaches, we have identified the individual contributions of differential cell elongation and proliferation to defining the apical hook and reveal the role of auxin-ethylene crosstalk in balancing these two processes. © 2016 American Society of Plant Biologists. All rights reserved.
AU - Žádníková, Petra
AU - Wabnik, Krzysztof T
AU - Abuzeineh, Anas
AU - Gallemí, Marçal
AU - Van Der Straeten, Dominique
AU - Smith, Richard
AU - Inze, Dirk
AU - Friml, Jirí
AU - Prusinkiewicz, Przemysław
AU - Benková, Eva
ID - 1153
IS - 10
JF - Plant Cell
TI - A model of differential growth guided apical hook formation in plants
VL - 28
ER -
TY - JOUR
AB - Cellular locomotion is a central hallmark of eukaryotic life. It is governed by cell-extrinsic molecular factors, which can either emerge in the soluble phase or as immobilized, often adhesive ligands. To encode for direction, every cue must be present as a spatial or temporal gradient. Here, we developed a microfluidic chamber that allows measurement of cell migration in combined response to surface immobilized and soluble molecular gradients. As a proof of principle we study the response of dendritic cells to their major guidance cues, chemokines. The majority of data on chemokine gradient sensing is based on in vitro studies employing soluble gradients. Despite evidence suggesting that in vivo chemokines are often immobilized to sugar residues, limited information is available how cells respond to immobilized chemokines. We tracked migration of dendritic cells towards immobilized gradients of the chemokine CCL21 and varying superimposed soluble gradients of CCL19. Differential migratory patterns illustrate the potential of our setup to quantitatively study the competitive response to both types of gradients. Beyond chemokines our approach is broadly applicable to alternative systems of chemo- and haptotaxis such as cells migrating along gradients of adhesion receptor ligands vs. any soluble cue.
AU - Schwarz, Jan
AU - Bierbaum, Veronika
AU - Merrin, Jack
AU - Frank, Tino
AU - Hauschild, Robert
AU - Bollenbach, Mark Tobias
AU - Tay, Savaş
AU - Sixt, Michael K
AU - Mehling, Matthias
ID - 1154
JF - Scientific Reports
TI - A microfluidic device for measuring cell migration towards substrate bound and soluble chemokine gradients
VL - 6
ER -
TY - JOUR
AB - Let k, n, and r be positive integers with k < n and r≤⌊nk⌋. We determine the facets of the r-stable n, k-hypersimplex. As a result, it turns out that the r-stable n, k-hypersimplex has exactly 2n facets for every r<⌊nk⌋. We then utilize the equations of the facets to study when the r-stable hypersimplex is Gorenstein. For every k > 0 we identify an infinite collection of Gorenstein r-stable hypersimplices, consequently expanding the collection of r-stable hypersimplices known to have unimodal Ehrhart δ-vectors.
AU - Hibi, Takayugi
AU - Liam Solus
ID - 1156
IS - 4
JF - Annals of Combinatorics
TI - Facets of the r-stable (n, k)-hypersimplex
VL - 20
ER -
TY - JOUR
AB - We consider sample covariance matrices of the form Q = ( σ1/2X)(σ1/2X)∗, where the sample X is an M ×N random matrix whose entries are real independent random variables with variance 1/N and whereσ is an M × M positive-definite deterministic matrix. We analyze the asymptotic fluctuations of the largest rescaled eigenvalue of Q when both M and N tend to infinity with N/M →d ϵ (0,∞). For a large class of populations σ in the sub-critical regime, we show that the distribution of the largest rescaled eigenvalue of Q is given by the type-1 Tracy-Widom distribution under the additional assumptions that (1) either the entries of X are i.i.d. Gaussians or (2) that σ is diagonal and that the entries of X have a sub-exponential decay.
AU - Lee, Ji
AU - Schnelli, Kevin
ID - 1157
IS - 6
JF - Annals of Applied Probability
TI - Tracy-widom distribution for the largest eigenvalue of real sample covariance matrices with general population
VL - 26
ER -
TY - JOUR
AB - Speciation results from the progressive accumulation of mutations that decrease the probability of mating between parental populations or reduce the fitness of hybrids—the so-called species barriers. The speciation genomic literature, however, is mainly a collection of case studies, each with its own approach and specificities, such that a global view of the gradual process of evolution from one to two species is currently lacking. Of primary importance is the prevalence of gene flow between diverging entities, which is central in most species concepts and has been widely discussed in recent years. Here, we explore the continuum of speciation thanks to a comparative analysis of genomic data from 61 pairs of populations/species of animals with variable levels of divergence. Gene flow between diverging gene pools is assessed under an approximate Bayesian computation (ABC) framework. We show that the intermediate "grey zone" of speciation, in which taxonomy is often controversial, spans from 0.5% to 2% of net synonymous divergence, irrespective of species life history traits or ecology. Thanks to appropriate modeling of among-locus variation in genetic drift and introgression rate, we clarify the status of the majority of ambiguous cases and uncover a number of cryptic species. Our analysis also reveals the high incidence in animals of semi-isolated species (when some but not all loci are affected by barriers to gene flow) and highlights the intrinsic difficulty, both statistical and conceptual, of delineating species in the grey zone of speciation.
AU - Roux, Camille
AU - Fraisse, Christelle
AU - Romiguier, Jonathan
AU - Anciaux, Youann
AU - Galtier, Nicolas
AU - Bierne, Nicolas
ID - 1158
IS - 12
JF - PLoS Biology
TI - Shedding light on the grey zone of speciation along a continuum of genomic divergence
VL - 14
ER -
TY - CONF
AB - A drawing of a graph G is radial if the vertices of G are placed on concentric circles C1, … , Ck with common center c, and edges are drawn radially: every edge intersects every circle centered at c at most once. G is radial planar if it has a radial embedding, that is, a crossing-free radial drawing. If the vertices of G are ordered or partitioned into ordered levels (as they are for leveled graphs), we require that the assignment of vertices to circles corresponds to the given ordering or leveling. A pair of edges e and f in a graph is independent if e and f do not share a vertex. We show that a graph G is radial planar if G has a radial drawing in which every two independent edges cross an even number of times; the radial embedding has the same leveling as the radial drawing. In other words, we establish the strong Hanani-Tutte theorem for radial planarity. This characterization yields a very simple algorithm for radial planarity testing.
AU - Fulek, Radoslav
AU - Pelsmajer, Michael
AU - Schaefer, Marcus
ID - 1164
TI - Hanani-Tutte for radial planarity II
VL - 9801
ER -
TY - CONF
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 - 1165
TI - C-planarity of embedded cyclic c-graphs
VL - 9801
ER -
TY - CONF
AB - POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory suffice. Moreover, the existing solution to the problem is explicit, which first requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we first study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efficient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach. © 2016, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved.
AU - Chatterjee, Krishnendu
AU - Chmelik, Martin
AU - Davies, Jessica
ID - 1166
T2 - Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence
TI - A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps
VL - 2016
ER -