@article{9351, abstract = {We consider the many-body quantum evolution of a factorized initial data, in the mean-field regime. We show that fluctuations around the limiting Hartree dynamics satisfy large deviation estimates that are consistent with central limit theorems that have been established in the last years. }, author = {Kirkpatrick, Kay and Rademacher, Simone Anna Elvira and Schlein, Benjamin}, issn = {1424-0637}, journal = {Annales Henri Poincare}, pages = {2595--2618}, publisher = {Springer Nature}, title = {{A large deviation principle in many-body quantum dynamics}}, doi = {10.1007/s00023-021-01044-1}, volume = {22}, year = {2021}, } @article{9352, abstract = {This paper provides an a priori error analysis of a localized orthogonal decomposition method for the numerical stochastic homogenization of a model random diffusion problem. If the uniformly elliptic and bounded random coefficient field of the model problem is stationary and satisfies a quantitative decorrelation assumption in the form of the spectral gap inequality, then the expected $L^2$ error of the method can be estimated, up to logarithmic factors, by $H+(\varepsilon/H)^{d/2}$, $\varepsilon$ being the small correlation length of the random coefficient and $H$ the width of the coarse finite element mesh that determines the spatial resolution. The proof bridges recent results of numerical homogenization and quantitative stochastic homogenization.}, author = {Fischer, Julian L and Gallistl, Dietmar and Peterseim, Dietmar}, issn = {0036-1429}, journal = {SIAM Journal on Numerical Analysis}, number = {2}, pages = {660--674}, publisher = {Society for Industrial and Applied Mathematics}, title = {{A priori error analysis of a numerical stochastic homogenization method}}, doi = {10.1137/19M1308992}, volume = {59}, year = {2021}, } @inproceedings{9356, abstract = {In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime verification to monitors that attempt to estimate numerical values of quantitative trace properties (instead of attempting to conclude boolean values of trace specifications), such as maximal or average response time along a trace. Quantitative monitors are approximate: with every finite prefix, they can improve their estimate of the infinite trace's unknown property value. Consequently, quantitative monitors can be compared with regard to a precision-cost trade-off: better approximations of the property value require more monitor resources, such as states (in the case of finite-state monitors) or registers, and additional resources yield better approximations. We introduce a formal framework for quantitative and approximate monitoring, show how it conservatively generalizes the classical boolean setting for monitoring, and give several precision-cost trade-offs for monitors. For example, we prove that there are quantitative properties for which every additional register improves monitoring precision.}, author = {Henzinger, Thomas A and Sarac, Naci E}, booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Online}, publisher = {Institute of Electrical and Electronics Engineers}, title = {{Quantitative and approximate monitoring}}, doi = {10.1109/LICS52264.2021.9470547}, year = {2021}, } @article{9359, abstract = {We prove that the factorization homologies of a scheme with coefficients in truncated polynomial algebras compute the cohomologies of its generalized configuration spaces. Using Koszul duality between commutative algebras and Lie algebras, we obtain new expressions for the cohomologies of the latter. As a consequence, we obtain a uniform and conceptual approach for treating homological stability, homological densities, and arithmetic densities of generalized configuration spaces. Our results categorify, generalize, and in fact provide a conceptual understanding of the coincidences appearing in the work of Farb--Wolfson--Wood. Our computation of the stable homological densities also yields rational homotopy types, answering a question posed by Vakil--Wood. Our approach hinges on the study of homological stability of cohomological Chevalley complexes, which is of independent interest. }, author = {Ho, Quoc P}, issn = {1364-0380}, journal = {Geometry & Topology}, keywords = {Generalized configuration spaces, homological stability, homological densities, chiral algebras, chiral homology, factorization algebras, Koszul duality, Ran space}, number = {2}, pages = {813--912}, publisher = {Mathematical Sciences Publishers}, title = {{Homological stability and densities of generalized configuration spaces}}, doi = {10.2140/gt.2021.25.813}, volume = {25}, year = {2021}, } @article{9361, abstract = {The multimeric matrix (M) protein of clinically relevant paramyxoviruses orchestrates assembly and budding activity of viral particles at the plasma membrane (PM). We identified within the canine distemper virus (CDV) M protein two microdomains, potentially assuming α-helix structures, which are essential for membrane budding activity. Remarkably, while two rationally designed microdomain M mutants (E89R, microdomain 1 and L239D, microdomain 2) preserved proper folding, dimerization, interaction with the nucleocapsid protein, localization at and deformation of the PM, the virus-like particle formation, as well as production of infectious virions (as monitored using a membrane budding-complementation system), were, in sharp contrast, strongly impaired. Of major importance, raster image correlation spectroscopy (RICS) revealed that both microdomains contributed to finely tune M protein mobility specifically at the PM. Collectively, our data highlighted the cornerstone membrane budding-priming activity of two spatially discrete M microdomains, potentially by coordinating the assembly of productive higher oligomers at the PM.}, author = {Gast, Matthieu and Kadzioch, Nicole P. and Milius, Doreen and Origgi, Francesco and Plattet, Philippe}, issn = {23795042}, journal = {mSphere}, number = {2}, publisher = {American Society for Microbiology}, title = {{Oligomerization and cell egress controlled by two microdomains of canine distemper virus matrix protein}}, doi = {10.1128/mSphere.01024-20}, volume = {6}, year = {2021}, } @article{9362, abstract = {A central goal in systems neuroscience is to understand the functions performed by neural circuits. Previous top-down models addressed this question by comparing the behaviour of an ideal model circuit, optimised to perform a given function, with neural recordings. However, this requires guessing in advance what function is being performed, which may not be possible for many neural systems. To address this, we propose an inverse reinforcement learning (RL) framework for inferring the function performed by a neural network from data. We assume that the responses of each neuron in a network are optimised so as to drive the network towards ‘rewarded’ states, that are desirable for performing a given function. We then show how one can use inverse RL to infer the reward function optimised by the network from observing its responses. This inferred reward function can be used to predict how the neural network should adapt its dynamics to perform the same function when the external environment or network structure changes. This could lead to theoretical predictions about how neural network dynamics adapt to deal with cell death and/or varying sensory stimulus statistics.}, author = {Chalk, Matthew J and Tkačik, Gašper and Marre, Olivier}, issn = {19326203}, journal = {PLoS ONE}, number = {4}, publisher = {Public Library of Science}, title = {{Inferring the function performed by a recurrent neural network}}, doi = {10.1371/journal.pone.0248940}, volume = {16}, year = {2021}, } @article{9363, abstract = {Optogenetics has been harnessed to shed new mechanistic light on current and future therapeutic strategies. This has been to date achieved by the regulation of ion flow and electrical signals in neuronal cells and neural circuits that are known to be affected by disease. In contrast, the optogenetic delivery of trophic biochemical signals, which support cell survival and are implicated in degenerative disorders, has never been demonstrated in an animal model of disease. Here, we reengineered the human and Drosophila melanogaster REarranged during Transfection (hRET and dRET) receptors to be activated by light, creating one-component optogenetic tools termed Opto-hRET and Opto-dRET. Upon blue light stimulation, these receptors robustly induced the MAPK/ERK proliferative signaling pathway in cultured cells. In PINK1B9 flies that exhibit loss of PTEN-induced putative kinase 1 (PINK1), a kinase associated with familial Parkinson’s disease (PD), light activation of Opto-dRET suppressed mitochondrial defects, tissue degeneration and behavioral deficits. In human cells with PINK1 loss-of-function, mitochondrial fragmentation was rescued using Opto-dRET via the PI3K/NF-кB pathway. Our results demonstrate that a light-activated receptor can ameliorate disease hallmarks in a genetic model of PD. The optogenetic delivery of trophic signals is cell type-specific and reversible and thus has the potential to inspire novel strategies towards a spatio-temporal regulation of tissue repair.}, author = {Inglés Prieto, Álvaro and Furthmann, Nikolas and Crossman, Samuel H. and Tichy, Alexandra Madelaine and Hoyer, Nina and Petersen, Meike and Zheden, Vanessa and Bicher, Julia and Gschaider-Reichhart, Eva and György, Attila and Siekhaus, Daria E and Soba, Peter and Winklhofer, Konstanze F. and Janovjak, Harald L}, issn = {15537404}, journal = {PLoS genetics}, number = {4}, pages = {e1009479}, publisher = {Public Library of Science}, title = {{Optogenetic delivery of trophic signals in a genetic model of Parkinson's disease}}, doi = {10.1371/journal.pgen.1009479}, volume = {17}, year = {2021}, } @article{9365, abstract = {In this paper, we propose a new iterative method with alternated inertial step for solving split common null point problem in real Hilbert spaces. We obtain weak convergence of the proposed iterative algorithm. Furthermore, we introduce the notion of bounded linear regularity property for the split common null point problem and obtain the linear convergence property for the new algorithm under some mild assumptions. Finally, we provide some numerical examples to demonstrate the performance and efficiency of the proposed method.}, author = {Ogbuisi, Ferdinard U. and Shehu, Yekini and Yao, Jen Chih}, issn = {1029-4945}, journal = {Optimization}, publisher = {Taylor and Francis}, title = {{Convergence analysis of new inertial method for the split common null point problem}}, doi = {10.1080/02331934.2021.1914035}, year = {2021}, } @article{9368, abstract = {The quality control system for messenger RNA (mRNA) is fundamental for cellular activities in eukaryotes. To elucidate the molecular mechanism of 3'-Phosphoinositide-Dependent Protein Kinase1 (PDK1), a master regulator that is essential throughout eukaryotic growth and development, we employed a forward genetic approach to screen for suppressors of the loss-of-function T-DNA insertion double mutant pdk1.1 pdk1.2 in Arabidopsis thaliana. Notably, the severe growth attenuation of pdk1.1 pdk1.2 was rescued by sop21 (suppressor of pdk1.1 pdk1.2), which harbours a loss-of-function mutation in PELOTA1 (PEL1). PEL1 is a homologue of mammalian PELOTA and yeast (Saccharomyces cerevisiae) DOM34p, which each form a heterodimeric complex with the GTPase HBS1 (HSP70 SUBFAMILY B SUPPRESSOR1, also called SUPERKILLER PROTEIN7, SKI7), a protein that is responsible for ribosomal rescue and thereby assures the quality and fidelity of mRNA molecules during translation. Genetic analysis further revealed that a dysfunctional PEL1-HBS1 complex failed to degrade the T-DNA-disrupted PDK1 transcripts, which were truncated but functional, and thus rescued the growth and developmental defects of pdk1.1 pdk1.2. Our studies demonstrated the functionality of a homologous PELOTA-HBS1 complex and identified its essential regulatory role in plants, providing insights into the mechanism of mRNA quality control.}, author = {Kong, W and Tan, Shutang and Zhao, Q and Lin, DL and Xu, ZH and Friml, Jiří and Xue, HW}, issn = {1532-2548}, journal = {Plant Physiology}, number = {4}, pages = {2003--2020}, publisher = {American Society of Plant Biologists}, title = {{mRNA surveillance complex PELOTA-HBS1 eegulates phosphoinositide-sependent protein kinase1 and plant growth}}, doi = {10.1093/plphys/kiab199}, volume = {186}, year = {2021}, } @article{9374, abstract = {If there are no constraints on the process of speciation, then the number of species might be expected to match the number of available niches and this number might be indefinitely large. One possible constraint is the opportunity for allopatric divergence. In 1981, Felsenstein used a simple and elegant model to ask if there might also be genetic constraints. He showed that progress towards speciation could be described by the build‐up of linkage disequilibrium among divergently selected loci and between these loci and those contributing to other forms of reproductive isolation. Therefore, speciation is opposed by recombination, because it tends to break down linkage disequilibria. Felsenstein then introduced a crucial distinction between “two‐allele” models, which are subject to this effect, and “one‐allele” models, which are free from the recombination constraint. These fundamentally important insights have been the foundation for both empirical and theoretical studies of speciation ever since.}, author = {Butlin, Roger K. and Servedio, Maria R. and Smadja, Carole M. and Bank, Claudia and Barton, Nicholas H and Flaxman, Samuel M. and Giraud, Tatiana and Hopkins, Robin and Larson, Erica L. and Maan, Martine E. and Meier, Joana and Merrill, Richard and Noor, Mohamed A. F. and Ortiz‐Barrientos, Daniel and Qvarnström, Anna}, issn = {1558-5646}, journal = {Evolution}, keywords = {Genetics, Ecology, Evolution, Behavior and Systematics, General Agricultural and Biological Sciences}, number = {5}, pages = {978--988}, publisher = {Wiley}, title = {{Homage to Felsenstein 1981, or why are there so few/many species?}}, doi = {10.1111/evo.14235}, volume = {75}, year = {2021}, } @article{9375, abstract = {Genetic variation segregates as linked sets of variants, or haplotypes. Haplotypes and linkage are central to genetics and underpin virtually all genetic and selection analysis. And yet, genomic data often lack haplotype information, due to constraints in sequencing technologies. Here we present “haplotagging”, a simple, low-cost linked-read sequencing technique that allows sequencing of hundreds of individuals while retaining linkage information. We apply haplotagging to construct megabase-size haplotypes for over 600 individual butterflies (Heliconius erato and H. melpomene), which form overlapping hybrid zones across an elevational gradient in Ecuador. Haplotagging identifies loci controlling distinctive high- and lowland wing color patterns. Divergent haplotypes are found at the same major loci in both species, while chromosome rearrangements show no parallelism. Remarkably, in both species the geographic clines for the major wing pattern loci are displaced by 18 km, leading to the rise of a novel hybrid morph in the centre of the hybrid zone. We propose that shared warning signalling (Müllerian mimicry) may couple the cline shifts seen in both species, and facilitate the parallel co-emergence of a novel hybrid morph in both co-mimetic species. Our results show the power of efficient haplotyping methods when combined with large-scale sequencing data from natural populations.}, author = {Meier, Joana I. and Salazar, Patricio A. and Kučka, Marek and Davies, Robert William and Dréau, Andreea and Aldás, Ismael and Power, Olivia Box and Nadeau, Nicola J. and Bridle, Jon R. and Rolian, Campbell and Barton, Nicholas H and McMillan, W. Owen and Jiggins, Chris D. and Chan, Yingguang Frank}, issn = {0027-8424}, journal = {PNAS}, number = {25}, publisher = {Proceedings of the National Academy of Sciences}, title = {{Haplotype tagging reveals parallel formation of hybrid races in two butterfly species}}, doi = {10.1073/pnas.2015005118}, volume = {118}, year = {2021}, } @article{9376, abstract = {This paper presents a method for designing planar multistable compliant structures. Given a sequence of desired stable states and the corresponding poses of the structure, we identify the topology and geometric realization of a mechanism—consisting of bars and joints—that is able to physically reproduce the desired multistable behavior. In order to solve this problem efficiently, we build on insights from minimally rigid graph theory to identify simple but effective topologies for the mechanism. We then optimize its geometric parameters, such as joint positions and bar lengths, to obtain correct transitions between the given poses. Simultaneously, we ensure adequate stability of each pose based on an effective approximate error metric related to the elastic energy Hessian of the bars in the mechanism. As demonstrated by our results, we obtain functional multistable mechanisms of manageable complexity that can be fabricated using 3D printing. Further, we evaluated the effectiveness of our method on a large number of examples in the simulation and fabricated several physical prototypes.}, author = {Zhang, Ran and Auzinger, Thomas and Bickel, Bernd}, issn = {1557-7368}, journal = {ACM Transactions on Graphics}, keywords = {multistability, mechanism, computational design, rigidity}, number = {5}, publisher = {Association for Computing Machinery}, title = {{Computational design of planar multistable compliant structures}}, doi = {10.1145/3453477}, volume = {40}, year = {2021}, } @article{9379, abstract = {When B cells encounter membrane-bound antigens, the formation and coalescence of B cell antigen receptor (BCR) microclusters amplifies BCR signaling. The ability of B cells to probe the surface of antigen-presenting cells (APCs) and respond to APC-bound antigens requires remodeling of the actin cytoskeleton. Initial BCR signaling stimulates actin-related protein (Arp) 2/3 complex-dependent actin polymerization, which drives B cell spreading as well as the centripetal movement and coalescence of BCR microclusters at the B cell-APC synapse. Sustained actin polymerization depends on concomitant actin filament depolymerization, which enables the recycling of actin monomers and Arp2/3 complexes. Cofilin-mediated severing of actin filaments is a rate-limiting step in the morphological changes that occur during immune synapse formation. Hence, regulators of cofilin activity such as WD repeat-containing protein 1 (Wdr1), LIM domain kinase (LIMK), and coactosin-like 1 (Cotl1) may also be essential for actin-dependent processes in B cells. Wdr1 enhances cofilin-mediated actin disassembly. Conversely, Cotl1 competes with cofilin for binding to actin and LIMK phosphorylates cofilin and prevents it from binding to actin filaments. We now show that Wdr1 and LIMK have distinct roles in BCR-induced assembly of the peripheral actin structures that drive B cell spreading, and that cofilin, Wdr1, and LIMK all contribute to the actin-dependent amplification of BCR signaling at the immune synapse. Depleting Cotl1 had no effect on these processes. Thus, the Wdr1-LIMK-cofilin axis is critical for BCR-induced actin remodeling and for B cell responses to APC-bound antigens.}, author = {Bolger-Munro, Madison and Choi, Kate and Cheung, Faith and Liu, Yi Tian and Dang-Lawson, May and Deretic, Nikola and Keane, Connor and Gold, Michael R.}, issn = {2296-634X}, journal = {Frontiers in Cell and Developmental Biology}, keywords = {B cell, actin, immune synapse, cell spreading, cofilin, WDR1 (AIP1), LIM domain kinase, B cell receptor (BCR)}, publisher = {Frontiers Media}, title = {{The Wdr1-LIMK-Cofilin axis controls B cell antigen receptor-induced actin remodeling and signaling at the immune synapse}}, doi = {10.3389/fcell.2021.649433}, volume = {9}, year = {2021}, } @article{9380, abstract = {Shigella are pathogens originating within the Escherichia lineage but frequently classified as a separate genus. Shigella genomes contain numerous insertion sequences (ISs) that lead to pseudogenisation of affected genes and an increase of non-homologous recombination. Here, we study 414 genomes of E. coli and Shigella strains to assess the contribution of genomic rearrangements to Shigella evolution. We found that Shigella experienced exceptionally high rates of intragenomic rearrangements and had a decreased rate of homologous recombination compared to pathogenic and non-pathogenic E. coli. The high rearrangement rate resulted in independent disruption of syntenic regions and parallel rearrangements in different Shigella lineages. Specifically, we identified two types of chromosomally encoded E3 ubiquitin-protein ligases acquired independently by all Shigella strains that also showed a high level of sequence conservation in the promoter and further in the 5′-intergenic region. In the only available enteroinvasive E. coli (EIEC) strain, which is a pathogenic E. coli with a phenotype intermediate between Shigella and non-pathogenic E. coli, we found a rate of genome rearrangements comparable to those in other E. coli and no functional copies of the two Shigella-specific E3 ubiquitin ligases. These data indicate that the accumulation of ISs influenced many aspects of genome evolution and played an important role in the evolution of intracellular pathogens. Our research demonstrates the power of comparative genomics-based on synteny block composition and an important role of non-coding regions in the evolution of genomic islands.}, author = {Seferbekova, Zaira and Zabelkin, Alexey and Yakovleva, Yulia and Afasizhev, Robert and Dranenko, Natalia O. and Alexeev, Nikita and Gelfand, Mikhail S. and Bochkareva, Olga}, issn = {1664-302X}, journal = {Frontiers in Microbiology}, publisher = {Frontiers}, title = {{High rates of genome rearrangements and pathogenicity of Shigella spp}}, doi = {10.3389/fmicb.2021.628622}, volume = {12}, year = {2021}, } @article{9381, abstract = {A game of rock-paper-scissors is an interesting example of an interaction where none of the pure strategies strictly dominates all others, leading to a cyclic pattern. In this work, we consider an unstable version of rock-paper-scissors dynamics and allow individuals to make behavioural mistakes during the strategy execution. We show that such an assumption can break a cyclic relationship leading to a stable equilibrium emerging with only one strategy surviving. We consider two cases: completely random mistakes when individuals have no bias towards any strategy and a general form of mistakes. Then, we determine conditions for a strategy to dominate all other strategies. However, given that individuals who adopt a dominating strategy are still prone to behavioural mistakes in the observed behaviour, we may still observe extinct strategies. That is, behavioural mistakes in strategy execution stabilise evolutionary dynamics leading to an evolutionary stable and, potentially, mixed co-existence equilibrium.}, author = {Kleshnina, Maria and Streipert, Sabrina S. and Filar, Jerzy A. and Chatterjee, Krishnendu}, issn = {15537358}, journal = {PLoS Computational Biology}, number = {4}, publisher = {Public Library of Science}, title = {{Mistakes can stabilise the dynamics of rock-paper-scissors games}}, doi = {10.1371/journal.pcbi.1008523}, volume = {17}, year = {2021}, } @article{9383, abstract = {A primary roadblock to our understanding of speciation is that it usually occurs over a timeframe that is too long to study from start to finish. The idea of a speciation continuum provides something of a solution to this problem; rather than observing the entire process, we can simply reconstruct it from the multitude of speciation events that surround us. But what do we really mean when we talk about the speciation continuum, and can it really help us understand speciation? We explored these questions using a literature review and online survey of speciation researchers. Although most researchers were familiar with the concept and thought it was useful, our survey revealed extensive disagreement about what the speciation continuum actually tells us. This is due partly to the lack of a clear definition. Here, we provide an explicit definition that is compatible with the Biological Species Concept. That is, the speciation continuum is a continuum of reproductive isolation. After outlining the logic of the definition in light of alternatives, we explain why attempts to reconstruct the speciation process from present‐day populations will ultimately fail. We then outline how we think the speciation continuum concept can continue to act as a foundation for understanding the continuum of reproductive isolation that surrounds us.}, author = {Stankowski, Sean and Ravinet, Mark}, issn = {1558-5646}, journal = {Evolution}, number = {6}, pages = {1256--1273}, publisher = {Oxford University Press}, title = {{Defining the speciation continuum}}, doi = {10.1111/evo.14215}, volume = {75}, year = {2021}, } @article{9387, abstract = {We report the complete analysis of a deterministic model of deleterious mutations and negative selection against them at two haploid loci without recombination. As long as mutation is a weaker force than selection, mutant alleles remain rare at the only stable equilibrium, and otherwise, a variety of dynamics are possible. If the mutation-free genotype is absent, generally the only stable equilibrium is the one that corresponds to fixation of the mutant allele at the locus where it is less deleterious. This result suggests that fixation of a deleterious allele that follows a click of the Muller’s ratchet is governed by natural selection, instead of random drift.}, author = {Khudiakova, Kseniia and Neretina, Tatiana Yu. and Kondrashov, Alexey S.}, issn = {0022-5193}, journal = {Journal of Theoretical Biology}, keywords = {General Biochemistry, Genetics and Molecular Biology, Modelling and Simulation, Statistics and Probability, General Immunology and Microbiology, Applied Mathematics, General Agricultural and Biological Sciences, General Medicine}, publisher = {Elsevier }, title = {{Two linked loci under mutation-selection balance and Muller’s ratchet}}, doi = {10.1016/j.jtbi.2021.110729}, volume = {524}, year = {2021}, } @misc{9389, abstract = {This .zip File contains the transport data for "Non-topological zero bias peaks in full-shell nanowires induced by flux tunable Andreev states" by M. Valentini, et. al. The measurements were done using Labber Software and the data is stored in the hdf5 file format. Instructions of how to read the data are in "Notebook_Valentini.pdf".}, author = {Valentini, Marco}, publisher = {Institute of Science and Technology Austria}, title = {{Research data for "Non-topological zero bias peaks in full-shell nanowires induced by flux tunable Andreev states"}}, doi = {10.15479/AT:ISTA:9389}, year = {2021}, } @article{9392, abstract = {Humans conceptualize the diversity of life by classifying individuals into types we call ‘species’1. The species we recognize influence political and financial decisions and guide our understanding of how units of diversity evolve and interact. Although the idea of species may seem intuitive, a debate about the best way to define them has raged even before Darwin2. So much energy has been devoted to the so-called ‘species problem’ that no amount of discourse will ever likely solve it2,3. Dozens of species concepts are currently recognized3, but we lack a concrete understanding of how much researchers actually disagree and the factors that cause them to think differently1,2. To address this, we used a survey to quantify the species problem for the first time. The results indicate that the disagreement is extensive: two randomly chosen respondents will most likely disagree on the nature of species. The probability of disagreement is not predicted by researcher experience or broad study system, but tended to be lower among researchers with similar focus, training and who study the same organism. Should we see this diversity of perspectives as a problem? We argue that we should not.}, author = {Stankowski, Sean and Ravinet, Mark}, issn = {18790445}, journal = {Current Biology}, number = {9}, pages = {R428--R429}, publisher = {Cell Press}, title = {{Quantifying the use of species concepts}}, doi = {10.1016/j.cub.2021.03.060}, volume = {31}, year = {2021}, } @article{9393, abstract = {We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff, the ratio, and the minimum initial credit for energy property. The algorithmic problem given a graph and a quantitative property asks to compute the optimal value (the infimum value over all traces) from every node of the graph. We consider graphs with bounded treewidth—a class that contains the control flow graphs of most programs. Let n denote the number of nodes of a graph, m the number of edges (for bounded treewidth 𝑚=𝑂(𝑛)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for the minimum initial credit problem we show that (1) for general graphs the problem can be solved in 𝑂(𝑛2⋅𝑚) time and the associated decision problem in 𝑂(𝑛⋅𝑚) time, improving the previous known 𝑂(𝑛3⋅𝑚⋅log(𝑛⋅𝑊)) and 𝑂(𝑛2⋅𝑚) bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm that requires 𝑂(𝑛⋅log𝑛) time. Second, for bounded treewidth graphs we present an algorithm that approximates the mean-payoff value within a factor of 1+𝜖 in time 𝑂(𝑛⋅log(𝑛/𝜖)) as compared to the classical exact algorithms on general graphs that require quadratic time. Third, for the ratio property we present an algorithm that for bounded treewidth graphs works in time 𝑂(𝑛⋅log(|𝑎⋅𝑏|))=𝑂(𝑛⋅log(𝑛⋅𝑊)), when the output is 𝑎𝑏, as compared to the previously best known algorithm on general graphs with running time 𝑂(𝑛2⋅log(𝑛⋅𝑊)). We have implemented some of our algorithms and show that they present a significant speedup on standard benchmarks.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Pavlogiannis, Andreas}, issn = {1572-8102}, journal = {Formal Methods in System Design}, pages = {401--428}, publisher = {Springer}, title = {{Faster algorithms for quantitative verification in bounded treewidth graphs}}, doi = {10.1007/s10703-021-00373-5}, volume = {57}, year = {2021}, }