@inproceedings{4489, abstract = {Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible. In this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation; the post- calculus, on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.}, author = {Henzinger, Thomas A and Kupferman, Orna and Qadeer, Shaz}, booktitle = {Proceedings of the 10th International Conference on Computer Aided Verification}, isbn = {9783540646082}, location = {Vancouver, Canada}, pages = {195 -- 206}, publisher = {Springer}, title = {{From pre-historic to post-modern symbolic model checking}}, doi = {10.1007/BFb0028745}, volume = {1427}, year = {1998}, } @inproceedings{4490, abstract = {A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters). A specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship. First, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively.}, author = {Henzinger, Thomas A and Raskin, Jean and Schobbens, Pierre}, booktitle = {Proceedings of the 25th International Colloqium on Automata, Languages and Programming}, isbn = {9783540647812}, location = {Aalborg, Denmark}, pages = {580 -- 591}, publisher = {Springer}, title = {{The regular real-time languages}}, doi = {10.1007/BFb0055086}, volume = {1443}, year = {1998}, } @article{4491, abstract = {We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology}, author = {Henzinger, Thomas A and Ho, Pei and Wong Toi, Howard}, issn = {0018-9162}, journal = {IEEE Transactions on Automatic Control}, number = {4}, pages = {540 -- 554}, publisher = {IEEE}, title = {{Algorithmic analysis of nonlinear hybrid systems}}, doi = {10.1109/9.664156 }, volume = {43}, year = {1998}, } @article{4492, abstract = {Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves theω-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch.}, author = {Henzinger, Thomas A and Kopke, Peter and Puri, Anuj and Varaiya, P.}, isbn = {0022-0000}, journal = {Journal of Computer and System Sciences}, number = {1}, pages = {94 -- 124}, publisher = {Elsevier}, title = {{What's decidable about hybrid automata?}}, doi = {10.1006/jcss.1998.1581}, volume = {57}, year = {1998}, } @inproceedings{4515, abstract = {We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable.}, author = {Henzinger, Thomas A}, booktitle = {Proceedings of the 9th Interantional Conference on Concurrency Theory}, isbn = {978-3-540-64896-3}, location = {Nice, France}, pages = {439 -- 454}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{It's about time: Real-time logics reviewed}}, doi = {10.1007/BFb0055640}, volume = {1466}, 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{8527, abstract = {We introduce a new potential-theoretic definition of the dimension spectrum of a probability measure for q > 1 and explain its relation to prior definitions. We apply this definition to prove that if and is a Borel probability measure with compact support in , then under almost every linear transformation from to , the q-dimension of the image of is ; in particular, the q-dimension of is preserved provided . We also present results on the preservation of information dimension and pointwise dimension. Finally, for and q > 2 we give examples for which is not preserved by any linear transformation into . All results for typical linear transformations are also proved for typical (in the sense of prevalence) continuously differentiable functions.}, author = {Hunt, Brian R and Kaloshin, Vadim}, issn = {0951-7715}, journal = {Nonlinearity}, keywords = {Mathematical Physics, General Physics and Astronomy, Applied Mathematics, Statistical and Nonlinear Physics}, number = {5}, pages = {1031--1046}, publisher = {IOP Publishing}, title = {{How projections affect the dimension spectrum of fractal measures}}, doi = {10.1088/0951-7715/10/5/002}, volume = {10}, year = {1997}, } @article{8528, abstract = {In the present paper, we give a definition of prevalent ("metrically prevalent" ) sets in nonlinear function spaces. A subset of a Euclidean space is said to be metrically prevalent if its complement has measure zero. There is no natural way to generalize the definition of a set of measure zero in a finite-dimensional space to the infinite-dimensional case [6]. Therefore, it is necessary to give a special definition of a metrically prevalent set (set of full measure) in an infinite-dimensional space. There are various ways to do so. We suggest one of the possible ways to define the class of metrically prevalent sets in the space of smooth maps of one smooth manifold into another. It is shown in this paper that the class of metrically prevalent sets has natural properties; in particular, the intersection of finitely many metrically prevalent sets is metrically prevalent. The main result of the paper is a prevalent version of Thorn's transversality theorem. It is common practice in singularity theory and the theory of dynamical systems to say that a property holds for "almost every" map (or flow) if it holds for a residual set, i.e., a set that contains a countable intersection of open dense sets in the corresponding function space. However, even in finite-dimensional spaces such a set can have arbitrarily small (say, zero) Lebesgue measure. We prove that Thorn's transversality theorem holds for an essentially "thicker" set than a residual set. It seems reasonable to revise from the prevalent point of view the classical results of singularity theory and theory of dynamical systems, including the multijet transversality theorem, Mather's stability theorem, Kupka-Smale's theorem for dynamical systems, etc. We shall do this elsewhere. The notion of prevalence in linear Banach spaces was introduced and investigated in [8]. One of the possible ways to define a class of prevalent sets in the space of smooth maps of manifolds, which essentially differs from that presented in this paper, is given in [7]. Definitions of typicalness based on the Lebesgue measure in a finite-dimensional space were suggested by Kolmogorov [10] and Arnold [11]. These definitions were cited and discussed in [9]. Here we only point out that the finite-dimensional analog of Arnold's definition allows prevalent sets to have arbitrarily small measure, whereas the prevalent sets in the sense of the finite-dimensional analog of the definition given in the present paper are necessarily of full measure. Our definition is a modification of that due to Arnold. I wish to thank Yu. S. Illyashenko for constant attention to this work and useful discussions and R. I. Bogdanov for help in the preparation of this paper. }, author = {Kaloshin, Vadim}, issn = {0016-2663}, journal = {Functional Analysis and Its Applications}, keywords = {Applied Mathematics, Analysis}, number = {2}, pages = {95--99}, publisher = {Springer Nature}, title = {{Prevalence in the space of finitely smooth maps}}, doi = {10.1007/bf02466014}, volume = {31}, year = {1997}, } @article{11666, abstract = {This article describes the Digital Continuous Profiling Infrastructure, a sampling-based profiling system designed to run continuously on production systems. The system supports multiprocessors, works on unmodified executables, and collects profiles for entire systems, including user programs, shared libraries, and the operating system kernel. Samples are collected at a high rate (over 5200 samples/sec. per 333MHz processor), yet with low overhead (1–3% slowdown for most workloads). Analysis tools supplied with the profiling system use the sample data to produce a precise and accurate accounting, down to the level of pipeline stalls incurred by individual instructions, of where time is bring spent. When instructions incur stalls, the tools identify possible reasons, such as cache misses, branch mispredictions, and functional unit contention. The fine-grained instruction-level analysis guides users and automated optimizers to the causes of performance problems and provides important insights for fixing them.}, author = {Anderson, Jennifer M. and Berc, Lance M. and Dean, Jeffrey and Ghemawat, Sanjay and Henzinger, Monika H and Leung, Shun-Tak A. and Sites, Richard L. and Vandevoorde, Mark T. and Waldspurger, Carl A. and Weihl, William E.}, issn = {1557-7333}, journal = {ACM Transactions on Computer Systems}, number = {4}, pages = {357--390}, publisher = {Association for Computing Machinery}, title = {{Continuous profiling: Where have all the cycles gone?}}, doi = {10.1145/265924.265925}, volume = {15}, year = {1997}, } @article{11765, abstract = {This paper presents insertions-only algorithms for maintaining the exact and/or approximate size of the minimum edge cut and the minimum vertex cut of a graph. The algorithms output the approximate or exact sizekin timeO(1) and a cut of sizekin time linear in its size. For the minimum edge cut problem and for any 0 < ε ≤ 1, the amortized time per insertion isO(1/ε2) for a (2 + ε)-approximation,O((log λ)((log n)/ε)2) for a (1 + ε)-approximation, andO(λ log n) for the exact size, wherenis the number of nodes in the graph and λ is the size of the minimum cut. The (2 + ε)-approximation algorithm and the exact algorithm are deterministic; the (1 + ε)-approximation algorithm is randomized. We also present a static 2-approximation algorithm for the size κ of the minimum vertex cut in a graph, which takes time. This is a factor of κ faster than the best algorithm for computing the exact size, which takes time. We give an insertions-only algorithm for maintaining a (2 + ε)-approximation of the minimum vertex cut with amortized insertion timeO(n/ε).}, author = {Henzinger, Monika H}, issn = {0196-6774}, journal = {Journal of Algorithms}, number = {1}, pages = {194--220}, publisher = {Elsevier}, title = {{A static 2-approximation algorithm for vertex connectivity and incremental approximation algorithms for edge and vertex connectivity}}, doi = {10.1006/jagm.1997.0855}, volume = {24}, year = {1997}, } @article{11767, abstract = {We give a linear-time algorithm for single-source shortest paths in planar graphs with nonnegative edge-lengths. Our algorithm also yields a linear-time algorithm for maximum flow in a planar graph with the source and sink on the same face. For the case where negative edge-lengths are allowed, we give an algorithm requiringO(n4/3 log(nL)) time, whereLis the absolute value of the most negative length. This algorithm can be used to obtain similar bounds for computing a feasible flow in a planar network, for finding a perfect matching in a planar bipartite graph, and for finding a maximum flow in a planar graph when the source and sink are not on the same face. We also give parallel and dynamic versions of these algorithms.}, author = {Henzinger, Monika H and Klein, Philip and Rao, Satish and Subramanian, Sairam}, issn = {0022-0000}, journal = {Journal of Computer and System Sciences}, number = {1}, pages = {3--23}, publisher = {Elsevier}, title = {{Faster shortest-path algorithms for planar graphs}}, doi = {10.1006/jcss.1997.1493}, volume = {55}, year = {1997}, } @inproceedings{11803, abstract = {We present the first fully dynamic algorithm for maintaining a minimum spanning tree in time o(√n) per operation. To be precise, the algorithm uses O(n 1/3 log n) amortized time per update operation. The algorithm is fairly simple and deterministic. An immediate consequence is the first fully dynamic deterministic algorithm for maintaining connectivity and, bipartiteness in amortized time O(n 1/3 log n) per update, with O(1) worst case time per query.}, author = {Henzinger, Monika H and King, Valerie}, booktitle = {24th International Colloquium on Automata, Languages and Programming}, isbn = {9783540631651}, issn = {1611-3349}, location = {Bologna, Italy}, pages = {594–604}, publisher = {Springer Nature}, title = {{Maintaining minimum spanning trees in dynamic graphs}}, doi = {10.1007/3-540-63165-8_214}, volume = {1256}, year = {1997}, } @article{11849, abstract = {This paper describes the DIGlTAL Continuous Profiling Infrastmcture, a sampling-based profiling system designed to run continuously on production systems. The system supports multiprocessors, works on unmodified executable& and collects profiles for entire systems, including user programs, shared libraries, and the operating system kernel. Samples are collected at a high rate (over 5200 samples/secper333-MHz processor), yet with low overhead (l-3% slowdown for most workloads). Analysis tools supplied with the profiling system use the sample data to produce an accurate accounting, down to the level of pipeline stalls incurred by individual instructions, of where time is being spent. When instructions incur stalls, the tools identify possible reasons, such as cache misses, branch mispredictions, and functional unit contention. The fine-grained instruction-level analysis guides users and automated optimizers to the causes of performance problems and provides important insights for fixing them. }, author = {Anderson, Jennifer M. and Berc, Lance M. and Dean, Jeffrey and Ghemawat, Sanjay and Henzinger, Monika H and Leung, Shun-Tak A. and Sites, Richard L. and Vandevoorde, Mark T. and Waldspurger, Carl A. and Weihl, William E.}, issn = {0163-5980}, journal = {ACM SIGOPS Operating Systems Review}, number = {5}, pages = {1--14}, publisher = {Association for Computing Machinery}, title = {{Continuous profiling: Where have all the cycles gone?}}, doi = {10.1145/269005.266637}, volume = {31}, year = {1997}, } @article{11883, abstract = {In dynamic graph algorithms the following provide-or-bound problem has to be solved quickly: Given a set S containing a subset R and a way of generating random elements from S testing for membership in R, either (i) provide an element of R, or (ii) give a (small) upper bound on the size of R that holds with high probability. We give an optimal algorithm for this problem. This algorithm improves the time per operation for various dynamic graph algorithms by a factor of O(log n). For example, it improves the time per update for fully dynamic connectivity from O(log3n) to O(log2n).}, author = {Henzinger, Monika H and Thorup, Mikkel}, issn = {1098-2418}, journal = {Random Structures and Algorithms}, number = {4}, pages = {369--379}, publisher = {Wiley}, title = {{Sampling to provide or to bound: With applications to fully dynamic graph algorithms}}, doi = {10.1002/(sici)1098-2418(199712)11:4<369::aid-rsa5>3.0.co;2-x}, volume = {11}, year = {1997}, } @article{2493, abstract = {A specific antiserum against substance P receptor (SPR) labels nonprincipal neurons in the cerebral cortex of the rat (T. Kaneko et al. [1994], Neuroscience 60:199-211; Y. Nakaya et al. [1994], J. Comp. Neurol. 347:249-274). In the present study, we aimed to identify the types of SPR- immunoreactive neurons in the hippocampus according to their content of neurochemical markers, which label interneuron populations with distinct termination patterns. Markers for perisomatic inhibitory cells, parvalbumin and cholecystokinin (CCK), colocalized with SPR in pyramidallike basket cells in the dentate gyrus and in large multipolar or bitufted cells within all hippocampal subfields respectively. A dense meshwork of SPR-immunoreactive spiny dendrites in the hilus and stratum lucidum of the CA3 region belonged largely to inhibitory cells terminating in the distal dendritic region of granule cells, as indicated by the somatostatin and neuropeptide Y (NPY) content. In addition, SPR and NPY were colocalized in numerous multipolar interneurons with dendrites branching close to the soma. Twenty-five percent of the SPR-immunoreactive cells overlapped with calretinin-positive neurons in all hippocampal subfields, showing that interneurons specialized to contact other gamma-aminobutyric acid-ergic cells may also contain SPR. On the basis of the known termination pattern of the colocalized markers, we conclude that SPR-positive interneurons are functionally heterogeneous and participate in different inhibitory processes: (1) perisomatic inhibition of principal cells (CCK-containing cells, and parvalbumin-positive cells in the dentate gyrus), (2) feedback dendritic inhibition in the entorhinal termination zone (somatostatin and NPY-containing cells), and (3) innervation of other interneurons (calretinin-containing cells).}, author = {Acsády, László and Katona, István and Gulyás, Attila and Shigemoto, Ryuichi and Freund, Tamás}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {3}, pages = {320 -- 336}, publisher = {Wiley-Blackwell}, title = {{Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus}}, doi = {10.1002/(SICI)1096-9861(19970217)378:3<320::AID-CNE2>3.0.CO;2-5}, volume = {378}, year = {1997}, } @article{2575, abstract = {It was examined electron microscopically in the rat if a metabotropic glutamate receptor, mGluR7, might be localized in axon terminals of nociceptive, primary afferent fibers in laminae I and II of the spinal dorsal horn. Nociceptive nature of axon terminals showing mGluR7-like immunoreactivity (mGluR7-LI) was indicated by binding to the isolectin I-B4 from Griffonia simplicifolia (I-B4), or by substance P-like immunoreactivity (SP-LI). Axon terminals labeled with immunogold particles indicating mGluR7-LI were usually filled with round synaptic vesicles and were in asymmetric synaptic contact with dendritic or somatic profiles; occasionally they contained pleomorphic vesicles and were in symmetric synaptic contact with somatic profiles in lamina II. The double-labeling studies revealed that most of axon terminals with I-B4 labeling as well as a small population of axon terminals with SP-LI, showed mGluR7-LI. About one-third or much smaller population of axon terminals with mGluR7-LI in laminae I and II were labeled, respectively, with I-B4 or SP-LI; these were in asymmetric synaptic contact with dendritic profiles.}, author = {Li, He and Ohishi, Hitoshi and Kinoshita, Ayae and Shigemoto, Ryuichi and Nomura, Sakashi and Mizuno, Noboru}, issn = {0304-3940}, journal = {Neuroscience Letters}, number = {3}, pages = {153 -- 156}, publisher = {Elsevier}, title = {{Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat}}, doi = {10.1016/S0304-3940(97)13429-2}, volume = {223}, year = {1997}, } @article{2576, abstract = {Primary afferent neurons containing substance P (SP) are apparently implicated in the transmission of noxious information from the periphery to the central nervous system, and SP released from primary afferent neurons acts on second-order neurons with the SP receptor (SPR). In the rat, nociceptive information reached the hypothalamus not only through indirect pathways but also directly through trigeminohypothalamic and spinohypothalamic pathways. Thus, in the present study, the distribution pattern of trigeminohypothalamic and spinohypothalamic tract neurons showing SPR-like immunoreactivity (SPR-LI) was examined in the rat by a retrograde tract-tracing method combined with immunofluorescence histochemistry for SPR. A substantial number of trigeminal and spinal neurons with SPR-LI were retrogradely labeled with Fluore-Gold (FG) injected into the hypothalamic regions. These neurons were distributed mainly in lamina I of the medullary and spinal dorsal horns, lateral spinal nucleus, regions around the central canal of the spinal cord, and the lateral aspect of the deep part of the spinal dorsal horn. A number of SPR-LI neurons in the spinal parasympathetic nucleus were labeled with FG injected into the area around the paraventricular hypothalamic nucleus. Some SPR-LI neurons in the lateral spinal nucleus and the lateral aspect of the deep part of the spinal dorsal horn were also labeled with FG injected into the septal region. On the basis of the distribution areas of SPR-LI trigeminal and spinal neurons projecting to the hypothalamic and septal regions, it is likely that these neurons are involved in the transmission of somatic and/or visceral noxious information.}, author = {Li, Jin and Kaneko, Takeshi and Shigemoto, Ryuichi and Mizuno, Noboru}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {4}, pages = {508 -- 521}, publisher = {Wiley-Blackwell}, title = {{Distribution of trigeminohypothalamic and spinohypothalamic tract neurons displaying substance P receptor-like immunoreactivity in the rat}}, doi = {10.1002/(SICI)1096-9861(19970224)378:4<508::AID-CNE6>3.0.CO;2-6}, volume = {378}, year = {1997}, }