@article{304,
  abstract     = {Additive manufacturing has recently seen drastic improvements in resolution, making it now possible to fabricate features at scales of hundreds or even dozens of nanometers, which previously required very expensive lithographic methods.
As a result, additive manufacturing now seems poised for optical applications, including those relevant to computer graphics, such as material design, as well as display and imaging applications.
 
In this work, we explore the use of additive manufacturing for generating structural colors, where the structures are designed using a fabrication-aware optimization process.
This requires a combination of full-wave simulation, a feasible parameterization of the design space, and a tailored optimization procedure.
Many of these components should be re-usable for the design of other optical structures at this scale.
 
We show initial results of material samples fabricated based on our designs.
While these suffer from the prototype character of state-of-the-art fabrication hardware, we believe they clearly demonstrate the potential of additive nanofabrication for structural colors and other graphics applications.},
  author       = {Auzinger, Thomas and Heidrich, Wolfgang and Bickel, Bernd},
  journal      = {ACM Transactions on Graphics},
  number       = {4},
  publisher    = {ACM},
  title        = {{Computational design of nanostructural color for additive manufacturing}},
  doi          = {10.1145/3197517.3201376},
  volume       = {37},
  year         = {2018},
}

@article{305,
  abstract     = {The hanging-drop network (HDN) is a technology platform based on a completely open microfluidic network at the bottom of an inverted, surface-patterned substrate. The platform is predominantly used for the formation, culturing, and interaction of self-assembled spherical microtissues (spheroids) under precisely controlled flow conditions. Here, we describe design, fabrication, and operation of microfluidic hanging-drop networks.},
  author       = {Misun, Patrick and Birchler, Axel and Lang, Moritz and Hierlemann, Andreas and Frey, Olivier},
  journal      = {Methods in Molecular Biology},
  pages        = {183 -- 202},
  publisher    = {Springer},
  title        = {{Fabrication and operation of microfluidic hanging drop networks}},
  doi          = {10.1007/978-1-4939-7792-5_15},
  volume       = {1771},
  year         = {2018},
}

@article{306,
  abstract     = {A cornerstone of statistical inference, the maximum entropy framework is being increasingly applied to construct descriptive and predictive models of biological systems, especially complex biological networks, from large experimental data sets. Both its broad applicability and the success it obtained in different contexts hinge upon its conceptual simplicity and mathematical soundness. Here we try to concisely review the basic elements of the maximum entropy principle, starting from the notion of ‘entropy’, and describe its usefulness for the analysis of biological systems. As examples, we focus specifically on the problem of reconstructing gene interaction networks from expression data and on recent work attempting to expand our system-level understanding of bacterial metabolism. Finally, we highlight some extensions and potential limitations of the maximum entropy approach, and point to more recent developments that are likely to play a key role in the upcoming challenges of extracting structures and information from increasingly rich, high-throughput biological data.},
  author       = {De Martino, Andrea and De Martino, Daniele},
  journal      = {Heliyon},
  number       = {4},
  publisher    = {Elsevier},
  title        = {{An introduction to the maximum entropy approach and its application to inference problems in biology}},
  doi          = {10.1016/j.heliyon.2018.e00596},
  volume       = {4},
  year         = {2018},
}

@article{308,
  abstract     = {Migrating cells penetrate tissue barriers during development, inflammatory responses, and tumor metastasis. We study if migration in vivo in such three-dimensionally confined environments requires changes in the mechanical properties of the surrounding cells using embryonic Drosophila melanogaster hemocytes, also called macrophages, as a model. We find that macrophage invasion into the germband through transient separation of the apposing ectoderm and mesoderm requires cell deformations and reductions in apical tension in the ectoderm. Interestingly, the genetic pathway governing these mechanical shifts acts downstream of the only known tumor necrosis factor superfamily member in Drosophila, Eiger, and its receptor, Grindelwald. Eiger-Grindelwald signaling reduces levels of active Myosin in the germband ectodermal cortex through the localization of a Crumbs complex component, Patj (Pals-1-associated tight junction protein). We therefore elucidate a distinct molecular pathway that controls tissue tension and demonstrate the importance of such regulation for invasive migration in vivo.},
  author       = {Ratheesh, Aparna and Biebl, Julia and Smutny, Michael and Veselá, Jana and Papusheva, Ekaterina and Krens, Gabriel and Kaufmann, Walter and György, Attila and Casano, Alessandra M and Siekhaus, Daria E},
  journal      = {Developmental Cell},
  number       = {3},
  pages        = {331 -- 346},
  publisher    = {Elsevier},
  title        = {{Drosophila TNF modulates tissue tension in the embryo to facilitate macrophage invasive migration}},
  doi          = {10.1016/j.devcel.2018.04.002},
  volume       = {45},
  year         = {2018},
}

