@article{2583, abstract = {Substance P receptor (SPR)-immunoreactive neurons projecting to the periaqueductal gray (PAG) were examined in the rat spinal trigeminal nucleus and spinal cord by a retrograde tracing method combined with immunofluorescence histochemistry. After injection of Fluoro-gold (FG) into the PAG, SPR-immunoreactive neurons labeled with FG were observed mainly in the lateral spinal nucleus and lamina I of the medullary and spinal dorsal horns and additionally in laminae V and X of the spinal cord.}, author = {Li, Jin and Ding, Yu and Xiong, Kang and Li, Ji and Shigemoto, Ryuichi and Mizuno, Noboru}, issn = {0168-0102}, journal = {Neuroscience Research}, number = {3}, pages = {219 -- 225}, publisher = {Elsevier}, title = {{Substance P receptor (NK1)-immunoreactive neurons projecting to the periaqueductal gray: Distribution in the spinal trigeminal nucleus and the spinal cord of the rat}}, doi = {10.1016/S0168-0102(97)00132-6}, volume = {30}, year = {1998}, } @article{2584, abstract = {The distributions of two alternative splicing variants of metabotropic glutamate receptor mGluR7, mGluR7a and mGluR7b, were examined immunohistochemically in the rat and mouse by using variant-specific antibodies raised against C-terminal portions of rat mGluR7a and human mGluR7b. Many regions throughout the central nervous system (CNS) showed mGluR7-like immunoreactivities (LI). The distribution patterns of mGluR7-LI in the rat were substantially the same as those in the mouse, although some species differences were observed in a few regions. Intense mGluR7a-LI was seen in the main and accessory olfactory bulbs, anterior olfactory nucleus, islands of Calleja, superficial layers of the olfactory tubercle, piriform cortex and entorhinal cortex, periamygdaloid cortex, amygdalohippocampal area, hippocampus, layer I of the neocortical regions, globus pallidus, superficial layers of the superior colliculus, locus coeruleus, and superficial layers of the medullary and spinal dorsal horns. The distribution of mGluR7b was more restricted. It was intense in the islands of Calleja, substantia innominata, hippocampus, ventral pallidum, and globus pallidus. The medial habenular nucleus also showed intense mGluR7a-LI in the rat but not in the mouse. For both mGluR7a- and mGluR7b-LI, localization in the active zones of presynaptic axon terminals was confirmed electron microscopically at synapses of both the asymmetrical and symmetrical types. It is noteworthy that mGluR7a-LI is seen preferentially in relay nuclei of the sensory pathways and that both mGluR7a- and mGluR7b-LI are observed not only in presumed glutamatergic axon terminals, but also in non-glutamatergic axon terminals including presumed inhibitory ones. Thus, mGluR7 may play roles not only as an autoreceptor in glutamatergic axon terminals, but also as a presynaptic heteroreceptor in non-glutamatergic axon terminals in various CNS regions.}, author = {Kinoshita, Ayae and Shigemoto, Ryuichi and Ohishi, Hitoshi and Van Der Putten, Herman and Mizuno, Noboru}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {3}, pages = {332 -- 352}, publisher = {Wiley-Blackwell}, title = {{Immunohistochemical localization of metabotropic glutamate receptors, mGluR7a and mGluR7b, in the central nervous system of the adult rat and mouse: A light and electron microscopic study}}, doi = {10.1002/(SICI)1096-9861(19980413)393:3<332::AID-CNE6>3.0.CO;2-2}, volume = {393}, year = {1998}, } @article{2585, abstract = {Localization of metabetropic glutamate receptor subtypes, mGluR1, mGluRlu, mGluR2/3, mGluR4a, mGluR5, mGluR7a, mGluR7b, and mGluR8, was examined in some of the target areas of projection fibers from the main and accessory olfactory bulbs (MOB and AOB) by using subtype-specific antibodies. The superficial layer of the olfactory tubercle and layer Ia of the pitiform cortex, the target areas of MOB, showed marked mGluR1-, mGluR5-, mGluR7a-, and mGluR8-like immunoreactivities (-LI), and rather weak mGluR2/3-LI. The periamygdaloid cortical region including the target areas of both MOB and AOB showed intense mGluR2/3-LI as well as marked mGluRl-, mGluR5-, mGluR7a-, and mGluRS-LI. No significant mGluR1a-, mGluR4a-, or mGluR7b-LI was seen in these regions. After transection of the lateral olfactory tract, mGluR2/3-, mGluR7a-, and mGluR8-LI were reduced markedly in the target regions on the side ipsilateral to the transection; no significant changes were detected in mGluR1- or mGIuR5-LI. Double labeling experiments indicated light and electron microscopically colocalization of mGluR7a- and mGluRS-LI in axon terminals on dendritic shafts of presumed interneurons in the superficial layer of the olfactory tubercle and layer Ia of the piriform cortex. Electron microscopically mGluR2/3-LI was seen in preterminal and terminal portions of axons, whereas mGluR7a- and mGluRS-LI were associated with presynaptic membrane specialization. Immunolabeled axon terminals were filled with round synaptic vesicles and constituted asymmetric synapses with dendritic profiles. The results suggest that glutamate release from axon terminals of projection fibers from MOB and AOB is regulated presynaptically and differentially through mGluR2/3, mGluR7a, and/or mGluRS.}, author = {Wada, Eiki and Shigemoto, Ryuichi and Kinoshita, Ayae and Ohishi, Hitoshi and Mizuno, Noboru}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {4}, pages = {493 -- 504}, publisher = {Wiley-Blackwell}, title = {{Metabotropic glutamate receptor subtypes in axon terminals of projection fibers from the main and accessory olfactory bulbs: A light and electron microscopic immunohistochemical study in the rat}}, doi = {10.1002/(SICI)1096-9861(19980420)393:4<493::AID-CNE8>3.0.CO;2-W}, volume = {393}, year = {1998}, } @article{2586, abstract = {The role of inhibitory Golgi cells in cerebellar function was investigated by selectively ablating Golgi cells expressing human interleukin-2 receptor α subunit in transgenic mice, using the immunotoxin- mediated cell targeting technique. Golgi cell disruption caused severe acute motor disorders. These mice showed gradual recovery but retained a continuing inability to perform compound movements. Optical and electrical recordings combined with immunocytological analysis indicated that elimination of Golgi cells not only reduces GABA-mediated inhibition but also attenuates functional NMDA receptors in granule cells. These results demonstrate that synaptic integration involving both GABA inhibition and NMDA receptor activation is essential for compound motor coordination. Furthermore, this integration can adapt after Golgi cell elimination so as not to evoke overexcitation by the reduction of NMDA receptors.}, author = {Watanabe, Dai and Inokawa, Hitoshi and Hashimoto, Kouichi and Suzuki, Noboru and Kano, Masanobu and Shigemoto, Ryuichi and Hirano, Tomoo and Toyama, Keisuke and Kaneko, Satoshi and Yokoi, Mineto and Moriyoshi, Koki and Suzuki, Misao and Kobayashi, Kazuto and Nagatsu, Toshiharu and Kreitman, Robert and Pastan, Ira and Nakanishi, Shigetada}, issn = {0092-8674}, journal = {Cell}, number = {1}, pages = {17 -- 27}, publisher = {Cell Press}, title = {{Ablation of cerebellar Golgi cells disrupts synaptic integration involving GABA inhibition and NMDA receptor activation in motor coordination}}, doi = {10.1016/S0092-8674(00)81779-1}, volume = {95}, year = {1998}, } @article{2588, abstract = {B-type receptors for the neurotransmitter GABA (γ-aminobutyric acid) inhibit neuronal activity through G-protein-coupled second-messenger systems, which regulate the release of neurotransmitters and the activity of ion channels and adenylyl cyclase. Physiological and biochemical studies show that there are differences in drug efficiencies at different GABA(B) receptors, so it is expected that GABA(B)-receptor (GABA(B)R) subtypes exist. Two GABA(B)-receptor splice variants have been cloned (GABA(B)R1a and GABA(B)R1b), but native GABA(B) receptors and recombinant receptors showed unexplained differences in agonist-binding potencies. Moreover, the activation of presumed effector ion channels in heterologous cells expressing the recombinant receptors proved difficult. Here we describe a new GABA(B) receptor subtype, GABA(B)R2, which does not bind available GABA(B) antagonists with measurable potency. GABA(B)R1a, GABA(B)R1b and GABA(B)R2 alone do not activate Kir3-type potassium channels efficiently, but co- expression of these receptors yields a robust coupling to activation of Kir3 channels. We provide evidence for the assembly of heteromeric GABA(B) receptors in vivo and show that GABA(B)R2 and GABA(B)R1a/b proteins immunoprecipitate and localize together at dendritic spines. The heteromeric receptor complexes exhibit a significant increase in agonist- and partial- agonist-binding potencies as compared with individual receptors and probably represent the predominant native GABA(B) receptor. Heteromeric assembly among G-protein-coupled receptors has not, to our knowledge, been described before. }, author = {Kaupmann, Klemens and Malitschek, Barbara and Schuler, Valérie and Heid, Jacob and Froestl, Wolfgang and Beck, Pascal and Mosbacher, Johannes and Bischoff, Serge and Kulik, Ákos and Shigemoto, Ryuichi and Karschin, Andreas and Bettler, Bernhard}, issn = {0028-0836}, journal = {Nature}, number = {6712}, pages = {683 -- 687}, publisher = {Nature Publishing Group}, title = {{ GABA(B)-receptor subtypes assemble into functional heteromeric complexes}}, doi = {10.1038/25360}, volume = {396}, year = {1998}, } @article{2589, abstract = {Immunoreactivity for the substance P receptor (NK1 receptor) has been investigated by light and electron microscopy in the dorsal vagal complexes of adult rats and cats. The general pattern of NK1 immunoreactivity was similar for both rat and cat. Numerous NK1-immunoreactive neurons were present in the area postrema, the nucleus of the solitary tract, and the dorsal motor nucleus of the vagus nerve. The density of labelled neurons differed between the subnuclei of the nucleus of the solitary tract. Overall, the efferent neurons of the dorsal motor nucleus of the vagus nerve highly expressed NK1 when compared to neurons in the nucleus of the solitary tract. The results are discussed with reference to the viscerotopic organisation of the dorsal vagal complex. Ultrastructural analysis demonstrated that NK1 immunoreactivity was present only at the membrane surface of somatic and dendritic profiles of neurons. No labelling was found in axon terminals, axons, or glial processes. NK1 immunoreactivity, as revealed by a preembedding immunogold technique in serial ultrathin sections; was preferentially located at nonsynaptic sites. A semiquantitative study suggested that the density of NK1 receptors is statistically higher at membrane sites free of any contact (synaptic or not) with axon terminals. The subcellular localisation of NK1 immunoreactivity was similar for neurons of both rat and cat. These results suggest that in the dorsal vagal complex, substance P might act on NK1 receptors through a process of volume transmission.}, author = {Baude, Agnès and Shigemoto, Ryuichi}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {2}, pages = {181 -- 196}, publisher = {Wiley-Blackwell}, title = {{Cellular and subcellular distribution of substance P receptor immunoreactivity in the dorsal vagal complex of the rat and cat: A light and electron microscope study}}, doi = {10.1002/(SICI)1096-9861(19981214)402:2<181::AID-CNE4>3.0.CO;2-B}, volume = {402}, year = {1998}, } @article{2590, abstract = {Unipolar brush cells (UBCs) are a class of small neurons that are densely concentrated in the granular layers of the vestibulocerebellar cortex and dorsal cochlear nucleus. The UBCs form giant synapses with individual mossy fibre rosettes on the dendrioles which make up their brush formations and are provided with numerous, unusual non-synaptic appendages. In accord with the glutamatergic nature of mossy fibres, our previous post-embedding immunocytochemical studies indicated that various ionotropic glutamate receptor subunits are localized at the post-synaptic densities of the giant synapses, whereas the non-synaptic appendages are immunonegative. On the contrary, the metabotropic glutamate receptors mGluR1α and mGluR2/3 are situated at the non-synaptic appendages and are lacking at the post-synaptic densities. Other authors, however, have shown that antibodies to these metabotropic receptors stain both appendages and post-synaptic densities. In the present study, we have re-evaluated the distribution of metabotropic glutamate receptors in the UBCs of the cerebellum and the cochlear nuclear complex by light and electron microscopic pre-embedding immunocytochemistry with subtype-specific antibodies. We confirm that UBCs dendritic brushes are densely immunostained by antibody to mGluR1α particularly in the cerebellum and that antibody to mGluR2/3 labels at least a percentage of the UBC brushes in both the cerebellum and cochlear nuclei. At the ultrastructural level, it appears that mGluR1α and mGluR2/3 immunoreactivities are not associated with the post-synaptic densities of the giant mossy fibre-UBC synapses, but instead are concentrated on the non-synaptic appendages of the cerebellar UBCs. The non-synaptic appendages, therefore, may be an important avenue for regulating the excitability of UBCs and mediating glutamate effects on their still unknown intracellular signal transduction cascades. We also show that the pre-synaptic densities of UBC dendrodendritic junctions are mGluR2/3 positive. As previously demonstrated, antibodies to mGluR1α and mGluR2/3 label subsets of Golgi cells. Antibody to mGluR5 does not stain UBCs in the cerebellum and cochlear nucleus and reveals the somatodendritic compartment of Golgi cells situated in the core of the cerebellar granular layer, whilst cochlear nucleus Golgi cells are mGluR5 negative.}, author = {Jaarsma, Dick and Diño, Maria and Ohishi, Hitoshi and Shigemoto, Ryuichi and Mugnaini, Enrico}, issn = {0300-4864}, journal = {Journal of Neurocytology}, number = {5}, pages = {303 -- 327}, publisher = {Kluwer}, title = {{ Metabotropic glutamate receptors are associated with non-synaptic appendages of unipolar brush cells in rat cerebellar cortex and cochlear nuclear complex}}, doi = {10.1023/A:1006982023657}, volume = {27}, year = {1998}, } @inbook{2695, abstract = {We study a quantum particle in a random potential in two scaling limits: the low density limit (or Boltzman-Grad) and the weak coupling limit. The low density limit is the quantum analogue of the Lorentz gas. In both cases, the phase space density of the quantum evolution defined through the Wigner transform or the Husimi function converges weakly to a linear Boltz-mann equation with collision kernel given by the quantum scattering cross section. }, author = {Erdös, László and Yau, Horng}, booktitle = {Advances in Differential Equations and Mathematical Physics}, issn = {0271-4132}, pages = {137 -- 155}, publisher = {American Mathematical Society}, title = {{Linear Boltzmann equation as scaling limit of quantum Lorentz gas}}, doi = {10.1090/conm/217}, volume = {217}, year = {1998}, } @article{2728, abstract = {We obtain the Lifschitz tail, i.e. the exact low energy asymptotics of the integrated density of states (IDS) of the two-dimensional magnetic Schrödinger operator with a uniform magnetic field and random Poissonian impurities. The single site potential is repulsive and it has a finite but nonzero range. We show that the IDS is a continuous function of the energy at the bottom of the spectrum. This result complements the earlier (nonrigorous) calculations by Brézin, Gross and Itzykson which predict that the IDS is discontinuous at the bottom of the spectrum for zero range (Dirac delta) impurities at low density. We also elucidate the reason behind this apparent controversy. Our methods involve magnetic localization techniques (both in space and energy) in addition to a modified version of the "enlargement of obstacles" method developed by A.-S. Sznitman.}, author = {Erdös, László}, issn = {0044-3719}, journal = {Probability Theory and Related Fields}, number = {3}, pages = {321 -- 371}, publisher = {Springer}, title = {{Lifschitz tail in a magnetic field: The nonclassical regime}}, doi = {10.1007/s004400050193}, volume = {112}, year = {1998}, } @article{11680, abstract = {We present a model for edge updates with restricted randomness in dynamic graph algorithms and a general technique for analyzing the expected running time of an update operation. This model is able to capture the average case in many applications, since (1) it allows restrictions on the set of edges which can be used for insertions and (2) the type (insertion or deletion) of each update operation is arbitrary, i.e., not random. We use our technique to analyze existing and new dynamic algorithms for the following problems: maximum cardinality matching, minimum spanning forest, connectivity, 2-edge connectivity, k -edge connectivity, k -vertex connectivity, and bipartiteness. Given a random graph G with m 0 edges and n vertices and a sequence of l update operations such that the graph contains m i edges after operation i , the expected time for performing the updates for any l is O(llogn+∑li=1n/m−−√i) in the case of minimum spanning forests, connectivity, 2-edge connectivity, and bipartiteness. The expected time per update operation is O(n) in the case of maximum matching. We also give improved bounds for k -edge and k -vertex connectivity. Additionally we give an insertions-only algorithm for maximum cardinality matching with worst-case O(n) amortized time per insertion.}, author = {Alberts, D. and Henzinger, Monika H}, issn = {1432-0541}, journal = {Algorithmica}, keywords = {Dynamic graph algorithm, Average-case analysis, Minimum spanning forest, Connectivity, Bipartiteness, Maximum matching.}, pages = {31--60}, publisher = {Springer Nature}, title = {{Average-case analysis of dynamic graph algorithms}}, doi = {10.1007/pl00009186}, volume = {20}, year = {1998}, } @article{11681, abstract = {We prove lower bounds on the complexity of maintaining fully dynamic k -edge or k -vertex connectivity in plane graphs and in (k-1) -vertex connected graphs. We show an amortized lower bound of Ω (log n / {k (log log n} + log b)) per edge insertion, deletion, or query operation in the cell probe model, where b is the word size of the machine and n is the number of vertices in G . We also show an amortized lower bound of Ω (log n /(log log n + log b)) per operation for fully dynamic planarity testing in embedded graphs. These are the first lower bounds for fully dynamic connectivity problems.}, author = {Henzinger, Monika H and Fredman, M. L.}, issn = {1432-0541}, journal = {Algorithmica}, keywords = {Dynamic planarity testing, Dynamic connectivity testing, Lower bounds, Cell probe model}, number = {3}, pages = {351--362}, publisher = {Springer Nature}, title = {{Lower bounds for fully dynamic connectivity problems in graphs}}, doi = {10.1007/pl00009228}, volume = {22}, year = {1998}, } @inproceedings{11682, abstract = {We consider the parametric minimum spanning tree problem, in which we are given a graph with edge weights that are linear functions of a parameter /spl lambda/ and wish to compute the sequence of minimum spanning trees generated as /spl lambda/ varies. We also consider the kinetic minimum spanning tree problem, in which /spl lambda/ represents time and the graph is subject in addition to changes such as edge insertions, deletions, and modifications of the weight functions as time progresses. We solve both problems in time O(n/sup 2/3/log/sup 4/3/) per combinatorial change in the tree (or randomized O(n/sup 2/3/log/sup 4/3/ n) per change). Our time bounds reduce to O(n/sup 1/2/log/sup 3/2/ n) per change (O(n/sup 1/2/log n) randomized) for planar graphs or other minor-closed families of graphs, and O(n/sup 1/4/log/sup 3/2/ n) per change (O(n/sup 1/4/ log n) randomized) for planar graphs with weight changes but no insertions or deletions.}, author = {Agarwal, P. K. and EppsteinL. J. Guibas, D. and Henzinger, Monika H}, booktitle = {Proceedings of the 39th Annual Symposium on Foundations of Computer Science}, isbn = {0-8186-9172-7}, issn = {0272-5428}, location = {Palo Alto, CA, United States}, pages = {596--605}, title = {{Parametric and kinetic minimum spanning trees}}, doi = {10.1109/SFCS.1998.743510}, year = {1998}, } @article{1954, abstract = { We have examined the effects of heat stress on electron transfer in the thylakoid membrane of an engineered plastid ndh deletion mutant, Δ1, incapable of performing the Ndh-mediated reduction of the plastoquinone pool in the chloroplast. Upon heat stress in the dark, the rate of PSII- independent reduction of PSI after subsequent illumination by far-red light is dramatically enhanced in both Δ1 and a wild-type control plant (WT). In contrast, in the dark, only the WT shows an increase in the reduction state of the plastoquinone pool. We conclude that the heat stress-induced reduction of the intersystem electron transport chain can be mediated by Ndh- independent pathways in the light but that in the dark the dominant pathway for reduction of the plastoquinone pool is catalysed by the Ndh complex. Our results therefore demonstrate a functional role for the Ndh complex in the dark. }, author = {Sazanov, Leonid A and Burrows, Paul and Nixon, Peter}, issn = {0014-5793}, journal = {FEBS Letters}, number = {1}, pages = {115 -- 118}, publisher = {Elsevier}, title = {{The chloroplast Ndh complex mediates the dark reduction of the plastoquinone pool in response to heat stress in tobacco leaves}}, doi = {10.1016/S0014-5793(98)00573-0}, volume = {429}, year = {1998}, } @article{1955, abstract = {The plastid genomes of several plants contain homologues, termed ndh genes, of genes encoding subunits of the NADH:ubiquinone oxidoreductase or complex I of mitochondria and eubacteria. The functional significance of the Ndh proteins in higher plants is uncertain. We show here that tobacco chloroplasts contain a protein complex of 550 kDa consisting of at least three of the ndh gene products: NdhI, NdhJ and NdhK. We have constructed mutant tobacco plants with disrupted ndhC, ndhK and ndhJ plastid genes, indicating that the Ndh complex is dispensible for plant growth under optimal growth conditions. Chlorophyll fluorescence analysis shows that in vivo the Ndh complex catalyses the post-illumination reduction of the plastoquinone pool and in the light optimizes the induction of photosynthesis under conditions of water stress. We conclude that the Ndh complex catalyses the reduction of the plastoquinone pool using stromal reductant and so acts as a respiratory complex. Overall, our data are compatible with the participation of the Ndh complex in cyclic electron flow around the photosystem I complex in the light and possibly in a chloroplast respiratory chain in the dark.}, author = {Burrows, Paul and Sazanov, Leonid A and Sváb, Zóra and Maliga, Pàl and Nixon, Peter}, issn = {0261-4189}, journal = {EMBO Journal}, number = {4}, pages = {868 -- 876}, publisher = {Wiley-Blackwell}, title = {{Identification of a functional respiratory complex in chloroplasts through analysis of tobacco mutants containing disrupted plastid ndh genes}}, doi = {10.1093/emboj/17.4.868}, volume = {17}, year = {1998}, } @article{1956, abstract = { The plastid genomes of several plants contain ndh genes-homologues of genes encoding subunits of the proton-pumping NADH:ubiquinone oxidoreductase, or complex I, involved in respiration in mitochondria and eubacteria. From sequence similarities with these genes, the ndh gene products have been suggested to form a large protein complex (Ndh complex); however, the structure and function of this complex remains to be established. Herein we report the isolation of the Ndh complex from the chloroplasts of the higher plant Pisum sativum. The purification procedure involved selective solubilization of the thylakoid membrane with dodecyl maltoside, followed by two anion-exchange chromatography steps and one size-exclusion chromatography step. The isolated Ndh complex has an apparent total molecular mass of approximately 550 kDa and according to SDS/PAGE consists of at least 16 subunits including NdhA, NdhI, NdhJ, NdhK, and NdhH, which were identified by N-terminal sequencing and immunoblotting. The Ndh complex showed an NADH- and deamino-NADH-specific dehydrogenase activity, characteristic of complex I, when either ferricyanide or the quinones menadione and duroquinone were used as electron acceptors. This study describes the isolation of the chloroplast analogue of the respiratory complex I and provides direct evidence for the function of the plastid Ndh complex as an NADH:plastoquinone oxidoreductase. Our results are compatible with a dual role for the Ndh complex in the chloro-respiratory and cyclic photophosphorylation pathways.}, author = {Sazanov, Leonid A and Burrows, Paul and Nixon, Peter}, issn = {0027-8424}, journal = {PNAS}, number = {3}, pages = {1319 -- 1324}, publisher = {National Academy of Sciences}, title = {{The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes}}, doi = {10.1073/pnas.95.3.1319}, volume = {95}, year = {1998}, } @inproceedings{4603, abstract = {Alternating transition systems are a general model for composite systems which allow the study of collaborative as well as adversarial relationships between individual system components. Unlike in labeled transition systems, where each transition corresponds to a possible step of the system (which may involve some or all components), in alternating transition systems, each transition corresponds to a possible move in a game between the components. In this paper, we study refinement relations between alternating transition systems, such as “Does the implementation refine the set A of specification components without constraining the components not in A?” In particular, we generalize the definitions of the simulation and trace containment preorders from labeled transition systems to alternating transition systems. The generalizations are called alternating simulation and alternating trace containment. Unlike existing refinement relations, they allow the refinement of individual components within the context of a composite system description. We show that, like ordinary simulation, alternating simulation can be checked in polynomial time using a fixpoint computation algorithm. While ordinary trace containment is PSPACE-complete, we establish alternating trace containment to be EXPTIME-complete. Finally, we present logical characterizations for the two preorders in terms of ATL, a temporal logic capable of referring to games between system components.}, author = {Alur, Rajeev and Henzinger, Thomas A and Kupferman, Orna and Vardi, Moshe}, booktitle = {Proceedings of the 9th Interantional Conference on Concurrency Theory}, isbn = {978-3-540-64896-3}, location = {Nice, France}, pages = {163 -- 178}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Alternating refinement relations}}, doi = {10.1007/BFb0055622}, volume = {1466}, year = {1998}, } @inproceedings{4604, author = {Alur, Rajeev and Henzinger, Thomas A and Mang, Freddy and Qadeer, Shaz and Rajamani, Sriram and Tasiran, Serdar}, booktitle = {Proceedings of the 10th International Conference on Computer Aided Verification}, isbn = {9783540646082}, location = {Vancouver, Canada}, pages = {521 -- 525}, publisher = {Springer}, title = {{Mocha: Modularity in model checking}}, doi = {10.1007/BFb0028774}, volume = {1427}, year = {1998}, } @inproceedings{4606, abstract = {In formal design verification, successful model checking is typically preceded by a laborious manual process of constructing design abstractions. We present a methodology for partially—and in some cases, fully—bypassing the abstraction process. For this purpose, we provide to the designer abstraction operators which, if used judiciously in the description of a design, structure the corresponding state space hierarchically. This structure can then be exploited by verification tools, and makes possible the automatic and exhaustive exploration of state spaces that would otherwise be out of scope for existing model checkers. Specifically, we present the following contributions: - A temporal abstraction operator that aggregates transitions and hides intermediate steps. Mathematically, our abstraction operator is a function that maps a flat transition system into a two-level hierarchy where each atomic upper-level transition expands into an entire lower-level transition system. For example, an arithmetic operation may expand into a sequence of bit operations. - A BDD-based algorithm for the symbolic exploration of multi-level hierarchies of transition systems. The algorithm traverses a level-n transition by expanding the corresponding level-(n − 1) transition system on-the-fly. The level-n successors of a state are determined by computing a level-(n − 1) reach set, which is then immediately released from memory. In this fashion, we can exhaustively explore hierarchically structured state spaces whose flat counterparts cause memory overflows. - We experimentally demonstrate the efficiency of our method with three examples—a multiplier, a cache coherence protocol, and a multiprocessor system. In the first two examples, we obtain significant improvements in run times and peak BDD sizes over traditional state-space search. The third example cannot be model checked at all using conventional methods (without manual abstractions), but can be analyzed fully automatically using transition hierarchies.}, author = {Alur, Rajeev and Henzinger, Thomas A and Rajamani, Sriram}, booktitle = {Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783540643562}, location = {Lisbon, Portugal}, pages = {330 -- 344}, publisher = {Springer}, title = {{Symbolic exploration of transition hierarchies}}, doi = {10.1007/BFb0054181}, volume = {1384}, year = {1998}, } @inproceedings{4639, abstract = {An open system can be modeled as a two-player game between the system and its environment. At each round of the game, player 1 (the system) and player 2 (the environment) independently and simultaneously choose moves, and the two choices determine the next state of the game. Properties of open systems can be modeled as objectives of these two-player games. For the basic objective of reachability-can player 1 force the game to a given set of target states?-there are three types of winning states, according to the degree of certainty with which player 1 can reach the target. From type-1 states, player 1 has a deterministic strategy to always reach the target. From type-2 states, player 1 has a randomized strategy to reach the target with probability 1. From type-3 states, player 1 has for every real ε>0 a randomized strategy to reach the target with probability greater than 1-ε. We show that for finite state spaces, all three sets of winning states can be computed in polynomial time: type-1 states in linear time, and type-2 and type-3 states in quadratic time. The algorithms to compute the three sets of winning states also enable the construction of the winning and spoiling strategies. Finally, we apply our results by introducing a temporal logic in which all three kinds of winning conditions can be specified, and which can be model checked in polynomial time. This logic, called Randomized ATL, is suitable for reasoning about randomized behavior in open (two-agent) as well as multi-agent systems}, author = {De Alfaro, Luca and Henzinger, Thomas A and Kupferman, Orna}, booktitle = { Proceedings 39th Annual Symposium on Foundations of Computer Science}, isbn = {0818691727}, location = {Palo Alto, CA, United States of America}, pages = {564 -- 575}, publisher = {IEEE}, title = {{Concurrent reachability games}}, doi = {10.1109/SFCS.1998.743507 }, year = {1998}, } @article{6160, abstract = {Natural isolates of C. elegans exhibit either solitary or social feeding behavior. Solitary foragers move slowly on a bacterial lawn and disperse across it, while social foragers move rapidly on bacteria and aggregate together. A loss-of-function mutation in the npr-1 gene, which encodes a predicted G protein–coupled receptor similar to neuropeptide Y receptors, causes a solitary strain to take on social behavior. Two isoforms of NPR-1 that differ at a single residue occur in the wild. One isoform, NPR-1 215F, is found exclusively in social strains, while the other isoform, NPR-1 215V, is found exclusively in solitary strains. An NPR-1 215V transgene can induce solitary feeding behavior in a wild social strain. Thus, isoforms of a putative neuropeptide receptor generate natural variation in C. elegans feeding behavior.}, author = {de Bono, Mario and Bargmann, Cornelia I}, issn = {0092-8674}, journal = {Cell}, number = {5}, pages = {679--689}, publisher = {Elsevier}, title = {{Natural variation in a neuropeptide Y receptor homolog modifies social behavior and food response in C. elegans}}, doi = {10.1016/s0092-8674(00)81609-8}, volume = {94}, year = {1998}, }