@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}, } @article{2577, abstract = {The cloned cDNA for rat prostacyclin synthase was found to contain a 1503-bp open reading frame which encoded a 501-amino acid protein sharing 84% identity with the human enzyme. RNA blot analysis revealed that the rat prostacyclin synthase mRNA, as a single species of 2.1 kb, is expressed abundantly in the aorta and uterus. High levels of expression were also observed in the stomach, lung, heart, testis, liver, and skeletal muscle. Low but significant expression was also seen in the brain and kidney. Furthermore, the regional distribution and cellular localization of prostacyclin synthase mRNA were examined by in situ hybridization analysis of rat tissue sections. The definitive signals for the mRNA were localized in smooth muscle cells of the arteries, bronchi and uterus, and in the cells of the fibrous tunic surrounding the seminiferous tubules, which are characterized as smooth muscle cells. Besides smooth muscle cells, signal were also detected in the fibroblasts of the heart myocardium, lung parenchyma cells and kidney inner medulla tubules and interstitial cells.}, author = {Tone, Yoshinori and Inoue, Hiroyasu and Hara, Shuntaro and Yokoyama, Chieko and Hatae, Toshihisa and Oida, Hiroji and Narumiya, Shuh and Shigemoto, Ryuichi and Yukawa, Susumu and Tanabe, Tadashi}, issn = {0171-9335}, journal = {European Journal of Cell Biology}, number = {3}, pages = {268 -- 277}, publisher = {Elsevier}, title = {{The regional distribution and cellular localization of mRNA encoding rat prostacyclin synthase}}, volume = {72}, year = {1997}, } @article{2578, abstract = {The distribution of immunoreactivity to the neurokinin3 receptor (NK3R) was examined in segments C7, T11-12, L1-2, and L4-6 of the rat spinal cord. NK3R immunoreactivity was visualized by using two antisera generated against sequences of amino acids contained in the C-terminal region of the NK3R. NK3R-immunoreactive cells were numerous in the substantia gelatinosa of all spinal segments examined as well as the dorsal commissural nucleus of spinal segments L1-2. Isolated, immunoreactive cells were scattered throughout other regions of the spinal cord. The relationship of NK3R-immunoreactivity with neurons was demonstrated by colocalization with microtubule associated protein 2-immunoreactivity in individual cells. Within neurons, NK3R- immunoreactivity was associated predominately with the plasma membrane of cell bodies and dendrites. Within the substantia gelatinosa, 86% of nitric oxide synthase (NOS)-immunoreactive neurons were also NK3R-immunoreactive. Although NOS-immunoreactive neurons were found throughout all other regions of the spinal cord in the segments examined, these were not NK3R- immunoreactive. When preganglionic sympathetic neurons in spinal segments T11-12 and L1-2 were visualized by intraperitoneal injection of Fluorogold, less than 1% of the Fluorogold-labeled neurons were also immunoreactive for NK3R. The large number of NK3R-immunoreactive neurons in the substantia gelatinosa suggests that some effects of tachykinins an somatosensation may be mediated by NK3R.}, author = {Seybold, Virginia and Grković, Ivica and Portbury, Andrea and Ding, Yu and Shigemoto, Ryuichi and Mizuno, Noboru and Furness, John and Southwell, Bridget}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {4}, pages = {439 -- 448}, publisher = {Wiley-Blackwell}, title = {{Relationship of NK3 receptor-immunoreactivity to subpopulations of neurons in rat spinal cord}}, doi = {10.1002/(SICI)1096-9861(19970519)381:4<439::AID-CNE4>3.0.CO;2-3}, volume = {381}, year = {1997}, } @article{2579, abstract = {The localisation of the neurokinin 3 receptor (NK3r) in the rat gastrointestinal tract has been studied by using a polyclonal antiserum against the C-terminal portion (amino acids 388-452) of the rat NK3r. In the oesophagus, immunoreactivity for the NK3r was found on smooth muscle cells of the muscularis mucosae. NK3r immunoreactivity was not present on muscle cells of other regions. Nerve cell bodies immunoreactive for NK3r were seen in the myenteric and submucous plexuses of the small and large intestine, but not in the stomach or oesophagus. Immunoreactivity was largely confined to nerve cell surfaces. The reaction product was on the cell soma and initial parts of axons. Reactivity was not seen on nerve terminals. Immunoreactive nerve cells had Dogiel Type II morphology. Patterns of co-localisation of NK3r and immunoreactivity for other markers were examined in the ileum, to provide a basis from which to deduce the functional identity of NK3r-immunoreactive nerve cells. Most of the NK3r-immunoreactive nerve cells were also immunoreactive for the calcium-binding proteins, calretinin and calbindin, and all were immunoreactive for the NK1 receptor (NK1r). Nerve cells that were immunoreactive for nitric oxide synthase were not immunoreactive for either NK3r or NK1r. The projections of the calbindin and calretinin neurons were determined by nerve lesion studies. Their morphology, projections to the mucosa and other ganglia and immunoreactivity for the calcium-binding proteins suggest that the NK3r-immunoreactive neurons are intrinsic sensory neurons.}, author = {Mann, Patricia and Southwell, Bridget and Ding, Yu and Shigemoto, Ryuichi and Mizuno, Noboru and Furness, John}, issn = {0044-3794}, journal = {Cell and Tissue Research}, number = {1}, pages = {1 -- 9}, publisher = {Springer}, title = {{Localisation of neurokinin 3 (NK3) receptor immunoreactivity in the rat gastrointestinal tract}}, doi = {10.1007/s004410050846}, volume = {289}, year = {1997}, } @article{2580, abstract = {Two group I metabotropic glutamate receptor subtypes, mGluR1 and mGluR5, have been reported to occur in highest concentration in an annulus surrounding the edge of the postsynaptic membrane specialisation. In order to determine whether such a distribution is uniform amongst postsynaptic mGluRs, their distribution was compared quantitatively by a pre-embedding silver-intensified immunogold technique at electron microscopic level in hippocampal pyramidal cells (mGluR5), cerebellar Purkinje cells (mGluR1α) and Golgi cells (mGluR2). The results show that mGluR1α, mGluR5 and mGluR2 each have a distinct distribution in relation to the glutamatergic synaptic junctions. On dendritic spines, mGluRlα and mGluR5 showed the highest receptor density in a perisynaptic annulus (defined as within 60 nm of the edge of the synapse) followed by a decreasing extrasynaptic (60-900 nm) receptor level, but the gradient of decrease and the proportion of the perisynaptic pool (mGluR1α, ~ 50%; vs mGluR5, ~ 25%) were different for the two receptors. The distributions of mGluRlα and mGluR5 also differed significantly from simulated random distributions. In contrast, mGluR2 was not closely associated with glutamatergic synapses in the dendritic plasma membrane of cerebellar Golgi cells and its distribution relative to synapses is not different from simulated random distribution in the membrane. The somatic membrane, the axon and the synaptic boutons of the GABAergic Golgi cells also contained immunoreactive mGluR2 that is not associated with synaptic specialisations. In the hippocampal CA1 area the distribution of immunoparticles for mGluR5 on individual spines was established using serial sections. The results indicate that dendritic spines of pyramidal cells are heterogeneous with respect to the ratio of perisynaptic to extrasynaptic mGluR5 pools and about half of the immunopositive spines lack the perisynaptic pool. The quantitative comparison of receptor distributions demonstrates that mGluRlα and mGluR5, but not mGluR2, are highly compartmentalised in different plasma membrane domains. The unique distribution of each mGluR subtype may reflect requirements for different transduction and effector mechanisms between cell types and different domains of the same cell, and suggests that the precise placement of receptors is a crucial factor contributing to neuronal communication.}, author = {Luján, Rafael and Roberts, John and Shigemoto, Ryuichi and Ohishi, Hitoshi and Somogyi, Péter}, issn = {0891-0618}, journal = {Journal of Chemical Neuroanatomy}, number = {4}, pages = {219 -- 241}, publisher = {Elsevier}, title = {{Differential plasma membrane distribution of metabotropic glutamate receptors mGluR1α, mGluR2 and mGluR5, relative to neurotransmitter release sites}}, doi = {10.1016/S0891-0618(97)00051-3}, volume = {13}, year = {1997}, } @article{2581, abstract = {It is well known that striatonigral neurons produce substance P (SP); however, no SP receptor (SPR) has so far been found in the substantia nigra. On the other hand, a previous study in the rat striatum indicated that SPR was expressed only in cholinergic or somatostatinergic intrinsic neurons (Kaneko et al. [1993] Brain Res. 631:297-303). Thus, it was assumed that SP produced by striatenigral neurons might be released through their intrastriatal axon collaterals to act upon intrinsic neurons in the striatum. To confirm this assumption, the distribution of axon collaterals of striatonigral neurons was examined in the striatum of the rat. The experiments were performed on brain slices by combining retrograde labeling with tetramethylrhodamine-dextran amine, electrophysiological recording, intracellular staining with biocytin, and immunocytochemistry for SPR. The distribution of axons of cholinergic striatal neurons (a group of SP-negative intrinsic striatal neurons) was also examined. It was observed that 16% of varicosities of intrastriatal axon collaterals of striatonigral neurons, as well as 6% of axonal varicosities of cholinergic neurons, were in close apposition to dendrites and cell bodies of SPB-immunoreactive striatal neurons. Since SPR-immunoreactive striatal neurons constituted only 2.7% of the total population of striatal neurons (Kaneko et al. [1993] Brain Res. 631:297-303), it appeared that axonal varicosities of striatonigral neurons were preferentially apposed to SPR-immunoreactive striatal neurons and that the varicosities in close apposition to SPR-immunoreactive neurons were derived more frequently from striatonigral neurons than from cholinergic interneurons. Confocal laser scanning microscopy indicated that axonal varicosities in close apposition to SPR-immunoreactive cells showed synaptophysin immunoreactivity, a marker of synaptic vesicles. In intrastriatal axons of striatonigral neurons, it was further revealed from electron microscopy that axonal varicosities in close apposition to SPR- immunoreactive dendrites, at least a part of them, made synapses of the symmetric type. Striatonigral neurons might release SP preferentially around cholinergic or somatostatinergic intrinsic neurons to regulate them through SP-SPR interactions.}, author = {Lee, Teffy and Kaneko, Takeshi and Shigemoto, Ryuichi and Nomura, Sakashi and Mizuno, Noboru}, issn = {0021-9967}, journal = {Journal of Comparative Neurology}, number = {2}, pages = {250 -- 264}, publisher = {Wiley-Blackwell}, title = {{Collateral projections from striatonigral neurons to substance P receptor-expressing intrinsic neurons in the striatum of the rat}}, doi = {10.1002/(SICI)1096-9861(19971117)388:2<250::AID-CNE5>3.0.CO;2-0}, volume = {388}, year = {1997}, } @article{2582, abstract = {Neurotransmission in the hippocampus is modulated variously through presynaptic metabotropic glutamate receptors (mGluRs). To establish the precise localization of presynaptic mGluRs in the rat hippocampus, we used subtype-specific antibodies for eight mGluRs (mGluR1-mGluR8) for immunohistochemistry combined with lesioning of the three major hippocampal pathways: the perforant path, mossy fiber, and Schaffer collateral. Immunoreactivity for group II (mGluR2) and group III (mGluR4a, mGluR7a, mGluR7b, and mGluR8) mGluRs was predominantly localized to presynaptic elements, whereas that for group I mGluRs (mGluR1 and mGluR5) was localized to postsynaptic elements. The medial perforant path was strongly immunoreactive for mGluR2 and mGluR7a throughout the hippocampus, and the lateral perforant path was prominently immunoreactive for mGluR8 in the dentate gyrus and CA3 area. The messy fiber was labeled for mGluR2, mGluR7a, and mGluR7b, whereas the Schaffer collateral was labeled only for mGluR7a. Electron microscopy further revealed the spatial segregation of group II and group III mGluRs within presynaptic elements. Immunolabeling for the group III receptors was predominantly observed in presynaptic active zones of asymmetrical and symmetrical synapses, whereas that for the group II receptor (mGluR2) was found in preterminal rather than terminal portions of axons. Target cell-specific segregation of receptors, first reported for mGluR7a (Shigemoto et al., 1996), was also apparent for the other group III mGluRs, suggesting that transmitter release is differentially regulated by 2-amino- 4-phosphonobutyrate-sensitive mGluRs in individual synapses on single axons according to the identity of postsynaptic neurons.}, author = {Shigemoto, Ryuichi and Kinoshita, Ayae and Wada, Eiki and Nomura, Sakashi and Ohishi, Hitoshi and Takada, Masahiko and Flor, Peter and Neki, Akio and Abe, Takaaki and Nakanishi, Shigetada and Mizuno, Noboru}, issn = {0270-6474}, journal = {Journal of Neuroscience}, number = {19}, pages = {7503 -- 7522}, publisher = {Society for Neuroscience}, title = {{Differential presynaptic localization of metabotropic glutamate receptor subtypes in the rat hippocampus}}, doi = {10.1523/JNEUROSCI.17-19-07503.1997}, volume = {17}, year = {1997}, } @article{2727, abstract = {Diamagnetism of the magnetic Schrödinger operator and paramagnetism of the Pauli operator are rigorously proven for nonhomogeneous magnetic fields in the large field, in the large temperature and in the semiclassical asymptotic regimes. New counterexamples are presented which show that neither dia-nor paramagnetism is true in a robust sense (without asymptotics). In particular, we demonstrate that the recent diamagnetic comparison result by Loss and Thaller [M. Loss and B. Thaller, Commun. Math. Phys. (submitted)] is essentially the best one can hope for.}, author = {Erdös, László}, issn = {0022-2488}, journal = {Journal of Mathematical Physics}, number = {3}, pages = {1289 -- 1317}, publisher = {American Institute of Physics}, title = {{Dia- and paramagnetism for nonhomogeneous magnetic fields}}, doi = {10.1063/1.531909}, volume = {38}, year = {1997}, } @article{2729, abstract = {We give the leading order semiclassical asymptotics for the sum of the negative eigenvalues of the Pauli operator (in dimension two and three) with a strong non-homogeneous magnetic field. As in [LSY-II] for homogeneous field, this result can be used to prove that the magnetic Thomas-Fermi theory gives the leading order ground state energy of large atoms. We develop a new localization scheme well suited to the anisotropic character of the strong magnetic field. We also use the basic Lieb-Thirring estimate obtained in our companion paper [ES-I].}, author = {Erdös, László and Solovej, Jan}, issn = {0010-3616}, journal = {Communications in Mathematical Physics}, number = {3}, pages = {599 -- 656}, publisher = {Springer}, title = {{Semiclassical eigenvalue estimates for the Pauli operator with strong non-homogeneous magnetic fields, II. Leading order asymptotic estimates}}, doi = {10.1007/s002200050181}, volume = {188}, 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}, } @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}, } @inproceedings{4583, abstract = {In a trace-based world, the modular specification, verification, and control of live systems require each module to be receptive; that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves. We study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We define the receptiveness of such a module as the existence of a winning strategy in a game of the module against its environment. By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of prepositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. Finally, we present an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules.}, author = {Alur, Rajeev and Henzinger, Thomas A}, booktitle = {8th International Conference on Concurrency Theory}, isbn = {9783540691884}, location = {Warsaw, Poland}, pages = {74 -- 88}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Modularity for timed and hybrid systems}}, doi = {10.1007/3-540-63141-0_6}, volume = {1243}, year = {1997}, } @article{4584, abstract = {This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.}, author = {Alur, Rajeev and Henzinger, Thomas A}, issn = {1433-2779}, journal = {Software Tools For Technology Transfer}, number = {1-2}, pages = {86 -- 109}, publisher = {Springer}, title = {{Real-time system = discrete system + clock variables}}, doi = {10.1007/s100090050007}, volume = {1}, year = {1997}, } @inproceedings{4605, abstract = {A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. In this survey, we demonstrate symbolic algorithms for the verification of and controller synthesis for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically}, author = {Alur, Rajeev and Henzinger, Thomas A and Wong Toi, Howard}, booktitle = {Proceedings of the 36th IEEE Conference on Decision and Control}, isbn = {0780341872}, location = {San Diego, CA, USA}, pages = {702 -- 707}, publisher = {IEEE}, title = {{Symbolic analysis of hybrid systems}}, doi = {10.1109/CDC.1997.650717 }, year = {1997}, } @article{4607, abstract = {We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem.}, author = {Alur, Rajeev and Courcoubetis, Costas and Henzinger, Thomas A}, issn = {0925-9856}, journal = {Formal Methods in System Design}, number = {2}, pages = {137 -- 156}, publisher = {Springer}, title = {{Computing accumulated delays in real-time systems}}, doi = {10.1023/A:1008626013578}, volume = {11}, year = {1997}, } @inproceedings{4608, abstract = {State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy.}, author = {Alur, Rajeev and Brayton, Robert and Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram}, booktitle = {9th International Conference on Computer Aided Verification}, isbn = {9783540631668}, location = {Haifa, Israel}, pages = {340 -- 351}, publisher = {Springer}, title = {{Partial-order reduction in symbolic state-space exploration}}, doi = {10.1007/3-540-63166-6_34}, volume = {1254}, year = {1997}, } @inproceedings{4609, abstract = {Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas}, author = {Alur, Rajeev and Henzinger, Thomas A and Kupferman, Orna}, booktitle = {Proceedings of the 38th Annual Symposium on Foundations of Computer Science}, issn = {0004-5411}, location = {Washington, DC, United States}, pages = {100 -- 109}, publisher = {Association for Computing Machinery (ACM)}, title = {{Alternating-time temporal logic}}, doi = {10.1145/585265.585270}, year = {1997}, }