@article{1215,
  abstract     = {Two generalizations of Itô formula to infinite-dimensional spaces are given.
The first one, in Hilbert spaces, extends the classical one by taking advantage of
cancellations when they occur in examples and it is applied to the case of a group
generator. The second one, based on the previous one and a limit procedure, is an Itô
formula in a special class of Banach spaces having a product structure with the noise
in a Hilbert component; again the key point is the extension due to a cancellation. This
extension to Banach spaces and in particular the specific cancellation are motivated
by path-dependent Itô calculus.},
  author       = {Flandoli, Franco and Russo, Francesco and Zanco, Giovanni A},
  journal      = {Journal of Theoretical Probability},
  number       = {2},
  pages        = {789--826},
  publisher    = {Springer},
  title        = {{Infinite-dimensional calculus under weak spatial regularity of the processes}},
  doi          = {10.1007/s10959-016-0724-2},
  volume       = {31},
  year         = {2018},
}

@misc{13055,
  abstract     = {Dataset for manuscript 'Social network plasticity decreases disease transmission in a eusocial insect'
Compared to previous versions: - raw image files added
                                                     - correction of URLs within README.txt file
},
  author       = {Stroeymeyt, Nathalie and Grasse, Anna V and Crespi, Alessandro and Mersch, Danielle and Cremer, Sylvia and Keller, Laurent},
  publisher    = {Zenodo},
  title        = {{Social network plasticity decreases disease transmission in a eusocial insect}},
  doi          = {10.5281/ZENODO.1322669},
  year         = {2018},
}

