@inproceedings{4380, abstract = {Cloud computing is an emerging paradigm aimed to offer users pay-per-use computing resources, while leaving the burden of managing the computing infrastructure to the cloud provider. We present a new programming and pricing model that gives the cloud user the flexibility of trading execution speed and price on a per-job basis. We discuss the scheduling and resource management challenges for the cloud provider that arise in the implementation of this model. We argue that techniques from real-time and embedded software can be useful in this context.}, author = {Henzinger, Thomas A and Tomar, Anmol and Singh, Vasu and Wies, Thomas and Zufferey, Damien}, location = {Arizona, USA}, pages = {1 -- 8}, publisher = {ACM}, title = {{A marketplace for cloud resources}}, doi = {10.1145/1879021.1879022}, year = {2010}, } @inproceedings{4381, abstract = {Cloud computing aims to give users virtually unlimited pay-per-use computing resources without the burden of managing the underlying infrastructure. We claim that, in order to realize the full potential of cloud computing, the user must be presented with a pricing model that offers flexibility at the requirements level, such as a choice between different degrees of execution speed and the cloud provider must be presented with a programming model that offers flexibility at the execution level, such as a choice between different scheduling policies. In such a flexible framework, with each job, the user purchases a virtual computer with the desired speed and cost characteristics, and the cloud provider can optimize the utilization of resources across a stream of jobs from different users. We designed a flexible framework to test our hypothesis, which is called FlexPRICE (Flexible Provisioning of Resources in a Cloud Environment) and works as follows. A user presents a job to the cloud. The cloud finds different schedules to execute the job and presents a set of quotes to the user in terms of price and duration for the execution. The user then chooses a particular quote and the cloud is obliged to execute the job according to the chosen quote. FlexPRICE thus hides the complexity of the actual scheduling decisions from the user, but still provides enough flexibility to meet the users actual demands. We implemented FlexPRICE in a simulator called PRICES that allows us to experiment with our framework. We observe that FlexPRICE provides a wide range of execution options-from fast and expensive to slow and cheap-- for the whole spectrum of data-intensive and computation-intensive jobs. We also observe that the set of quotes computed by FlexPRICE do not vary as the number of simultaneous jobs increases.}, author = {Henzinger, Thomas A and Tomar, Anmol and Singh, Vasu and Wies, Thomas and Zufferey, Damien}, location = {Miami, USA}, pages = {83 -- 90}, publisher = {IEEE}, title = {{FlexPRICE: Flexible provisioning of resources in a cloud environment}}, doi = {10.1109/CLOUD.2010.71}, year = {2010}, } @inproceedings{4382, abstract = {Transactional memory (TM) has shown potential to simplify the task of writing concurrent programs. Inspired by classical work on databases, formal definitions of the semantics of TM executions have been proposed. Many of these definitions assumed that accesses to shared data are solely performed through transactions. In practice, due to legacy code and concurrency libraries, transactions in a TM have to share data with non-transactional operations. The semantics of such interaction, while widely discussed by practitioners, lacks a clear formal specification. Those interactions can vary, sometimes in subtle ways, between TM implementations and underlying memory models. We propose a correctness condition for TMs, parametrized opacity, to formally capture the now folklore notion of strong atomicity by stipulating the two following intuitive requirements: first, every transaction appears as if it is executed instantaneously with respect to other transactions and non-transactional operations, and second, non-transactional operations conform to the given underlying memory model. We investigate the inherent cost of implementing parametrized opacity. We first prove that parametrized opacity requires either instrumenting non-transactional operations (for most memory models) or writing to memory by transactions using potentially expensive read-modify-write instructions (such as compare-and-swap). Then, we show that for a class of practical relaxed memory models, parametrized opacity can indeed be implemented with constant-time instrumentation of non-transactional writes and no instrumentation of non-transactional reads. We show that, in practice, parametrizing the notion of correctness allows developing more efficient TM implementations.}, author = {Guerraoui, Rachid and Henzinger, Thomas A and Kapalka, Michal and Singh, Vasu}, location = {Santorini, Greece}, pages = {263 -- 272}, publisher = {ACM}, title = {{Transactions in the jungle}}, doi = {10.1145/1810479.1810529}, year = {2010}, } @inproceedings{4388, abstract = {GIST is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with ω-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Jobstmann, Barbara and Radhakrishna, Arjun}, location = {Edinburgh, UK}, pages = {665 -- 669}, publisher = {Springer}, title = {{GIST: A solver for probabilistic games}}, doi = {10.1007/978-3-642-14295-6_57}, volume = {6174}, year = {2010}, } @inproceedings{4389, abstract = {Digital components play a central role in the design of complex embedded systems. These components are interconnected with other, possibly analog, devices and the physical environment. This environment cannot be entirely captured and can provide inaccurate input data to the component. It is thus important for digital components to have a robust behavior, i.e. the presence of a small change in the input sequences should not result in a drastic change in the output sequences. In this paper, we study a notion of robustness for sequential circuits. However, since sequential circuits may have parts that are naturally discontinuous (e.g., digital controllers with switching behavior), we need a flexible framework that accommodates this fact and leaves discontinuous parts of the circuit out from the robustness analysis. As a consequence, we consider sequential circuits that have their input variables partitioned into two disjoint sets: control and disturbance variables. Our contributions are (1) a definition of robustness for sequential circuits as a form of continuity with respect to disturbance variables, (2) the characterization of the exact class of sequential circuits that are robust according to our definition, (3) an algorithm to decide whether a sequential circuit is robust or not.}, author = {Doyen, Laurent and Henzinger, Thomas A and Legay, Axel and Nickovic, Dejan}, pages = {77 -- 84}, publisher = {IEEE}, title = {{Robustness of sequential circuits}}, doi = {10.1109/ACSD.2010.26}, year = {2010}, } @inproceedings{4390, abstract = {Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.}, author = {Cerny, Pavol and Radhakrishna, Arjun and Zufferey, Damien and Chaudhuri, Swarat and Alur, Rajeev}, location = {Edinburgh, UK}, pages = {465 -- 479}, publisher = {Springer}, title = {{Model checking of linearizability of concurrent list implementations}}, doi = {10.1007/978-3-642-14295-6_41}, volume = {6174}, year = {2010}, } @inbook{4392, abstract = {While a boolean notion of correctness is given by a preorder on systems and properties, a quantitative notion of correctness is defined by a distance function on systems and properties, where the distance between a system and a property provides a measure of “fit” or “desirability.” In this article, we explore several ways how the simulation preorder can be generalized to a distance function. This is done by equipping the classical simulation game between a system and a property with quantitative objectives. In particular, for systems that satisfy a property, a quantitative simulation game can measure the “robustness” of the satisfaction, that is, how much the system can deviate from its nominal behavior while still satisfying the property. For systems that violate a property, a quantitative simulation game can measure the “seriousness” of the violation, that is, how much the property has to be modified so that it is satisfied by the system. These distances can be computed in polynomial time, since the computation reduces to the value problem in limit average games with constant weights. Finally, we demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes. }, author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun}, booktitle = {Time For Verification: Essays in Memory of Amir Pnueli}, editor = {Manna, Zohar and Peled, Doron}, pages = {42 -- 60}, publisher = {Springer}, title = {{Quantitative Simulation Games}}, doi = {10.1007/978-3-642-13754-9_3}, volume = {6200}, year = {2010}, } @inproceedings{4393, abstract = {Boolean notions of correctness are formalized by preorders on systems. Quantitative measures of correctness can be formalized by real-valued distance functions between systems, where the distance between implementation and specification provides a measure of “fit” or “desirability.” We extend the simulation preorder to the quantitative setting, by making each player of a simulation game pay a certain price for her choices. We use the resulting games with quantitative objectives to define three different simulation distances. The correctness distance measures how much the specification must be changed in order to be satisfied by the implementation. The coverage distance measures how much the implementation restricts the degrees of freedom offered by the specification. The robustness distance measures how much a system can deviate from the implementation description without violating the specification. We consider these distances for safety as well as liveness specifications. The distances can be computed in polynomial time for safety specifications, and for liveness specifications given by weak fairness constraints. We show that the distance functions satisfy the triangle inequality, that the distance between two systems does not increase under parallel composition with a third system, and that the distance between two systems can be bounded from above and below by distances between abstractions of the two systems. These properties suggest that our simulation distances provide an appropriate basis for a quantitative theory of discrete systems. We also demonstrate how the robustness distance can be used to measure how many transmission errors are tolerated by error correcting codes.}, author = {Cerny, Pavol and Henzinger, Thomas A and Radhakrishna, Arjun}, location = {Paris, France}, pages = {235 -- 268}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Simulation distances}}, doi = {10.1007/978-3-642-15375-4_18}, volume = {6269}, year = {2010}, } @inproceedings{4395, abstract = {The problem of locally transforming or translating programs without altering their semantics is central to the construction of correct compilers. For concurrent shared-memory programs this task is challenging because (1) concurrent threads can observe transformations that would be undetectable in a sequential program, and (2) contemporary multiprocessors commonly use relaxed memory models that complicate the reasoning. In this paper, we present a novel proof methodology for verifying that a local program transformation is sound with respect to a specific hardware memory model, in the sense that it is not observable in any context. The methodology is based on a structural induction and relies on a novel compositional denotational semantics for relaxed memory models that formalizes (1) the behaviors of program fragments as a set of traces, and (2) the effect of memory model relaxations as local trace rewrite operations. To apply this methodology in practice, we implemented a semi- automated tool called Traver and used it to verify/falsify several compiler transformations for a number of different hardware memory models.}, author = {Burckhardt, Sebastian and Musuvathi, Madanlal and Singh, Vasu}, editor = {Gupta, Rajiv}, location = {Pahos, Cyprus}, pages = {104 -- 123}, publisher = {Springer}, title = {{Verifying local transformations on relaxed memory models}}, doi = {10.1007/978-3-642-11970-5_7}, volume = {6011}, year = {2010}, } @inproceedings{4396, abstract = {Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.}, author = {Beyer, Dirk and Henzinger, Thomas A and Théoduloz, Grégory and Zufferey, Damien}, editor = {Rosenblum, David and Taenzer, Gabriele}, location = {Paphos, Cyprus}, pages = {263 -- 277}, publisher = {Springer}, title = {{Shape refinement through explicit heap analysis}}, doi = {10.1007/978-3-642-12029-9_19}, volume = {6013}, year = {2010}, } @article{2498, abstract = {Activation of G protein-gated inwardly-rectifying K+ (GIRK or Kir3) channels by metabotropic gamma-aminobutyric acid (B) (GABAB) receptors is an essential signalling pathway controlling neuronal excitability and synaptic transmission in the brain. To investigate the relationship between GIRK channel subunits and GABAB receptors in cerebellar Purkinje cells at post- and pre-synaptic sites, we used biochemical, functional and immunohistochemical techniques. Co-immunoprecipitation analysis demonstrated that GIRK subunits are co-assembled with GABAB receptors in the cerebellum. Immunoelectron microscopy showed that the subunit composition of GIRK channels in Purkinje cell spines is compartment-dependent. Thus, at extrasynaptic sites GIRK channels are formed by GIRK1/GIRK2/GIRK3, post-synaptic densities contain GIRK2/GIRK3 and dendritic shafts contain GIRK1/GIRK3. The post-synaptic association of GIRK subunits with GABAB receptors in Purkinje cells is supported by the subcellular regulation of the ion channel and the receptor in mutant mice. At pre-synaptic sites, GIRK channels localized to parallel fibre terminals are formed by GIRK1/GIRK2/GIRK3 and co-localize with GABAB receptors. Consistent with this morphological evidence we demonstrate their functional interaction at axon terminals in the cerebellum by showing that GIRK channels play a role in the inhibition of glutamate release by GABAB receptors. The association of GIRK channels and GABA B receptors with excitatory synapses at both post- and pre-synaptic sites indicates their intimate involvement in the modulation of glutamatergic neurotransmission in the cerebellum.}, author = {Fernández-Alacid, Laura and Aguado, Carolina and Ciruela, Francisco and Martín, Ricardo J and Colón, José and Cabañero, María José and Gassmann, Martin and Watanabe, Masahiko and Ryuichi Shigemoto and Wickman, Kevin D and Bettler, Bernhard and Sánchez-Prieto, José and Luján, Rafael}, journal = {Journal of Neurochemistry}, number = {4}, pages = {1363 -- 1376}, publisher = {Wiley-Blackwell}, title = {{ Subcellular compartment-specific molecular diversity of pre- and post-synaptic GABAB-activated GIRK channels in Purkinje cells}}, doi = {10.1111/j.1471-4159.2009.06229.x}, volume = {110}, year = {2009}, } @article{2499, abstract = {G protein-coupled receptors (GPCRs) have critical functions in intercellular communication. Although a wide range of different receptors have been identified in the same cells, the mechanism by which signals are integrated remains elusive. The ability of GPCRs to form dimers or larger hetero-oligomers is thought to generate such signal integration. We examined the molecular mechanisms responsible for the GABAB receptor-mediated potentiation of the mGlu receptor signalling reported in Purkinje neurons. We showed that this effect does not require a physical interaction between both receptors. Instead, it is the result of a more general mechanism in which the βγ subunits produced by the Gi-coupled GABAB receptor enhance the mGlu-mediated Gq response. Most importantly, this mechanism could be generally applied to other pairs of Gi- and Gq-coupled receptors and the signal integration varied depending on the time delay between activation of each receptor. Such a mechanism helps explain specific properties of cells expressing two different Gi- and Gq-coupled receptors activated by a single transmitter, or properties of GPCRs naturally coupled to both types of the G protein.}, author = {Rives, Marie L and Vol, Claire and Fukazawa, Yugo and Tinel, Norbert and Trinquet, Eric and Ayoub, Mohammed A and Ryuichi Shigemoto and Pin, Jean-Philippe and Prezèau, Laurent}, journal = {EMBO Journal}, number = {15}, pages = {2195 -- 2208}, publisher = {Wiley-Blackwell}, title = {{Crosstalk between GABAB and mGlu1a receptors reveals new insight into GPCR signal integration}}, doi = {10.1038/emboj.2009.177}, volume = {28}, year = {2009}, } @article{2500, abstract = {To examine the intrasynaptic arrangement of postsynaptic receptors in relation to the functional role of the synapse,we quantitatively analyzed the two-dimensional distribution of AMPA and NMDA receptors (AMPARs and NMDARs, respectively) using SDS-digested freeze-fracture replica labeling (SDS-FRL) and assessed the implication of distribution differences on the postsynaptic responses by simulation. In the dorsal lateral geniculate nucleus, corticogeniculate (CG) synapses were twice as large as retinogeniculate (RG) synapses but expressed similar numbers of AMPARs. Two-dimensional views of replicas revealed that AMPARs form microclusters in both synapses to a similar extent, resulting in larger AMPAR-lacking areas in the CG synapses. Despite the broad difference in the AMPAR distribution within a synapse, our simulations based on the actual receptor distributions suggested that the AMPAR quantal response at individual RG synapses is only slightly larger in amplitude, less variable, and faster in kinetics than that at CG synapses having a similar number of the receptors. NMDARs at the CG synapses were expressed twice as many as those in the RG synapses. Electrophysiological recordings confirmed a larger contribution of NMDAR relative to AMPAR-mediated responses in CG synapses. We conclude that synapse size and the density and distribution of receptors have minor influences on quantal responses and that the number of receptors acts as a predominant postsynaptic determinant of the synaptic strength mediated by both the AMPARs and NMDARs. }, author = {Tarusawa, Etsuko and Matsui, Ko and Budisantoso, Timotheus and Molnár, Elek and Watanabe, Masahiko and Matsui, Minoru and Fukazawa, Yugo and Ryuichi Shigemoto}, journal = {Journal of Neuroscience}, number = {41}, pages = {12896 -- 12908}, publisher = {Society for Neuroscience}, title = {{Input-specific intrasynaptic arrangements of ionotropic glutamate receptors and their impact on postsynaptic responses}}, doi = {10.1523/JNEUROSCI.6160-08.2009}, volume = {29}, year = {2009}, } @article{2501, abstract = {The brain-specific immediate early gene Arc/Arg3.1 is induced in response to a variety of stimuli, including sensory and behavior-linked neural activity. Here we report the generation of transgenic mice, termed TgArc/Arg3.1-d4EGFP, expressing a 4-h half-life form of enhanced green fluorescent protein (d4EGFP) under the control of the Arc/Arg3.1 promoter. We show that d4EGFP-mediated fluorescence faithfully reports Arc/Arg3.1 induction in response to physiological, pathological and pharmacological stimuli, and that this fluorescence permits electrical recording from activated neurons in the live mouse. Moreover, the fluorescent Arc/Arg3.1 indicator revealed activity changes in circumscribed brain areas in distinct modes of stress and in a mouse model of Alzheimer's disease. These findings identify the TgArc/Arg3.1-d4EGFP mouse as a versatile tool to monitor Arc/Arg3.1 induction in neural circuits, both in vitro and in vivo.}, author = {Grinevich, Valery V and Kolleker, Alexander and Eliava, Marina I and Takada, Naoki and Takuma, Hiroshi and Fukazawa, Yugo and Ryuichi Shigemoto and Kuhl, Dietmar and Waters, Jack and Seeburg, Peter H and Osten, Pavel}, journal = {Journal of Neuroscience Methods}, number = {1}, pages = {25 -- 36}, publisher = {Elsevier}, title = {{Fluorescent Arc/Arg3.1 indicator mice: A versatile tool to study brain activity changes in vitro and in vivo}}, doi = {10.1016/j.jneumeth.2009.07.015}, volume = {184}, year = {2009}, } @article{2502, abstract = {In order to acquire phase-contrast images with adequate contrast, conventional TEM requires large amount of defocus. Increasing the defocus improves the low-frequency components but attenuates the high-frequency ones. On the other hand, Zernike phase-contrast TEM (ZPC-TEM) can recover low-frequency components without losing the high-frequency ones under in-focus conditions. ZPC-TEM however, has another problem, especially in imaging of complex biological specimens such as cells and tissues; strong halos appear around specimen structures, and these halos hinder the interpretation of images. Due to this problem, the application of ZPC-TEM has been restricted to imaging of smaller particles. In order to improve the halo appearance, we fabricated a new quarter-wave thin film phase-plate with a smaller central hole and tested it on vitreous biological specimens. ZPC-TEM with the new plate could successfully visualize, in in-focus images, the intracellular fine features of cultured cells and brain tissues. This result indicates that reduction of the central hole diameter makes ZPC-TEM applicable on size scales ranging from protein particles to tissue sections. The application of ZPC-TEM to vitreous biological specimens will be a powerful method to advance the new field of imaging science for ultrastructures in close-to-physiological state.}, author = {Fukuda, Yoshiyuki and Fukazawa, Yugo and Danev, Radostin S and Ryuichi Shigemoto and Nagayama, Kuniaki}, journal = {Journal of Structural Biology}, number = {3}, pages = {476 -- 484}, publisher = {Academic Press}, title = {{Tuning of the Zernike phase-plate for visualization of detailed ultrastructure in complex biological specimens}}, doi = {10.1016/j.jsb.2009.08.011}, volume = {168}, year = {2009}, } @article{2680, abstract = {GABA B receptor subtypes are based on the subunit isoforms GABA B1a and GABA B1b, which associate with GABA B2 subunits to form pharmacologically indistinguishable GABA B(1a,2) and GABA B(1b,2) receptors. Studies with mice selectively expressing GABA B1a or GABA B1b subunits revealed that GABA B(1a,2) receptors are more abundant than GABA B(1b,2) receptors at glutamatergic terminals. Accordingly, it was found that GABA B(1a,2) receptors are more efficient than GABA B(1b,2) receptors in inhibiting glutamate release when maximally activated by exogenous application of the agonist baclofen. Here, we used a combination of genetic, ultrastructural and electrophysiological approaches to analyze to what extent GABA B(1a,2) and GABA B(1b,2) receptors inhibit glutamate release in response to physiological activation. We first show that at hippocampal mossy fiber (MF)-CA3 pyramidal neuron synapses more GABA B1a than GABA B1b protein is present at presynaptic sites, consistent with the findings at other glutamatergic synapses. In the presence of baclofen at concentrations ≥1 μM, both GABA B(1a,2) and GABA B(1b,2) receptors contribute to presynaptic inhibition of glutamate release. However, at lower concentrations of baclofen, selectively GABA B(1a,2) receptors contribute to presynaptic inhibition. Remarkably, exclusively GABA B(1a,2) receptors inhibit glutamate release in response to synaptically released GABA. Specifically, we demonstrate that selectively GABA B(1a,2) receptors mediate heterosynaptic depression of MF transmission, a physiological phenomenon involving transsynaptic inhibition of glutamate release via presynaptic GABA B receptors. Our data demonstrate that the difference in GABA B1a and GABA B1b protein levels at MF terminals is sufficient to produce a strictly GABA B1a-specific effect under physiological conditions. This consolidates that the differential subcellular localization of the GABA B1a and GABA B1b proteins is of regulatory relevance. }, author = {Guetg, Nicole and Seddik, Riad and Vigot, Réjan and Tureček, Rostislav and Gassmann, Martin and Vogt, Kaspar E and Bräuner-Osborne, Hans and Ryuichi Shigemoto and Kretz, Oliver and Frotscher, Michael and Kulik, Ákos and Bettler, Bernhard}, journal = {Journal of Neuroscience}, number = {5}, pages = {1414 -- 1423}, publisher = {Society for Neuroscience}, title = {{The GABA B1a isoform mediates heterosynaptic depression at hippocampal mossy fiber synapses}}, doi = {10.1523/JNEUROSCI.3697-08.2009}, volume = {29}, year = {2009}, } @article{2682, abstract = {The living cell imaging using a two-photon microscope using gold nanoplates and nanoparticle aggregates was demonstrated. The dimensions of the nanoplates were determined through scanning electron microscopy (SEM) and atomic force microscopy. The height of a 100 nm base-length nanotriangle was around 10 nm, while the height of 300 nm base-length nanotriangle was around 12 nm. A spectrophotometer was also used to determine the extinction spectra of gold nanoparticle colloids. Two-photon-induced photoluminescence (TPIPL) under far-field excitation was tested for gold nanoplates on a glass substrate using two-photon laser scanning microscopy (TPLSM). It was observed that living-cell microscopic imaging can be carried out with TPIPL from gold nanoplates and aggregated nanosphere. This method provided a platform for developing tools for biological and biomedical studies.}, author = {Jiang, Yuqiang and Horimoto, Noriko N and Imura, Kohei and Matsui, Ko and Ryuichi Shigemoto}, journal = {Advanced Materials}, number = {22}, pages = {2309 -- 2313}, publisher = {Wiley-Blackwell}, title = {{Bioimaging with two-photon-induced luminescence from triangular nanoplates and nanoparticle aggregates of gold}}, doi = {10.1002/adma.200802312}, volume = {21}, year = {2009}, } @article{2683, abstract = {GABAb receptor (GABAbR)-mediated suppression of glutamate release is critical for limiting glutamatergic transmission across the central nervous system (CNS). Here we show that, upon tetanic stimulation of afferents to lateral amygdala, presynaptic GABAbR-mediated inhibition only occurs in glutamatergic inputs to principle neurons (PNs), not to interneurons (INs), despite the presence of GABAbR in terminals to both types of neurons. The selectivity is caused by differential local GABA accumulation; it requires GABA reuptake and parallels distinct spatial distributions of presynaptic GABAbR in terminals to PNs and INs. Moreover, GABAbR-mediated suppression of theta-burst-induced long-term potentiation (LTP) occurs only in the inputs to PNs, not to INs. Thus, target-cell-specific control of glutamate release by presynaptic GABAbR orchestrates the inhibitory dominance inside amygdala and might contribute to prevention of nonadaptive defensive behaviors.}, author = {Pan, Bingxing and Dong, Yu-Lin and Ito, Wataru and Yanagawa, Yuchio and Ryuichi Shigemoto and Morozov, Alexei A}, journal = {Neuron}, number = {6}, pages = {917 -- 929}, publisher = {Elsevier}, title = {{Selective gating of glutamatergic inputs to excitatory neurons of amygdala by presynaptic GABAb receptor}}, doi = {10.1016/j.neuron.2009.01.029}, volume = {61}, year = {2009}, } @article{2684, abstract = {Calcium-activated potassium channels have been shown to be critically involved in neuronal function, but an elucidation of their detailed roles awaits identification of the microdomains where they are located. This study was undertaken to unravel the precise subcellular distribution of the large-conductance calcium-activated potassium channels (called BK, KCa1.1, or Slo1) in the somatodendritic compartment of cerebellar Purkinje cells by means of postembedding immunogold cytochemistry and SDS-digested freeze-fracture replica labeling (SDS-FRL). We found BK channels to be unevenly distributed over the Purkinje cell plasma membrane. At distal dendritic compartments, BK channels were scattered over the plasma membrane of dendritic shafts and spines but absent from postsynaptic densities. At the soma and proximal dendrites, BK channels formed two distinct pools. One pool was scattered over the plasma membrane, whereas the other pool was clustered in plasma membrane domains overlying subsurface cisterns. The labeling density ratio of clustered to scattered channels was about 60:1, established in SDS-FRL. Subsurface cisterns, also called hypolemmal cisterns, are subcompartments of the endoplasmic reticulum likely representing calciosomes that unload and refill Ca2+ independently. Purkinje cell subsurface cisterns are enriched in inositol 1,4,5-triphosphate receptors that mediate the effects of several neurotransmitters, hormones, and growth factors by releasing Ca2+ into the cytosol, generating local Ca2+ sparks. Such increases in cytosolic [Ca2+] may be sufficient for BK channel activation. Clustered BK channels in the plasma membrane may thus participate in building a functional unit (plasmerosome) with the underlying calciosome that contributes significantly to local signaling in Purkinje cells.}, author = {Walter Kaufmann and Ferraguti, Francesco and Fukazawa, Yugo and Kasugai, Yu and Ryuichi Shigemoto and Laake, Petter and Sexton, Joseph A and Ruth, Peter and Wietzorrek, Georg and Knaus, Hans G and Storm, Johan F and Ottersen, Ole P}, journal = {Journal of Comparative Neurology}, number = {2}, pages = {215 -- 230}, publisher = {Wiley-Blackwell}, title = {{Large-conductance calcium-activated potassium channels in Purkinje cell plasma membranes are clustered at sites of hypolemmal microdomains}}, doi = {10.1002/cne.22066}, volume = {515}, year = {2009}, } @article{2685, abstract = {Conduction velocity (CV) of myelinated axons has been shown to be regulated by oligodendrocytes even after myelination has been completed. However, how myelinating oligodendrocytes regulate CV, and what the significance of this regulation is for normal brain function remain unknown. To address these questions, we analyzed a transgenic mouse line harboring extra copies of the myelin proteolipid protein 1 (plp1) gene (plp1tg/- mice) at 2 months of age. At this stage, the plp1tg/- mice have an unaffected myelin structure with a normally appearing ion channel distribution, but the CV in all axonal tracts tested in the CNS is greatly reduced. We also found decreased axonal diameters and slightly abnormal paranodal structures, both of which can be a cause for the reduced CV. Interestingly the plp1tg/- mice showed altered anxiety-like behaviors, reduced prepulse inhibitions, spatial learning deficits and working memory deficit, all of which are schizophrenia-related behaviors. Our results implicate that abnormalities in the neuron-glia interactions at the paranodal junctions can result in reduced CV in the CNS, which then induces behavioral abnormalities related to schizophrenia.}, author = {Tanaka, Hisataka and Ma, Jianmei and Tanaka, Kenji F and Takao, Keizo and Komada, Munekazu and Tanda, Koichi and Suzuki, Ayaka and Ishibashi, Tomoko and Baba, Hiroko and Isa, Tadashi and Ryuichi Shigemoto and Ono, Katsuhiko and Miyakawa, Tsuyoshi and Ikenaka, Kazuhiro}, journal = {Journal of Neuroscience}, number = {26}, pages = {8363 -- 8371}, publisher = {Society for Neuroscience}, title = {{Mice with altered myelin proteolipid protein gene expression display cognitive deficits accompanied by abnormal neuron-glia interactions and decreased conduction velocities}}, doi = {10.1523/JNEUROSCI.3216-08.2009}, volume = {29}, year = {2009}, }