@inproceedings{1607, abstract = {We consider the core algorithmic problems related to verification of systems with respect to three classical quantitative properties, namely, the mean-payoff property, the ratio property, 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 constant treewidth, and it is well-known that the control-flow graphs of most programs have constant treewidth. Let n denote the number of nodes of a graph, m the number of edges (for constant treewidth graphs m=O(n)) and W the largest absolute value of the weights. Our main theoretical results are as follows. First, for constant treewidth graphs we present an algorithm that approximates the mean-payoff value within a multiplicative factor of ϵ in time O(n⋅log(n/ϵ)) and linear space, as compared to the classical algorithms that require quadratic time. Second, for the ratio property we present an algorithm that for constant treewidth graphs works in time O(n⋅log(|a⋅b|))=O(n⋅log(n⋅W)), when the output is ab, as compared to the previously best known algorithm with running time O(n2⋅log(n⋅W)). Third, for the minimum initial credit problem we show that (i) for general graphs the problem can be solved in O(n2⋅m) time and the associated decision problem can be solved in O(n⋅m) time, improving the previous known O(n3⋅m⋅log(n⋅W)) and O(n2⋅m) bounds, respectively; and (ii) for constant treewidth graphs we present an algorithm that requires O(n⋅logn) time, improving the previous known O(n4⋅log(n⋅W)) bound. 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}, location = {San Francisco, CA, USA}, pages = {140 -- 157}, publisher = {Springer}, title = {{Faster algorithms for quantitative verification in constant treewidth graphs}}, doi = {10.1007/978-3-319-21690-4_9}, volume = {9206}, year = {2015}, } @inproceedings{1714, abstract = {We present a flexible framework for the automated competitive analysis of on-line scheduling algorithms for firm-deadline real-time tasks based on multi-objective graphs: Given a task set and an on-line scheduling algorithm specified as a labeled transition system, along with some optional safety, liveness, and/or limit-average constraints for the adversary, we automatically compute the competitive ratio of the algorithm w.r.t. A clairvoyant scheduler. We demonstrate the flexibility and power of our approach by comparing the competitive ratio of several on-line algorithms, including Dover, that have been proposed in the past, for various task sets. Our experimental results reveal that none of these algorithms is universally optimal, in the sense that there are task sets where other schedulers provide better performance. Our framework is hence a very useful design tool for selecting optimal algorithms for a given application.}, author = {Chatterjee, Krishnendu and Pavlogiannis, Andreas and Kößler, Alexander and Schmid, Ulrich}, booktitle = {Real-Time Systems Symposium}, location = {Rome, Italy}, number = {January}, pages = {118 -- 127}, publisher = {IEEE}, title = {{A framework for automated competitive analysis of on-line scheduling of firm-deadline tasks}}, doi = {10.1109/RTSS.2014.9}, volume = {2015}, year = {2015}, } @inproceedings{1633, abstract = {We present a method for simulating brittle fracture under the assumptions of quasi-static linear elastic fracture mechanics (LEFM). Using the boundary element method (BEM) and Lagrangian crack-fronts, we produce highly detailed fracture surfaces. The computational cost of the BEM is alleviated by using a low-resolution mesh and interpolating the resulting stress intensity factors when propagating the high-resolution crack-front. Our system produces physics-based fracture surfaces with high spatial and temporal resolution, taking spatial variation of material toughness and/or strength into account. It also allows for crack initiation to be handled separately from crack propagation, which is not only more reasonable from a physics perspective, but can also be used to control the simulation. Separating the resolution of the crack-front from the resolution of the computational mesh increases the efficiency and therefore the amount of visual detail on the resulting fracture surfaces. The BEM also allows us to re-use previously computed blocks of the system matrix.}, author = {Hahn, David and Wojtan, Christopher J}, location = {Los Angeles, CA, United States}, number = {4}, publisher = {ACM}, title = {{High-resolution brittle fracture simulation with boundary elements}}, doi = {10.1145/2766896}, volume = {34}, year = {2015}, } @article{1537, abstract = {3D amoeboid cell migration is central to many developmental and disease-related processes such as cancer metastasis. Here, we identify a unique prototypic amoeboid cell migration mode in early zebrafish embryos, termed stable-bleb migration. Stable-bleb cells display an invariant polarized balloon-like shape with exceptional migration speed and persistence. Progenitor cells can be reversibly transformed into stable-bleb cells irrespective of their primary fate and motile characteristics by increasing myosin II activity through biochemical or mechanical stimuli. Using a combination of theory and experiments, we show that, in stable-bleb cells, cortical contractility fluctuations trigger a stochastic switch into amoeboid motility, and a positive feedback between cortical flows and gradients in contractility maintains stable-bleb cell polarization. We further show that rearward cortical flows drive stable-bleb cell migration in various adhesive and non-adhesive environments, unraveling a highly versatile amoeboid migration phenotype.}, author = {Ruprecht, Verena and Wieser, Stefan and Callan Jones, Andrew and Smutny, Michael and Morita, Hitoshi and Sako, Keisuke and Barone, Vanessa and Ritsch Marte, Monika and Sixt, Michael K and Voituriez, Raphaël and Heisenberg, Carl-Philipp J}, journal = {Cell}, number = {4}, pages = {673 -- 685}, publisher = {Cell Press}, title = {{Cortical contractility triggers a stochastic switch to fast amoeboid cell motility}}, doi = {10.1016/j.cell.2015.01.008}, volume = {160}, year = {2015}, } @article{1591, abstract = {Auxin participates in a multitude of developmental processes, as well as responses to environmental cues. Compared with other plant hormones, auxin exhibits a unique property, as it undergoes directional, cell-to-cell transport facilitated by plasma membrane-localized transport proteins. Among them, a prominent role has been ascribed to the PIN family of auxin efflux facilitators. PIN proteins direct polar auxin transport on account of their asymmetric subcellular localizations. In this review, we provide an overview of the multiple developmental roles of PIN proteins, including the atypical endoplasmic reticulum-localized members of the family, and look at the family from an evolutionary perspective. Next, we cover the cell biological and molecular aspects of PIN function, in particular the establishment of their polar subcellular localization. Hormonal and environmental inputs into the regulation of PIN action are summarized as well.}, author = {Adamowski, Maciek and Friml, Jirí}, journal = {Plant Cell}, number = {1}, pages = {20 -- 32}, publisher = {American Society of Plant Biologists}, title = {{PIN-dependent auxin transport: Action, regulation, and evolution}}, doi = {10.1105/tpc.114.134874}, volume = {27}, year = {2015}, } @article{1677, abstract = {We consider real symmetric and complex Hermitian random matrices with the additional symmetry hxy = hN-y,N-x. The matrix elements are independent (up to the fourfold symmetry) and not necessarily identically distributed. This ensemble naturally arises as the Fourier transform of a Gaussian orthogonal ensemble. Italso occurs as the flip matrix model - an approximation of the two-dimensional Anderson model at small disorder. We show that the density of states converges to the Wigner semicircle law despite the new symmetry type. We also prove the local version of the semicircle law on the optimal scale.}, author = {Alt, Johannes}, journal = {Journal of Mathematical Physics}, number = {10}, publisher = {American Institute of Physics}, title = {{The local semicircle law for random matrices with a fourfold symmetry}}, doi = {10.1063/1.4932606}, volume = {56}, year = {2015}, } @article{1678, abstract = {High-throughput live-cell screens are intricate elements of systems biology studies and drug discovery pipelines. Here, we demonstrate an optogenetics-assisted method that avoids the need for chemical activators and reporters, reduces the number of operational steps and increases information content in a cell-based small-molecule screen against human protein kinases, including an orphan receptor tyrosine kinase. This blueprint for all-optical screening can be adapted to many drug targets and cellular processes.}, author = {Inglés Prieto, Álvaro and Gschaider-Reichhart, Eva and Muellner, Markus and Nowak, Matthias and Nijman, Sebastian and Grusch, Michael and Janovjak, Harald L}, journal = {Nature Chemical Biology}, number = {12}, pages = {952 -- 954}, publisher = {Nature Publishing Group}, title = {{Light-assisted small-molecule screening against protein kinases}}, doi = {10.1038/nchembio.1933}, volume = {11}, year = {2015}, } @article{1576, abstract = {Gene expression is controlled primarily by interactions between transcription factor proteins (TFs) and the regulatory DNA sequence, a process that can be captured well by thermodynamic models of regulation. These models, however, neglect regulatory crosstalk: the possibility that noncognate TFs could initiate transcription, with potentially disastrous effects for the cell. Here, we estimate the importance of crosstalk, suggest that its avoidance strongly constrains equilibrium models of TF binding, and propose an alternative nonequilibrium scheme that implements kinetic proofreading to suppress erroneous initiation. This proposal is consistent with the observed covalent modifications of the transcriptional apparatus and predicts increased noise in gene expression as a trade-off for improved specificity. Using information theory, we quantify this trade-off to find when optimal proofreading architectures are favored over their equilibrium counterparts. Such architectures exhibit significant super-Poisson noise at low expression in steady state.}, author = {Cepeda Humerez, Sarah A and Rieckh, Georg and Tkacik, Gasper}, journal = {Physical Review Letters}, number = {24}, publisher = {American Physical Society}, title = {{Stochastic proofreading mechanism alleviates crosstalk in transcriptional regulation}}, doi = {10.1103/PhysRevLett.115.248101}, volume = {115}, year = {2015}, } @unpublished{8183, abstract = {We study conditions under which a finite simplicial complex $K$ can be mapped to $\mathbb R^d$ without higher-multiplicity intersections. An almost $r$-embedding is a map $f: K\to \mathbb R^d$ such that the images of any $r$ pairwise disjoint simplices of $K$ do not have a common point. We show that if $r$ is not a prime power and $d\geq 2r+1$, then there is a counterexample to the topological Tverberg conjecture, i.e., there is an almost $r$-embedding of the $(d+1)(r-1)$-simplex in $\mathbb R^d$. This improves on previous constructions of counterexamples (for $d\geq 3r$) based on a series of papers by M. \"Ozaydin, M. Gromov, P. Blagojevi\'c, F. Frick, G. Ziegler, and the second and fourth present authors. The counterexamples are obtained by proving the following algebraic criterion in codimension 2: If $r\ge3$ and if $K$ is a finite $2(r-1)$-complex then there exists an almost $r$-embedding $K\to \mathbb R^{2r}$ if and only if there exists a general position PL map $f:K\to \mathbb R^{2r}$ such that the algebraic intersection number of the $f$-images of any $r$ pairwise disjoint simplices of $K$ is zero. This result can be restated in terms of cohomological obstructions or equivariant maps, and extends an analogous codimension 3 criterion by the second and fourth authors. As another application we classify ornaments $f:S^3 \sqcup S^3\sqcup S^3\to \mathbb R^5$ up to ornament concordance. It follows from work of M. Freedman, V. Krushkal and P. Teichner that the analogous criterion for $r=2$ is false. We prove a lemma on singular higher-dimensional Borromean rings, yielding an elementary proof of the counterexample.}, author = {Avvakumov, Sergey and Mabillard, Isaac and Skopenkov, A. and Wagner, Uli}, booktitle = {arXiv}, title = {{Eliminating higher-multiplicity intersections, III. Codimension 2}}, year = {2015}, } @misc{5441, abstract = {We study algorithmic questions for concurrent systems where the transitions are labeled from a complete, closed semiring, and path properties are algebraic with semiring operations. The algebraic path properties can model dataflow analysis problems, the shortest path problem, and many other natural problems that arise in program analysis. We consider that each component of the concurrent system is a graph with constant treewidth, a property satisfied by the controlflow graphs of most programs. We allow for multiple possible queries, which arise naturally in demand driven dataflow analysis. The study of multiple queries allows us to consider the tradeoff between the resource usage of the one-time preprocessing and for each individual query. The traditional approach constructs the product graph of all components and applies the best-known graph algorithm on the product. In this approach, even the answer to a single query requires the transitive closure (i.e., the results of all possible queries), which provides no room for tradeoff between preprocessing and query time. Our main contributions are algorithms that significantly improve the worst-case running time of the traditional approach, and provide various tradeoffs depending on the number of queries. For example, in a concurrent system of two components, the traditional approach requires hexic time in the worst case for answering one query as well as computing the transitive closure, whereas we show that with one-time preprocessing in almost cubic time, each subsequent query can be answered in at most linear time, and even the transitive closure can be computed in almost quartic time. Furthermore, we establish conditional optimality results showing that the worst-case running time of our algorithms cannot be improved without achieving major breakthroughs in graph algorithms (i.e., improving the worst-case bound for the shortest path problem in general graphs). Preliminary experimental results show that our algorithms perform favorably on several benchmarks.}, author = {Chatterjee, Krishnendu and Ibsen-Jensen, Rasmus and Goharshady, Amir and Pavlogiannis, Andreas}, issn = {2664-1690}, pages = {24}, publisher = {IST Austria}, title = {{Algorithms for algebraic path properties in concurrent systems of constant treewidth components}}, doi = {10.15479/AT:IST-2015-340-v1-1}, year = {2015}, }