@misc{13059,
  abstract     = {This dataset contains a GitHub repository containing all the data, analysis, Nextflow workflows and Jupyter notebooks to replicate the manuscript titled "Fast and accurate large multiple sequence alignments with a root-to-leaf regressive method".
It also contains the Multiple Sequence Alignments (MSAs) generated and well as the main figures and tables from the manuscript.
The repository is also available at GitHub (https://github.com/cbcrg/dpa-analysis) release `v1.2`.
For details on how to use the regressive alignment algorithm, see the T-Coffee software suite (https://github.com/cbcrg/tcoffee).},
  author       = {Garriga, Edgar and di Tommaso, Paolo and Magis, Cedrik and Erb, Ionas and Mansouri, Leila and Baltzis, Athanasios and Laayouni, Hafid and Kondrashov, Fyodor and Floden, Evan and Notredame, Cedric},
  publisher    = {Zenodo},
  title        = {{Fast and accurate large multiple sequence alignments with a root-to-leaf regressive method}},
  doi          = {10.5281/ZENODO.2025846},
  year         = {2018},
}

@article{132,
  abstract     = {Pancreas development involves a coordinated process in which an early phase of cell segregation is followed by a longer phase of lineage restriction, expansion, and tissue remodeling. By combining clonal tracing and whole-mount reconstruction with proliferation kinetics and single-cell transcriptional profiling, we define the functional basis of pancreas morphogenesis. We show that the large-scale organization of mouse pancreas can be traced to the activity of self-renewing precursors positioned at the termini of growing ducts, which act collectively to drive serial rounds of stochastic ductal bifurcation balanced by termination. During this phase of branching morphogenesis, multipotent precursors become progressively fate-restricted, giving rise to self-renewing acinar-committed precursors that are conveyed with growing ducts, as well as ductal progenitors that expand the trailing ducts and give rise to delaminating endocrine cells. These findings define quantitatively how the functional behavior and lineage progression of precursor pools determine the large-scale patterning of pancreatic sub-compartments.},
  author       = {Sznurkowska, Magdalena and Hannezo, Edouard B and Azzarelli, Roberta and Rulands, Steffen and Nestorowa, Sonia and Hindley, Christopher and Nichols, Jennifer and Göttgens, Berthold and Huch, Meritxell and Philpott, Anna and Simons, Benjamin},
  journal      = {Developmental Cell},
  number       = {3},
  pages        = {360 -- 375},
  publisher    = {Cell Press},
  title        = {{Defining lineage potential and fate behavior of precursors during pancreas development}},
  doi          = {10.1016/j.devcel.2018.06.028},
  volume       = {46},
  year         = {2018},
}

@article{134,
  abstract     = {The current state of the art in real-time two-dimensional water wave simulation requires developers to choose between efficient Fourier-based methods, which lack interactions with moving obstacles, and finite-difference or finite element methods, which handle environmental interactions but are significantly more expensive. This paper attempts to bridge this long-standing gap between complexity and performance, by proposing a new wave simulation method that can faithfully simulate wave interactions with moving obstacles in real time while simultaneously preserving minute details and accommodating very large simulation domains.

Previous methods for simulating 2D water waves directly compute the change in height of the water surface, a strategy which imposes limitations based on the CFL condition (fast moving waves require small time steps) and Nyquist's limit (small wave details require closely-spaced simulation variables). This paper proposes a novel wavelet transformation that discretizes the liquid motion in terms of amplitude-like functions that vary over space, frequency, and direction, effectively generalizing Fourier-based methods to handle local interactions. Because these new variables change much more slowly over space than the original water height function, our change of variables drastically reduces the limitations of the CFL condition and Nyquist limit, allowing us to simulate highly detailed water waves at very large visual resolutions. Our discretization is amenable to fast summation and easy to parallelize. We also present basic extensions like pre-computed wave paths and two-way solid fluid coupling. Finally, we argue that our discretization provides a convenient set of variables for artistic manipulation, which we illustrate with a novel wave-painting interface.},
  author       = {Jeschke, Stefan and Skrivan, Tomas and Mueller Fischer, Matthias and Chentanez, Nuttapong and Macklin, Miles and Wojtan, Christopher J},
  journal      = {ACM Transactions on Graphics},
  number       = {4},
  publisher    = {ACM},
  title        = {{Water surface wavelets}},
  doi          = {10.1145/3197517.3201336},
  volume       = {37},
  year         = {2018},
}

@article{135,
  abstract     = {The Fluid Implicit Particle method (FLIP) reduces numerical dissipation by combining particles with grids. To improve performance, the subsequent narrow band FLIP method (NB‐FLIP) uses a FLIP‐based fluid simulation only near the liquid surface and a traditional grid‐based fluid simulation away from the surface. This spatially‐limited FLIP simulation significantly reduces the number of particles and alleviates a computational bottleneck. In this paper, we extend the NB‐FLIP idea even further, by allowing a simulation to transition between a FLIP‐like fluid simulation and a grid‐based simulation in arbitrary locations, not just near the surface. This approach leads to even more savings in memory and computation, because we can concentrate the particles only in areas where they are needed. More importantly, this new method allows us to seamlessly transition to smooth implicit surface geometry wherever the particle‐based simulation is unnecessary. Consequently, our method leads to a practical algorithm for avoiding the noisy surface artifacts associated with particle‐based liquid simulations, while simultaneously maintaining the benefits of a FLIP simulation in regions of dynamic motion.},
  author       = {Sato, Takahiro and Wojtan, Christopher J and Thuerey, Nils and Igarashi, Takeo and Ando, Ryoichi},
  issn         = {0167-7055},
  journal      = {Computer Graphics Forum},
  number       = {2},
  pages        = {169 -- 177},
  publisher    = {Wiley},
  title        = {{Extended narrow band FLIP for liquid simulations}},
  doi          = {10.1111/cgf.13351},
  volume       = {37},
  year         = {2018},
}

@article{136,
  abstract     = {Recent studies suggest that unstable, nonchaotic solutions of the Navier-Stokes equation may provide deep insights into fluid turbulence. In this article, we present a combined experimental and numerical study exploring the dynamical role of unstable equilibrium solutions and their invariant manifolds in a weakly turbulent, electromagnetically driven, shallow fluid layer. Identifying instants when turbulent evolution slows down, we compute 31 unstable equilibria of a realistic two-dimensional model of the flow. We establish the dynamical relevance of these unstable equilibria by showing that they are closely visited by the turbulent flow. We also establish the dynamical relevance of unstable manifolds by verifying that they are shadowed by turbulent trajectories departing from the neighborhoods of unstable equilibria over large distances in state space.},
  author       = {Suri, Balachandra and Tithof, Jeffrey and Grigoriev, Roman and Schatz, Michael},
  journal      = {Physical Review E},
  number       = {2},
  publisher    = {American Physical Society},
  title        = {{Unstable equilibria and invariant manifolds in quasi-two-dimensional Kolmogorov-like flow}},
  doi          = {10.1103/PhysRevE.98.023105},
  volume       = {98},
  year         = {2018},
}

@article{137,
  abstract     = {Fluorescent sensors are an essential part of the experimental toolbox of the life sciences, where they are used ubiquitously to visualize intra- and extracellular signaling. In the brain, optical neurotransmitter sensors can shed light on temporal and spatial aspects of signal transmission by directly observing, for instance, neurotransmitter release and spread. Here we report the development and application of the first optical sensor for the amino acid glycine, which is both an inhibitory neurotransmitter and a co-agonist of the N-methyl-d-aspartate receptors (NMDARs) involved in synaptic plasticity. Computational design of a glycine-specific binding protein allowed us to produce the optical glycine FRET sensor (GlyFS), which can be used with single and two-photon excitation fluorescence microscopy. We took advantage of this newly developed sensor to test predictions about the uneven spatial distribution of glycine in extracellular space and to demonstrate that extracellular glycine levels are controlled by plasticity-inducing stimuli.},
  author       = {Zhang, William and Herde, Michel and Mitchell, Joshua and Whitfield, Jason and Wulff, Andreas and Vongsouthi, Vanessa and Sanchez Romero, Inmaculada and Gulakova, Polina and Minge, Daniel and Breithausen, Björn and Schoch, Susanne and Janovjak, Harald L and Jackson, Colin and Henneberger, Christian},
  journal      = {Nature Chemical Biology},
  number       = {9},
  pages        = {861 -- 869},
  publisher    = {Nature Publishing Group},
  title        = {{Monitoring hippocampal glycine with the computationally designed optical sensor GlyFS}},
  doi          = {10.1038/s41589-018-0108-2},
  volume       = {14},
  year         = {2018},
}

@article{139,
  abstract     = {Genome-scale diversity data are increasingly available in a variety of biological systems, and can be used to reconstruct the past evolutionary history of species divergence. However, extracting the full demographic information from these data is not trivial, and requires inferential methods that account for the diversity of coalescent histories throughout the genome. Here, we evaluate the potential and limitations of one such approach. We reexamine a well-known system of mussel sister species, using the joint site frequency spectrum (jSFS) of synonymousmutations computed either fromexome capture or RNA-seq, in an Approximate Bayesian Computation (ABC) framework. We first assess the best sampling strategy (number of: individuals, loci, and bins in the jSFS), and show that model selection is robust to variation in the number of individuals and loci. In contrast, different binning choices when summarizing the jSFS, strongly affect the results: including classes of low and high frequency shared polymorphisms can more effectively reveal recent migration events. We then take advantage of the flexibility of ABC to compare more realistic models of speciation, including variation in migration rates through time (i.e., periodic connectivity) and across genes (i.e., genome-wide heterogeneity in migration rates). We show that these models were consistently selected as the most probable, suggesting that mussels have experienced a complex history of gene flow during divergence and that the species boundary is semi-permeable. Our work provides a comprehensive evaluation of ABC demographic inference in mussels based on the coding jSFS, and supplies guidelines for employing different sequencing techniques and sampling strategies. We emphasize, perhaps surprisingly, that inferences are less limited by the volume of data, than by the way in which they are analyzed.},
  author       = {Fraisse, Christelle and Roux, Camille and Gagnaire, Pierre and Romiguier, Jonathan and Faivre, Nicolas and Welch, John and Bierne, Nicolas},
  journal      = {PeerJ},
  number       = {7},
  publisher    = {PeerJ},
  title        = {{The divergence history of European blue mussel species reconstructed from Approximate Bayesian Computation: The effects of sequencing techniques and sampling strategies}},
  doi          = {10.7717/peerj.5198},
  volume       = {2018},
  year         = {2018},
}

@article{14,
  abstract     = {The intercellular transport of auxin is driven by PIN-formed (PIN) auxin efflux carriers. PINs are localized at the plasma membrane (PM) and on constitutively recycling endomembrane vesicles. Therefore, PINs can mediate auxin transport either by direct translocation across the PM or by pumping auxin into secretory vesicles (SVs), leading to its secretory release upon fusion with the PM. Which of these two mechanisms dominates is a matter of debate. Here, we addressed the issue with a mathematical modeling approach. We demonstrate that the efficiency of secretory transport depends on SV size, half-life of PINs on the PM, pH, exocytosis frequency and PIN density. 3D structured illumination microscopy (SIM) was used to determine PIN density on the PM. Combining this data with published values of the other parameters, we show that the transport activity of PINs in SVs would have to be at least 1000× greater than on the PM in order to produce a comparable macroscopic auxin transport. If both transport mechanisms operated simultaneously and PINs were equally active on SVs and PM, the contribution of secretion to the total auxin flux would be negligible. In conclusion, while secretory vesicle-mediated transport of auxin is an intriguing and theoretically possible model, it is unlikely to be a major mechanism of auxin transport inplanta.},
  author       = {Hille, Sander and Akhmanova, Maria and Glanc, Matous and Johnson, Alexander J and Friml, Jirí},
  issn         = {1422-0067},
  journal      = {International Journal of Molecular Sciences},
  number       = {11},
  publisher    = {MDPI},
  title        = {{Relative contribution of PIN-containing secretory vesicles and plasma membrane PINs to the directed auxin transport: Theoretical estimation}},
  doi          = {10.3390/ijms19113566},
  volume       = {19},
  year         = {2018},
}

@inproceedings{140,
  abstract     = {Reachability analysis is difficult for hybrid automata with affine differential equations, because the reach set needs to be approximated. Promising abstraction techniques usually employ interval methods or template polyhedra. Interval methods account for dense time and guarantee soundness, and there are interval-based tools that overapproximate affine flowpipes. But interval methods impose bounded and rigid shapes, which make refinement expensive and fixpoint detection difficult. Template polyhedra, on the other hand, can be adapted flexibly and can be unbounded, but sound template refinement for unbounded reachability analysis has been implemented only for systems with piecewise constant dynamics. We capitalize on the advantages of both techniques, combining interval arithmetic and template polyhedra, using the former to abstract time and the latter to abstract space. During a CEGAR loop, whenever a spurious error trajectory is found, we compute additional space constraints and split time intervals, and use these space-time interpolants to eliminate the counterexample. Space-time interpolation offers a lazy, flexible framework for increasing precision while guaranteeing soundness, both for error avoidance and fixpoint detection. To the best of out knowledge, this is the first abstraction refinement scheme for the reachability analysis over unbounded and dense time of affine hybrid systems, which is both sound and automatic. We demonstrate the effectiveness of our algorithm with several benchmark examples, which cannot be handled by other tools.},
  author       = {Frehse, Goran and Giacobbe, Mirco and Henzinger, Thomas A},
  issn         = {0302-9743},
  location     = {Oxford, United Kingdom},
  pages        = {468 -- 486},
  publisher    = {Springer},
  title        = {{Space-time interpolants}},
  doi          = {10.1007/978-3-319-96145-3_25},
  volume       = {10981},
  year         = {2018},
}

@inproceedings{141,
  abstract     = {Given a model and a specification, the fundamental model-checking problem asks for algorithmic verification of whether the model satisfies the specification. We consider graphs and Markov decision processes (MDPs), which are fundamental models for reactive systems. One of the very basic specifications that arise in verification of reactive systems is the strong fairness (aka Streett) objective. Given different types of requests and corresponding grants, the objective requires that for each type, if the request event happens infinitely often, then the corresponding grant event must also happen infinitely often. All ω -regular objectives can be expressed as Streett objectives and hence they are canonical in verification. To handle the state-space explosion, symbolic algorithms are required that operate on a succinct implicit representation of the system rather than explicitly accessing the system. While explicit algorithms for graphs and MDPs with Streett objectives have been widely studied, there has been no improvement of the basic symbolic algorithms. The worst-case numbers of symbolic steps required for the basic symbolic algorithms are as follows: quadratic for graphs and cubic for MDPs. In this work we present the first sub-quadratic symbolic algorithm for graphs with Streett objectives, and our algorithm is sub-quadratic even for MDPs. Based on our algorithmic insights we present an implementation of the new symbolic approach and show that it improves the existing approach on several academic benchmark examples.},
  author       = {Chatterjee, Krishnendu and Henzinger, Monika H and Loitzenbauer, Veronika and Oraee, Simin and Toman, Viktor},
  location     = {Oxford, United Kingdom},
  pages        = {178--197},
  publisher    = {Springer},
  title        = {{Symbolic algorithms for graphs and Markov decision processes with fairness objectives}},
  doi          = {10.1007/978-3-319-96142-2_13},
  volume       = {10982},
  year         = {2018},
}

@inproceedings{142,
  abstract     = {We address the problem of analyzing the reachable set of a polynomial nonlinear continuous system by over-approximating the flowpipe of its dynamics. The common approach to tackle this problem is to perform a numerical integration over a given time horizon based on Taylor expansion and interval arithmetic. However, this method results to be very conservative when there is a large difference in speed between trajectories as time progresses. In this paper, we propose to use combinations of barrier functions, which we call piecewise barrier tube (PBT), to over-approximate flowpipe. The basic idea of PBT is that for each segment of a flowpipe, a coarse box which is big enough to contain the segment is constructed using sampled simulation and then in the box we compute by linear programming a set of barrier functions (called barrier tube or BT for short) which work together to form a tube surrounding the flowpipe. The benefit of using PBT is that (1) BT is independent of time and hence can avoid being stretched and deformed by time; and (2) a small number of BTs can form a tight over-approximation for the flowpipe, which means that the computation required to decide whether the BTs intersect the unsafe set can be reduced significantly. We implemented a prototype called PBTS in C++. Experiments on some benchmark systems show that our approach is effective.},
  author       = {Kong, Hui and Bartocci, Ezio and Henzinger, Thomas A},
  location     = {Oxford, United Kingdom},
  pages        = {449 -- 467},
  publisher    = {Springer},
  title        = {{Reachable set over-approximation for nonlinear systems using piecewise barrier tubes}},
  doi          = {10.1007/978-3-319-96145-3_24},
  volume       = {10981},
  year         = {2018},
}

@inproceedings{143,
  abstract     = {Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form Θ(nk), for some integer k d, where d is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal k. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a k such that the termination complexity is (nk). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.},
  author       = {Brázdil, Tomáš and Chatterjee, Krishnendu and Kučera, Antonín and Novotny, Petr and Velan, Dominik and Zuleger, Florian},
  isbn         = {978-1-4503-5583-4},
  location     = {Oxford, United Kingdom},
  pages        = {185 -- 194},
  publisher    = {IEEE},
  title        = {{Efficient algorithms for asymptotic bounds on termination time in VASS}},
  doi          = {10.1145/3209108.3209191},
  volume       = {F138033},
  year         = {2018},
}

@inproceedings{144,
  abstract     = {The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety -languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines.},
  author       = {Ferrere, Thomas and Henzinger, Thomas A and Saraç, Ege},
  location     = {Oxford, UK},
  pages        = {394 -- 403},
  publisher    = {IEEE},
  title        = {{A theory of register monitors}},
  doi          = {10.1145/3209108.3209194},
  volume       = {Part F138033},
  year         = {2018},
}

@article{145,
  abstract     = {Aged proteins can become hazardous to cellular function, by accumulating molecular damage. This implies that cells should preferentially rely on newly produced ones. We tested this hypothesis in cultured hippocampal neurons, focusing on synaptic transmission. We found that newly synthesized vesicle proteins were incorporated in the actively recycling pool of vesicles responsible for all neurotransmitter release during physiological activity. We observed this for the calcium sensor Synaptotagmin 1, for the neurotransmitter transporter VGAT, and for the fusion protein VAMP2 (Synaptobrevin 2). Metabolic labeling of proteins and visualization by secondary ion mass spectrometry enabled us to query the entire protein makeup of the actively recycling vesicles, which we found to be younger than that of non-recycling vesicles. The young vesicle proteins remained in use for up to ~ 24 h, during which they participated in recycling a few hundred times. They were afterward reluctant to release and were degraded after an additional ~ 24–48 h. We suggest that the recycling pool of synaptic vesicles relies on newly synthesized proteins, while the inactive reserve pool contains older proteins.},
  author       = {Truckenbrodt, Sven M and Viplav, Abhiyan and Jähne, Sebsatian and Vogts, Angela and Denker, Annette and Wildhagen, Hanna and Fornasiero, Eugenio and Rizzoli, Silvio},
  issn         = {0261-4189},
  journal      = {The EMBO Journal},
  number       = {15},
  publisher    = {Wiley},
  title        = {{Newly produced synaptic vesicle proteins are preferentially used in synaptic transmission}},
  doi          = {10.15252/embj.201798044},
  volume       = {37},
  year         = {2018},
}

