@inproceedings{1256, abstract = {Simulink is widely used for model driven development (MDD) of industrial software systems. Typically, the Simulink based development is initiated from Stateflow modeling, followed by simulation, validation and code generation mapped to physical execution platforms. However, recent industrial trends have raised the demands of rigorous verification on safety-critical applications, which is unfortunately challenging for Simulink. In this paper, we present an approach to bridge the Stateflow based model driven development and a well- defined rigorous verification. First, we develop a self- contained toolkit to translate Stateflow model into timed automata, where major advanced modeling features in Stateflow are supported. Taking advantage of the strong verification capability of Uppaal, we can not only find bugs in Stateflow models which are missed by Simulink Design Verifier, but also check more important temporal properties. Next, we customize a runtime verifier for the generated nonintrusive VHDL and C code of Stateflow model for monitoring. The major strength of the customization is the flexibility to collect and analyze runtime properties with a pure software monitor, which opens more opportunities for engineers to achieve high reliability of the target system compared with the traditional act that only relies on Simulink Polyspace. We incorporate these two parts into original Stateflow based MDD seamlessly. In this way, safety-critical properties are both verified at the model level, and at the consistent system implementation level with physical execution environment in consideration. We apply our approach on a train controller design, and the verified implementation is tested and deployed on a real hardware platform.}, author = {Jiang, Yu and Yang, Yixiao and Liu, Han and Kong, Hui and Gu, Ming and Sun, Jiaguang and Sha, Lui}, location = {Vienna, Austria}, publisher = {IEEE}, title = {{From stateflow simulation to verified implementation: A verification approach and a real-time train controller design}}, doi = {10.1109/RTAS.2016.7461337}, year = {2016}, } @article{1257, abstract = {We consider products of random matrices that are small, independent identically distributed perturbations of a fixed matrix (Formula presented.). Focusing on the eigenvalues of (Formula presented.) of a particular size we obtain a limit to a SDE in a critical scaling. Previous results required (Formula presented.) to be a (conjugated) unitary matrix so it could not have eigenvalues of different modulus. From the result we can also obtain a limit SDE for the Markov process given by the action of the random products on the flag manifold. Applying the result to random Schrödinger operators we can improve some results by Valko and Virag showing GOE statistics for the rescaled eigenvalue process of a sequence of Anderson models on long boxes. In particular, we solve a problem posed in their work.}, author = {Sadel, Christian and Virág, Bálint}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {881 -- 919}, publisher = {Springer}, title = {{A central limit theorem for products of random matrices and GOE statistics for the Anderson model on long boxes}}, doi = {10.1007/s00220-016-2600-4}, volume = {343}, year = {2016}, } @article{1258, abstract = {When plants grow in close proximity basic resources such as light can become limiting. Under such conditions plants respond to anticipate and/or adapt to the light shortage, a process known as the shade avoidance syndrome (SAS). Following genetic screening using a shade-responsive luciferase reporter line (PHYB:LUC), we identified DRACULA2 (DRA2), which encodes an Arabidopsis homolog of mammalian nucleoporin 98, a component of the nuclear pore complex (NPC). DRA2, together with other nucleoporins, participates positively in the control of the hypocotyl elongation response to plant proximity, a role that can be considered dependent on the nucleocytoplasmic transport of macromolecules (i.e. is transport dependent). In addition, our results reveal a specific role for DRA2 in controlling shade-induced gene expression. We suggest that this novel regulatory role of DRA2 is transport independent and that it might rely on its dynamic localization within and outside of the NPC. These results provide mechanistic insights in to how SAS responses are rapidly established by light conditions. They also indicate that nucleoporins have an active role in plant signaling.}, author = {Gallemi Rovira, Marcal and Galstyan, Anahit and Paulišić, Sandi and Then, Christiane and Ferrández Ayela, Almudena and Lorenzo Orts, Laura and Roig Villanova, Irma and Wang, Xuewen and Micol, José and Ponce, Maria and Devlin, Paul and Martínez García, Jaime}, journal = {Development}, number = {9}, pages = {1623 -- 1631}, publisher = {Company of Biologists}, title = {{DRACULA2 is a dynamic nucleoporin with a role in regulating the shade avoidance syndrome in Arabidopsis}}, doi = {10.1242/dev.130211}, volume = {143}, year = {2016}, } @article{1259, abstract = {We consider the Bogolubov–Hartree–Fock functional for a fermionic many-body system with two-body interactions. For suitable interaction potentials that have a strong enough attractive tail in order to allow for two-body bound states, but are otherwise sufficiently repulsive to guarantee stability of the system, we show that in the low-density limit the ground state of this model consists of a Bose–Einstein condensate of fermion pairs. The latter can be described by means of the Gross–Pitaevskii energy functional.}, author = {Bräunlich, Gerhard and Hainzl, Christian and Seiringer, Robert}, journal = {Mathematical Physics, Analysis and Geometry}, number = {2}, publisher = {Springer}, title = {{Bogolubov–Hartree–Fock theory for strongly interacting fermions in the low density limit}}, doi = {10.1007/s11040-016-9209-x}, volume = {19}, year = {2016}, } @article{1260, abstract = {In this work, the Gardner problem of inferring interactions and fields for an Ising neural network from given patterns under a local stability hypothesis is addressed under a dual perspective. By means of duality arguments, an integer linear system is defined whose solution space is the dual of the Gardner space and whose solutions represent mutually unstable patterns. We propose and discuss Monte Carlo methods in order to find and remove unstable patterns and uniformly sample the space of interactions thereafter. We illustrate the problem on a set of real data and perform ensemble calculation that shows how the emergence of phase dominated by unstable patterns can be triggered in a nonlinear discontinuous way.}, author = {De Martino, Daniele}, journal = {International Journal of Modern Physics C}, number = {6}, publisher = {World Scientific Publishing}, title = {{The dual of the space of interactions in neural network models}}, doi = {10.1142/S0129183116500674}, volume = {27}, year = {2016}, } @article{1261, abstract = {We consider a non-standard finite-volume discretization of a strongly non-linear fourth order diffusion equation on the d-dimensional cube, for arbitrary . The scheme preserves two important structural properties of the equation: the first is the interpretation as a gradient flow in a mass transportation metric, and the second is an intimate relation to a linear Fokker-Planck equation. Thanks to these structural properties, the scheme possesses two discrete Lyapunov functionals. These functionals approximate the entropy and the Fisher information, respectively, and their dissipation rates converge to the optimal ones in the discrete-to-continuous limit. Using the dissipation, we derive estimates on the long-time asymptotics of the discrete solutions. Finally, we present results from numerical experiments which indicate that our discretization is able to capture significant features of the complex original dynamics, even with a rather coarse spatial resolution.}, author = {Maas, Jan and Matthes, Daniel}, journal = {Nonlinearity}, number = {7}, pages = {1992 -- 2023}, publisher = {IOP Publishing Ltd.}, title = {{Long-time behavior of a finite volume discretization for a fourth order diffusion equation}}, doi = {10.1088/0951-7715/29/7/1992}, volume = {29}, year = {2016}, } @article{1262, abstract = {Emerging infectious diseases (EIDs) have contributed significantly to the current biodiversity crisis, leading to widespread epidemics and population loss. Owing to genetic variation in pathogen virulence, a complete understanding of species decline requires the accurate identification and characterization of EIDs. We explore this issue in the Western honeybee, where increasing mortality of populations in the Northern Hemisphere has caused major concern. Specifically, we investigate the importance of genetic identity of the main suspect in mortality, deformed wing virus (DWV), in driving honeybee loss. Using laboratory experiments and a systematic field survey, we demonstrate that an emerging DWV genotype (DWV-B) is more virulent than the established DWV genotype (DWV-A) and is widespread in the landscape. Furthermore, we show in a simple model that colonies infected with DWV-B collapse sooner than colonies infected with DWV-A. We also identify potential for rapid DWV evolution by revealing extensive genome-wide recombination in vivo. The emergence of DWV-B in naive honeybee populations, including via recombination with DWV-A, could be of significant ecological and economic importance. Our findings emphasize that knowledge of pathogen genetic identity and diversity is critical to understanding drivers of species decline.}, author = {Mcmahon, Dino and Natsopoulou, Myrsini and Doublet, Vincent and Fürst, Matthias and Weging, Silvio and Brown, Mark and Gogol Döring, Andreas and Paxton, Robert}, journal = {Proceedings of the Royal Society of London Series B Biological Sciences}, number = {1833}, publisher = {Royal Society, The}, title = {{Elevated virulence of an emerging viral genotype as a driver of honeybee loss}}, doi = {10.1098/rspb.2016.0811}, volume = {283}, year = {2016}, } @article{1263, abstract = {Linking classical microwave electrical circuits to the optical telecommunication band is at the core of modern communication. Future quantum information networks will require coherent microwave-to-optical conversion to link electronic quantum processors and memories via low-loss optical telecommunication networks. Efficient conversion can be achieved with electro-optical modulators operating at the single microwave photon level. In the standard electro-optic modulation scheme, this is impossible because both up- and down-converted sidebands are necessarily present. Here, we demonstrate true single-sideband up- or down-conversion in a triply resonant whispering gallery mode resonator by explicitly addressing modes with asymmetric free spectral range. Compared to previous experiments, we show a 3 orders of magnitude improvement of the electro-optical conversion efficiency, reaching 0.1% photon number conversion for a 10 GHz microwave tone at 0.42 mW of optical pump power. The presented scheme is fully compatible with existing superconducting 3D circuit quantum electrodynamics technology and can be used for nonclassical state conversion and communication. Our conversion bandwidth is larger than 1 MHz and is not fundamentally limited.}, author = {Rueda, Alfredo and Sedlmeir, Florian and Collodo, Michele and Vogl, Ulrich and Stiller, Birgit and Schunk, Gerhard and Strekalov, Dmitry and Marquardt, Christoph and Fink, Johannes M and Painter, Oskar and Leuchs, Gerd and Schwefel, Harald}, journal = {Optica}, number = {6}, pages = {597 -- 604}, publisher = {Optica Publishing Group}, title = {{Efficient microwave to optical photon conversion: An electro-optical realization}}, doi = {10.1364/OPTICA.3.000597}, volume = {3}, year = {2016}, } @article{1264, abstract = {n contrast with the wealth of recent reports about the function of μ-adaptins and clathrin adaptor protein (AP) complexes, there is very little information about the motifs that determine the sorting of membrane proteins within clathrin-coated vesicles in plants. Here, we investigated putative sorting signals in the large cytosolic loop of the Arabidopsis (Arabidopsis thaliana) PIN-FORMED1 (PIN1) auxin transporter, which are involved in binding μ-adaptins and thus in PIN1 trafficking and localization. We found that Phe-165 and Tyr-280, Tyr-328, and Tyr-394 are involved in the binding of different μ-adaptins in vitro. However, only Phe-165, which binds μA(μ2)- and μD(μ3)-adaptin, was found to be essential for PIN1 trafficking and localization in vivo. The PIN1:GFP-F165A mutant showed reduced endocytosis but also localized to intracellular structures containing several layers of membranes and endoplasmic reticulum (ER) markers, suggesting that they correspond to ER or ER-derived membranes. While PIN1:GFP localized normally in a μA (μ2)-adaptin mutant, it accumulated in big intracellular structures containing LysoTracker in a μD (μ3)-adaptin mutant, consistent with previous results obtained with mutants of other subunits of the AP-3 complex. Our data suggest that Phe-165, through the binding of μA (μ2)- and μD (μ3)-adaptin, is important for PIN1 endocytosis and for PIN1 trafficking along the secretory pathway, respectively.}, author = {Sancho Andrés, Gloria and Soriano Ortega, Esther and Gao, Caiji and Bernabé Orts, Joan and Narasimhan, Madhumitha and Müller, Anna and Tejos, Ricardo and Jiang, Liwen and Friml, Jirí and Aniento, Fernando and Marcote, Maria}, journal = {Plant Physiology}, number = {3}, pages = {1965 -- 1982}, publisher = {American Society of Plant Biologists}, title = {{Sorting motifs involved in the trafficking and localization of the PIN1 auxin efflux carrier}}, doi = {10.1104/pp.16.00373}, volume = {171}, year = {2016}, } @article{1265, abstract = {Extracellular matrices (ECMs) are central to the advent of multicellular life, and their mechanical propertiesare modulated by and impinge on intracellular signaling pathways that regulate vital cellular functions. High spatial-resolution mapping of mechanical properties in live cells is, however, extremely challenging. Thus, our understanding of how signaling pathways process physiological signals to generate appropriate mechanical responses is limited. We introduce fluorescence emission-Brillouin scattering imaging (FBi), a method for the parallel and all-optical measurements of mechanical properties and fluorescence at the submicrometer scale in living organisms. Using FBi, we showed thatchanges in cellular hydrostatic pressure and cytoplasm viscoelasticity modulate the mechanical signatures of plant ECMs. We further established that the measured "stiffness" of plant ECMs is symmetrically patternedin hypocotyl cells undergoing directional growth. Finally, application of this method to Arabidopsis thaliana with photoreceptor mutants revealed that red and far-red light signals are essential modulators of ECM viscoelasticity. By mapping the viscoelastic signatures of a complex ECM, we provide proof of principlefor the organism-wide applicability of FBi for measuring the mechanical outputs of intracellular signaling pathways. As such, our work has implications for investigations of mechanosignaling pathways and developmental biology.}, author = {Elsayad, Kareem and Werner, Stephanie and Gallemi Rovira, Marcal and Kong, Jixiang and Guajardo, Edmundo and Zhang, Lijuan and Jaillais, Yvon and Greb, Thomas and Belkhadir, Youssef}, journal = {Science Signaling}, number = {435}, publisher = {American Association for the Advancement of Science}, title = {{Mapping the subcellular mechanical properties of live cells in tissues with fluorescence emission-Brillouin imaging}}, doi = {10.1126/scisignal.aaf6326}, volume = {9}, year = {2016}, } @article{1266, abstract = {Cortical networks exhibit ‘global oscillations’, in which neural spike times are entrained to an underlying oscillatory rhythm, but where individual neurons fire irregularly, on only a fraction of cycles. While the network dynamics underlying global oscillations have been well characterised, their function is debated. Here, we show that such global oscillations are a direct consequence of optimal efficient coding in spiking networks with synaptic delays and noise. To avoid firing unnecessary spikes, neurons need to share information about the network state. Ideally, membrane potentials should be strongly correlated and reflect a ‘prediction error’ while the spikes themselves are uncorrelated and occur rarely. We show that the most efficient representation is when: (i) spike times are entrained to a global Gamma rhythm (implying a consistent representation of the error); but (ii) few neurons fire on each cycle (implying high efficiency), while (iii) excitation and inhibition are tightly balanced. This suggests that cortical networks exhibiting such dynamics are tuned to achieve a maximally efficient population code.}, author = {Chalk, Matthew J and Gutkin, Boris and Denève, Sophie}, journal = {eLife}, number = {2016JULY}, publisher = {eLife Sciences Publications}, title = {{Neural oscillations as a signature of efficient coding in the presence of synaptic delays}}, doi = {10.7554/eLife.13824}, volume = {5}, year = {2016}, } @article{1267, abstract = {We give a simplified proof of the nonexistence of large nuclei in the liquid drop model and provide an explicit bound. Our bound is within a factor of 2.3 of the conjectured value and seems to be the first quantitative result.}, author = {Frank, Rupert and Killip, Rowan and Nam, Phan}, journal = {Letters in Mathematical Physics}, number = {8}, pages = {1033 -- 1036}, publisher = {Springer}, title = {{Nonexistence of large nuclei in the liquid drop model}}, doi = {10.1007/s11005-016-0860-8}, volume = {106}, year = {2016}, } @article{1268, author = {Milutinovic, Barbara and Kurtz, Joachim}, journal = {Seminars in Immunology}, number = {4}, pages = {328 -- 342}, publisher = {Academic Press}, title = {{Immune memory in invertebrates}}, doi = {10.1016/j.smim.2016.05.004}, volume = {28}, year = {2016}, } @article{1269, abstract = {Plants are continuously exposed to a myriad of external signals such as fluctuating nutrients availability, drought, heat, cold, high salinity, or pathogen/pest attacks that can severely affect their development, growth, and fertility. As sessile organisms, plants must therefore be able to sense and rapidly react to these external inputs, activate efficient responses, and adjust development to changing conditions. In recent years, significant progress has been made towards understanding the molecular mechanisms underlying the intricate and complex communication between plants and the environment. It is now becoming increasingly evident that hormones have an important regulatory role in plant adaptation and defense mechanisms.}, author = {Benková, Eva}, journal = {Plant Molecular Biology}, number = {6}, pages = {597}, publisher = {Springer}, title = {{Plant hormones in interactions with the environment}}, doi = {10.1007/s11103-016-0501-8}, volume = {91}, year = {2016}, } @article{1270, abstract = {A crucial step in the early development of multicellular organisms involves the establishment of spatial patterns of gene expression which later direct proliferating cells to take on different cell fates. These patterns enable the cells to infer their global position within a tissue or an organism by reading out local gene expression levels. The patterning system is thus said to encode positional information, a concept that was formalized recently in the framework of information theory. Here we introduce a toy model of patterning in one spatial dimension, which can be seen as an extension of Wolpert's paradigmatic "French Flag" model, to patterning by several interacting, spatially coupled genes subject to intrinsic and extrinsic noise. Our model, a variant of an Ising spin system, allows us to systematically explore expression patterns that optimally encode positional information. We find that optimal patterning systems use positional cues, as in the French Flag model, together with gene-gene interactions to generate combinatorial codes for position which we call "Counter" patterns. Counter patterns can also be stabilized against noise and variations in system size or morphogen dosage by longer-range spatial interactions of the type invoked in the Turing model. The simple setup proposed here qualitatively captures many of the experimentally observed properties of biological patterning systems and allows them to be studied in a single, theoretically consistent framework.}, author = {Hillenbrand, Patrick and Gerland, Ulrich and Tkacik, Gasper}, journal = {PLoS One}, number = {9}, publisher = {Public Library of Science}, title = {{Beyond the French flag model: Exploiting spatial and gene regulatory interactions for positional information}}, doi = {10.1371/journal.pone.0163628}, volume = {11}, year = {2016}, } @article{1271, abstract = {Background: High directional persistence is often assumed to enhance the efficiency of chemotactic migration. Yet, cells in vivo usually display meandering trajectories with relatively low directional persistence, and the control and function of directional persistence during cell migration in three-dimensional environments are poorly understood. Results: Here, we use mesendoderm progenitors migrating during zebrafish gastrulation as a model system to investigate the control of directional persistence during migration in vivo. We show that progenitor cells alternate persistent run phases with tumble phases that result in cell reorientation. Runs are characterized by the formation of directed actin-rich protrusions and tumbles by enhanced blebbing. Increasing the proportion of actin-rich protrusions or blebs leads to longer or shorter run phases, respectively. Importantly, both reducing and increasing run phases result in larger spatial dispersion of the cells, indicative of reduced migration precision. A physical model quantitatively recapitulating the migratory behavior of mesendoderm progenitors indicates that the ratio of tumbling to run times, and thus the specific degree of directional persistence of migration, are critical for optimizing migration precision. Conclusions: Together, our experiments and model provide mechanistic insight into the control of migration directionality for cells moving in three-dimensional environments that combine different protrusion types, whereby the proportion of blebs to actin-rich protrusions determines the directional persistence and precision of movement by regulating the ratio of tumbling to run times.}, author = {Diz Muñoz, Alba and Romanczuk, Pawel and Yu, Weimiao and Bergert, Martin and Ivanovitch, Kenzo and Salbreux, Guillame and Heisenberg, Carl-Philipp J and Paluch, Ewa}, journal = {BMC Biology}, number = {1}, publisher = {BioMed Central}, title = {{Steering cell migration by alternating blebs and actin-rich protrusions}}, doi = {10.1186/s12915-016-0294-x}, volume = {14}, year = {2016}, } @article{1272, abstract = {We study different means to extend offsetting based on skeletal structures beyond the well-known constant-radius and mitered offsets supported by Voronoi diagrams and straight skeletons, for which the orthogonal distance of offset elements to their respective input elements is constant and uniform over all input elements. Our main contribution is a new geometric structure, called variable-radius Voronoi diagram, which supports the computation of variable-radius offsets, i.e., offsets whose distance to the input is allowed to vary along the input. We discuss properties of this structure and sketch a prototype implementation that supports the computation of variable-radius offsets based on this new variant of Voronoi diagrams.}, author = {Held, Martin and Huber, Stefan and Palfrader, Peter}, journal = {Computer-Aided Design and Applications}, number = {5}, pages = {712 -- 721}, publisher = {Taylor and Francis}, title = {{Generalized offsetting of planar structures using skeletons}}, doi = {10.1080/16864360.2016.1150718}, volume = {13}, year = {2016}, } @article{1273, abstract = {Lateral root primordia (LRP) originate from pericycle stem cells located deep within parental root tissues. LRP emerge through overlying root tissues by inducing auxin-dependent cell separation and hydraulic changes in adjacent cells. The auxin-inducible auxin influx carrier LAX3 plays a key role concentrating this signal in cells overlying LRP. Delimiting LAX3 expression to two adjacent cell files overlying new LRP is crucial to ensure that auxin-regulated cell separation occurs solely along their shared walls. Multiscale modeling has predicted that this highly focused pattern of expression requires auxin to sequentially induce auxin efflux and influx carriers PIN3 and LAX3, respectively. Consistent with model predictions, we report that auxin-inducible LAX3 expression is regulated indirectly by AUXIN RESPONSE FACTOR 7 (ARF7). Yeast one-hybrid screens revealed that the LAX3 promoter is bound by the transcription factor LBD29, which is a direct target for regulation by ARF7. Disrupting auxin-inducible LBD29 expression or expressing an LBD29-SRDX transcriptional repressor phenocopied the lax3 mutant, resulting in delayed lateral root emergence. We conclude that sequential LBD29 and LAX3 induction by auxin is required to coordinate cell separation and organ emergence.}, author = {Porco, Silvana and Larrieu, Antoine and Du, Yujuan and Gaudinier, Allison and Goh, Tatsuaki and Swarup, Kamal and Swarup, Ranjan and Kuempers, Britta and Bishopp, Anthony and Lavenus, Julien and Casimiro, Ilda and Hill, Kristine and Benková, Eva and Fukaki, Hidehiro and Brady, Siobhan and Scheres, Ben and Peéet, Benjamin and Bennett, Malcolm}, journal = {Development}, number = {18}, pages = {3340 -- 3349}, publisher = {Company of Biologists}, title = {{Lateral root emergence in Arabidopsis is dependent on transcription factor LBD29 regulation of auxin influx carrier LAX3}}, doi = {10.1242/dev.136283}, volume = {143}, year = {2016}, } @article{1274, abstract = {Synchronized tissue polarization during regeneration or de novo vascular tissue formation is a plant-specific example of intercellular communication and coordinated development. According to the canalization hypothesis, the plant hormone auxin serves as polarizing signal that mediates directional channel formation underlying the spatio-temporal vasculature patterning. A necessary part of canalization is a positive feedback between auxin signaling and polarity of the intercellular auxin flow. The cellular and molecular mechanisms of this process are still poorly understood, not the least, because of a lack of a suitable model system. We show that the main genetic model plant, Arabidopsis (Arabidopsis thaliana) can be used to study the canalization during vascular cambium regeneration and new vasculature formation. We monitored localized auxin responses, directional auxin-transport channels formation, and establishment of new vascular cambium polarity during regenerative processes after stem wounding. The increased auxin response above and around the wound preceded the formation of PIN1 auxin transporter-marked channels from the primarily homogenous tissue and the transient, gradual changes in PIN1 localization preceded the polarity of newly formed vascular tissue. Thus, Arabidopsis is a useful model for studies of coordinated tissue polarization and vasculature formation after wounding allowing for genetic and mechanistic dissection of the canalization hypothesis.}, author = {Mazur, Ewa and Benková, Eva and Friml, Jirí}, journal = {Scientific Reports}, publisher = {Nature Publishing Group}, title = {{Vascular cambium regeneration and vessel formation in wounded inflorescence stems of Arabidopsis}}, doi = {10.1038/srep33754}, volume = {6}, year = {2016}, } @article{1275, author = {Callan Jones, Andrew and Ruprecht, Verena and Wieser, Stefan and Heisenberg, Carl-Philipp J and Voituriez, Raphaël}, journal = {Physical Review Letters}, number = {13}, publisher = {American Physical Society}, title = {{Callan-Jones et al. Reply}}, doi = {10.1103/PhysRevLett.117.139802}, volume = {117}, year = {2016}, }