@article{1545, abstract = {We provide general conditions for which bosonic quadratic Hamiltonians on Fock spaces can be diagonalized by Bogoliubov transformations. Our results cover the case when quantum systems have infinite degrees of freedom and the associated one-body kinetic and paring operators are unbounded. Our sufficient conditions are optimal in the sense that they become necessary when the relevant one-body operators commute.}, author = {Nam, Phan and Napiórkowski, Marcin M and Solovej, Jan}, journal = {Journal of Functional Analysis}, number = {11}, pages = {4340 -- 4368}, publisher = {Academic Press}, title = {{Diagonalization of bosonic quadratic Hamiltonians by Bogoliubov transformations}}, doi = {10.1016/j.jfa.2015.12.007}, volume = {270}, year = {2016}, } @article{1059, abstract = {A range of bright and photostable rhodamines and carbopyronines with absorption maxima in the range of λ=500-630 nm were prepared, and enabled the specific labeling of cytoskeletal filaments using HaloTag technology followed by staining with 1 μm solutions of the dye-ligand conjugates. The synthesis, photophysical parameters, fluorogenic behavior, and structure-property relationships of the new dyes are discussed. Light microscopy with stimulated emission depletion (STED) provided one- and two-color images of living cells with an optical resolution of 40-60 nm.}, author = {Butkevich, Alexey and Mitronova, Gyuzel and Sidenstein, Sven and Klocke, Jessica and Kamin, Dirk and Meineke, Dirk and D'Este, Elisa and Kraemer, Philip and Danzl, Johann G and Belov, Vladimir and Hell, Stefan}, journal = {Angewandte Chemie - International Edition}, number = {10}, pages = {3290 -- 3294}, publisher = {Wiley-Blackwell}, title = {{Fluorescent rhodamines and fluorogenic carbopyronines for super-resolution STED microscopy in living cells}}, doi = {10.1002/anie.201511018}, volume = {55}, year = {2016}, } @article{1060, abstract = {Superresolution fluorescence microscopy of multiple fluorophores still requires development. Here we present simultaneous three-colour stimulated emission depletion (STED) nanoscopy relying on a single STED beam at 620 nm. Toggling the STED beam between two or more power levels ("multilevelSTEDv) optimizes resolution and contrast in all colour channels, which are intrinsically co-aligned and well separated. Three-colour recording is demonstrated by imaging the nanoscale cytoskeletal organization in cultured hippocampal neurons. The down to ∼35 nm resolution identified periodic actin/betaII spectrin lattices along dendrites and spines; however, at presynaptic and postsynaptic sites, these patterns were found to be absent. Both our multicolour scheme and the 620 nm STED line should be attractive for routine STED microscopy applications.}, author = {Sidenstein, Sven and D'Este, Elisa and Böhm, Marvin and Danzl, Johann G and Belov, Vladimir and Hell, Stefan}, journal = {Scientific Reports}, pages = {1 -- 8}, publisher = {Nature Publishing Group}, title = {{Multicolour multilevel STED nanoscopy of actin/spectrin organization at synapses}}, doi = {10.1038/srep26725}, volume = {6}, year = {2016}, } @inproceedings{1068, abstract = {Games on graphs provide the appropriate framework to study several central problems in computer science, such as verification and synthesis of reactive systems. One of the most basic objectives for games on graphs is the liveness (or Büchi) objective that given a target set of vertices requires that some vertex in the target set is visited infinitely often. We study generalized Büchi objectives (i.e., conjunction of liveness objectives), and implications between two generalized Büchi objectives (known as GR(1) objectives), that arise in numerous applications in computer-aided verification. We present improved algorithms and conditional super-linear lower bounds based on widely believed assumptions about the complexity of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider graph games with n vertices, m edges, and generalized Büchi objectives with k conjunctions. First, we present an algorithm with running time O(k*n^2), improving the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm is optimal for dense graphs under (A1). Second, we show that the basic algorithm for the problem is optimal for sparse graphs when the target sets have constant size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1 k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time algorithm for m > n^{1.5}. }, author = {Chatterjee, Krishnendu and Dvorák, Wolfgang and Henzinger, Monika H and Loitzenbauer, Veronika}, location = {Krakow, Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Conditionally optimal algorithms for generalized Büchi Games}}, doi = {10.4230/LIPIcs.MFCS.2016.25}, volume = {58}, year = {2016}, } @inproceedings{1069, abstract = {The Continuous Skolem Problem asks whether a real-valued function satisfying a linear differen- tial equation has a zero in a given interval of real numbers. This is a fundamental reachability problem for continuous linear dynamical systems, such as linear hybrid automata and continuous- time Markov chains. Decidability of the problem is currently open – indeed decidability is open even for the sub-problem in which a zero is sought in a bounded interval. In this paper we show decidability of the bounded problem subject to Schanuel’s Conjecture, a unifying conjecture in transcendental number theory. We furthermore analyse the unbounded problem in terms of the frequencies of the differential equation, that is, the imaginary parts of the characteristic roots. We show that the unbounded problem can be reduced to the bounded problem if there is at most one rationally linearly independent frequency, or if there are two rationally linearly independent frequencies and all characteristic roots are simple. We complete the picture by showing that de- cidability of the unbounded problem in the case of two (or more) rationally linearly independent frequencies would entail a major new effectiveness result in Diophantine approximation, namely computability of the Diophantine-approximation types of all real algebraic numbers.}, author = {Chonev, Ventsislav K and Ouaknine, Joël and Worrell, James}, location = {Rome, Italy}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{On the skolem problem for continuous linear dynamical systems}}, doi = {10.4230/LIPIcs.ICALP.2016.100}, volume = {55}, year = {2016}, } @inproceedings{1070, abstract = {We present a logic that extends CTL (Computation Tree Logic) with operators that express synchronization properties. A property is synchronized in a system if it holds in all paths of a certain length. The new logic is obtained by using the same path quantifiers and temporal operators as in CTL, but allowing a different order of the quantifiers. This small syntactic variation induces a logic that can express non-regular properties for which known extensions of MSO with equality of path length are undecidable. We show that our variant of CTL is decidable and that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We analogously consider quantifier exchange in extensions of CTL, and we present operators defined using basic operators of CTL* that express the occurrence of infinitely many synchronization points. We show that the model-checking problem remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide if the Next operator is allowed in the logics, thus the classical bisimulation quotient can be used for state-space reduction before model checking. }, author = {Chatterjee, Krishnendu and Doyen, Laurent}, location = {Rome, Italy}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Computation tree logic for synchronization properties}}, doi = {10.4230/LIPIcs.ICALP.2016.98}, volume = {55}, year = {2016}, } @inproceedings{10746, abstract = {Vortex states in superconducting (SC) structures, their dynamics and ways to manipulate them are topics of great interest. We report a new method of magnetic force microscopy (MFM) that allows the study of vortex states in mesoscopic SC samples. For the case of a SC ring, which is biased to a half-integer flux quantum, the flux modulation through the ring caused by the motion of the magnetic tip drives the ring between two consecutive fluxoid states. The corresponding current switching in the ring produces strong position-dependent forces on the cantilever. In the regime where the frequency of the thermally activated jumps between fluxoid states is close to the frequency of the cantilever, large changes in the cantilever frequency and dissipation are observed. This effect may be understood as a stochastic resonance (SR) process. These changes in the cantilever’s mechanical properties are used to “image” the barrier energies between fluxoid states. Additionally, SR imaging of the barrier energies are used to study the effect of the locally applied magnetic field from the MFM tip on the barrier heights. We report the results of measurements for Al rings. Further, the same imaging technique can be applied to more sophisticated SC structures such as arrays of Josephson junctions.}, author = {Polshyn, Hryhoriy and Naibert, Tyler and Chua, Victor and Budakian, Raffi}, booktitle = {APS March Meeting 2016}, issn = {0003-0503}, location = {Baltimore, MD, United States}, number = {2}, publisher = {American Physical Society}, title = {{Study of vortex states and dynamics in mesoscopic superconducting samples with MFM}}, volume = {61}, year = {2016}, } @inproceedings{10747, abstract = {Vortex interactions are key to explaining the behavior of many two dimensional superconducting systems. We report on the development of a technique to locally probe vortex interactions in a 2D array of Josephson junctions. Scanning a magnetic tip attached to an ultra-soft cantilever over the array produces changes in the frequency of the cantilever along certain lines, forming geometric patterns in the scans. Different tip-surface separations and external magnetic fields produce a number of different patterns. These patterns correspond to tip locations in which two configurations of vortices in the lattice have degenerate energies. By imaging the locations of these degeneracies, information on the local vortex interactions may be obtained.}, author = {Naibert, Tyler and Polshyn, Hryhoriy and Wolin, Brian and Durkin, Malcolm and Garrido Menacho, Rita and Shem, Ian Mondragon and Chua, Victor and Hughes, Taylor and Mason, Nadya and Budakian, Raffi}, booktitle = {APS March Meeting 2016}, issn = {0003-0503}, location = {Baltimore, MD, United States}, number = {2}, publisher = {American Physical Society}, title = {{Stochastic resonance magnetic force microscopy imaging of Josephson arrays}}, volume = {61}, year = {2016}, } @article{1081, abstract = {The asymmetric localization of proteins in the plasma membrane domains of eukaryotic cells is a fundamental manifestation of cell polarity that is central to multicellular organization and developmental patterning. In plants, the mechanisms underlying the polar localization of cargo proteins are still largely unknown and appear to be fundamentally distinct from those operating in mammals. Here, we present a systematic, quantitative comparative analysis of the polar delivery and subcellular localization of proteins that characterize distinct polar plasma membrane domains in plant cells. The combination of microscopic analyses and computational modeling revealed a mechanistic framework common to diverse polar cargos and underlying the establishment and maintenance of apical, basal, and lateral polar domains in plant cells. This mechanism depends on the polar secretion, constitutive endocytic recycling, and restricted lateral diffusion of cargos within the plasma membrane. Moreover, our observations suggest that polar cargo distribution involves the individual protein potential to form clusters within the plasma membrane and interact with the extracellular matrix. Our observations provide insights into the shared cellular mechanisms of polar cargo delivery and polarity maintenance in plant cells.}, author = {Łangowski, Łukasz and Wabnik, Krzysztof T and Li, Hongjiang and Vanneste, Steffen and Naramoto, Satoshi and Tanaka, Hirokazu and Friml, Jirí}, journal = {Cell Discovery}, publisher = {Nature Publishing Group}, title = {{Cellular mechanisms for cargo delivery and polarity maintenance at different polar domains in plant cells}}, doi = {10.1038/celldisc.2016.18}, volume = {2}, year = {2016}, } @inproceedings{10810, abstract = {The main goal of the SCP-ECG standard is to address ECG data and related metadata structuring, semantics and syntax, with the objective of facilitating interoperability and thus supporting and promoting the exchange of the relevant information for unary and serial ECG diagnosis. Starting with version V3.0, the standard now also provides support for the storage of continuous, long-term ECG recordings and affords a repository for selected ECG sequences and the related metadata to accommodate stress tests, drug trials and protocol-based ECG recordings. The global and per-lead measurements sections have been extended and three new sections have been introduced for storing beat-by-beat and/or spike-by-spike measurements and annotations. The used terminology and the provided measurements and annotations have been harmonized with the ISO/IEEE 11073-10102 Annotated ECG standard. Emphasis has also been put on harmonizing the Universal Statement Codes with the CDISC and the categorized AHA statement codes and similarly the drug and implanted devices codes with the ATC and NASPE/BPEG codes. }, author = {Rubel, Paul and Pani, Danilo and Schlögl, Alois and Fayn, Jocelyne and Badilini, Fabio and Macfarlane, Peter and Varri, Alpo}, booktitle = {2016 Computing in Cardiology Conference}, issn = {2325-887X}, location = {Vancouver, Canada}, pages = {309--312}, publisher = {Computing in Cardiology}, title = {{SCP-ECG V3.0: An enhanced standard communication protocol for computer-assisted electrocardiography}}, doi = {10.22489/cinc.2016.090-500}, volume = {43}, year = {2016}, } @inproceedings{1082, abstract = {In many applications, it is desirable to extract only the relevant aspects of data. A principled way to do this is the information bottleneck (IB) method, where one seeks a code that maximises information about a relevance variable, Y, while constraining the information encoded about the original data, X. Unfortunately however, the IB method is computationally demanding when data are high-dimensional and/or non-gaussian. Here we propose an approximate variational scheme for maximising a lower bound on the IB objective, analogous to variational EM. Using this method, we derive an IB algorithm to recover features that are both relevant and sparse. Finally, we demonstrate how kernelised versions of the algorithm can be used to address a broad range of problems with non-linear relation between X and Y.}, author = {Chalk, Matthew J and Marre, Olivier and Tkacik, Gasper}, location = {Barcelona, Spain}, pages = {1965--1973}, publisher = {Neural Information Processing Systems Foundation}, title = {{Relevant sparse codes with variational information bottleneck}}, volume = {29}, year = {2016}, } @article{1083, abstract = { Cholecystokinin-expressing interneurons (CCK-INs) mediate behavior state-dependent inhibition in cortical circuits and themselves receive strong GABAergic input. However, it remains unclear to what extent GABABreceptors (GABABRs) contribute to their inhibitory control. Using immunoelectron microscopy, we found that CCK-INs in the rat hippocampus possessed high levels of dendritic GABABRs and KCTD12 auxiliary proteins, whereas postsynaptic effector Kir3 channels were present at lower levels. Consistently, whole-cell recordings revealed slow GABABR-mediated inhibitory postsynaptic currents (IPSCs) in most CCK-INs. In spite of the higher surface density of GABABRs in CCK-INs than in CA1 principal cells, the amplitudes of IPSCs were comparable, suggesting that the expression of Kir3 channels is the limiting factor for the GABABR currents in these INs. Morphological analysis showed that CCK-INs were diverse, comprising perisomatic-targeting basket cells (BCs), as well as dendrite-targeting (DT) interneurons, including a previously undescribed DT type. GABABR-mediated IPSCs in CCK-INs were large in BCs, but small in DT subtypes. In response to prolonged activation, GABABR-mediated currents displayed strong desensitization, which was absent in KCTD12-deficient mice. This study highlights that GABABRs differentially control CCK-IN subtypes, and the kinetics and desensitization of GABABR-mediated currents are modulated by KCTD12 proteins. }, author = {Booker, Sam and Althof, Daniel and Gross, Anna and Loreth, Desiree and Müller, Johanna and Unger, Andreas and Fakler, Bernd and Varro, Andrea and Watanabe, Masahiko and Gassmann, Martin and Bettler, Bernhard and Shigemoto, Ryuichi and Vida, Imre and Kulik, Ákos}, journal = {Cerebral Cortex}, number = {3}, pages = {2318 -- 2334}, publisher = {Oxford University Press}, title = {{KCTD12 auxiliary proteins modulate kinetics of GABAB receptor-mediated inhibition in Cholecystokinin-containing interneurons}}, doi = {10.1093/cercor/bhw090}, volume = {27}, year = {2016}, } @article{1088, abstract = {Cell geometry is tightly coupled to gene expression patterns within the tissue microenvironment. This perspective synthesizes evidence that the 3D organization of chromosomes is a critical intermediate for geometric control of genomic programs. Using a combination of experiments and modeling we outline approaches to decipher the mechano-genomic code that governs cellular homeostasis and reprogramming.}, author = {Uhler, Caroline and Shivashankar, G V}, journal = {BioArchitecture}, number = {4}, pages = {76 -- 84}, publisher = {Taylor & Francis}, title = {{Geometric control and modeling of genome reprogramming}}, doi = {10.1080/19490992.2016.1201620}, volume = {6}, year = {2016}, } @inproceedings{1090, abstract = { While weighted automata provide a natural framework to express quantitative properties, many basic properties like average response time cannot be expressed with weighted automata. Nested weighted automata extend weighted automata and consist of a master automaton and a set of slave automata that are invoked by the master automaton. Nested weighted automata are strictly more expressive than weighted automata (e.g., average response time can be expressed with nested weighted automata), but the basic decision questions have higher complexity (e.g., for deterministic automata, the emptiness question for nested weighted automata is PSPACE-hard, whereas the corresponding complexity for weighted automata is PTIME). We consider a natural subclass of nested weighted automata where at any point at most a bounded number k of slave automata can be active. We focus on automata whose master value function is the limit average. We show that these nested weighted automata with bounded width are strictly more expressive than weighted automata (e.g., average response time with no overlapping requests can be expressed with bound k=1, but not with non-nested weighted automata). We show that the complexity of the basic decision problems (i.e., emptiness and universality) for the subclass with k constant matches the complexity for weighted automata. Moreover, when k is part of the input given in unary we establish PSPACE-completeness.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Otop, Jan}, location = {Krakow; Poland}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Nested weighted limit-average automata of bounded width}}, doi = {10.4230/LIPIcs.MFCS.2016.24}, volume = {58}, year = {2016}, } @inbook{1094, abstract = {Immunogold labeling of freeze-fracture replicas has recently been used for high-resolution visualization of protein localization in electron microscopy. This method has higher labeling efficiency than conventional immunogold methods for membrane molecules allowing precise quantitative measurements. However, one of the limitations of freeze-fracture replica immunolabeling is difficulty in keeping structural orientation and identifying labeled profiles in complex tissues like brain. The difficulty is partly due to fragmentation of freeze-fracture replica preparations during labeling procedures and limited morphological clues on the replica surface. To overcome these issues, we introduce here a grid-glued replica method combined with SEM observation. This method allows histological staining before dissolving the tissue and easy handling of replicas during immunogold labeling, and keeps the whole replica surface intact without fragmentation. The procedure described here is also useful for matched double-replica analysis allowing further identification of labeled profiles in corresponding P-face and E-face.}, author = {Harada, Harumi and Shigemoto, Ryuichi}, booktitle = {High-Resolution Imaging of Cellular Proteins}, issn = {1611-3349}, pages = {203 -- 216}, publisher = {Springer}, title = {{Immunogold protein localization on grid-glued freeze-fracture replicas}}, doi = {10.1007/978-1-4939-6352-2_12}, volume = {1474}, year = {2016}, } @inproceedings{1095, abstract = { The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Nevertheless, for applications that do not require all guarantees offered by linearizability, recent research has focused on improving performance and scalability of concurrent data structures by relaxing their semantics. In this paper, we present local linearizability, a relaxed consistency condition that is applicable to container-type concurrent data structures like pools, queues, and stacks. While linearizability requires that the effect of each operation is observed by all threads at the same time, local linearizability only requires that for each thread T, the effects of its local insertion operations and the effects of those removal operations that remove values inserted by T are observed by all threads at the same time. We investigate theoretical and practical properties of local linearizability and its relationship to many existing consistency conditions. We present a generic implementation method for locally linearizable data structures that uses existing linearizable data structures as building blocks. Our implementations show performance and scalability improvements over the original building blocks and outperform the fastest existing container-type implementations. }, author = {Haas, Andreas and Henzinger, Thomas A and Holzer, Andreas and Kirsch, Christoph and Lippautz, Michael and Payer, Hannes and Sezgin, Ali and Sokolova, Ana and Veith, Helmut}, booktitle = {Leibniz International Proceedings in Informatics}, location = {Quebec City; Canada}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Local linearizability for concurrent container-type data structures}}, doi = {10.4230/LIPIcs.CONCUR.2016.6}, volume = {59}, year = {2016}, } @inproceedings{1097, abstract = {We present an interactive system for computational design, optimization, and fabrication of multicopters. Our computational approach allows non-experts to design, explore, and evaluate a wide range of different multicopters. We provide users with an intuitive interface for assembling a multicopter from a collection of components (e.g., propellers, motors, and carbon fiber rods). Our algorithm interactively optimizes shape and controller parameters of the current design to ensure its proper operation. In addition, we allow incorporating a variety of other metrics (such as payload, battery usage, size, and cost) into the design process and exploring tradeoffs between them. We show the efficacy of our method and system by designing, optimizing, fabricating, and operating multicopters with complex geometries and propeller configurations. We also demonstrate the ability of our optimization algorithm to improve the multicopter performance under different metrics.}, author = {Du, Tao and Schulz, Adriana and Zhu, Bo and Bickel, Bernd and Matusik, Wojciech}, location = {Macao, China}, number = {6}, publisher = {ACM}, title = {{Computational multicopter design}}, doi = {10.1145/2980179.2982427}, volume = {35}, year = {2016}, } @inproceedings{1098, abstract = {Better understanding of the potential benefits of information transfer and representation learning is an important step towards the goal of building intelligent systems that are able to persist in the world and learn over time. In this work, we consider a setting where the learner encounters a stream of tasks but is able to retain only limited information from each encountered task, such as a learned predictor. In contrast to most previous works analyzing this scenario, we do not make any distributional assumptions on the task generating process. Instead, we formulate a complexity measure that captures the diversity of the observed tasks. We provide a lifelong learning algorithm with error guarantees for every observed task (rather than on average). We show sample complexity reductions in comparison to solving every task in isolation in terms of our task complexity measure. Further, our algorithmic framework can naturally be viewed as learning a representation from encountered tasks with a neural network.}, author = {Pentina, Anastasia and Urner, Ruth}, location = {Barcelona, Spain}, pages = {3619--3627}, publisher = {Neural Information Processing Systems Foundation}, title = {{Lifelong learning with weighted majority votes}}, volume = {29}, year = {2016}, } @inproceedings{1099, abstract = {We present FlexMolds, a novel computational approach to automatically design flexible, reusable molds that, once 3D printed, allow us to physically fabricate, by means of liquid casting, multiple copies of complex shapes with rich surface details and complex topology. The approach to design such flexible molds is based on a greedy bottom-up search of possible cuts over an object, evaluating for each possible cut the feasibility of the resulting mold. We use a dynamic simulation approach to evaluate candidate molds, providing a heuristic to generate forces that are able to open, detach, and remove a complex mold from the object it surrounds. We have tested the approach with a number of objects with nontrivial shapes and topologies.}, author = {Malomo, Luigi and Pietroni, Nico and Bickel, Bernd and Cignoni, Paolo}, location = {Macao, China}, number = {6}, publisher = {ACM}, title = {{FlexMolds: Automatic design of flexible shells for molding}}, doi = {10.1145/2980179.2982397}, volume = {35}, year = {2016}, } @article{1101, abstract = {Optical sensors based on the phenomenon of Förster resonance energy transfer (FRET) are powerful tools that have advanced the study of small molecules in biological systems. However, sensor construction is not trivial and often requires multiple rounds of engineering or an ability to screen large numbers of variants. A method that would allow the accurate rational design of FRET sensors would expedite the production of biologically useful sensors. Here, we present Rangefinder, a computational algorithm that allows rapid in silico screening of dye attachment sites in a ligand-binding protein for the conjugation of a dye molecule to act as a Förster acceptor for a fused fluorescent protein. We present three ratiometric fluorescent sensors designed with Rangefinder, including a maltose sensor with a dynamic range of >300% and the first sensors for the most abundant sialic acid in human cells, N-acetylneuraminic acid. Provided a ligand-binding protein exists, it is our expectation that this model will facilitate the design of an optical sensor for any small molecule of interest.}, author = {Mitchell, Joshua and Whitfield, Jason and Zhang, William and Henneberger, Christian and Janovjak, Harald L and O'Mara, Megan and Jackson, Colin}, journal = {ACS SENSORS}, number = {11}, pages = {1286 -- 1290}, publisher = {American Chemical Society}, title = {{Rangefinder: A semisynthetic FRET sensor design algorithm}}, doi = {10.1021/acssensors.6b00576}, volume = {1}, year = {2016}, }