@article{1351, abstract = {The behaviour of gene regulatory networks (GRNs) is typically analysed using simulation-based statistical testing-like methods. In this paper, we demonstrate that we can replace this approach by a formal verification-like method that gives higher assurance and scalability. We focus on Wagner’s weighted GRN model with varying weights, which is used in evolutionary biology. In the model, weight parameters represent the gene interaction strength that may change due to genetic mutations. For a property of interest, we synthesise the constraints over the parameter space that represent the set of GRNs satisfying the property. We experimentally show that our parameter synthesis procedure computes the mutational robustness of GRNs—an important problem of interest in evolutionary biology—more efficiently than the classical simulation method. We specify the property in linear temporal logic. We employ symbolic bounded model checking and SMT solving to compute the space of GRNs that satisfy the property, which amounts to synthesizing a set of linear constraints on the weights.}, author = {Giacobbe, Mirco and Guet, Calin C and Gupta, Ashutosh and Henzinger, Thomas A and Paixao, Tiago and Petrov, Tatjana}, issn = {0001-5903}, journal = {Acta Informatica}, number = {8}, pages = {765 -- 787}, publisher = {Springer}, title = {{Model checking the evolution of gene regulatory networks}}, doi = {10.1007/s00236-016-0278-x}, volume = {54}, year = {2017}, } @article{1367, abstract = {One of the major challenges in physically based modelling is making simulations efficient. Adaptive models provide an essential solution to these efficiency goals. These models are able to self-adapt in space and time, attempting to provide the best possible compromise between accuracy and speed. This survey reviews the adaptive solutions proposed so far in computer graphics. Models are classified according to the strategy they use for adaptation, from time-stepping and freezing techniques to geometric adaptivity in the form of structured grids, meshes and particles. Applications range from fluids, through deformable bodies, to articulated solids.}, author = {Manteaux, Pierre and Wojtan, Christopher J and Narain, Rahul and Redon, Stéphane and Faure, François and Cani, Marie}, issn = {01677055}, journal = {Computer Graphics Forum}, number = {6}, pages = {312 -- 337}, publisher = {Wiley-Blackwell}, title = {{Adaptive physically based models in computer graphics}}, doi = {10.1111/cgf.12941}, volume = {36}, year = {2017}, } @article{1407, abstract = {We consider the problem of computing the set of initial states of a dynamical system such that there exists a control strategy to ensure that the trajectories satisfy a temporal logic specification with probability 1 (almost-surely). We focus on discrete-time, stochastic linear dynamics and specifications given as formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over linear predicates in the states of the system. We propose a solution based on iterative abstraction-refinement, and turn-based 2-player probabilistic games. While the theoretical guarantee of our algorithm after any finite number of iterations is only a partial solution, we show that if our algorithm terminates, then the result is the set of all satisfying initial states. Moreover, for any (partial) solution our algorithm synthesizes witness control strategies to ensure almost-sure satisfaction of the temporal logic specification. While the proposed algorithm guarantees progress and soundness in every iteration, it is computationally demanding. We offer an alternative, more efficient solution for the reachability properties that decomposes the problem into a series of smaller problems of the same type. All algorithms are demonstrated on an illustrative case study.}, author = {Svoreňová, Mária and Kretinsky, Jan and Chmelik, Martin and Chatterjee, Krishnendu and Cěrná, Ivana and Belta, Cǎlin}, journal = {Nonlinear Analysis: Hybrid Systems}, number = {2}, pages = {230 -- 253}, publisher = {Elsevier}, title = {{Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games}}, doi = {10.1016/j.nahs.2016.04.006}, volume = {23}, year = {2017}, } @inproceedings{14205, abstract = {Two of the most fundamental prototypes of greedy optimization are the matching pursuit and Frank-Wolfe algorithms. In this paper, we take a unified view on both classes of methods, leading to the first explicit convergence rates of matching pursuit methods in an optimization sense, for general sets of atoms. We derive sublinear (1/t) convergence for both classes on general smooth objectives, and linear convergence on strongly convex objectives, as well as a clear correspondence of algorithm variants. Our presented algorithms and rates are affine invariant, and do not need any incoherence or sparsity assumptions.}, author = {Locatello, Francesco and Khanna, Rajiv and Tschannen, Michael and Jaggi, Martin}, booktitle = {Proceedings of the 20th International Conference on Artificial Intelligence and Statistics}, location = {Fort Lauderdale, FL, United States}, pages = {860--868}, publisher = {ML Research Press}, title = {{A unified optimization view on generalized matching pursuit and Frank-Wolfe}}, volume = {54}, year = {2017}, } @inproceedings{14206, abstract = {Greedy optimization methods such as Matching Pursuit (MP) and Frank-Wolfe (FW) algorithms regained popularity in recent years due to their simplicity, effectiveness and theoretical guarantees. MP and FW address optimization over the linear span and the convex hull of a set of atoms, respectively. In this paper, we consider the intermediate case of optimization over the convex cone, parametrized as the conic hull of a generic atom set, leading to the first principled definitions of non-negative MP algorithms for which we give explicit convergence rates and demonstrate excellent empirical performance. In particular, we derive sublinear (O(1/t)) convergence on general smooth and convex objectives, and linear convergence (O(e−t)) on strongly convex objectives, in both cases for general sets of atoms. Furthermore, we establish a clear correspondence of our algorithms to known algorithms from the MP and FW literature. Our novel algorithms and analyses target general atom sets and general objective functions, and hence are directly applicable to a large variety of learning settings.}, author = {Locatello, Francesco and Tschannen, Michael and Rätsch, Gunnar and Jaggi, Martin}, booktitle = {Advances in Neural Information Processing Systems}, isbn = {9781510860964}, location = {Long Beach, CA, United States}, title = {{Greedy algorithms for cone constrained optimization with convergence guarantees}}, year = {2017}, } @article{1433, abstract = {Phat is an open-source C. ++ library for the computation of persistent homology by matrix reduction, targeted towards developers of software for topological data analysis. We aim for a simple generic design that decouples algorithms from data structures without sacrificing efficiency or user-friendliness. We provide numerous different reduction strategies as well as data types to store and manipulate the boundary matrix. We compare the different combinations through extensive experimental evaluation and identify optimization techniques that work well in practical situations. We also compare our software with various other publicly available libraries for persistent homology.}, author = {Bauer, Ulrich and Kerber, Michael and Reininghaus, Jan and Wagner, Hubert}, issn = { 0747-7171}, journal = {Journal of Symbolic Computation}, pages = {76 -- 90}, publisher = {Academic Press}, title = {{Phat - Persistent homology algorithms toolbox}}, doi = {10.1016/j.jsc.2016.03.008}, volume = {78}, year = {2017}, } @article{1228, abstract = {Since 2006, reprogrammed cells have increasingly been used as a biomedical research technique in addition to neuro-psychiatric methods. These rapidly evolving techniques allow for the generation of neuronal sub-populations, and have sparked interest not only in monogenetic neuro-psychiatric diseases, but also in poly-genetic and poly-aetiological disorders such as schizophrenia (SCZ) and bipolar disorder (BPD). This review provides a summary of 19 publications on reprogrammed adult somatic cells derived from patients with SCZ, and five publications using this technique in patients with BPD. As both disorders are complex and heterogeneous, there is a plurality of hypotheses to be tested in vitro. In SCZ, data on alterations of dopaminergic transmission in vitro are sparse, despite the great explanatory power of the so-called DA hypothesis of SCZ. Some findings correspond to perturbations of cell energy metabolism, and observations in reprogrammed cells suggest neuro-developmental alterations. Some studies also report on the efficacy of medicinal compounds to revert alterations observed in cellular models. However, due to the paucity of replication studies, no comprehensive conclusions can be drawn from studies using reprogrammed cells at the present time. In the future, findings from cell culture methods need to be integrated with clinical, epidemiological, pharmacological and imaging data in order to generate a more comprehensive picture of SCZ and BPD.}, author = {Sauerzopf, Ulrich and Sacco, Roberto and Novarino, Gaia and Niello, Marco and Weidenauer, Ana and Praschak Rieder, Nicole and Sitte, Harald and Willeit, Matthaeus}, journal = {European Journal of Neuroscience}, number = {1}, pages = {45 -- 57}, publisher = {Wiley-Blackwell}, title = {{Are reprogrammed cells a useful tool for studying dopamine dysfunction in psychotic disorders? A review of the current evidence}}, doi = {10.1111/ejn.13418}, volume = {45}, year = {2017}, } @article{1294, abstract = {We study controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize the expected mean-payoff performance and stability (also known as variability in the literature). We argue that the basic notion of expressing the stability using the statistical variance of the mean payoff is sometimes insufficient, and propose an alternative definition. We show that a strategy ensuring both the expected mean payoff and the variance below given bounds requires randomization and memory, under both the above definitions. We then show that the problem of finding such a strategy can be expressed as a set of constraints.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín}, journal = {Journal of Computer and System Sciences}, pages = {144 -- 170}, publisher = {Elsevier}, title = {{Trading performance for stability in Markov decision processes}}, doi = {10.1016/j.jcss.2016.09.009}, volume = {84}, year = {2017}, } @inproceedings{13160, abstract = {Transforming deterministic ω -automata into deterministic parity automata is traditionally done using variants of appearance records. We present a more efficient variant of this approach, tailored to Rabin automata, and several optimizations applicable to all appearance records. We compare the methods experimentally and find out that our method produces smaller automata than previous approaches. Moreover, the experiments demonstrate the potential of our method for LTL synthesis, using LTL-to-Rabin translators. It leads to significantly smaller parity automata when compared to state-of-the-art approaches on complex formulae.}, author = {Kretinsky, Jan and Meggendorfer, Tobias and Waldmann, Clara and Weininger, Maximilian}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783662545768}, issn = {1611-3349}, location = {Uppsala, Sweden}, pages = {443--460}, publisher = {Springer}, title = {{Index appearance record for transforming Rabin automata into parity automata}}, doi = {10.1007/978-3-662-54577-5_26}, volume = {10205}, year = {2017}, } @article{1063, abstract = {Severe environmental change can drive a population extinct unless the population adapts in time to the new conditions (“evolutionary rescue”). How does biparental sexual reproduction influence the chances of population persistence compared to clonal reproduction or selfing? In this article, we set up a one‐locus two‐allele model for adaptation in diploid species, where rescue is contingent on the establishment of the mutant homozygote. Reproduction can occur by random mating, selfing, or clonally. Random mating generates and destroys the rescue mutant; selfing is efficient at generating it but at the same time depletes the heterozygote, which can lead to a low mutant frequency in the standing genetic variation. Due to these (and other) antagonistic effects, we find a nontrivial dependence of population survival on the rate of sex/selfing, which is strongly influenced by the dominance coefficient of the mutation before and after the environmental change. Importantly, since mating with the wild‐type breaks the mutant homozygote up, a slow decay of the wild‐type population size can impede rescue in randomly mating populations.}, author = {Uecker, Hildegard}, issn = {0014-3820}, journal = {Evolution}, number = {4}, pages = {845 -- 858}, publisher = {Wiley-Blackwell}, title = {{Evolutionary rescue in randomly mating, selfing, and clonal populations}}, doi = {10.1111/evo.13191}, volume = {71}, year = {2017}, } @article{1065, abstract = {We consider the problem of reachability in pushdown graphs. We study the problem for pushdown graphs with constant treewidth. Even for pushdown graphs with treewidth 1, for the reachability problem we establish the following: (i) the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem would contradict the k-clique conjecture and imply faster combinatorial algorithms for cliques in graphs.}, author = {Chatterjee, Krishnendu and Osang, Georg F}, issn = {0020-0190}, journal = {Information Processing Letters}, pages = {25 -- 29}, publisher = {Elsevier}, title = {{Pushdown reachability with constant treewidth}}, doi = {10.1016/j.ipl.2017.02.003}, volume = {122}, year = {2017}, } @article{1066, abstract = {Simulation is an attractive alternative to language inclusion for automata as it is an under-approximation of language inclusion, but usually has much lower complexity. Simulation has also been extended in two orthogonal directions, namely, (1) fair simulation, for simulation over specified set of infinite runs; and (2) quantitative simulation, for simulation between weighted automata. While fair trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial time. For weighted automata, the (quantitative) language inclusion problem is undecidable in general, whereas the (quantitative) simulation reduces to quantitative games, which admit pseudo-polynomial time algorithms. In this work, we study (quantitative) simulation for weighted automata with Büchi acceptance conditions, i.e., we generalize fair simulation from non-weighted automata to weighted automata. We show that imposing Büchi acceptance conditions on weighted automata changes many fundamental properties of the simulation games, yet they still admit pseudo-polynomial time algorithms.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan and Velner, Yaron}, journal = {Information and Computation}, number = {2}, pages = {143 -- 166}, publisher = {Elsevier}, title = {{Quantitative fair simulation games}}, doi = {10.1016/j.ic.2016.10.006}, volume = {254}, year = {2017}, } @article{1067, abstract = {Embryo morphogenesis relies on highly coordinated movements of different tissues. However, remarkably little is known about how tissues coordinate their movements to shape the embryo. In zebrafish embryogenesis, coordinated tissue movements first become apparent during “doming,” when the blastoderm begins to spread over the yolk sac, a process involving coordinated epithelial surface cell layer expansion and mesenchymal deep cell intercalations. Here, we find that active surface cell expansion represents the key process coordinating tissue movements during doming. By using a combination of theory and experiments, we show that epithelial surface cells not only trigger blastoderm expansion by reducing tissue surface tension, but also drive blastoderm thinning by inducing tissue contraction through radial deep cell intercalations. Thus, coordinated tissue expansion and thinning during doming relies on surface cells simultaneously controlling tissue surface tension and radial tissue contraction.}, author = {Morita, Hitoshi and Grigolon, Silvia and Bock, Martin and Krens, Gabriel and Salbreux, Guillaume and Heisenberg, Carl-Philipp J}, issn = {1534-5807}, journal = {Developmental Cell}, number = {4}, pages = {354 -- 366}, publisher = {Cell Press}, title = {{The physical basis of coordinated tissue spreading in zebrafish gastrulation}}, doi = {10.1016/j.devcel.2017.01.010}, volume = {40}, year = {2017}, } @article{1072, abstract = {Given a finite set of points in Rn and a radius parameter, we study the Čech, Delaunay–Čech, Delaunay (or alpha), and Wrap complexes in the light of generalized discrete Morse theory. Establishing the Čech and Delaunay complexes as sublevel sets of generalized discrete Morse functions, we prove that the four complexes are simple-homotopy equivalent by a sequence of simplicial collapses, which are explicitly described by a single discrete gradient field.}, author = {Bauer, Ulrich and Edelsbrunner, Herbert}, journal = {Transactions of the American Mathematical Society}, number = {5}, pages = {3741 -- 3762}, publisher = {American Mathematical Society}, title = {{The Morse theory of Čech and delaunay complexes}}, doi = {10.1090/tran/6991}, volume = {369}, year = {2017}, } @article{1073, abstract = {Let X and Y be finite simplicial sets (e.g. finite simplicial complexes), both equipped with a free simplicial action of a finite group G. Assuming that Y is d-connected and dimX≤2d, for some d≥1, we provide an algorithm that computes the set of all equivariant homotopy classes of equivariant continuous maps |X|→|Y|; the existence of such a map can be decided even for dimX≤2d+1. This yields the first algorithm for deciding topological embeddability of a k-dimensional finite simplicial complex into Rn under the condition k≤23n−1. More generally, we present an algorithm that, given a lifting-extension problem satisfying an appropriate stability assumption, computes the set of all homotopy classes of solutions. This result is new even in the non-equivariant situation.}, author = {Čadek, Martin and Krcál, Marek and Vokřínek, Lukáš}, issn = {01795376}, journal = {Discrete & Computational Geometry}, number = {4}, pages = {915 -- 965}, publisher = {Springer}, title = {{Algorithmic solvability of the lifting extension problem}}, doi = {10.1007/s00454-016-9855-6}, volume = {54}, year = {2017}, } @article{1076, abstract = {Signatures of the Coulomb corrections in the photoelectron momentum distribution during laser-induced ionization of atoms or ions in tunneling and multiphoton regimes are investigated analytically in the case of a one-dimensional problem. A high-order Coulomb-corrected strong-field approximation is applied, where the exact continuum state in the S matrix is approximated by the eikonal Coulomb-Volkov state including the second-order corrections to the eikonal. Although without high-order corrections our theory coincides with the known analytical R-matrix (ARM) theory, we propose a simplified procedure for the matrix element derivation. Rather than matching the eikonal Coulomb-Volkov wave function with the bound state as in the ARM theory to remove the Coulomb singularity, we calculate the matrix element via the saddle-point integration method by time as well as by coordinate, and in this way avoiding the Coulomb singularity. The momentum shift in the photoelectron momentum distribution with respect to the ARM theory due to high-order corrections is analyzed for tunneling and multiphoton regimes. The relation of the quantum corrections to the tunneling delay time is discussed.}, author = {Klaiber, Michael and Daněk, Jiří and Yakaboylu, Enderalp and Hatsagortsyan, Karen and Keitel, Christoph}, issn = {2469-9926}, journal = { Physical Review A - Atomic, Molecular, and Optical Physics}, number = {2}, publisher = {American Physical Society}, title = {{Strong-field ionization via a high-order Coulomb-corrected strong-field approximation}}, doi = {10.1103/PhysRevA.95.023403}, volume = {95}, year = {2017}, } @article{1077, abstract = {Viral capsids are structurally constrained by interactions among the amino acids (AAs) of their constituent proteins. Therefore, epistasis is expected to evolve among physically interacting sites and to influence the rates of substitution. To study the evolution of epistasis, we focused on the major structural protein of the fX174 phage family by first reconstructing the ancestral protein sequences of 18 species using a Bayesian statistical framework. The inferred ancestral reconstruction differed at eight AAs, for a total of 256 possible ancestral haplotypes. For each ancestral haplotype and the extant species, we estimated, in silico, the distribution of free energies and epistasis of the capsid structure. We found that free energy has not significantly increased but epistasis has. We decomposed epistasis up to fifth order and found that higher-order epistasis sometimes compensates pairwise interactions making the free energy seem additive. The dN/dS ratio is low, suggesting strong purifying selection, and that structure is under stabilizing selection. We synthesized phages carrying ancestral haplotypes of the coat protein gene and measured their fitness experimentally. Our findings indicate that stabilizing mutations can have higher fitness, and that fitness optima do not necessarily coincide with energy minima.}, author = {Fernandes Redondo, Rodrigo A and Vladar, Harold and Włodarski, Tomasz and Bollback, Jonathan P}, issn = {1742-5689}, journal = {Journal of the Royal Society Interface}, number = {126}, publisher = {Royal Society of London}, title = {{Evolutionary interplay between structure, energy and epistasis in the coat protein of the ϕX174 phage family}}, doi = {10.1098/rsif.2016.0139}, volume = {14}, year = {2017}, } @article{1078, abstract = {One of the key questions in understanding plant development is how single cells behave in a larger context of the tissue. Therefore, it requires the observation of the whole organ with a high spatial- as well as temporal resolution over prolonged periods of time, which may cause photo-toxic effects. This protocol shows a plant sample preparation method for light-sheet microscopy, which is characterized by mounting the plant vertically on the surface of a gel. The plant is mounted in such a way that the roots are submerged in a liquid medium while the leaves remain in the air. In order to ensure photosynthetic activity of the plant, a custom-made lighting system illuminates the leaves. To keep the roots in darkness the water surface is covered with sheets of black plastic foil. This method allows long-term imaging of plant organ development in standardized conditions. }, author = {Von Wangenheim, Daniel and Hauschild, Robert and Friml, Jirí}, journal = {Journal of visualized experiments JoVE}, number = {119}, publisher = {Journal of Visualized Experiments}, title = {{Light sheet fluorescence microscopy of plant roots growing on the surface of a gel}}, doi = {10.3791/55044}, volume = {2017}, year = {2017}, } @article{1079, abstract = {We study the ionization problem in the Thomas-Fermi-Dirac-von Weizsäcker theory for atoms and molecules. We prove the nonexistence of minimizers for the energy functional when the number of electrons is large and the total nuclear charge is small. This nonexistence result also applies to external potentials decaying faster than the Coulomb potential. In the case of arbitrary nuclear charges, we obtain the nonexistence of stable minimizers and radial minimizers.}, author = {Nam, Phan and Van Den Bosch, Hanne}, issn = {1385-0172}, journal = {Mathematical Physics, Analysis and Geometry}, number = {2}, publisher = {Springer}, title = {{Nonexistence in Thomas Fermi-Dirac-von Weizsäcker theory with small nuclear charges}}, doi = {10.1007/s11040-017-9238-0}, volume = {20}, year = {2017}, } @article{1080, abstract = {Reconstructing the evolutionary history of metastases is critical for understanding their basic biological principles and has profound clinical implications. Genome-wide sequencing data has enabled modern phylogenomic methods to accurately dissect subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented depth. However, existing methods are not designed to infer metastatic seeding patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny of metastases and map subclones to their anatomic locations. Treeomics infers comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers. Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing artifacts; 7% of variants were misclassified by conventional statistical methods. These artifacts can skew phylogenies by creating illusory tumour heterogeneity among distinct samples. In silico benchmarking on simulated tumour phylogenies across a wide range of sample purities (15–95%) and sequencing depths (25-800 × ) demonstrates the accuracy of Treeomics compared with existing methods.}, author = {Reiter, Johannes and Makohon Moore, Alvin and Gerold, Jeffrey and Božić, Ivana and Chatterjee, Krishnendu and Iacobuzio Donahue, Christine and Vogelstein, Bert and Nowak, Martin}, issn = {2041-1723}, journal = {Nature Communications}, publisher = {Nature Publishing Group}, title = {{Reconstructing metastatic seeding patterns of human cancers}}, doi = {10.1038/ncomms14114}, volume = {8}, year = {2017}, }