@article{2926, abstract = {To fight infectious diseases, host immune defenses are employed at multiple levels. Sanitary behavior, such as pathogen avoidance and removal, acts as a first line of defense to prevent infection [1] before activation of the physiological immune system. Insect societies have evolved a wide range of collective hygiene measures and intensive health care toward pathogen-exposed group members [2]. One of the most common behaviors is allogrooming, in which nestmates remove infectious particles from the body surfaces of exposed individuals [3]. Here we show that, in invasive garden ants, grooming of fungus-exposed brood is effective beyond the sheer mechanical removal of fungal conidiospores; it also includes chemical disinfection through the application of poison produced by the ants themselves. Formic acid is the main active component of the poison. It inhibits fungal growth of conidiospores remaining on the brood surface after grooming and also those collected in the mouth of the grooming ant. This dual function is achieved by uptake of the poison droplet into the mouth through acidopore self-grooming and subsequent application onto the infectious brood via brood grooming. This extraordinary behavior extends the current understanding of grooming and the establishment of social immunity in insect societies.}, author = {Tragust, Simon and Mitteregger, Barbara and Barone, Vanessa and Konrad, Matthias and Ugelvig, Line V and Cremer, Sylvia}, journal = {Current Biology}, number = {1}, pages = {76 -- 82}, publisher = {Cell Press}, title = {{Ants disinfect fungus-exposed brood by oral uptake and spread of their poison}}, doi = {10.1016/j.cub.2012.11.034}, volume = {23}, year = {2013}, } @article{2918, abstract = {Oriented mitosis is essential during tissue morphogenesis. The Wnt/planar cell polarity (Wnt/PCP) pathway orients mitosis in a number of developmental systems, including dorsal epiblast cell divisions along the animal-vegetal (A-V) axis during zebrafish gastrulation. How Wnt signalling orients the mitotic plane is, however, unknown. Here we show that, in dorsal epiblast cells, anthrax toxin receptor 2a (Antxr2a) accumulates in a polarized cortical cap, which is aligned with the embryonic A-V axis and forecasts the division plane. Filamentous actin (F-actin) also forms an A-V polarized cap, which depends on Wnt/PCP and its effectors RhoA and Rock2. Antxr2a is recruited to the cap by interacting with actin. Antxr2a also interacts with RhoA and together they activate the diaphanous-related formin zDia2. Mechanistically, Antxr2a functions as a Wnt-dependent polarized determinant, which, through the action of RhoA and zDia2, exerts torque on the spindle to align it with the A-V axis. }, author = {Castanon, Irinka and Abrami, Laurence and Holtzer, Laurent and Heisenberg, Carl-Philipp J and Van Der Goot, Françoise and González Gaitán, Marcos}, journal = {Nature Cell Biology}, number = {1}, pages = {28 -- 39}, publisher = {Nature Publishing Group}, title = {{Anthrax toxin receptor 2a controls mitotic spindle positioning}}, doi = {10.1038/ncb2632}, volume = {15}, year = {2013}, } @article{2919, abstract = {The distribution of the phytohormone auxin regulates many aspects of plant development including growth response to gravity. Gravitropic root curvature involves coordinated and asymmetric cell elongation between the lower and upper side of the root, mediated by differential cellular auxin levels. The asymmetry in the auxin distribution is established and maintained by a spatio-temporal regulation of the PIN-FORMED (PIN) auxin transporter activity. We provide novel insights into the complex regulation of PIN abundance and activity during root gravitropism. We show that PIN2 turnover is differentially regulated on the upper and lower side of gravistimulated roots by distinct but partially overlapping auxin feedback mechanisms. In addition to regulating transcription and clathrin-mediated internalization, auxin also controls PIN abundance at the plasma membrane by promoting their vacuolar targeting and degradation. This effect of elevated auxin levels requires the activity of SKP-Cullin-F-box TIR1/AFB (SCF TIR1/AFB)-dependent pathway. Importantly, also suboptimal auxin levels mediate PIN degradation utilizing the same signalling pathway. These feedback mechanisms are functionally important during gravitropic response and ensure fine-tuning of auxin fluxes for maintaining as well as terminating asymmetric growth.}, author = {Baster, Pawel and Robert, Stéphanie and Kleine Vehn, Jürgen and Vanneste, Steffen and Kania, Urszula and Grunewald, Wim and De Rybel, Bert and Beeckman, Tom and Friml, Jirí}, journal = {EMBO Journal}, number = {2}, pages = {260 -- 274}, publisher = {Wiley-Blackwell}, title = {{SCF^TIR1 AFB-auxin signalling regulates PIN vacuolar trafficking and auxin fluxes during root gravitropism}}, doi = {10.1038/emboj.2012.310}, volume = {32}, year = {2013}, } @article{2920, abstract = {Cell polarisation in development is a common and fundamental process underlying embryo patterning and morphogenesis, and has been extensively studied over the past years. Our current knowledge of cell polarisation in development is predominantly based on studies that have analysed polarisation of single cells, such as eggs, or cellular aggregates with a stable polarising interface, such as cultured epithelial cells (St Johnston and Ahringer, 2010). However, in embryonic development, particularly of vertebrates, cell polarisation processes often encompass large numbers of cells that are placed within moving and proliferating tissues, and undergo mesenchymal-to-epithelial transitions with a highly complex spatiotemporal choreography. How such intricate cell polarisation processes in embryonic development are achieved has only started to be analysed. By using live imaging of neurulation in the transparent zebrafish embryo, Buckley et al (2012) now describe a novel polarisation strategy by which cells assemble an apical domain in the part of their cell body that intersects with the midline of the forming neural rod. This mechanism, along with the previously described mirror-symmetric divisions (Tawk et al, 2007), is thought to trigger formation of both neural rod midline and lumen.}, author = {Compagnon, Julien and Heisenberg, Carl-Philipp J}, journal = {EMBO Journal}, number = {1}, pages = {1 -- 3}, publisher = {Wiley-Blackwell}, title = {{Neurulation coordinating cell polarisation and lumen formation}}, doi = {10.1038/emboj.2012.325}, volume = {32}, year = {2013}, } @article{2858, abstract = {Tumor growth is caused by the acquisition of driver mutations, which enhance the net reproductive rate of cells. Driver mutations may increase cell division, reduce cell death, or allow cells to overcome density-limiting effects. We study the dynamics of tumor growth as one additional driver mutation is acquired. Our models are based on two-type branching processes that terminate in either tumor disappearance or tumor detection. In our first model, both cell types grow exponentially, with a faster rate for cells carrying the additional driver. We find that the additional driver mutation does not affect the survival probability of the lesion, but can substantially reduce the time to reach the detectable size if the lesion is slow growing. In our second model, cells lacking the additional driver cannot exceed a fixed carrying capacity, due to density limitations. In this case, the time to detection depends strongly on this carrying capacity. Our model provides a quantitative framework for studying tumor dynamics during different stages of progression. We observe that early, small lesions need additional drivers, while late stage metastases are only marginally affected by them. These results help to explain why additional driver mutations are typically not detected in fast-growing metastases.}, author = {Reiter, Johannes and Božić, Ivana and Allen, Benjamin and Chatterjee, Krishnendu and Nowak, Martin}, journal = {Evolutionary Applications}, number = {1}, pages = {34 -- 45}, publisher = {Wiley-Blackwell}, title = {{The effect of one additional driver mutation on tumor progression}}, doi = {10.1111/eva.12020}, volume = {6}, year = {2013}, } @article{2859, abstract = {Given a continuous function f:X-R on a topological space, we consider the preimages of intervals and their homology groups and show how to read the ranks of these groups from the extended persistence diagram of f. In addition, we quantify the robustness of the homology classes under perturbations of f using well groups, and we show how to read the ranks of these groups from the same extended persistence diagram. The special case X=R3 has ramifications in the fields of medical imaging and scientific visualization.}, author = {Bendich, Paul and Edelsbrunner, Herbert and Morozov, Dmitriy and Patel, Amit}, journal = {Homology, Homotopy and Applications}, number = {1}, pages = {51 -- 72}, publisher = {International Press}, title = {{Homology and robustness of level and interlevel sets}}, doi = {10.4310/HHA.2013.v15.n1.a3}, volume = {15}, year = {2013}, } @article{3116, abstract = {Multithreaded programs coordinate their interaction through synchronization primitives like mutexes and semaphores, which are managed by an OS-provided resource manager. We propose algorithms for the automatic construction of code-aware resource managers for multithreaded embedded applications. Such managers use knowledge about the structure and resource usage (mutex and semaphore usage) of the threads to guarantee deadlock freedom and progress while managing resources in an efficient way. Our algorithms compute managers as winning strategies in certain infinite games, and produce a compact code description of these strategies. We have implemented the algorithms in the tool Cynthesis. Given a multithreaded program in C, the tool produces C code implementing a code-aware resource manager. We show in experiments that Cynthesis produces compact resource managers within a few minutes on a set of embedded benchmarks with up to 6 threads. © 2012 Springer Science+Business Media, LLC.}, author = {Chatterjee, Krishnendu and De Alfaro, Luca and Faella, Marco and Majumdar, Ritankar and Raman, Vishwanath}, journal = {Formal Methods in System Design}, number = {2}, pages = {142 -- 174}, publisher = {Springer}, title = {{Code aware resource management}}, doi = {10.1007/s10703-012-0170-4}, volume = {42}, year = {2013}, } @article{2815, abstract = {The fact that a sum of isotropic Gaussian kernels can have more modes than kernels is surprising. Extra (ghost) modes do not exist in ℝ1 and are generally not well studied in higher dimensions. We study a configuration of n+1 Gaussian kernels for which there are exactly n+2 modes. We show that all modes lie on a finite set of lines, which we call axes, and study the restriction of the Gaussian mixture to these axes in order to discover that there are an exponential number of critical points in this configuration. Although the existence of ghost modes remained unknown due to the difficulty of finding examples in ℝ2, we show that the resilience of ghost modes grows like the square root of the dimension. In addition, we exhibit finite configurations of isotropic Gaussian kernels with superlinearly many modes.}, author = {Edelsbrunner, Herbert and Fasy, Brittany Terese and Rote, Günter}, journal = {Discrete & Computational Geometry}, number = {4}, pages = {797 -- 822}, publisher = {Springer}, title = {{Add isotropic Gaussian kernels at own risk: More and more resilient modes in higher dimensions}}, doi = {10.1007/s00454-013-9517-x}, volume = {49}, year = {2013}, } @inproceedings{1387, abstract = {Choices made by nondeterministic word automata depend on both the past (the prefix of the word read so far) and the future (the suffix yet to be read). In several applications, most notably synthesis, the future is diverse or unknown, leading to algorithms that are based on deterministic automata. Hoping to retain some of the advantages of nondeterministic automata, researchers have studied restricted classes of nondeterministic automata. Three such classes are nondeterministic automata that are good for trees (GFT; i.e., ones that can be expanded to tree automata accepting the derived tree languages, thus whose choices should satisfy diverse futures), good for games (GFG; i.e., ones whose choices depend only on the past), and determinizable by pruning (DBP; i.e., ones that embody equivalent deterministic automata). The theoretical properties and relative merits of the different classes are still open, having vagueness on whether they really differ from deterministic automata. In particular, while DBP ⊆ GFG ⊆ GFT, it is not known whether every GFT automaton is GFG and whether every GFG automaton is DBP. Also open is the possible succinctness of GFG and GFT automata compared to deterministic automata. We study these problems for ω-regular automata with all common acceptance conditions. We show that GFT=GFG⊃DBP, and describe a determinization construction for GFG automata.}, author = {Boker, Udi and Kuperberg, Denis and Kupferman, Orna and Skrzypczak, Michał}, location = {Riga, Latvia}, number = {PART 2}, pages = {89 -- 100}, publisher = {Springer}, title = {{Nondeterminism in the presence of a diverse or unknown future}}, doi = {10.1007/978-3-642-39212-2_11}, volume = {7966}, year = {2013}, } @inproceedings{2237, abstract = {We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.}, author = {Blanc, Régis and Gupta, Ashutosh and Kovács, Laura and Kragl, Bernhard}, location = {Stellenbosch, South Africa}, pages = {173 -- 181}, publisher = {Springer}, title = {{Tree interpolation in Vampire}}, doi = {10.1007/978-3-642-45221-5_13}, volume = {8312}, year = {2013}, } @inproceedings{2238, abstract = {We study the problem of achieving a given value in Markov decision processes (MDPs) with several independent discounted reward objectives. We consider a generalised version of discounted reward objectives, in which the amount of discounting depends on the states visited and on the objective. This definition extends the usual definition of discounted reward, and allows to capture the systems in which the value of different commodities diminish at different and variable rates. We establish results for two prominent subclasses of the problem, namely state-discount models where the discount factors are only dependent on the state of the MDP (and independent of the objective), and reward-discount models where they are only dependent on the objective (but not on the state of the MDP). For the state-discount models we use a straightforward reduction to expected total reward and show that the problem whether a value is achievable can be solved in polynomial time. For the reward-discount model we show that memory and randomisation of the strategies are required, but nevertheless that the problem is decidable and it is sufficient to consider strategies which after a certain number of steps behave in a memoryless way. For the general case, we show that when restricted to graphs (i.e. MDPs with no randomisation), pure strategies and discount factors of the form 1/n where n is an integer, the problem is in PSPACE and finite memory suffices for achieving a given value. We also show that when the discount factors are not of the form 1/n, the memory required by a strategy can be infinite. }, author = {Chatterjee, Krishnendu and Forejt, Vojtěch and Wojtczak, Dominik}, location = {Stellenbosch, South Africa}, pages = {228 -- 242}, publisher = {Springer}, title = {{Multi-objective discounted reward verification in graphs and MDPs}}, doi = {10.1007/978-3-642-45221-5_17}, volume = {8312}, year = {2013}, } @inproceedings{2243, abstract = {We show that modal logic over universally first-order definable classes of transitive frames is decidable. More precisely, let K be an arbitrary class of transitive Kripke frames definable by a universal first-order sentence. We show that the global and finite global satisfiability problems of modal logic over K are decidable in NP, regardless of choice of K. We also show that the local satisfiability and the finite local satisfiability problems of modal logic over K are decidable in NEXPTIME.}, author = {Michaliszyn, Jakub and Otop, Jan}, location = {Torino, Italy}, pages = {563 -- 577}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Elementary modal logics over transitive structures}}, doi = {10.4230/LIPIcs.CSL.2013.563}, volume = {23}, year = {2013}, } @article{2247, abstract = {Cooperative behavior, where one individual incurs a cost to help another, is a wide spread phenomenon. Here we study direct reciprocity in the context of the alternating Prisoner's Dilemma. We consider all strategies that can be implemented by one and two-state automata. We calculate the payoff matrix of all pairwise encounters in the presence of noise. We explore deterministic selection dynamics with and without mutation. Using different error rates and payoff values, we observe convergence to a small number of distinct equilibria. Two of them are uncooperative strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium is mixed and represents a cooperative alliance of several strategies, dominated by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent has cooperated; it defects once when the opponent has defected, but subsequently Forgiver attempts to re-establish cooperation even if the opponent has defected again. Forgiver is not an evolutionarily stable strategy, but the alliance, which it rules, is asymptotically stable. For a wide range of parameter values the most commonly observed outcome is convergence to the mixed equilibrium, dominated by Forgiver. Our results show that although forgiving might incur a short-term loss it can lead to a long-term gain. Forgiveness facilitates stable cooperation in the presence of exploitation and noise.}, author = {Zagorsky, Benjamin and Reiter, Johannes and Chatterjee, Krishnendu and Nowak, Martin}, journal = {PLoS One}, number = {12}, publisher = {Public Library of Science}, title = {{Forgiver triumphs in alternating prisoner's dilemma }}, doi = {10.1371/journal.pone.0080814}, volume = {8}, year = {2013}, } @inproceedings{2244, abstract = {We consider two systems (α1,...,αm) and (β1,...,βn) of curves drawn on a compact two-dimensional surface ℳ with boundary. Each αi and each βj is either an arc meeting the boundary of ℳ at its two endpoints, or a closed curve. The αi are pairwise disjoint except for possibly sharing endpoints, and similarly for the βj. We want to "untangle" the βj from the αi by a self-homeomorphism of ℳ; more precisely, we seek an homeomorphism φ: ℳ → ℳ fixing the boundary of ℳ pointwise such that the total number of crossings of the αi with the φ(βj) is as small as possible. This problem is motivated by an application in the algorithmic theory of embeddings and 3-manifolds. We prove that if ℳ is planar, i.e., a sphere with h ≥ 0 boundary components ("holes"), then O(mn) crossings can be achieved (independently of h), which is asymptotically tight, as an easy lower bound shows. In general, for an arbitrary (orientable or nonorientable) surface ℳ with h holes and of (orientable or nonorientable) genus g ≥ 0, we obtain an O((m + n)4) upper bound, again independent of h and g. }, author = {Matoušek, Jiří and Sedgwick, Eric and Tancer, Martin and Wagner, Uli}, location = {Bordeaux, France}, pages = {472 -- 483}, publisher = {Springer}, title = {{Untangling two systems of noncrossing curves}}, doi = {10.1007/978-3-319-03841-4_41}, volume = {8242}, year = {2013}, } @inproceedings{2445, abstract = {We develop program synthesis techniques that can help programmers fix concurrency-related bugs. We make two new contributions to synthesis for concurrency, the first improving the efficiency of the synthesized code, and the second improving the efficiency of the synthesis procedure itself. The first contribution is to have the synthesis procedure explore a variety of (sequential) semantics-preserving program transformations. Classically, only one such transformation has been considered, namely, the insertion of synchronization primitives (such as locks). Based on common manual bug-fixing techniques used by Linux device-driver developers, we explore additional, more efficient transformations, such as the reordering of independent instructions. The second contribution is to speed up the counterexample-guided removal of concurrency bugs within the synthesis procedure by considering partial-order traces (instead of linear traces) as counterexamples. A partial-order error trace represents a set of linear (interleaved) traces of a concurrent program all of which lead to the same error. By eliminating a partial-order error trace, we eliminate in a single iteration of the synthesis procedure all linearizations of the partial-order trace. We evaluated our techniques on several simplified examples of real concurrency bugs that occurred in Linux device drivers.}, author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten}, location = {St. Petersburg, Russia}, pages = {951 -- 967}, publisher = {Springer}, title = {{Efficient synthesis for concurrency by semantics-preserving transformations}}, doi = {10.1007/978-3-642-39799-8_68}, volume = {8044}, year = {2013}, } @inproceedings{2446, abstract = {The model-checking problem for probabilistic systems crucially relies on the translation of LTL to deterministic Rabin automata (DRW). Our recent Safraless translation [KE12, GKE12] for the LTL(F,G) fragment produces smaller automata as compared to the traditional approach. In this work, instead of DRW we consider deterministic automata with acceptance condition given as disjunction of generalized Rabin pairs (DGRW). The Safraless translation of LTL(F,G) formulas to DGRW results in smaller automata as compared to DRW. We present algorithms for probabilistic model-checking as well as game solving for DGRW conditions. Our new algorithms lead to improvement both in terms of theoretical bounds as well as practical evaluation. We compare PRISM with and without our new translation, and show that the new translation leads to significant improvements.}, author = {Chatterjee, Krishnendu and Gaiser, Andreas and Kretinsky, Jan}, location = {St. Petersburg, Russia}, pages = {559 -- 575}, publisher = {Springer}, title = {{Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis}}, doi = {10.1007/978-3-642-39799-8_37}, volume = {8044}, year = {2013}, } @inproceedings{2447, abstract = {Separation logic (SL) has gained widespread popularity because of its ability to succinctly express complex invariants of a program’s heap configurations. Several specialized provers have been developed for decidable SL fragments. However, these provers cannot be easily extended or combined with solvers for other theories that are important in program verification, e.g., linear arithmetic. In this paper, we present a reduction of decidable SL fragments to a decidable first-order theory that fits well into the satisfiability modulo theories (SMT) framework. We show how to use this reduction to automate satisfiability, entailment, frame inference, and abduction problems for separation logic using SMT solvers. Our approach provides a simple method of integrating separation logic into existing verification tools that provide SMT backends, and an elegant way of combining SL fragments with other decidable first-order theories. We implemented this approach in a verification tool and applied it to heap-manipulating programs whose verification involves reasoning in theory combinations. }, author = {Piskac, Ruzica and Wies, Thomas and Zufferey, Damien}, location = {St. Petersburg, Russia}, pages = {773 -- 789}, publisher = {Springer}, title = {{Automating separation logic using SMT}}, doi = {10.1007/978-3-642-39799-8_54}, volume = {8044}, year = {2013}, } @article{2448, abstract = {Cell-to-cell directional flow of the phytohormone auxin is primarily established by polar localization of the PIN auxin transporters, a process tightly regulated at multiple levels by auxin itself. We recently reported that, in the context of strong auxin flows, activity of the vacuolar ZIFL1.1 transporter is required for fine-tuning of polar auxin transport rates in the Arabidopsis root. In particular, ZIFL1.1 function protects plasma-membrane stability of the PIN2 carrier in epidermal root tip cells under conditions normally triggering PIN2 degradation. Here, we show that ZIFL1.1 activity at the root tip also promotes PIN1 plasma-membrane abundance in central cylinder cells, thus supporting the notion that ZIFL1.1 acts as a general positive modulator of polar auxin transport in roots.}, author = {Remy, Estelle and Baster, Pawel and Friml, Jirí and Duque, Paula}, journal = {Plant Signaling & Behavior}, number = {10}, publisher = {Landes Bioscience}, title = {{ZIFL1.1 transporter modulates polar auxin transport by stabilizing membrane abundance of multiple PINs in Arabidopsis root tip}}, doi = {10.4161/psb.25688}, volume = {8}, year = {2013}, } @article{2449, abstract = {Intracellular protein routing is mediated by vesicular transport which is tightly regulated in eukaryotes. The protein and lipid homeostasis depends on coordinated delivery of de novo synthesized or recycled cargoes to the plasma membrane by exocytosis and their subsequent removal by rerouting them for recycling or degradation. Here, we report the characterization of protein affected trafficking 3 (pat3) mutant that we identified by an epifluorescence-based forward genetic screen for mutants defective in subcellular distribution of Arabidopsis auxin transporter PIN1–GFP. While pat3 displays largely normal plant morphology and development in nutrient-rich conditions, it shows strong ectopic intracellular accumulations of different plasma membrane cargoes in structures that resemble prevacuolar compartments (PVC) with an aberrant morphology. Genetic mapping revealed that pat3 is defective in vacuolar protein sorting 35A (VPS35A), a putative subunit of the retromer complex that mediates retrograde trafficking between the PVC and trans-Golgi network. Similarly, a mutant defective in another retromer subunit, vps29, shows comparable subcellular defects in PVC morphology and protein accumulation. Thus, our data provide evidence that the retromer components VPS35A and VPS29 are essential for normal PVC morphology and normal trafficking of plasma membrane proteins in plants. In addition, we show that, out of the three VPS35 retromer subunits present in Arabidopsis thaliana genome, the VPS35 homolog A plays a prevailing role in trafficking to the lytic vacuole, presenting another level of complexity in the retromer-dependent vacuolar sorting. }, author = {Nodzyński, Tomasz and Feraru, Murguel and Hirsch, Sibylle and De Rycke, Riet and Nicuales, Claudiu and Van Leene, Jelle and De Jaeger, Geert and Vanneste, Steffen and Friml, Jirí}, journal = {Molecular Plant}, number = {6}, pages = {1849 -- 1862}, publisher = {Cell Press}, title = {{Retromer subunits VPS35A and VPS29 mediate prevacuolar compartment (PVC) function in Arabidopsis}}, doi = {10.1093/mp/sst044}, volume = {6}, year = {2013}, } @article{2466, abstract = {We introduce a new method for efficiently simulating liquid with extreme amounts of spatial adaptivity. Our method combines several key components to drastically speed up the simulation of large-scale fluid phenomena: We leverage an alternative Eulerian tetrahedral mesh discretization to significantly reduce the complexity of the pressure solve while increasing the robustness with respect to element quality and removing the possibility of locking. Next, we enable subtle free-surface phenomena by deriving novel second-order boundary conditions consistent with our discretization. We couple this discretization with a spatially adaptive Fluid-Implicit Particle (FLIP) method, enabling efficient, robust, minimally-dissipative simulations that can undergo sharp changes in spatial resolution while minimizing artifacts. Along the way, we provide a new method for generating a smooth and detailed surface from a set of particles with variable sizes. Finally, we explore several new sizing functions for determining spatially adaptive simulation resolutions, and we show how to couple them to our simulator. We combine each of these elements to produce a simulation algorithm that is capable of creating animations at high maximum resolutions while avoiding common pitfalls like inaccurate boundary conditions and inefficient computation.}, author = {Ando, Ryoichi and Thuerey, Nils and Wojtan, Christopher J}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Highly adaptive liquid simulations on tetrahedral meshes}}, doi = {10.1145/2461912.2461982}, volume = {32}, year = {2013}, } @article{2467, abstract = {This paper presents a method for computing topology changes for triangle meshes in an interactive geometric modeling environment. Most triangle meshes in practice do not exhibit desirable geometric properties, so we develop a solution that is independent of standard assumptions and robust to geometric errors. Specifically, we provide the first method for topology change applicable to arbitrary non-solid, non-manifold, non-closed, self-intersecting surfaces. We prove that this new method for topology change produces the expected conventional results when applied to solid (closed, manifold, non-self-intersecting) surfaces---that is, we prove a backwards-compatibility property relative to prior work. Beyond solid surfaces, we present empirical evidence that our method remains tolerant to a variety of surface aberrations through the incorporation of a novel error correction scheme. Finally, we demonstrate how topology change applied to non-solid objects enables wholly new and useful behaviors.}, author = {Bernstein, Gilbert and Wojtan, Christopher J}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Putting holes in holey geometry: Topology change for arbitrary surfaces}}, doi = {10.1145/2461912.2462027}, volume = {32}, year = {2013}, } @article{2468, abstract = {Our work concerns the combination of an Eulerian liquid simulation with a high-resolution surface tracker (e.g. the level set method or a Lagrangian triangle mesh). The naive application of a high-resolution surface tracker to a low-resolution velocity field can produce many visually disturbing physical and topological artifacts that limit their use in practice. We address these problems by defining an error function which compares the current state of the surface tracker to the set of physically valid surface states. By reducing this error with a gradient descent technique, we introduce a novel physics-based surface fairing method. Similarly, by treating this error function as a potential energy, we derive a new surface correction force that mimics the vortex sheet equations. We demonstrate our results with both level set and mesh-based surface trackers.}, author = {Bojsen-Hansen, Morten and Wojtan, Christopher J}, journal = {ACM Transactions on Graphics}, number = {4}, publisher = {ACM}, title = {{Liquid surface tracking with error compensation}}, doi = {10.1145/2461912.2461991}, volume = {32}, year = {2013}, } @article{2469, abstract = {Cadherins are transmembrane proteins that mediate cell–cell adhesion in animals. By regulating contact formation and stability, cadherins play a crucial role in tissue morphogenesis and homeostasis. Here, we review the three major unctions of cadherins in cell–cell contact formation and stability. Two of those functions lead to a decrease in interfacial ension at the forming cell–cell contact, thereby promoting contact expansion — first, by providing adhesion tension that lowers interfacial tension at the cell–cell contact, and second, by signaling to the actomyosin cytoskeleton in order to reduce cortex tension and thus interfacial tension at the contact. The third function of cadherins in cell–cell contact formation is to stabilize the contact by resisting mechanical forces that pull on the contact.}, author = {Maître, Jean-Léon and Heisenberg, Carl-Philipp J}, journal = {Current Biology}, number = {14}, pages = {R626 -- R633}, publisher = {Cell Press}, title = {{Three functions of cadherins in cell adhesion}}, doi = {10.1016/j.cub.2013.06.019}, volume = {23}, year = {2013}, } @article{2470, abstract = {Background:Auxin binding protein 1 (ABP1) is a putative auxin receptor and its function is indispensable for plant growth and development. ABP1 has been shown to be involved in auxin-dependent regulation of cell division and expansion, in plasma-membrane-related processes such as changes in transmembrane potential, and in the regulation of clathrin-dependent endocytosis. However, the ABP1-regulated downstream pathway remains elusive.Methodology/Principal Findings:Using auxin transport assays and quantitative analysis of cellular morphology we show that ABP1 regulates auxin efflux from tobacco BY-2 cells. The overexpression of ABP1can counterbalance increased auxin efflux and auxin starvation phenotypes caused by the overexpression of PIN auxin efflux carrier. Relevant mechanism involves the ABP1-controlled vesicle trafficking processes, including positive regulation of endocytosis of PIN auxin efflux carriers, as indicated by fluorescence recovery after photobleaching (FRAP) and pharmacological manipulations.Conclusions/Significance:The findings indicate the involvement of ABP1 in control of rate of auxin transport across plasma membrane emphasizing the role of ABP1 in regulation of PIN activity at the plasma membrane, and highlighting the relevance of ABP1 for the formation of developmentally important, PIN-dependent auxin gradients.}, author = {Čovanová, Milada and Sauer, Michael and Rychtář, Jan and Friml, Jirí and Petrášek, Jan and Zažímalová, Eva}, journal = {PLoS One}, number = {7}, publisher = {Public Library of Science}, title = {{Overexpression of the auxin binding PROTEIN1 modulates PIN-dependent auxin transport in tobacco cells}}, doi = {10.1371/journal.pone.0070050}, volume = {8}, year = {2013}, } @article{2471, abstract = {The impact of disulfide bonds on protein stability goes beyond simple equilibrium thermodynamics effects associated with the conformational entropy of the unfolded state. Indeed, disulfide crosslinks may play a role in the prevention of dysfunctional association and strongly affect the rates of irreversible enzyme inactivation, highly relevant in biotechnological applications. While these kinetic-stability effects remain poorly understood, by analogy with proposed mechanisms for processes of protein aggregation and fibrillogenesis, we propose that they may be determined by the properties of sparsely-populated, partially-unfolded intermediates. Here we report the successful design, on the basis of high temperature molecular-dynamics simulations, of six thermodynamically and kinetically stabilized variants of phytase from Citrobacter braakii (a biotechnologically important enzyme) with one, two or three engineered disulfides. Activity measurements and 3D crystal structure determination demonstrate that the engineered crosslinks do not cause dramatic alterations in the native structure. The inactivation kinetics for all the variants displays a strongly non-Arrhenius temperature dependence, with the time-scale for the irreversible denaturation process reaching a minimum at a given temperature within the range of the denaturation transition. We show this striking feature to be a signature of a key role played by a partially unfolded, intermediate state/ensemble. Energetic and mutational analyses confirm that the intermediate is highly unfolded (akin to a proposed critical intermediate in the misfolding of the prion protein), a result that explains the observed kinetic stabilization. Our results provide a rationale for the kinetic-stability consequences of disulfide-crosslink engineering and an experimental methodology to arrive at energetic/structural descriptions of the sparsely populated and elusive intermediates that play key roles in irreversible protein denaturation.}, author = {Sanchez Romero, Inmaculada and Ariza, Antonio and Wilson, Keith and Skjøt, Michael and Vind, Jesper and De Maria, Leonardo and Skov, Lars and Sánchez Ruiz, Jose}, journal = {PLoS One}, number = {7}, publisher = {Public Library of Science}, title = {{Mechanism of protein kinetic stabilization by engineered disulfide crosslinks}}, doi = {10.1371/journal.pone.0070013}, volume = {8}, year = {2013}, } @article{2472, abstract = {Plant-specific PIN-formed (PIN) efflux transporters for the plant hormone auxin are required for tissue-specific directional auxin transport and cellular auxin homeostasis. The Arabidopsis PIN protein family has been shown to play important roles in developmental processes such as embryogenesis, organogenesis, vascular tissue differentiation, root meristem patterning and tropic growth. Here we analyzed roles of the less characterised Arabidopsis PIN6 auxin transporter. PIN6 is auxin-inducible and is expressed during multiple auxin-regulated developmental processes. Loss of pin6 function interfered with primary root growth and lateral root development. Misexpression of PIN6 affected auxin transport and interfered with auxin homeostasis in other growth processes such as shoot apical dominance, lateral root primordia development, adventitious root formation, root hair outgrowth and root waving. These changes in auxin-regulated growth correlated with a reduction in total auxin transport as well as with an altered activity of DR5-GUS auxin response reporter. Overall, the data indicate that PIN6 regulates auxin homeostasis during plant development.}, author = {Cazzonelli, Christopher and Vanstraelen, Marleen and Simon, Sibu and Yin, Kuide and Carron Arthur, Ashley and Nisar, Nazia and Tarle, Gauri and Cuttriss, Abby and Searle, Iain and Benková, Eva and Mathesius, Ulrike and Masle, Josette and Friml, Jirí and Pogson, Barry}, journal = {PLoS One}, number = {7}, publisher = {Public Library of Science}, title = {{Role of the Arabidopsis PIN6 auxin transporter in auxin homeostasis and auxin-mediated development}}, doi = {10.1371/journal.pone.0070069}, volume = {8}, year = {2013}, } @article{2473, abstract = {When a mutation with selective advantage s spreads through a panmictic population, it may cause two lineages at a linked locus to coalesce; the probability of coalescence is exp(−2rT), where T∼log(2Ns)/s is the time to fixation, N is the number of haploid individuals, and r is the recombination rate. Population structure delays fixation, and so weakens the effect of a selective sweep. However, favourable alleles spread through a spatially continuous population behind a narrow wavefront; ancestral lineages are confined at the tip of this front, and so coalesce rapidly. In extremely dense populations, coalescence is dominated by rare fluctuations ahead of the front. However, we show that for moderate densities, a simple quasi-deterministic approximation applies: the rate of coalescence within the front is λ∼2g(η)/(ρℓ), where ρ is the population density and is the characteristic scale of the wavefront; g(η) depends only on the strength of random drift, . The net effect of a sweep on coalescence also depends crucially on whether two lineages are ever both within the wavefront at the same time: even in the extreme case when coalescence within the front is instantaneous, the net rate of coalescence may be lower than in a single panmictic population. Sweeps can also have a substantial impact on the rate of gene flow. A single lineage will jump to a new location when it is hit by a sweep, with mean square displacement ; this can be substantial if the species’ range, L, is large, even if the species-wide rate of sweeps per map length, Λ/R, is small. This effect is half as strong in two dimensions. In contrast, the rate of coalescence between lineages, at random locations in space and on the genetic map, is proportional to (c/L)(Λ/R), where c is the wavespeed: thus, on average, one-dimensional structure is likely to reduce coalescence due to sweeps, relative to panmixis. In two dimensions, genes must move along the front before they can coalesce; this process is rapid, being dominated by rare fluctuations. This leads to a dramatically higher rate of coalescence within the wavefront than if lineages simply diffused along the front. Nevertheless, the net rate of coalescence due to a sweep through a two-dimensional population is likely to be lower than it would be with panmixis.}, author = {Barton, Nicholas H and Etheridge, Alison and Kelleher, Jerome and Véber, Amandine}, journal = {Theoretical Population Biology}, number = {8}, pages = {75 -- 89}, publisher = {Elsevier}, title = {{Genetic hitch-hiking in spatially extended populations}}, doi = {10.1016/j.tpb.2012.12.001}, volume = {87}, year = {2013}, } @article{2516, abstract = {We study the problem of object recognition for categories for which we have no training examples, a task also called zero-data or zero-shot learning. This situation has hardly been studied in computer vision research, even though it occurs frequently: the world contains tens of thousands of different object classes and for only few of them image collections have been formed and suitably annotated. To tackle the problem we introduce attribute-based classification: objects are identified based on a high-level description that is phrased in terms of semantic attributes, such as the object's color or shape. Because the identification of each such property transcends the specific learning task at hand, the attribute classifiers can be pre-learned independently, e.g. from existing image datasets unrelated to the current task. Afterwards, new classes can be detected based on their attribute representation, without the need for a new training phase. In this paper we also introduce a new dataset, Animals with Attributes, of over 30,000 images of 50 animal classes, annotated with 85 semantic attributes. Extensive experiments on this and two more datasets show that attribute-based classification indeed is able to categorize images without access to any training images of the target classes.}, author = {Lampert, Christoph and Nickisch, Hannes and Harmeling, Stefan}, journal = {IEEE Transactions on Pattern Analysis and Machine Intelligence}, number = {3}, pages = {453 -- 465}, publisher = {IEEE}, title = {{Attribute-based classification for zero-shot learning of object categories}}, doi = {10.1109/TPAMI.2013.140}, volume = {36}, year = {2013}, } @inproceedings{2517, abstract = {Traditional formal methods are based on a Boolean satisfaction notion: a reactive system satisfies, or not, a given specification. We generalize formal methods to also address the quality of systems. As an adequate specification formalism we introduce the linear temporal logic LTL[F]. The satisfaction value of an LTL[F] formula is a number between 0 and 1, describing the quality of the satisfaction. The logic generalizes traditional LTL by augmenting it with a (parameterized) set F of arbitrary functions over the interval [0,1]. For example, F may contain the maximum or minimum between the satisfaction values of subformulas, their product, and their average. The classical decision problems in formal methods, such as satisfiability, model checking, and synthesis, are generalized to search and optimization problems in the quantitative setting. For example, model checking asks for the quality in which a specification is satisfied, and synthesis returns a system satisfying the specification with the highest quality. Reasoning about quality gives rise to other natural questions, like the distance between specifications. We formalize these basic questions and study them for LTL[F]. By extending the automata-theoretic approach for LTL to a setting that takes quality into an account, we are able to solve the above problems and show that reasoning about LTL[F] has roughly the same complexity as reasoning about traditional LTL.}, author = {Almagor, Shaull and Boker, Udi and Kupferman, Orna}, location = {Riga, Latvia}, number = {Part 2}, pages = {15 -- 27}, publisher = {Springer}, title = {{Formalizing and reasoning about quality}}, doi = {10.1007/978-3-642-39212-2_3}, volume = {7966}, year = {2013}, } @article{2410, abstract = {Here, we describe a novel virulent bacteriophage that infects Bacillus weihenstephanensis, isolated from soil in Austria. It is the first phage to be discovered that infects this species. Here, we present the complete genome sequence of this podovirus. }, author = {Fernandes Redondo, Rodrigo A and Kupczok, Anne and Stift, Gertraud and Bollback, Jonathan P}, journal = {Genome Announcements}, number = {3}, publisher = {American Society for Microbiology}, title = {{Complete genome sequence of the novel phage MG-B1 infecting bacillus weihenstephanensis}}, doi = {10.1128/genomeA.00216-13}, volume = {1}, year = {2013}, } @article{2412, abstract = {Background: The CRISPR/Cas system is known to act as an adaptive and heritable immune system in Eubacteria and Archaea. Immunity is encoded in an array of spacer sequences. Each spacer can provide specific immunity to invasive elements that carry the same or a similar sequence. Even in closely related strains, spacer content is very dynamic and evolves quickly. Standard models of nucleotide evolutioncannot be applied to quantify its rate of change since processes other than single nucleotide changes determine its evolution.Methods We present probabilistic models that are specific for spacer content evolution. They account for the different processes of insertion and deletion. Insertions can be constrained to occur on one end only or are allowed to occur throughout the array. One deletion event can affect one spacer or a whole fragment of adjacent spacers. Parameters of the underlying models are estimated for a pair of arrays by maximum likelihood using explicit ancestor enumeration.Results Simulations show that parameters are well estimated on average under the models presented here. There is a bias in the rate estimation when including fragment deletions. The models also estimate times between pairs of strains. But with increasing time, spacer overlap goes to zero, and thus there is an upper bound on the distance that can be estimated. Spacer content similarities are displayed in a distance based phylogeny using the estimated times.We use the presented models to analyze different Yersinia pestis data sets and find that the results among them are largely congruent. The models also capture the variation in diversity of spacers among the data sets. A comparison of spacer-based phylogenies and Cas gene phylogenies shows that they resolve very different time scales for this data set.Conclusions The simulations and data analyses show that the presented models are useful for quantifying spacer content evolution and for displaying spacer content similarities of closely related strains in a phylogeny. This allows for comparisons of different CRISPR arrays or for comparisons between CRISPR arrays and nucleotide substitution rates.}, author = {Kupczok, Anne and Bollback, Jonathan P}, journal = {BMC Evolutionary Biology}, number = {1}, pages = {54 -- 54}, publisher = {BioMed Central}, title = {{Probabilistic models for CRISPR spacer content evolution }}, doi = {10.1186/1471-2148-13-54}, volume = {13}, year = {2013}, } @inbook{2413, abstract = {Progress in understanding the global brain dynamics has remained slow to date in large part because of the highly multiscale nature of brain activity. Indeed, normal brain dynamics is characterized by complex interactions between multiple levels: from the microscopic scale of single neurons to the mesoscopic level of local groups of neurons, and finally to the macroscopic level of the whole brain. Among the most difficult tasks are those of identifying which scales are significant for a given particular function and describing how the scales affect each other. It is important to realize that the scales of time and space are linked together, or even intertwined, and that causal inference is far more ambiguous between than within levels. We approach this problem from the perspective of our recent work on simultaneous recording from micro- and macroelectrodes in the human brain. We propose a physiological description of these multilevel interactions, based on phase–amplitude coupling of neuronal oscillations that operate at multiple frequencies and on different spatial scales. Specifically, the amplitude of the oscillations on a particular spatial scale is modulated by phasic variations in neuronal excitability induced by lower frequency oscillations that emerge on a larger spatial scale. Following this general principle, it is possible to scale up or scale down the multiscale brain dynamics. It is expected that large-scale network oscillations in the low-frequency range, mediating downward effects, may play an important role in attention and consciousness.}, author = {Valderrama, Mario and Botella Soler, Vicente and Le Van Quyen, Michel}, booktitle = {Multiscale Analysis and Nonlinear Dynamics: From Genes to the Brain}, editor = {Meyer, Misha and Pesenson, Z.}, isbn = {9783527411986 }, publisher = {Wiley-VCH}, title = {{Neuronal oscillations scale up and scale down the brain dynamics }}, doi = {10.1002/9783527671632.ch08}, year = {2013}, } @article{2443, abstract = {The mode of action of auxin is based on its non-uniform distribution within tissues and organs. Despite the wide use of several auxin analogues in research and agriculture, little is known about the specificity of different auxin-related transport and signalling processes towards these compounds. Using seedlings of Arabidopsis thaliana and suspension-cultured cells of Nicotiana tabacum (BY-2), the physiological activity of several auxin analogues was investigated, together with their capacity to induce auxin-dependent gene expression, to inhibit endocytosis and to be transported across the plasma membrane. This study shows that the specificity criteria for different auxin-related processes vary widely. Notably, the special behaviour of some synthetic auxin analogues suggests that they might be useful tools in investigations of the molecular mechanism of auxin action. Thus, due to their differential stimulatory effects on DR5 expression, indole-3-propionic (IPA) and 2,4,5-trichlorophenoxy acetic (2,4,5-T) acids can serve in studies of TRANSPORT INHIBITOR RESPONSE 1/AUXIN SIGNALLING F-BOX (TIR1/AFB)-mediated auxin signalling, and 5-fluoroindole-3-acetic acid (5-F-IAA) can help to discriminate between transcriptional and non-transcriptional pathways of auxin signalling. The results demonstrate that the major determinants for the auxin-like physiological potential of a particular compound are very complex and involve its chemical and metabolic stability, its ability to distribute in tissues in a polar manner and its activity towards auxin signalling machinery.}, author = {Simon, Sibu and Kubeš, Martin and Baster, Pawel and Robert, Stéphanie and Dobrev, Petre and Friml, Jirí and Petrášek, Jan and Zažímalová, Eva}, journal = {New Phytologist}, number = {4}, pages = {1034 -- 1048}, publisher = {Wiley-Blackwell}, title = {{Defining the selectivity of processes along the auxin response chain: A study using auxin analogues}}, doi = {10.1111/nph.12437}, volume = {200}, year = {2013}, } @inproceedings{2444, abstract = {We consider two core algorithmic problems for probabilistic verification: the maximal end-component decomposition and the almost-sure reachability set computation for Markov decision processes (MDPs). For MDPs with treewidth k, we present two improved static algorithms for both the problems that run in time O(n·k 2.38·2k ) and O(m·logn· k), respectively, where n is the number of states and m is the number of edges, significantly improving the previous known O(n·k·√n· k) bound for low treewidth. We also present decremental algorithms for both problems for MDPs with constant treewidth that run in amortized logarithmic time, which is a huge improvement over the previously known algorithms that require amortized linear time.}, author = {Chatterjee, Krishnendu and Ła̧Cki, Jakub}, location = {St. Petersburg, Russia}, pages = {543 -- 558}, publisher = {Springer}, title = {{Faster algorithms for Markov decision processes with low treewidth}}, doi = {10.1007/978-3-642-39799-8_36}, volume = {8044}, year = {2013}, } @article{2300, abstract = {We consider Ising models in two and three dimensions with nearest neighbor ferromagnetic interactions and long-range, power law decaying, antiferromagnetic interactions. If the strength of the ferromagnetic coupling J is larger than a critical value Jc, then the ground state is homogeneous and ferromagnetic. As the critical value is approached from smaller values of J, it is believed that the ground state consists of a periodic array of stripes (d=2) or slabs (d=3), all of the same size and alternating magnetization. Here we prove rigorously that the ground state energy per site converges to that of the optimal periodic striped or slabbed state, in the limit that J tends to the ferromagnetic transition point. While this theorem does not prove rigorously that the ground state is precisely striped or slabbed, it does prove that in any suitably large box the ground state is striped or slabbed with high probability.}, author = {Giuliani, Alessandro and Lieb, Élliott and Seiringer, Robert}, journal = {Physical Review B}, number = {6}, publisher = {American Physical Society}, title = {{Realization of stripes and slabs in two and three dimensions}}, doi = {10.1103/PhysRevB.88.064401}, volume = {88}, year = {2013}, } @inproceedings{2301, abstract = {We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to "close" the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code; a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhan-dled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P); we have more confidence in the robustness of its design due to the language abstractions and verification provided by P.}, author = {Desai, Ankush and Gupta, Vivek and Jackson, Ethan and Qadeer, Shaz and Rajamani, Sriram and Zufferey, Damien}, booktitle = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation}, location = {Seattle, WA, United States}, pages = {321 -- 331}, publisher = {ACM}, title = {{P: Safe asynchronous event-driven programming}}, doi = {10.1145/2491956.2462184}, year = {2013}, } @article{2303, abstract = {MADM (Mosaic Analysis with Double Markers) technology offers a genetic approach in mice to visualize and concomitantly manipulate genetically defined cells at clonal level and single cell resolution. MADM employs Cre recombinase/loxP-dependent interchromosomal mitotic recombination to reconstitute two split marker genes—green GFP and red tdTomato—and can label sparse clones of homozygous mutant cells in one color and wild-type cells in the other color in an otherwise unlabeled background. At present, major MADM applications include lineage tracing, single cell labeling, conditional knockouts in small populations of cells and induction of uniparental chromosome disomy to assess effects of genomic imprinting. MADM can be applied universally in the mouse with the sole limitation being the specificity of the promoter controlling Cre recombinase expression. Here I review recent developments and extensions of the MADM technique and give an overview of the major discoveries and progresses enabled by the implementation of the novel genetic MADM tools.}, author = {Hippenmeyer, Simon}, journal = {Frontiers in Biology}, number = {6}, pages = {557 -- 568}, publisher = {Springer}, title = {{Dissection of gene function at clonal level using mosaic analysis with double markers}}, doi = {10.1007/s11515-013-1279-6}, volume = {8}, year = {2013}, } @article{2304, abstract = {This extended abstract is concerned with the irregularities of distribution of one-dimensional permuted van der Corput sequences that are generated from linear permutations. We show how to obtain upper bounds for the discrepancy and diaphony of these sequences, by relating them to Kronecker sequences and applying earlier results of Faure and Niederreiter.}, author = {Pausinger, Florian}, journal = {Electronic Notes in Discrete Mathematics}, pages = {43 -- 50}, publisher = {Elsevier}, title = {{Van der Corput sequences and linear permutations}}, doi = {10.1016/j.endm.2013.07.008}, volume = {43}, year = {2013}, } @inproceedings{2305, abstract = {We study the complexity of central controller synthesis problems for finite-state Markov decision processes, where the objective is to optimize both the expected mean-payoff performance of the system and its stability. e argue that the basic theoretical notion of expressing the stability in terms of the variance of the mean-payoff (called global variance in our paper) is not always sufficient, since it ignores possible instabilities on respective runs. For this reason we propose alernative definitions of stability, which we call local and hybrid variance, and which express how rewards on each run deviate from the run's own mean-payoff and from the expected mean-payoff, respectively. We show that a strategy ensuring both the expected mean-payoff and the variance below given bounds requires randomization and memory, under all the above semantics of variance. We then look at the problem of determining whether there is a such a strategy. For the global variance, we show that the problem is in PSPACE, and that the answer can be approximated in pseudo-polynomial time. For the hybrid variance, the analogous decision problem is in NP, and a polynomial-time approximating algorithm also exists. For local variance, we show that the decision problem is in NP. Since the overall performance can be traded for stability (and vice versa), we also present algorithms for approximating the associated Pareto curve in all the three cases. Finally, we study a special case of the decision problems, where we require a given expected mean-payoff together with zero variance. Here we show that the problems can be all solved in polynomial time.}, author = {Brázdil, Tomáš and Chatterjee, Krishnendu and Forejt, Vojtěch and Kučera, Antonín}, booktitle = {28th Annual ACM/IEEE Symposium}, location = {New Orleans, LA, United States}, pages = {331 -- 340}, publisher = {IEEE}, title = {{Trading performance for stability in Markov decision processes}}, doi = {10.1109/LICS.2013.39}, year = {2013}, } @inproceedings{2328, abstract = {Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on identifying the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof.}, author = {Henzinger, Thomas A and Sezgin, Ali and Vafeiadis, Viktor}, location = {Buenos Aires, Argentina}, pages = {242 -- 256}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Aspect-oriented linearizability proofs}}, doi = {10.1007/978-3-642-40184-8_18}, volume = {8052}, year = {2013}, } @article{2821, abstract = {Many key aspects of plant development are regulated by the polarized transport of the phytohormone auxin. Cellular auxin efflux, the rate-limiting step in this process, has been shown to rely on the coordinated action of PIN-formed (PIN) and B-type ATP binding cassette (ABCB) carriers. Here, we report that polar auxin transport in the Arabidopsis thaliana root also requires the action of a Major Facilitator Superfamily (MFS) transporter, Zinc-Induced Facilitator-Like 1 (ZIFL1). Sequencing, promoter-reporter, and fluorescent protein fusion experiments indicate that the full-length ZIFL1.1 protein and a truncated splice isoform, ZIFL1.3, localize to the tonoplast of root cells and the plasma membrane of leaf stomatal guard cells, respectively. Using reverse genetics, we show that the ZIFL1.1 transporter regulates various root auxin-related processes, while the ZIFL1.3 isoform mediates drought tolerance by regulating stomatal closure. Auxin transport and immunolocalization assays demonstrate that ZIFL1.1 indirectly modulates cellular auxin efflux during shootward auxin transport at the root tip, likely by regulating plasma membrane PIN2 abundance. Finally, heterologous expression in yeast revealed that ZIFL1.1 and ZIFL1.3 share H+-coupled K+ transport activity. Thus, by determining the subcellular and tissue distribution of two isoforms, alternative splicing dictates a dual function for the ZIFL1 transporter. We propose that this MFS carrier regulates stomatal movements and polar auxin transport by modulating potassium and proton fluxes in Arabidopsis cells.}, author = {Remy, Estelle and Cabrito, Tânia and Baster, Pawel and Batista, Rita and Teixeira, Miguel and Friml, Jirí and Sá Correia, Isabel and Duque, Paula}, journal = {Plant Cell}, number = {3}, pages = {901 -- 926}, publisher = {American Society of Plant Biologists}, title = {{A major facilitator superfamily transporter plays a dual role in polar auxin transport and drought stress tolerance in Arabidopsis}}, doi = {10.1105/tpc.113.110353}, volume = {25}, year = {2013}, } @article{2822, abstract = {Identification of genes that control root system architecture in crop plants requires innovations that enable high-throughput and accurate measurements of root system architecture through time. We demonstrate the ability of a semiautomated 3D in vivo imaging and digital phenotyping pipeline to interrogate the quantitative genetic basis of root system growth in a rice biparental mapping population, Bala x Azucena. We phenotyped >1,400 3D root models and >57,000 2D images for a suite of 25 traits that quantified the distribution, shape, extent of exploration, and the intrinsic size of root networks at days 12, 14, and 16 of growth in a gellan gum medium. From these data we identified 89 quantitative trait loci, some of which correspond to those found previously in soil-grown plants, and provide evidence for genetic tradeoffs in root growth allocations, such as between the extent and thoroughness of exploration. We also developed a multivariate method for generating and mapping central root architecture phenotypes and used it to identify five major quantitative trait loci (r2 = 24-37%), two of which were not identified by our univariate analysis. Our imaging and analytical platform provides a means to identify genes with high potential for improving root traits and agronomic qualities of crops.}, author = {Topp, Christopher and Iyer Pascuzzi, Anjali and Anderson, Jill and Lee, Cheng and Zurek, Paul and Symonova, Olga and Zheng, Ying and Bucksch, Alexander and Mileyko, Yuriy and Galkovskyi, Taras and Moore, Brad and Harer, John and Edelsbrunner, Herbert and Mitchell Olds, Thomas and Weitz, Joshua and Benfey, Philip}, journal = {PNAS}, number = {18}, pages = {E1695 -- E1704}, publisher = {National Academy of Sciences}, title = {{3D phenotyping and quantitative trait locus mapping identify core regions of the rice genome controlling root architecture}}, doi = {10.1073/pnas.1304354110}, volume = {110}, year = {2013}, } @article{2823, abstract = {The primary goal of restoration is to create self-sustaining ecological communities that are resilient to periodic disturbance. Currently, little is known about how restored communities respond to disturbance events such as fire and how this response compares to remnant vegetation. Following the 2003 fires in south-eastern Australia we examined the post-fire response of revegetation plantings and compared this to remnant vegetation. Ten burnt and 10 unburnt (control) sites were assessed for each of three types of vegetation (direct seeding revegetation, revegetation using nursery seedlings (tubestock) and remnant woodland). Sixty sampling sites were surveyed 6months after fire to quantify the initial survival of mid- and overstorey plant species in each type of vegetation. Three and 5years after fire all sites were resurveyed to assess vegetation structure, species diversity and vigour, as well as indicators of soil function. Overall, revegetation showed high (>60%) post-fire survival, but this varied among species depending on regeneration strategy (obligate seeder or resprouter). The native ground cover, mid- and overstorey in both types of plantings showed rapid recovery of vegetation structure and cover within 3years of fire. This recovery was similar to the burnt remnant woodlands. Non-native (exotic) ground cover initially increased after fire, but was no different in burnt and unburnt sites 5years after fire. Fire had no effect on species richness, but burnt direct seeding sites had reduced species diversity (Simpson's Diversity Index) while diversity was higher in burnt remnant woodlands. Indices of soil function in all types of vegetation had recovered to levels found in unburnt sites 5years after fire. These results indicate that even young revegetation (stands <10years old) showed substantial recovery from disturbance by fire. This suggests that revegetation can provide an important basis for restoring woodland communities in the fire-prone Australian environment.}, author = {Pickup, Melinda and Wilson, Susie and Freudenberger, David and Nicholls, Nick and Gould, Lori and Hnatiuk, Sarah and Delandre, Jeni}, journal = {Austral Ecology}, number = {3}, pages = {300 -- 312}, publisher = {Wiley-Blackwell}, title = {{Post-fire recovery of revegetated woodland communities in south-eastern Australia}}, doi = {10.1111/j.1442-9993.2012.02404.x}, volume = {38}, year = {2013}, } @article{2824, abstract = {We study synthesis of controllers for real-time systems, where the objective is to stay in a given safe set. The problem is solved by obtaining winning strategies in the setting of concurrent two player timed automaton games with safety objectives. To prevent a player from winning by blocking time, we restrict each player to strategies that ensure that the player cannot be responsible for causing a Zeno run. We construct winning strategies for the controller which require access only to (1) the system clocks (thus, controllers which require their own internal infinitely precise clocks are not necessary), and (2) a logarithmic (in the number of clocks) number of memory bits (i.e. a linear number of memory states). Precisely, we show that for safety objectives, a memory of size (3 + lg (| C | + 1)) bits suffices for winning controller strategies, where C is the set of clocks of the timed automaton game, significantly improving the previous known exponential memory states bound. We also settle the open question of whether winning region-based strategies require memory for safety objectives by showing with an example the necessity of memory for such strategies to win for safety objectives. Finally, we show that the decision problem of determining if there exists a receptive player-1 winning strategy for safety objectives is EXPTIME-complete over timed automaton games.}, author = {Chatterjee, Krishnendu and Prabhu, Vinayak}, journal = {Information and Computation}, pages = {83--119}, publisher = {Elsevier}, title = {{Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems}}, doi = {10.1016/j.ic.2013.04.003}, volume = {228-229}, year = {2013}, } @article{2827, abstract = {Removal of cargos from the cell surface via endocytosis is an efficient mechanism to regulate activities of plasma membrane (PM)-resident proteins, such as receptors or transporters. Salicylic acid (SA) is an important plant hormone that is traditionally associated with pathogen defense. Here, we describe an unanticipated effect of SA on subcellular endocytic cycling of proteins. Both exogenous treatments and endogenously enhanced SA levels repressed endocytosis of different PM proteins. The SA effect on endocytosis did not involve transcription or known components of the SA signaling pathway for transcriptional regulation. SA likely targets an endocytic mechanism that involves the coat protein clathrin, because SA interfered with the clathrin incidence at the PM and clathrin-deficient mutants were less sensitive to the impact of SA on the auxin distribution and root bending during the gravitropic response. By contrast, SA did not affect the ligand-induced endocytosis of the FLAGELLIN SENSING2 (FLS2) receptor during pathogen responses. Our data suggest that the established SA impact on transcription in plant immunity and the nontranscriptional effect of SA on clathrin-mediated endocytosis are independent mechanisms by which SA regulates distinct aspects of plant physiology.}, author = {Du, Yunlong and Tejos, Ricardo and Beck, Martina and Himschoot, Ellie and Li, Hongjiang and Robatzek, Silke and Vanneste, Steffen and Friml, Jirí}, journal = {PNAS}, number = {19}, pages = {7946 -- 7951}, publisher = {National Academy of Sciences}, title = {{Salicylic acid interferes with clathrin-mediated endocytic protein trafficking}}, doi = {10.1073/pnas.1220205110}, volume = {110}, year = {2013}, } @article{2828, abstract = {We study the complexity of valued constraint satisfaction problems (VCSPs) parametrized by a constraint language, a fixed set of cost functions over a finite domain. An instance of the problem is specified by a sum of cost functions from the language and the goal is to minimize the sum. Under the unique games conjecture, the approximability of finite-valued VCSPs is well understood, see Raghavendra [2008]. However, there is no characterization of finite-valued VCSPs, let alone general-valued VCSPs, that can be solved exactly in polynomial time, thus giving insights from a combinatorial optimization perspective. We consider the case of languages containing all possible unary cost functions. In the case of languages consisting of only {0, ∞}-valued cost functions (i.e., relations), such languages have been called conservative and studied by Bulatov [2003, 2011] and recently by Barto [2011]. Since we study valued languages, we call a language conservative if it contains all finite-valued unary cost functions. The computational complexity of conservative valued languages has been studied by Cohen et al. [2006] for languages over Boolean domains, by Deineko et al. [2008] for {0, 1}-valued languages (a.k.a Max-CSP), and by Takhanov [2010a] for {0, ∞}-valued languages containing all finite-valued unary cost functions (a.k.a. Min-Cost-Hom). We prove a Schaefer-like dichotomy theorem for conservative valued languages: if all cost functions in the language satisfy a certain condition (specified by a complementary combination of STP and MJN multimor-phisms), then any instance can be solved in polynomial time (via a new algorithm developed in this article), otherwise the language is NP-hard. This is the first complete complexity classification of general-valued constraint languages over non-Boolean domains. It is a common phenomenon that complexity classifications of problems over non-Boolean domains are significantly harder than the Boolean cases. The polynomial-time algorithm we present for the tractable cases is a generalization of the submodular minimization problem and a result of Cohen et al. [2008]. Our results generalize previous results by Takhanov [2010a] and (a subset of results) by Cohen et al. [2006] and Deineko et al. [2008]. Moreover, our results do not rely on any computer-assisted search as in Deineko et al. [2008], and provide a powerful tool for proving hardness of finite-valued and general-valued languages.}, author = {Kolmogorov, Vladimir and Živný, Stanislav}, journal = {Journal of the ACM}, number = {2}, publisher = {ACM}, title = {{The complexity of conservative valued CSPs}}, doi = {10.1145/2450142.2450146}, volume = {60}, year = {2013}, } @article{2829, abstract = {Laminar-turbulent intermittency is intrinsic to the transitional regime of a wide range of fluid flows including pipe, channel, boundary layer, and Couette flow. In the latter turbulent spots can grow and form continuous stripes, yet in the stripe-normal direction they remain interspersed by laminar fluid. We carry out direct numerical simulations in a long narrow domain and observe that individual turbulent stripes are transient. In agreement with recent observations in pipe flow, we find that turbulence becomes sustained at a distinct critical point once the spatial proliferation outweighs the inherent decaying process. By resolving the asymptotic size distributions close to criticality we can for the first time demonstrate scale invariance at the onset of turbulence.}, author = {Shi, Liang and Avila, Marc and Hof, Björn}, journal = {Physical Review Letters}, number = {20}, publisher = {American Physical Society}, title = {{Scale invariance at the onset of turbulence in couette flow}}, doi = {10.1103/PhysRevLett.110.204502}, volume = {110}, year = {2013}, } @article{2830, author = {Moussion, Christine and Sixt, Michael K}, journal = {Immunity}, number = {5}, pages = {853 -- 854}, publisher = {Cell Press}, title = {{A conduit to amplify innate immunity}}, doi = {10.1016/j.immuni.2013.05.005}, volume = {38}, year = {2013}, } @article{2831, abstract = {We consider Markov decision processes (MDPs) with Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure winning states from where the objective can be ensured with probability 1. Our contributions are as follows: First, we present the first subquadratic symbolic algorithm to compute the almost-sure winning set for MDPs with Büchi objectives; our algorithm takes O(n · √ m) symbolic steps as compared to the previous known algorithm that takes O(n 2) symbolic steps, where n is the number of states and m is the number of edges of the MDP. In practice MDPs have constant out-degree, and then our symbolic algorithm takes O(n · √ n) symbolic steps, as compared to the previous known O(n 2) symbolic steps algorithm. Second, we present a new algorithm, namely win-lose algorithm, with the following two properties: (a) the algorithm iteratively computes subsets of the almost-sure winning set and its complement, as compared to all previous algorithms that discover the almost-sure winning set upon termination; and (b) requires O(n · √ K) symbolic steps, where K is the maximal number of edges of strongly connected components (scc's) of the MDP. The win-lose algorithm requires symbolic computation of scc's. Third, we improve the algorithm for symbolic scc computation; the previous known algorithm takes linear symbolic steps, and our new algorithm improves the constants associated with the linear number of steps. In the worst case the previous known algorithm takes 5×n symbolic steps, whereas our new algorithm takes 4×n symbolic steps.}, author = {Chatterjee, Krishnendu and Henzinger, Monika and Joglekar, Manas and Shah, Nisarg}, journal = {Formal Methods in System Design}, number = {3}, pages = {301 -- 327}, publisher = {Springer}, title = {{Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives}}, doi = {10.1007/s10703-012-0180-2}, volume = {42}, year = {2013}, } @article{2832, abstract = {PIN-FORMED (PIN) proteins localize asymmetrically at the plasma membrane and mediate intercellular polar transport of the plant hormone auxin that is crucial for a multitude of developmental processes in plants. PIN localization is under extensive control by environmental or developmental cues, but mechanisms regulating PIN localization are not fully understood. Here we show that early endosomal components ARF GEF BEN1 and newly identified Sec1/Munc18 family protein BEN2 are involved in distinct steps of early endosomal trafficking. BEN1 and BEN2 are collectively required for polar PIN localization, for their dynamic repolarization, and consequently for auxin activity gradient formation and auxin-related developmental processes including embryonic patterning, organogenesis, and vasculature venation patterning. These results show that early endosomal trafficking is crucial for cell polarity and auxin-dependent regulation of plant architecture.}, author = {Tanaka, Hirokazu and Kitakura, Saeko and Rakusová, Hana and Uemura, Tomohiro and Feraru, Mugurel and De Rycke, Riet and Robert, Stéphanie and Kakimoto, Tatsuo and Friml, Jirí}, journal = {PLoS Genetics}, number = {5}, publisher = {Public Library of Science}, title = {{Cell polarity and patterning by PIN trafficking through early endosomal compartments in arabidopsis thaliana}}, doi = {10.1371/journal.pgen.1003540}, volume = {9}, year = {2013}, }