[{"main_file_link":[{"url":"https://epubs.siam.org/doi/10.1137/S0097539790179919"}],"scopus_import":"1","article_type":"original","month":"12","date_published":"1994-12-01T00:00:00Z","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-03T06:41:56Z","publist_id":"2092","publisher":"SIAM","date_created":"2018-12-11T12:06:33Z","oa_version":"None","publication":"SIAM Journal on Computing","_id":"4033","issue":"6","article_processing_charge":"No","type":"journal_article","author":[{"full_name":"Chazelle, Bernard","first_name":"Bernard","last_name":"Chazelle"},{"orcid":"0000-0002-9823-6833","full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Leonidas","last_name":"Guibas","full_name":"Guibas, Leonidas"},{"first_name":"John","last_name":"Hershberger","full_name":"Hershberger, John"},{"last_name":"Seidel","first_name":"Raimund","full_name":"Seidel, Raimund"},{"last_name":"Sharir","first_name":"Micha","full_name":"Sharir, Micha"}],"day":"01","title":"Selecting heavily covered points","volume":23,"status":"public","page":"1138 - 1151","abstract":[{"text":"A collection of geometric selection lemmas is proved, such as the following: For any set P of n points in three-dimensional space and any set S of m spheres, where each sphere passes through a distinct point pair in P. there exists a point x, not necessarily in P, that is enclosed by Ω(m2/(n2 log6 n2/m)) of the spheres in S. Similar results apply in arbitrary fixed dimensions, and for geometric bodies other than spheres. The results have applications in reducing the size of geometric structures, such as three-dimensional Delaunay triangulations and Gabriel graphs, by adding extra points to their defining sets.","lang":"eng"}],"quality_controlled":"1","citation":{"ama":"Chazelle B, Edelsbrunner H, Guibas L, Hershberger J, Seidel R, Sharir M. Selecting heavily covered points. <i>SIAM Journal on Computing</i>. 1994;23(6):1138-1151. doi:<a href=\"https://doi.org/10.1137/S0097539790179919 \">10.1137/S0097539790179919 </a>","ista":"Chazelle B, Edelsbrunner H, Guibas L, Hershberger J, Seidel R, Sharir M. 1994. Selecting heavily covered points. SIAM Journal on Computing. 23(6), 1138–1151.","ieee":"B. Chazelle, H. Edelsbrunner, L. Guibas, J. Hershberger, R. Seidel, and M. Sharir, “Selecting heavily covered points,” <i>SIAM Journal on Computing</i>, vol. 23, no. 6. SIAM, pp. 1138–1151, 1994.","mla":"Chazelle, Bernard, et al. “Selecting Heavily Covered Points.” <i>SIAM Journal on Computing</i>, vol. 23, no. 6, SIAM, 1994, pp. 1138–51, doi:<a href=\"https://doi.org/10.1137/S0097539790179919 \">10.1137/S0097539790179919 </a>.","apa":"Chazelle, B., Edelsbrunner, H., Guibas, L., Hershberger, J., Seidel, R., &#38; Sharir, M. (1994). Selecting heavily covered points. <i>SIAM Journal on Computing</i>. SIAM. <a href=\"https://doi.org/10.1137/S0097539790179919 \">https://doi.org/10.1137/S0097539790179919 </a>","short":"B. Chazelle, H. Edelsbrunner, L. Guibas, J. Hershberger, R. Seidel, M. Sharir, SIAM Journal on Computing 23 (1994) 1138–1151.","chicago":"Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, John Hershberger, Raimund Seidel, and Micha Sharir. “Selecting Heavily Covered Points.” <i>SIAM Journal on Computing</i>. SIAM, 1994. <a href=\"https://doi.org/10.1137/S0097539790179919 \">https://doi.org/10.1137/S0097539790179919 </a>."},"doi":"10.1137/S0097539790179919 ","extern":"1","year":"1994","publication_identifier":{"issn":["0097-5397"]},"language":[{"iso":"eng"}],"intvolume":"        23"},{"day":"01","status":"public","volume":13,"title":"Three-dimensional alpha shapes","article_processing_charge":"No","_id":"4037","type":"journal_article","issue":"1","publication":"ACM Transactions on Graphics","date_created":"2018-12-11T12:06:34Z","oa_version":"None","author":[{"full_name":"Edelsbrunner, Herbert","orcid":"0000-0002-9823-6833","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","first_name":"Herbert","last_name":"Edelsbrunner"},{"full_name":"Mücke, Ernst","last_name":"Mücke","first_name":"Ernst"}],"date_published":"1994-01-01T00:00:00Z","month":"01","publisher":"ACM","publist_id":"2088","date_updated":"2022-06-02T12:00:42Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/174462.156635","open_access":"1"}],"scopus_import":"1","language":[{"iso":"eng"}],"year":"1994","intvolume":"        13","extern":"1","citation":{"ama":"Edelsbrunner H, Mücke E. Three-dimensional alpha shapes. <i>ACM Transactions on Graphics</i>. 1994;13(1):43-72. doi:<a href=\"https://doi.org/10.1145/174462.156635\">10.1145/174462.156635</a>","mla":"Edelsbrunner, Herbert, and Ernst Mücke. “Three-Dimensional Alpha Shapes.” <i>ACM Transactions on Graphics</i>, vol. 13, no. 1, ACM, 1994, pp. 43–72, doi:<a href=\"https://doi.org/10.1145/174462.156635\">10.1145/174462.156635</a>.","ista":"Edelsbrunner H, Mücke E. 1994. Three-dimensional alpha shapes. ACM Transactions on Graphics. 13(1), 43–72.","ieee":"H. Edelsbrunner and E. Mücke, “Three-dimensional alpha shapes,” <i>ACM Transactions on Graphics</i>, vol. 13, no. 1. ACM, pp. 43–72, 1994.","chicago":"Edelsbrunner, Herbert, and Ernst Mücke. “Three-Dimensional Alpha Shapes.” <i>ACM Transactions on Graphics</i>. ACM, 1994. <a href=\"https://doi.org/10.1145/174462.156635\">https://doi.org/10.1145/174462.156635</a>.","short":"H. Edelsbrunner, E. Mücke, ACM Transactions on Graphics 13 (1994) 43–72.","apa":"Edelsbrunner, H., &#38; Mücke, E. (1994). Three-dimensional alpha shapes. <i>ACM Transactions on Graphics</i>. ACM. <a href=\"https://doi.org/10.1145/174462.156635\">https://doi.org/10.1145/174462.156635</a>"},"doi":"10.1145/174462.156635","quality_controlled":"1","acknowledgement":"National Science Foundation under grant CCR-8921421 and  Alan T. Waterman award, grant CCR-9118874.","oa":1,"abstract":[{"lang":"eng","text":"Frequently, data in scientific computing is in its abstract form a finite point set in space, and it is sometimes useful or required to compute what one might call the `'shape” of the set. For that purpose, this article introduces the formal notion of the family of alpha-shapes of a finite point set in R3. Each shape is a well-defined polytope, derived from the Delaunay triangulation of the point set, with a parameter alpha is-an-element-of R controlling the desired level of detail. An algorithm is presented that constructs the entire family of shapes for a given set of size n in time O(n2), worst case. A robust implementation of the algorithm is discussed, and several applications in the area of scientific computing are mentioned."}],"page":"43 - 72"},{"day":"01","volume":11,"title":"Algorithms for bichromatic line-segment problems and polyhedral terrains","status":"public","date_created":"2018-12-11T12:06:34Z","oa_version":"None","publication":"Algorithmica","_id":"4038","type":"journal_article","article_processing_charge":"No","issue":"2","author":[{"full_name":"Chazelle, Bernard","last_name":"Chazelle","first_name":"Bernard"},{"first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","last_name":"Edelsbrunner","full_name":"Edelsbrunner, Herbert","orcid":"0000-0002-9823-6833"},{"first_name":"Leonidas","last_name":"Guibas","full_name":"Guibas, Leonidas"},{"last_name":"Sharir","first_name":"Micha","full_name":"Sharir, Micha"}],"article_type":"original","month":"02","date_published":"1994-02-01T00:00:00Z","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-02T12:25:29Z","publist_id":"2089","publisher":"Springer","main_file_link":[{"url":"https://link.springer.com/article/10.1007/BF01182771"}],"scopus_import":"1","year":"1994","publication_identifier":{"issn":["0178-4617"]},"language":[{"iso":"eng"}],"intvolume":"        11","quality_controlled":"1","doi":"10.1007/BF01182771","citation":{"ama":"Chazelle B, Edelsbrunner H, Guibas L, Sharir M. Algorithms for bichromatic line-segment problems and polyhedral terrains. <i>Algorithmica</i>. 1994;11(2):116-132. doi:<a href=\"https://doi.org/10.1007/BF01182771\">10.1007/BF01182771</a>","ieee":"B. Chazelle, H. Edelsbrunner, L. Guibas, and M. Sharir, “Algorithms for bichromatic line-segment problems and polyhedral terrains,” <i>Algorithmica</i>, vol. 11, no. 2. Springer, pp. 116–132, 1994.","ista":"Chazelle B, Edelsbrunner H, Guibas L, Sharir M. 1994. Algorithms for bichromatic line-segment problems and polyhedral terrains. Algorithmica. 11(2), 116–132.","mla":"Chazelle, Bernard, et al. “Algorithms for Bichromatic Line-Segment Problems and Polyhedral Terrains.” <i>Algorithmica</i>, vol. 11, no. 2, Springer, 1994, pp. 116–32, doi:<a href=\"https://doi.org/10.1007/BF01182771\">10.1007/BF01182771</a>.","apa":"Chazelle, B., Edelsbrunner, H., Guibas, L., &#38; Sharir, M. (1994). Algorithms for bichromatic line-segment problems and polyhedral terrains. <i>Algorithmica</i>. Springer. <a href=\"https://doi.org/10.1007/BF01182771\">https://doi.org/10.1007/BF01182771</a>","short":"B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, Algorithmica 11 (1994) 116–132.","chicago":"Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, and Micha Sharir. “Algorithms for Bichromatic Line-Segment Problems and Polyhedral Terrains.” <i>Algorithmica</i>. Springer, 1994. <a href=\"https://doi.org/10.1007/BF01182771\">https://doi.org/10.1007/BF01182771</a>."},"extern":"1","acknowledgement":"Supported in part by the National Science Foundation under Grant CCR-8714565.","abstract":[{"lang":"eng","text":"We consider a variety of problems on the interaction between two sets of line segments in two and three dimensions. These problems range from counting the number of intersecting pairs between m blue segments and n red segments in the plane (assuming that two line segments are disjoint if they have the same color) to finding the smallest vertical distance between two nonintersecting polyhedral terrains in three-dimensional space. We solve these problems efficiently by using a variant of the segment tree. For the three-dimensional problems we also apply a variety of recent combinatorial and algorithmic techniques involving arrangements of lines in three-dimensional space, as developed in a companion paper."}],"page":"116 - 132"},{"abstract":[{"text":"Let P be a simple polygon with n vertices. We present a simple decomposition scheme that partitions the interior of P into O(n) so-called geodesic triangles, so that any line segment interior to P crosses at most 2 log n of these triangles. This decomposition can be used to preprocess P in a very simple manner, so that any ray-shooting query can be answered in time O(log n). The data structure requires O(n) storage and O(n log n) preprocessing time. By using more sophisticated techniques, we can reduce the preprocessing time to O(n). We also extend our general technique to the case of ray shooting amidst k polygonal obstacles with a total of n edges, so that a query can be answered in O(√ log n) time.","lang":"eng"}],"page":"54 - 68","intvolume":"        12","year":"1994","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0178-4617"]},"acknowledgement":"Work by Bernard Chazelle has been supported by NSF Grant CCR-87-00917. Work by Herbert Edelsbrunner has been supported by NSF Grant CCR-89-21421. Work by Micha Sharir has been supported by ONR Grants N00014-89-J-3042 and N00014-90-J-1284, by NSF Grant CCR-89-01484, and by grants from the U.S.-Israeli Binational Science Foundation, the Fund for Basic Research administered by the Israeli Academy of Sciences, and the G.I.F., the German-Israeli Foundation for Scientific Research and Development.","quality_controlled":"1","doi":"10.1007/BF01377183","citation":{"chicago":"Chazelle, Bernard, Herbert Edelsbrunner, Michelangelo Grigni, Leonidas Guibas, John Hershberger, Micha Sharir, and Jack Snoeyink. “Ray Shooting in Polygons Using Geodesic Triangulations.” <i>Algorithmica</i>. Springer, 1994. <a href=\"https://doi.org/10.1007/BF01377183\">https://doi.org/10.1007/BF01377183</a>.","short":"B. Chazelle, H. Edelsbrunner, M. Grigni, L. Guibas, J. Hershberger, M. Sharir, J. Snoeyink, Algorithmica 12 (1994) 54–68.","apa":"Chazelle, B., Edelsbrunner, H., Grigni, M., Guibas, L., Hershberger, J., Sharir, M., &#38; Snoeyink, J. (1994). Ray shooting in polygons using geodesic triangulations. <i>Algorithmica</i>. Springer. <a href=\"https://doi.org/10.1007/BF01377183\">https://doi.org/10.1007/BF01377183</a>","mla":"Chazelle, Bernard, et al. “Ray Shooting in Polygons Using Geodesic Triangulations.” <i>Algorithmica</i>, vol. 12, no. 1, Springer, 1994, pp. 54–68, doi:<a href=\"https://doi.org/10.1007/BF01377183\">10.1007/BF01377183</a>.","ieee":"B. Chazelle <i>et al.</i>, “Ray shooting in polygons using geodesic triangulations,” <i>Algorithmica</i>, vol. 12, no. 1. Springer, pp. 54–68, 1994.","ista":"Chazelle B, Edelsbrunner H, Grigni M, Guibas L, Hershberger J, Sharir M, Snoeyink J. 1994. Ray shooting in polygons using geodesic triangulations. Algorithmica. 12(1), 54–68.","ama":"Chazelle B, Edelsbrunner H, Grigni M, et al. Ray shooting in polygons using geodesic triangulations. <i>Algorithmica</i>. 1994;12(1):54-68. doi:<a href=\"https://doi.org/10.1007/BF01377183\">10.1007/BF01377183</a>"},"extern":"1","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-02T12:41:07Z","publist_id":"2090","publisher":"Springer","article_type":"original","month":"07","date_published":"1994-07-01T00:00:00Z","scopus_import":"1","main_file_link":[{"url":"https://link.springer.com/article/10.1007/BF01377183"}],"volume":12,"title":"Ray shooting in polygons using geodesic triangulations","status":"public","day":"01","author":[{"last_name":"Chazelle","first_name":"Bernard","full_name":"Chazelle, Bernard"},{"orcid":"0000-0002-9823-6833","full_name":"Edelsbrunner, Herbert","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","last_name":"Edelsbrunner"},{"full_name":"Grigni, Michelangelo","last_name":"Grigni","first_name":"Michelangelo"},{"full_name":"Guibas, Leonidas","first_name":"Leonidas","last_name":"Guibas"},{"last_name":"Hershberger","first_name":"John","full_name":"Hershberger, John"},{"full_name":"Sharir, Micha","first_name":"Micha","last_name":"Sharir"},{"last_name":"Snoeyink","first_name":"Jack","full_name":"Snoeyink, Jack"}],"oa_version":"None","date_created":"2018-12-11T12:06:35Z","publication":"Algorithmica","type":"journal_article","_id":"4039","issue":"1","article_processing_charge":"No"},{"acknowledgement":"We thank Dorothea Stratmann and Karin Angermayer for skillful technical assistance.","quality_controlled":"1","doi":"10.1016/s0021-9258(17)42186-7","citation":{"apa":"Leingärtner, A., Heisenberg, C.-P. J., Kolbeck, R., Thoenen, H., &#38; Lindholm, D. (1994). Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar granule neurons. <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology. <a href=\"https://doi.org/10.1016/s0021-9258(17)42186-7\">https://doi.org/10.1016/s0021-9258(17)42186-7</a>","short":"A. Leingärtner, C.-P.J. Heisenberg, R. Kolbeck, H. Thoenen, D. Lindholm, Journal of Biological Chemistry 269 (1994) 828–830.","chicago":"Leingärtner, Axel, Carl-Philipp J Heisenberg, Roland Kolbeck, Hans Thoenen, and Dan Lindholm. “Brain-Derived Neurotrophic Factor Increases Neurotrophin-3 Expression in Cerebellar Granule Neurons.” <i>Journal of Biological Chemistry</i>. American Society for Biochemistry and Molecular Biology, 1994. <a href=\"https://doi.org/10.1016/s0021-9258(17)42186-7\">https://doi.org/10.1016/s0021-9258(17)42186-7</a>.","ista":"Leingärtner A, Heisenberg C-PJ, Kolbeck R, Thoenen H, Lindholm D. 1994. Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar granule neurons. Journal of Biological Chemistry. 269(2), 828–830.","ieee":"A. Leingärtner, C.-P. J. Heisenberg, R. Kolbeck, H. Thoenen, and D. Lindholm, “Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar granule neurons,” <i>Journal of Biological Chemistry</i>, vol. 269, no. 2. American Society for Biochemistry and Molecular Biology, pp. 828–830, 1994.","mla":"Leingärtner, Axel, et al. “Brain-Derived Neurotrophic Factor Increases Neurotrophin-3 Expression in Cerebellar Granule Neurons.” <i>Journal of Biological Chemistry</i>, vol. 269, no. 2, American Society for Biochemistry and Molecular Biology, 1994, pp. 828–30, doi:<a href=\"https://doi.org/10.1016/s0021-9258(17)42186-7\">10.1016/s0021-9258(17)42186-7</a>.","ama":"Leingärtner A, Heisenberg C-PJ, Kolbeck R, Thoenen H, Lindholm D. Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar granule neurons. <i>Journal of Biological Chemistry</i>. 1994;269(2):828-830. doi:<a href=\"https://doi.org/10.1016/s0021-9258(17)42186-7\">10.1016/s0021-9258(17)42186-7</a>"},"extern":"1","intvolume":"       269","year":"1994","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0021-9258"],"eissn":["1083-351X"]},"page":"828 - 830","abstract":[{"lang":"eng","text":"Neurotrophin-3 (NT-3) is a member of the neurotrophin gene family and is highly expressed in the developing rat cerebellum. Here we show that brain-derived neurotrophic factor (BDNF) increased by approximately 10-fold the NT-3 mRNA levels in cultured cerebellar granule neurons isolated from postnatal rats, whereas nerve growth factor (NGF) and NT-3 itself had no effect. The effect of BDNF was additive to that of triiodothyronine (T3), which also increased NT-3 mRNA in these neurons. The drug K252a inhibited the BDNF-mediated stimulation of NT-3 expression, suggesting an involvement of trkB receptors. Nuclear run-on experiments showed that BDNF enhanced NT-3 transcription, whereas the stability of NT-3 mRNA remained unchanged. The data presented are the first demonstration that one neurotrophin regulates the expression of another and provide evidence that NT-3 production in granule neurons is regulated by both BDNF and T3."}],"oa":1,"author":[{"full_name":"Leingärtner, Axel","last_name":"Leingärtner","first_name":"Axel"},{"first_name":"Carl-Philipp J","id":"39427864-F248-11E8-B48F-1D18A9856A87","last_name":"Heisenberg","full_name":"Heisenberg, Carl-Philipp J","orcid":"0000-0002-0912-4566"},{"full_name":"Kolbeck, Roland","first_name":"Roland","last_name":"Kolbeck"},{"first_name":"Hans","last_name":"Thoenen","full_name":"Thoenen, Hans"},{"first_name":"Dan","last_name":"Lindholm","full_name":"Lindholm, Dan"}],"oa_version":"None","date_created":"2018-12-11T12:07:25Z","publication":"Journal of Biological Chemistry","_id":"4179","issue":"2","type":"journal_article","article_processing_charge":"No","title":"Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar granule neurons","volume":269,"status":"public","day":"14","scopus_import":"1","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0021925817421867?via%3Dihub","open_access":"1"}],"publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"1941","date_updated":"2022-06-02T10:23:48Z","publisher":"American Society for Biochemistry and Molecular Biology","article_type":"original","month":"01","date_published":"1994-01-14T00:00:00Z"},{"day":"12","title":"NMDA potentiates NGF-induced sprouting of septal cholinergic fibres","volume":5,"status":"public","date_created":"2018-12-11T12:07:33Z","oa_version":"None","type":"journal_article","_id":"4202","article_processing_charge":"No","issue":"4","publication":"Neuroreport","author":[{"orcid":"0000-0002-0912-4566","full_name":"Heisenberg, Carl-Philipp J","id":"39427864-F248-11E8-B48F-1D18A9856A87","first_name":"Carl-Philipp J","last_name":"Heisenberg"},{"full_name":"Cooper, John","first_name":"John","last_name":"Cooper"},{"full_name":"Berke, J","last_name":"Berke","first_name":"J"},{"full_name":"Sofroniew, Michael","first_name":"Michael","last_name":"Sofroniew"}],"date_published":"1994-01-12T00:00:00Z","month":"01","article_type":"original","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publisher":"Lippincott, Williams & Wilkins","publist_id":"1915","date_updated":"2022-06-02T10:07:25Z","main_file_link":[{"url":"https://journals.lww.com/neuroreport/Abstract/1994/01120/NMDA_potentiates_NGF_induced_sprouting_of_septal.10.aspx"}],"scopus_import":"1","year":"1994","publication_identifier":{"issn":["0959-4965"]},"language":[{"iso":"eng"}],"intvolume":"         5","doi":"10.1097/00001756-199401120-00010 ","citation":{"ama":"Heisenberg C-PJ, Cooper J, Berke J, Sofroniew M. NMDA potentiates NGF-induced sprouting of septal cholinergic fibres. <i>Neuroreport</i>. 1994;5(4):413-416. doi:<a href=\"https://doi.org/10.1097/00001756-199401120-00010 \">10.1097/00001756-199401120-00010 </a>","apa":"Heisenberg, C.-P. J., Cooper, J., Berke, J., &#38; Sofroniew, M. (1994). NMDA potentiates NGF-induced sprouting of septal cholinergic fibres. <i>Neuroreport</i>. Lippincott, Williams &#38; Wilkins. <a href=\"https://doi.org/10.1097/00001756-199401120-00010 \">https://doi.org/10.1097/00001756-199401120-00010 </a>","chicago":"Heisenberg, Carl-Philipp J, John Cooper, J Berke, and Michael Sofroniew. “NMDA Potentiates NGF-Induced Sprouting of Septal Cholinergic Fibres.” <i>Neuroreport</i>. Lippincott, Williams &#38; Wilkins, 1994. <a href=\"https://doi.org/10.1097/00001756-199401120-00010 \">https://doi.org/10.1097/00001756-199401120-00010 </a>.","short":"C.-P.J. Heisenberg, J. Cooper, J. Berke, M. Sofroniew, Neuroreport 5 (1994) 413–416.","ieee":"C.-P. J. Heisenberg, J. Cooper, J. Berke, and M. Sofroniew, “NMDA potentiates NGF-induced sprouting of septal cholinergic fibres,” <i>Neuroreport</i>, vol. 5, no. 4. Lippincott, Williams &#38; Wilkins, pp. 413–416, 1994.","ista":"Heisenberg C-PJ, Cooper J, Berke J, Sofroniew M. 1994. NMDA potentiates NGF-induced sprouting of septal cholinergic fibres. Neuroreport. 5(4), 413–416.","mla":"Heisenberg, Carl-Philipp J., et al. “NMDA Potentiates NGF-Induced Sprouting of Septal Cholinergic Fibres.” <i>Neuroreport</i>, vol. 5, no. 4, Lippincott, Williams &#38; Wilkins, 1994, pp. 413–16, doi:<a href=\"https://doi.org/10.1097/00001756-199401120-00010 \">10.1097/00001756-199401120-00010 </a>."},"quality_controlled":"1","extern":"1","abstract":[{"lang":"eng","text":"NERVE growth factor (NGF) injected into the otherwise unlesioned adult rat septum induced sprouting of presumptive cholinergic fibres positive for p75(NGFR) and acetylcholinesterase (AChE). These fibres did not stain for tyrosine hydroxylase and therefore did not represent sympathetic ingrowth. Neurofilament staining on adjacent sections revealed fibres with similar morphology, suggesting new outgrowth in the form of sprouting rather than the upregulation of p75(NGFR) and AChE in pre-existing fibres. Simultaneous injections of subneurotoxic doses of N-methyl-D-aspartate (NMDA) significantly potentiated the effect of NGF on cholinergic fibre sprouting and caused pronounced glial fibrillary acidic protein (GFAP)positive astrocytosis. Application of NMDA alone did not elicit sprouting of this type. These findings indicate that NGF can induce the sprouting of uninjured adult rat septal cholinergic fibres in vivo and suggest that reactive astrocytes are not inhibitory to cholinergic axonal outgrowth, and might serve as a substrate for growing axons in the presence of NGF."}],"page":"413 - 416"},{"abstract":[{"lang":"eng","text":"We propose a methodology for the specification, verification, and design of hybrid systems. The methodology consists of the computational model of Concrete Phase Transition Systems (cptss), the specification language of Hybrid Temporal Logic (htl), the graphical system description language of Hybrid Automata, and a proof system for verifying that hybrid automata satisfy their HTL specifications. The novelty of the approach lies in the continuous-time logic, which allows specification of both point-based and interval-based properties (i.e., properties which describe changes over an interval) and provides direct references to derivatives of variables, and in the proof system that supports verification of point-based and interval-based properties. The proof rules demonstrate that sound and convenient induction rules can be established for continuous-time logics. The proof rules are illustrated on several examples."}],"alternative_title":["LNCS"],"page":"431 - 454","language":[{"iso":"eng"}],"year":"1994","intvolume":"       863","extern":"1","citation":{"ista":"Kapur A, Henzinger TA, Manna Z, Pnueli A. 1994. Proving safety properties of hybrid systems. 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 863, 431–454.","ieee":"A. Kapur, T. A. Henzinger, Z. Manna, and A. Pnueli, “Proving safety properties of hybrid systems,” in <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, Lübeck, Germany, 1994, vol. 863, pp. 431–454.","mla":"Kapur, Arjun, et al. “Proving Safety Properties of Hybrid Systems.” <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, vol. 863, Springer, 1994, pp. 431–54, doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_177\">10.1007/3-540-58468-4_177</a>.","apa":"Kapur, A., Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1994). Proving safety properties of hybrid systems. In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i> (Vol. 863, pp. 431–454). Lübeck, Germany: Springer. <a href=\"https://doi.org/10.1007/3-540-58468-4_177\">https://doi.org/10.1007/3-540-58468-4_177</a>","short":"A. Kapur, T.A. Henzinger, Z. Manna, A. Pnueli, in:, 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1994, pp. 431–454.","chicago":"Kapur, Arjun, Thomas A Henzinger, Zohar Manna, and Amir Pnueli. “Proving Safety Properties of Hybrid Systems.” In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, 863:431–54. Springer, 1994. <a href=\"https://doi.org/10.1007/3-540-58468-4_177\">https://doi.org/10.1007/3-540-58468-4_177</a>.","ama":"Kapur A, Henzinger TA, Manna Z, Pnueli A. Proving safety properties of hybrid systems. In: <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>. Vol 863. Springer; 1994:431-454. doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_177\">10.1007/3-540-58468-4_177</a>"},"doi":"10.1007/3-540-58468-4_177","quality_controlled":"1","conference":{"location":"Lübeck, Germany","end_date":"1994-09-23","start_date":"1994-09-19","name":"FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems"},"acknowledgement":"Supported in part by the National Science Foundation under grants CCR-92-23226 and CCR-9200794, by the Defense Advanced Research Projects Agency under grants NAG2-703 and NAG2-892, by the United States Air Force Office of Scientific Research under contracts F49620-93-1-0139 and F49620-93-1-0056, and by the European Community ESPRIT Basic Research Action Project 6021 (REACT). Supported in part by a National Science Foundation Graduate Research Fellowship.","date_published":"1994-01-01T00:00:00Z","month":"01","publisher":"Springer","date_updated":"2022-06-02T09:46:37Z","publist_id":"309","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-58468-4_177"}],"scopus_import":"1","day":"01","status":"public","volume":863,"title":"Proving safety properties of hybrid systems","_id":"4420","article_processing_charge":"No","type":"conference","publication":"3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","date_created":"2018-12-11T12:08:46Z","oa_version":"None","author":[{"first_name":"Arjun","last_name":"Kapur","full_name":"Kapur, Arjun"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Zohar","last_name":"Manna","full_name":"Manna, Zohar"},{"full_name":"Pnueli, Amir","last_name":"Pnueli","first_name":"Amir"}]},{"acknowledgement":"Supported in part by the National Science Foundation under grant CCR-9200794, by the United States Air Force Office of Scientific Research under contract F49620- 93-1-0056, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","conference":{"name":"FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems","end_date":"1994-09-23","start_date":"1994-09-19","location":"Lübeck, Gernany"},"quality_controlled":"1","doi":"10.1007/3-540-58468-4_173","citation":{"apa":"Henzinger, T. A., &#38; Kopke, P. (1994). Verification methods for the divergent runs of clock systems. In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i> (Vol. 863, pp. 351–372). Lübeck, Gernany: Springer. <a href=\"https://doi.org/10.1007/3-540-58468-4_173\">https://doi.org/10.1007/3-540-58468-4_173</a>","short":"T.A. Henzinger, P. Kopke, in:, 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1994, pp. 351–372.","chicago":"Henzinger, Thomas A, and Peter Kopke. “Verification Methods for the Divergent Runs of Clock Systems.” In <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, 863:351–72. Springer, 1994. <a href=\"https://doi.org/10.1007/3-540-58468-4_173\">https://doi.org/10.1007/3-540-58468-4_173</a>.","ista":"Henzinger TA, Kopke P. 1994. Verification methods for the divergent runs of clock systems. 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 863, 351–372.","ieee":"T. A. Henzinger and P. Kopke, “Verification methods for the divergent runs of clock systems,” in <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, Lübeck, Gernany, 1994, vol. 863, pp. 351–372.","mla":"Henzinger, Thomas A., and Peter Kopke. “Verification Methods for the Divergent Runs of Clock Systems.” <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, vol. 863, Springer, 1994, pp. 351–72, doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_173\">10.1007/3-540-58468-4_173</a>.","ama":"Henzinger TA, Kopke P. Verification methods for the divergent runs of clock systems. In: <i>3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>. Vol 863. Springer; 1994:351-372. doi:<a href=\"https://doi.org/10.1007/3-540-58468-4_173\">10.1007/3-540-58468-4_173</a>"},"extern":"1","intvolume":"       863","year":"1994","language":[{"iso":"eng"}],"alternative_title":["LNCS"],"page":"351 - 372","abstract":[{"text":"We present a methodology for proving temporal properties of the divergent runs of reactive systems with real-valued clocks. A run diverges if time advances beyond any bound. Since the divergent runs of a system may satisfy liveness properties that are not satisfied by some convergent runs, the standard proof rules are incomplete if only divergent runs are considered. First, we develop a sound and complete proof calculus for divergence, which is based on translating clock systems into discrete systems. Then, we show that simpler proofs can be obtained for stronger divergence assumptions, such as unknown -divergence, which requires that all delays have a minimum duration of some unknown constant . We classify all real-time systems into an infinite hierarchy, according to how well they admit the translation of eventuality properties into equivalent safety properties.","lang":"eng"}],"author":[{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Kopke","first_name":"Peter","full_name":"Kopke, Peter"}],"date_created":"2018-12-11T12:08:52Z","oa_version":"None","publication":"3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","article_processing_charge":"No","_id":"4440","type":"conference","title":"Verification methods for the divergent runs of clock systems","volume":863,"status":"public","day":"01","scopus_import":"1","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-58468-4_173"}],"publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"287","date_updated":"2022-06-02T09:35:58Z","publisher":"Springer","date_published":"1994-01-01T00:00:00Z","month":"01"},{"article_type":"original","date_published":"1994-08-01T00:00:00Z","month":"08","publist_id":"227","date_updated":"2022-06-02T09:24:58Z","publisher":"Elsevier","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub"}],"scopus_import":"1","day":"01","status":"public","title":"Temporal proof methodologies for timed transition systems","volume":112,"publication":"Information and Computation","_id":"4501","article_processing_charge":"No","type":"journal_article","issue":"2","oa_version":"None","date_created":"2018-12-11T12:09:10Z","author":[{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"},{"last_name":"Manna","first_name":"Zohar","full_name":"Manna, Zohar"},{"last_name":"Pnueli","first_name":"Amir","full_name":"Pnueli, Amir"}],"abstract":[{"lang":"eng","text":"We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-;time properties of reactive systems. The abstract notion of timed transition systems generalizes traditional transition systems conservatively: qualitative fairness requirements are replaced (and superseded) by quantitative lower-bound and upper-bound timing constraints on transitions. This framework can model real-time systems that communicate either through shared variables or by message passing and real-time issues such as timeouts, process priorities (interrupts), and process scheduling. We exhibit two styles for the specification of real-time systems. While the first approach uses time-bounded versions of the temporal operators, the second approach allows explicit references to time through a special clock variable. Corresponding to the two styles of specification, we present and compare two different proof methodologies for the verification of timing requirements that are expressed in these styles. For the bounded-operator style, we provide a set of proof rules for establishing bounded-invariance and bounded-responce properties of timed transition systems. This approach generalizes the standard temporal proof rules for verifying invariance and response properties conservatively. For the explicit-clock style, we exploit the observation that every time-bounded property is a safety property and use the standard temporal proof rules for establishing safety properties."}],"oa":1,"page":"273 - 337","publication_identifier":{"issn":["0890-5401"]},"language":[{"iso":"eng"}],"year":"1994","intvolume":"       112","extern":"1","quality_controlled":"1","doi":"10.1006/inco.1994.1060","citation":{"ama":"Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. 1994;112(2):273-337. doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>","apa":"Henzinger, T. A., Manna, Z., &#38; Pnueli, A. (1994). Temporal proof methodologies for timed transition systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>","chicago":"Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1060\">https://doi.org/10.1006/inco.1994.1060</a>.","short":"T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994) 273–337.","ista":"Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed transition systems. Information and Computation. 112(2), 273–337.","ieee":"T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for timed transition systems,” <i>Information and Computation</i>, vol. 112, no. 2. Elsevier, pp. 273–337, 1994.","mla":"Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition Systems.” <i>Information and Computation</i>, vol. 112, no. 2, Elsevier, 1994, pp. 273–337, doi:<a href=\"https://doi.org/10.1006/inco.1994.1060\">10.1006/inco.1994.1060</a>."},"acknowledgement":"This research was supported in part by an IBM graduate fellowship, by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139 and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium on Principles of Programming Languages RIMP911. "},{"date_published":"1994-06-01T00:00:00Z","month":"06","article_type":"original","publisher":"Elsevier","date_updated":"2022-06-02T09:02:02Z","publist_id":"226","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub"}],"scopus_import":"1","day":"01","status":"public","volume":111,"title":"Symbolic model checking for real-time systems","type":"journal_article","_id":"4503","issue":"2","article_processing_charge":"No","publication":"Information and Computation","oa_version":"None","date_created":"2018-12-11T12:09:11Z","author":[{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"},{"full_name":"Nicollin, Xavier","first_name":"Xavier","last_name":"Nicollin"},{"full_name":"Sifakis, Joseph","last_name":"Sifakis","first_name":"Joseph"},{"last_name":"Yovine","first_name":"Sergio","full_name":"Yovine, Sergio"}],"abstract":[{"text":"We describe finite-state programs over real-numbered time in a guarded-command language with real-valued clocks or, equivalently, as finite automata with real-valued clocks. Model checking answers the question which states of a real-time program satisfy a branching-time specification (given in an extension of CTL with clock variables). We develop an algorithm that computes this set of states symbolically as a fixpoint of a functional on state predicates, without constructing the state space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered time. Unfortunately, many standard program properties, such as response for all nonzeno execution sequences (during which time diverges), cannot be characterized by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable to the expressiveness of timed CTL. Fortunately, this result does not impair the symbolic verification of &quot;implementable&quot; real-time programs-those whose safety constraints are machine-closed with respect to diverging time and whose fairness constraints are restricted to finite upper bounds on clock values. All timed CTL properties of such programs are shown to be computable as finitely approximable fixpoints in a simple decidable theory.","lang":"eng"}],"page":"193 - 244","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0890-5401"]},"year":"1994","intvolume":"       111","extern":"1","doi":"10.1006/inco.1994.1045","citation":{"chicago":"Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>.","short":"T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation 111 (1994) 193–244.","apa":"Henzinger, T. A., Nicollin, X., Sifakis, J., &#38; Yovine, S. (1994). Symbolic model checking for real-time systems. <i>Information and Computation</i>. Elsevier. <a href=\"https://doi.org/10.1006/inco.1994.1045\">https://doi.org/10.1006/inco.1994.1045</a>","mla":"Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.” <i>Information and Computation</i>, vol. 111, no. 2, Elsevier, 1994, pp. 193–244, doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>.","ieee":"T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking for real-time systems,” <i>Information and Computation</i>, vol. 111, no. 2. Elsevier, pp. 193–244, 1994.","ista":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking for real-time systems. Information and Computation. 111(2), 193–244.","ama":"Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for real-time systems. <i>Information and Computation</i>. 1994;111(2):193-244. doi:<a href=\"https://doi.org/10.1006/inco.1994.1045\">10.1006/inco.1994.1045</a>"},"quality_controlled":"1","acknowledgement":"We thank Peter Kopke for a careful reading."},{"publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-02T08:45:57Z","publist_id":"119","publisher":"IEEE","abstract":[{"text":"Fairness is a mathematical abstraction: in a multiprogramming environment, fairness abstracts the details of admissible (“fair”) schedulers; in a distributed environment, fairness abstracts the speeds of independent processors. We argue that the standard definition of fairness often is unnecessarily weak and can be replaced by the stronger, yet still abstract, notion of finitary fairness. While standard weak fairness requires that no enabled transition is postponed forever, finitary weak fairness requires that for every run of a system there is an unknown bound k such that no enabled transition is postponed more than k consecutive times. In general, the finitary restriction fin(F) of any given fairness assumption F is the union of all w-regular safety properties that are contained in F. The adequacy of the proposed abstraction is demonstrated in two ways. Suppose that we prove a program property under the assumption of finitary fairness. In a multiprogramming environment, the program then satisfies the property for all fair finite-state schedulers. In a distributed environment, the program then satisfies the property for all choices of lower and upper bounds on the speeds (or timings) of processors","lang":"eng"}],"date_published":"1994-01-01T00:00:00Z","month":"01","scopus_import":"1","page":"52 - 61","main_file_link":[{"url":"https://ieeexplore.ieee.org/document/316087"}],"title":"Finitary fairness","status":"public","year":"1994","day":"01","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0018-9162"]},"author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"conference":{"location":"Paris, France","end_date":"\t1994-07-07","start_date":"1994-07-04","name":"LICS: Logic in Computer Science"},"quality_controlled":"1","oa_version":"None","date_created":"2018-12-11T12:09:37Z","doi":"10.1109/LICS.1994.316087 ","citation":{"ieee":"R. Alur and T. A. Henzinger, “Finitary fairness,” in <i>Proceedings 9th Annual IEEE Symposium on Logic in Computer Science</i>, Paris, France, 1994, pp. 52–61.","ista":"Alur R, Henzinger TA. 1994. Finitary fairness. Proceedings 9th Annual IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 52–61.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Finitary Fairness.” <i>Proceedings 9th Annual IEEE Symposium on Logic in Computer Science</i>, IEEE, 1994, pp. 52–61, doi:<a href=\"https://doi.org/10.1109/LICS.1994.316087 \">10.1109/LICS.1994.316087 </a>.","apa":"Alur, R., &#38; Henzinger, T. A. (1994). Finitary fairness. In <i>Proceedings 9th Annual IEEE Symposium on Logic in Computer Science</i> (pp. 52–61). Paris, France: IEEE. <a href=\"https://doi.org/10.1109/LICS.1994.316087 \">https://doi.org/10.1109/LICS.1994.316087 </a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Finitary Fairness.” In <i>Proceedings 9th Annual IEEE Symposium on Logic in Computer Science</i>, 52–61. IEEE, 1994. <a href=\"https://doi.org/10.1109/LICS.1994.316087 \">https://doi.org/10.1109/LICS.1994.316087 </a>.","short":"R. Alur, T.A. Henzinger, in:, Proceedings 9th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1994, pp. 52–61.","ama":"Alur R, Henzinger TA. Finitary fairness. In: <i>Proceedings 9th Annual IEEE Symposium on Logic in Computer Science</i>. IEEE; 1994:52-61. doi:<a href=\"https://doi.org/10.1109/LICS.1994.316087 \">10.1109/LICS.1994.316087 </a>"},"extern":"1","publication":"Proceedings 9th Annual IEEE Symposium on Logic in Computer Science","_id":"4586","type":"conference","article_processing_charge":"No"},{"status":"public","title":"Real-time system = discrete system + clock variables","volume":2,"day":"01","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}],"_id":"4590","article_processing_charge":"No","type":"book_chapter","publication":"Theories and Experiences for Real-Time System Development","oa_version":"None","date_created":"2018-12-11T12:09:38Z","publisher":"World Scientific Publishing","date_updated":"2022-06-02T08:07:57Z","publist_id":"117","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","date_published":"1994-01-01T00:00:00Z","month":"01","series_title":"AMAST Series in Computing","main_file_link":[{"url":"https://link.springer.com/article/10.1007/s100090050007"}],"intvolume":"         2","language":[{"iso":"eng"}],"publication_identifier":{"isbn":[" 9789810219239"]},"year":"1994","acknowledgement":"The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.","extern":"1","doi":"10.1142/9789812831583_0001","citation":{"ama":"Alur R, Henzinger TA. Real-time system = discrete system + clock variables. In: Rus T, Rattray C, eds. <i>Theories and Experiences for Real-Time System Development</i>. Vol 2. AMAST Series in Computing. World Scientific Publishing; 1994:1-29. doi:<a href=\"https://doi.org/10.1142/9789812831583_0001\">10.1142/9789812831583_0001</a>","ista":"Alur R, Henzinger TA. 1994.Real-time system = discrete system + clock variables. In: Theories and Experiences for Real-Time System Development. AMAST Series in Computing, vol. 2, 1–29.","ieee":"R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,” in <i>Theories and Experiences for Real-Time System Development</i>, vol. 2, T. Rus and C. Rattray, Eds. World Scientific Publishing, 1994, pp. 1–29.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Theories and Experiences for Real-Time System Development</i>, edited by Teodor Rus and Charles Rattray, vol. 2, World Scientific Publishing, 1994, pp. 1–29, doi:<a href=\"https://doi.org/10.1142/9789812831583_0001\">10.1142/9789812831583_0001</a>.","apa":"Alur, R., &#38; Henzinger, T. A. (1994). Real-time system = discrete system + clock variables. In T. Rus &#38; C. Rattray (Eds.), <i>Theories and Experiences for Real-Time System Development</i> (Vol. 2, pp. 1–29). World Scientific Publishing. <a href=\"https://doi.org/10.1142/9789812831583_0001\">https://doi.org/10.1142/9789812831583_0001</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System + Clock Variables.” In <i>Theories and Experiences for Real-Time System Development</i>, edited by Teodor Rus and Charles Rattray, 2:1–29. AMAST Series in Computing. World Scientific Publishing, 1994. <a href=\"https://doi.org/10.1142/9789812831583_0001\">https://doi.org/10.1142/9789812831583_0001</a>.","short":"R. Alur, T.A. Henzinger, in:, T. Rus, C. Rattray (Eds.), Theories and Experiences for Real-Time System Development, World Scientific Publishing, 1994, pp. 1–29."},"quality_controlled":"1","keyword":["real-time systems","clock variables"],"abstract":[{"text":"We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the &quot;freeze&quot; quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.","lang":"eng"}],"page":"1 - 29","alternative_title":["AMAST Series in Computing"],"editor":[{"last_name":"Rus","first_name":"Teodor","full_name":"Rus, Teodor"},{"full_name":"Rattray, Charles","first_name":"Charles","last_name":"Rattray"}]},{"extern":"1","citation":{"ieee":"R. Alur and T. A. Henzinger, “A really temporal logic,” <i>Journal of the ACM</i>, vol. 41, no. 1. ACM, pp. 181–204, 1994.","ista":"Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1), 181–204.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “A Really Temporal Logic.” <i>Journal of the ACM</i>, vol. 41, no. 1, ACM, 1994, pp. 181–204, doi:<a href=\"https://doi.org/10.1145/174644.174651\">10.1145/174644.174651</a>.","apa":"Alur, R., &#38; Henzinger, T. A. (1994). A really temporal logic. <i>Journal of the ACM</i>. ACM. <a href=\"https://doi.org/10.1145/174644.174651\">https://doi.org/10.1145/174644.174651</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” <i>Journal of the ACM</i>. ACM, 1994. <a href=\"https://doi.org/10.1145/174644.174651\">https://doi.org/10.1145/174644.174651</a>.","short":"R. Alur, T.A. Henzinger, Journal of the ACM 41 (1994) 181–204.","ama":"Alur R, Henzinger TA. A really temporal logic. <i>Journal of the ACM</i>. 1994;41(1):181-204. doi:<a href=\"https://doi.org/10.1145/174644.174651\">10.1145/174644.174651</a>"},"doi":"10.1145/174644.174651","quality_controlled":"1","acknowledgement":"We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance. Moshe Vardi and Joe Halpern gave us very helpful advice for refining our undecidability results; in particular, they pointed out to us the completeness of a problem on Turing machines.\r\n","publication_identifier":{"issn":["0004-5411"]},"language":[{"iso":"eng"}],"year":"1994","intvolume":"        41","page":"181 - 204","abstract":[{"lang":"eng","text":"We introduce a temporal logic for the specification of real-time systems. Our logic, TPTL, employs a novel quantifier construct for referencing time: the freeze quantifier binds a variable to the time of the local temporal context. TPTL is both a natural language for specification and a suitable formalism for verification. We present a tableau-based decision procedure and a model-checking algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable."}],"_id":"4591","issue":"1","type":"journal_article","article_processing_charge":"No","publication":"Journal of the ACM","oa_version":"None","date_created":"2018-12-11T12:09:38Z","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger"}],"day":"01","status":"public","title":"A really temporal logic","volume":41,"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/174644.174651"}],"scopus_import":"1","date_published":"1994-01-01T00:00:00Z","month":"01","article_type":"original","publisher":"ACM","publist_id":"118","date_updated":"2022-06-02T08:23:46Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published"},{"conference":{"name":"CONCUR: Concurrency Theory","end_date":"1994-08-25","start_date":"1994-08-22","location":"Uppsala, Sweden"},"acknowledgement":"ESPRIT BRA project REACT, National Science Foundation under grant CCR-9200794,  United States Air Force Office of Scientific Research contract F49620-93-1-0056","citation":{"chicago":"Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “The Observational Power of Clocks.” In <i>5th International Conference on Concurrency Theory</i>, 836:162–77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994. <a href=\"https://doi.org/10.1007/BFb0015008\">https://doi.org/10.1007/BFb0015008</a>.","short":"R. Alur, C. Courcoubetis, T.A. Henzinger, in:, 5th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994, pp. 162–177.","apa":"Alur, R., Courcoubetis, C., &#38; Henzinger, T. A. (1994). The observational power of clocks. In <i>5th International Conference on Concurrency Theory</i> (Vol. 836, pp. 162–177). Uppsala, Sweden: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0015008\">https://doi.org/10.1007/BFb0015008</a>","mla":"Alur, Rajeev, et al. “The Observational Power of Clocks.” <i>5th International Conference on Concurrency Theory</i>, vol. 836, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994, pp. 162–77, doi:<a href=\"https://doi.org/10.1007/BFb0015008\">10.1007/BFb0015008</a>.","ista":"Alur R, Courcoubetis C, Henzinger TA. 1994. The observational power of clocks. 5th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 836, 162–177.","ieee":"R. Alur, C. Courcoubetis, and T. A. Henzinger, “The observational power of clocks,” in <i>5th International Conference on Concurrency Theory</i>, Uppsala, Sweden, 1994, vol. 836, pp. 162–177.","ama":"Alur R, Courcoubetis C, Henzinger TA. The observational power of clocks. In: <i>5th International Conference on Concurrency Theory</i>. Vol 836. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1994:162-177. doi:<a href=\"https://doi.org/10.1007/BFb0015008\">10.1007/BFb0015008</a>"},"doi":"10.1007/BFb0015008","quality_controlled":"1","extern":"1","intvolume":"       836","year":"1994","publication_identifier":{"isbn":["3540583297"]},"language":[{"iso":"eng"}],"page":"162 - 177","alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"We develop a theory of equivalences for timed systems. Two systems are equivalent iff external observers cannot observe differences in their behavior. The notion of equivalence depends, therefore, on the distinguishing power of the observers. The power of an observer to measure time results in untimed, clock, and timed equivalences: an untimed observer cannot measure the time difference between events; a clock observer uses a clock to measure time differences with finite precision; a timed observer is able to measure time differences with arbitrary precision.\r\nWe show that the distinguishing power of clock observers grows with the number of observers, and approaches, in the limit, the distinguishing power of a timed observer. More precisely, given any equivalence for untimed systems, two timed systems are k-clock congruent, for a nonnegative integer k, iff their compositions with every environment that uses k clocks are untimed equivalent. Both k-clock bisimulation congruence and k-clock trace congruence form strict decidable hierarchies that converge towards the corresponding timed equivalences. Moreover, k-clock bisimulation congruence and k-clock trace congruence provide an adequate and abstract semantics for branching-time and linear-time logics with k clocks.\r\nOur results impact on the verification of timed systems in two ways. First, our decision procedure for k-clock bisimulation congruence leads to a new, symbolic, decision procedure for timed bisimilarity. Second, timed trace equivalence is known to be undecidable. If the number of environment clocks is bounded, however, then our decision procedure for k-clock trace congruence allows the verification of timed systems in a trace model."}],"author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"full_name":"Courcoubetis, Costas","first_name":"Costas","last_name":"Courcoubetis"},{"orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"oa_version":"None","date_created":"2018-12-11T12:09:46Z","article_processing_charge":"No","_id":"4614","type":"conference","publication":"5th International Conference on Concurrency Theory","volume":836,"title":"The observational power of clocks","status":"public","day":"01","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/BFb0015008"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publist_id":"93","date_updated":"2022-06-02T07:41:46Z","date_published":"1994-01-01T00:00:00Z","month":"01"},{"abstract":[{"text":"We introduce the class of event- recording timed automata (ERA). An event-recording automaton contains, for every event a, a clock that records the time of the last occurrence of a. The class ERA is, on one hand, expressive enough to model (finite) timed transition systems and, on the other hand, determinizable and closed under all boolean operations. As a result, the language inclusion problem is decidable for event-recording automata. We present a translation from timed transition systems to event-recording automata, which leads to an algorithm for checking if two timed transition systems have the same set of timed behaviors. We also consider event-predicting timed automata (EPA), which contain clocks that predict the time of the next occurrence of an event. The class of event-clock automata (ECA), which contain both event-recording and event-predicting clocks, is a suitable specification language for real-time properties. We provide an algorithm for checking if a timed automaton meets a specification that is given as an event-clock automaton.","lang":"eng"}],"alternative_title":["LNCS"],"page":"1 - 13","intvolume":"       818","year":"1994","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783540484691"]},"acknowledgement":"Supported in part by the Office of Naval Research under contract N00014-91-J-1219, the National Science Foundation under grant CCR-8701103, and by DARPA/NSF under grant CCR-9014363.\r\nSupported in part by the National Science Foundation under grant CCR-9200794 and by the United States Air Force Office of Scientific Research under contract F49620-93-1-0056.","conference":{"name":"CAV: Computer Aided Verification","end_date":"1994-06-23","start_date":"1994-06-21","location":"Stanford, CA, United States of America"},"quality_controlled":"1","doi":"10.1007/3-540-58179-0_39","citation":{"ista":"Alur R, Fix L, Henzinger TA. 1994. A determinizable class of timed automata. International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 818, 1–13.","ieee":"R. Alur, L. Fix, and T. A. Henzinger, “A determinizable class of timed automata,” in <i>International Conference on Computer Aided Verification</i>, Stanford, CA, United States of America, 1994, vol. 818, pp. 1–13.","mla":"Alur, Rajeev, et al. “A Determinizable Class of Timed Automata.” <i>International Conference on Computer Aided Verification</i>, vol. 818, Springer, 1994, pp. 1–13, doi:<a href=\"https://doi.org/10.1007/3-540-58179-0_39\">10.1007/3-540-58179-0_39</a>.","apa":"Alur, R., Fix, L., &#38; Henzinger, T. A. (1994). A determinizable class of timed automata. In <i>International Conference on Computer Aided Verification</i> (Vol. 818, pp. 1–13). Stanford, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-58179-0_39\">https://doi.org/10.1007/3-540-58179-0_39</a>","short":"R. Alur, L. Fix, T.A. Henzinger, in:, International Conference on Computer Aided Verification, Springer, 1994, pp. 1–13.","chicago":"Alur, Rajeev, Limor Fix, and Thomas A Henzinger. “A Determinizable Class of Timed Automata.” In <i>International Conference on Computer Aided Verification</i>, 818:1–13. Springer, 1994. <a href=\"https://doi.org/10.1007/3-540-58179-0_39\">https://doi.org/10.1007/3-540-58179-0_39</a>.","ama":"Alur R, Fix L, Henzinger TA. A determinizable class of timed automata. In: <i>International Conference on Computer Aided Verification</i>. Vol 818. Springer; 1994:1-13. doi:<a href=\"https://doi.org/10.1007/3-540-58179-0_39\">10.1007/3-540-58179-0_39</a>"},"extern":"1","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publist_id":"92","date_updated":"2022-06-01T14:37:25Z","publisher":"Springer","date_published":"1994-01-01T00:00:00Z","month":"01","scopus_import":"1","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-58179-0_39"}],"title":"A determinizable class of timed automata","volume":818,"status":"public","day":"01","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"Fix","first_name":"Limor","full_name":"Fix, Limor"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724"}],"date_created":"2018-12-11T12:09:46Z","oa_version":"None","publication":"International Conference on Computer Aided Verification","_id":"4615","article_processing_charge":"No","type":"conference"},{"abstract":[{"text":"We extend the timed-automaton model for real-time systems [AD90] to a formal model for hybrid systems: while the continuous variables of a timed automaton are clocks that measure time, the continuous variables of a hybrid system are governed by arbitrary differential equations. We then adopt the verification methodology for timed automata [ACD90, ACD+92, HNSY92] to analyze hybrid systems: while the verification problem is decidable for timed automata, we obtain semidecision procedures for the class of hybrid systems whose continuous variables change in a piecewise linear fashion. ","lang":"eng"}],"alternative_title":["LNCIS"],"page":"331 - 351","intvolume":"       199","year":"1994","publication_identifier":{"isbn":["978-3-540-19896-3"]},"language":[{"iso":"eng"}],"conference":{"name":"ICAOS: Analysis and Optimization of Systems - Discrete-Event Systems","end_date":"1994-06-17","start_date":"1994-06-15","location":"Sophia-Antipolis, France"},"citation":{"chicago":"Alur, Rajeev, Costas Courcoubetis, Thomas A Henzinger, Pei Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis of Hybrid Systems.” In <i>11th International Conference on Analysis and Optimization of Systems Discrete Event Systems</i>, 199:331–51. Springer, 1994. <a href=\"https://doi.org/10.1007/BFb0033565\">https://doi.org/10.1007/BFb0033565</a>.","short":"R. Alur, C. Courcoubetis, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, in:, 11th International Conference on Analysis and Optimization of Systems Discrete Event Systems, Springer, 1994, pp. 331–351.","apa":"Alur, R., Courcoubetis, C., Henzinger, T. A., Ho, P., Nicollin, X., Olivero, A., … Yovine, S. (1994). The algorithmic analysis of hybrid systems. In <i>11th International Conference on Analysis and Optimization of Systems Discrete Event Systems</i> (Vol. 199, pp. 331–351). Sophia-Antipolis, France: Springer. <a href=\"https://doi.org/10.1007/BFb0033565\">https://doi.org/10.1007/BFb0033565</a>","mla":"Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” <i>11th International Conference on Analysis and Optimization of Systems Discrete Event Systems</i>, vol. 199, Springer, 1994, pp. 331–51, doi:<a href=\"https://doi.org/10.1007/BFb0033565\">10.1007/BFb0033565</a>.","ieee":"R. Alur <i>et al.</i>, “The algorithmic analysis of hybrid systems,” in <i>11th International Conference on Analysis and Optimization of Systems Discrete Event Systems</i>, Sophia-Antipolis, France, 1994, vol. 199, pp. 331–351.","ista":"Alur R, Courcoubetis C, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis J, Yovine S. 1994. The algorithmic analysis of hybrid systems. 11th International Conference on Analysis and Optimization of Systems Discrete Event Systems. ICAOS: Analysis and Optimization of Systems - Discrete-Event Systems, LNCIS, vol. 199, 331–351.","ama":"Alur R, Courcoubetis C, Henzinger TA, et al. The algorithmic analysis of hybrid systems. In: <i>11th International Conference on Analysis and Optimization of Systems Discrete Event Systems</i>. Vol 199. Springer; 1994:331-351. doi:<a href=\"https://doi.org/10.1007/BFb0033565\">10.1007/BFb0033565</a>"},"doi":"10.1007/BFb0033565","quality_controlled":"1","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publisher":"Springer","publist_id":"91","date_updated":"2022-06-01T14:14:31Z","month":"01","date_published":"1994-01-01T00:00:00Z","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/BFb0033565"}],"volume":199,"title":"The algorithmic analysis of hybrid systems","status":"public","day":"01","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"Courcoubetis","first_name":"Costas","full_name":"Courcoubetis, Costas"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A"},{"full_name":"Ho, Pei","last_name":"Ho","first_name":"Pei"},{"first_name":"Xavier","last_name":"Nicollin","full_name":"Nicollin, Xavier"},{"full_name":"Olivero, Alfredo","last_name":"Olivero","first_name":"Alfredo"},{"first_name":"Joseph","last_name":"Sifakis","full_name":"Sifakis, Joseph"},{"first_name":"Sergio","last_name":"Yovine","full_name":"Yovine, Sergio"}],"date_created":"2018-12-11T12:09:46Z","oa_version":"None","article_processing_charge":"No","type":"conference","_id":"4617","publication":"11th International Conference on Analysis and Optimization of Systems Discrete Event Systems"},{"year":"1994","publication_identifier":{"issn":["0306-4522"]},"language":[{"iso":"eng"}],"pmid":1,"intvolume":"        60","citation":{"mla":"Kaneko, Takeshi, et al. “Morphological and Chemical Characteristics of Substance P Receptor Immunoreactive Neurons in the Rat Neocortex.” <i>Neuroscience</i>, vol. 60, no. 1, Elsevier, 1994, pp. 199–211, doi:<a href=\"https://doi.org/10.1016/0306-4522(94)90215-1\">10.1016/0306-4522(94)90215-1</a>.","ieee":"T. Kaneko, R. Shigemoto, S. Nakanishi, and N. Mizuno, “Morphological and chemical characteristics of substance P receptor immunoreactive neurons in the rat neocortex,” <i>Neuroscience</i>, vol. 60, no. 1. Elsevier, pp. 199–211, 1994.","ista":"Kaneko T, Shigemoto R, Nakanishi S, Mizuno N. 1994. Morphological and chemical characteristics of substance P receptor immunoreactive neurons in the rat neocortex. Neuroscience. 60(1), 199–211.","short":"T. Kaneko, R. Shigemoto, S. Nakanishi, N. Mizuno, Neuroscience 60 (1994) 199–211.","chicago":"Kaneko, Takeshi, Ryuichi Shigemoto, Shigetada Nakanishi, and Noboru Mizuno. “Morphological and Chemical Characteristics of Substance P Receptor Immunoreactive Neurons in the Rat Neocortex.” <i>Neuroscience</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1016/0306-4522(94)90215-1\">https://doi.org/10.1016/0306-4522(94)90215-1</a>.","apa":"Kaneko, T., Shigemoto, R., Nakanishi, S., &#38; Mizuno, N. (1994). Morphological and chemical characteristics of substance P receptor immunoreactive neurons in the rat neocortex. <i>Neuroscience</i>. Elsevier. <a href=\"https://doi.org/10.1016/0306-4522(94)90215-1\">https://doi.org/10.1016/0306-4522(94)90215-1</a>","ama":"Kaneko T, Shigemoto R, Nakanishi S, Mizuno N. Morphological and chemical characteristics of substance P receptor immunoreactive neurons in the rat neocortex. <i>Neuroscience</i>. 1994;60(1):199-211. doi:<a href=\"https://doi.org/10.1016/0306-4522(94)90215-1\">10.1016/0306-4522(94)90215-1</a>"},"doi":"10.1016/0306-4522(94)90215-1","quality_controlled":"1","extern":"1","acknowledgement":"We are grateful for photographic help of Mr A. Uesugi, and the support of Drs S. Fukuchi, T. Fukuda, R. Hayashi, M. Katsurada, Y. Kitani, K. Kumagai, H. Kuroda, H. Matsubara, H. Matsushima, C. Minakuchi, M. Nishio, G. Niwa, H. Ckla, M. Ohbayashi, S. Ohbayashi, H. Ohtsuka, S. Tamaki, E. Watanabe, K. Yoshino and Y. Yoshino. This work was supported in part by Grants-in-Aid for Scientific Research on Priority Areas 05248207 and 05267104, and Scientific Research (B) 05454658 and (C) 05680658 from the Ministry of Education, Science and Culture of Japan.","abstract":[{"text":"Substance P receptor-expressing neurons in the rat cerebral neocortex were examined by single- and double-immunolabeling methods with an affinity-purified specific antibody to substance P receptor. Substance P receptor immunoreactivity was observed exclusively in non-pyramidal neurons. About a quarter of these substance P receptor-positive neocortical neurons showed intense immunoreactivity, and the other three quarters displayed weak substance P receptor immunoreactivity. The neurons showing intense substance P receptor immunoreactivity were large multipolar cells with a few long aspiny or sparsely-spiny dendrites, and were scattered throughout the neocortical layers except for layer I, and also in the underlying white matter. The weakly immunoreactive neurons were medium-sized multipolar cells with oval to round somata and aspiny varicose dendrites, and were distributed in all cortical layers with a bias to layers II-III and the superficial part of layer V. The double-immunofluorescence study revealed that almost all substance P receptor-positive neurons were immunoreactive for GABA, but negative for glutaminase. Substance P receptor immunoreactivity in GABAergic neocortical neurons were further examined by the double-immunofluorescence method with antibodies to markers for subgroups of GABAergic neurons. Somatostatin immunoreactivity was found in 89% of neurons with intense substance P receptor immunoreactivity, and in 1.5% of neurons with weak substance P receptor immunoreactivity. Neuropeptide Y immunoreactivity was also observed in 92% of neurons with intense immunoreactivity for substance P receptor, and in 1.6% of neurons with weak immunoreactivity for substance P receptor. In contrast, parvalbumin immunoreactivity was seen in 1.3% of neurons with intense substance P receptor immunoreactivity, and in 59% of weak substance P receptor immunoreactivity. Calbindin D28k immunoreactivity was found in 12 and 19% of neurons, respectively, with weak and intense immunoreactivities for substance P receptor. Virtually no cells showing substance P receptor immunoreactivity displayed immunoreactivity for vasoactive intestinal polypeptide or choline acetyltransferase. These results indicate that the neocortical neurons expressing substance P receptor constitute a subpopulation of GABAergic non-pyramidal cells, and are segregated into neurons with intense immunoreactivity and those with weak immunoreactivity for substance P receptor; the vast majority of neurons with intense substance P receptor immunoreactivity contain somatostatin and neuropeptide Y, and the majority of neurons with weak substance P receptor immunoreactivity have parvalbumin.","lang":"eng"}],"page":"199 - 211","external_id":{"pmid":["8052413"]},"day":"01","title":"Morphological and chemical characteristics of substance P receptor immunoreactive neurons in the rat neocortex","volume":60,"status":"public","oa_version":"None","date_created":"2018-12-11T11:57:58Z","issue":"1","_id":"2488","type":"journal_article","article_processing_charge":"No","publication":"Neuroscience","author":[{"first_name":"Takeshi","last_name":"Kaneko","full_name":"Kaneko, Takeshi"},{"orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","last_name":"Shigemoto"},{"last_name":"Nakanishi","first_name":"Shigetada","full_name":"Nakanishi, Shigetada"},{"last_name":"Mizuno","first_name":"Noboru","full_name":"Mizuno, Noboru"}],"month":"05","date_published":"1994-05-01T00:00:00Z","article_type":"original","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publisher":"Elsevier","date_updated":"2022-06-09T12:22:16Z","publist_id":"4413","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/0306452294902151?via%3Dihub"}],"scopus_import":"1"},{"pmid":1,"intvolume":"       347","year":"1994","publication_identifier":{"issn":["0021-9967"]},"language":[{"iso":"eng"}],"acknowledgement":"We are grateful to  Mr.  Akira  Uesugi for photographic help and for the support of Drs. Satoru Fukuchi, Toshio Fukuda, Ritsu Hayashi, Mizuho Katsurada, Yutaka Kitani, Keiko Kumagai,  Toshihiko Kuroda,  Hiroshi  Matsubara, Hiroshi Matsushima, Chisato Minakuchi, Masatoshi Nishio, Gonpei  Niwa Hajime Oda, Masahiko  Ohbayashi, Sei-ichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, Eizo Watan- abe, Kazuo Yoshino, and Toshiaki Yoshino. This work was supported in part by research grants from the Ministry of Education, Science and Culture of Japan.","citation":{"mla":"Akazawa, Chihiro, et al. “Differential Expression of Five N-Methyl-D-Aspartate Receptor Subunit MRNAs in the Cerebellum of Developing and Adult Rats.” <i>Journal of Comparative Neurology</i>, vol. 347, no. 1, Wiley-Blackwell, 1994, pp. 150–60, doi:<a href=\"https://doi.org/10.1002/cne.903470112\">10.1002/cne.903470112</a>.","ieee":"C. Akazawa, R. Shigemoto, Y. Bessho, S. Nakanishi, and N. Mizuno, “Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing and adult rats,” <i>Journal of Comparative Neurology</i>, vol. 347, no. 1. Wiley-Blackwell, pp. 150–160, 1994.","ista":"Akazawa C, Shigemoto R, Bessho Y, Nakanishi S, Mizuno N. 1994. Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing and adult rats. Journal of Comparative Neurology. 347(1), 150–160.","chicago":"Akazawa, Chihiro, Ryuichi Shigemoto, Yasumasa Bessho, Shigetada Nakanishi, and Noboru Mizuno. “Differential Expression of Five N-Methyl-D-Aspartate Receptor Subunit MRNAs in the Cerebellum of Developing and Adult Rats.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 1994. <a href=\"https://doi.org/10.1002/cne.903470112\">https://doi.org/10.1002/cne.903470112</a>.","short":"C. Akazawa, R. Shigemoto, Y. Bessho, S. Nakanishi, N. Mizuno, Journal of Comparative Neurology 347 (1994) 150–160.","apa":"Akazawa, C., Shigemoto, R., Bessho, Y., Nakanishi, S., &#38; Mizuno, N. (1994). Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing and adult rats. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/cne.903470112\">https://doi.org/10.1002/cne.903470112</a>","ama":"Akazawa C, Shigemoto R, Bessho Y, Nakanishi S, Mizuno N. Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing and adult rats. <i>Journal of Comparative Neurology</i>. 1994;347(1):150-160. doi:<a href=\"https://doi.org/10.1002/cne.903470112\">10.1002/cne.903470112</a>"},"doi":"10.1002/cne.903470112","quality_controlled":"1","extern":"1","abstract":[{"text":"Five N-methyl-D-aspartate (NMDA) receptor subunits have been identified thus far: NR1, NR2A, NR2B, NR2C, and NR2D. Here, we have analyzed the expression patterns of mRNAs for the NMDA receptor subunits in the developing and adult rats by in situ hybridization. The developmental changes of the expression patterns were most salient in the cerebellum. In the external granular layer, hybridization signals of mRNAs for NR1, NR2A, NR2B, and NR2C appeared by postnatal day 3, but no NR2D mRNA was expressed at any developmental stage examined. The NR1 mRNA was expressed in all cerebellar neurons at all developmental stages examined. The signals for the NR2A mRNA appeared in Purkinje cells and granule cells during the second postnatal week. The signals for the NR2B mRNA in granule cells were seen transiently during the first 2 weeks after birth. The signals for NR2C mRNA appeared in granule cells and glial cells during the second postnatal week. The signals for NR2D mRNA appeared transiently in Purkinje cells during the first 8 postnatal days; in adult rats, these were seen in stellate and Golgi cells. In the cerebellar nuclei, mRNAs for NR1, NR2A, NR2B, and NR2D were more or less expressed on postnatal day 0, while expression signals for the NR2C mRNA were first detected in postnatal day 14. Thus, the most conspicuous changes of expression patterns were observed in the cerebellar cortex during the first 2 weeks after birth, when development and maturation of the cerebellum proceed most rapidly.","lang":"eng"}],"page":"150 - 160","external_id":{"pmid":["7798379"]},"volume":347,"title":"Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing and adult rats","status":"public","day":"01","author":[{"last_name":"Akazawa","first_name":"Chihiro","full_name":"Akazawa, Chihiro"},{"orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi","last_name":"Shigemoto","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Bessho, Yasumasa","last_name":"Bessho","first_name":"Yasumasa"},{"full_name":"Nakanishi, Shigetada","last_name":"Nakanishi","first_name":"Shigetada"},{"first_name":"Noboru","last_name":"Mizuno","full_name":"Mizuno, Noboru"}],"date_created":"2018-12-11T11:57:58Z","oa_version":"None","issue":"1","_id":"2489","type":"journal_article","article_processing_charge":"No","publication":"Journal of Comparative Neurology","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_status":"published","publisher":"Wiley-Blackwell","publist_id":"4412","date_updated":"2022-06-09T12:11:20Z","month":"09","date_published":"1994-09-01T00:00:00Z","article_type":"original","scopus_import":"1","main_file_link":[{"url":"https://onlinelibrary.wiley.com/doi/10.1002/cne.903470112"}]},{"volume":62,"title":"Distribution of the messenger rna for the prostaglandin e receptor subtype ep3 in the mouse nervous system","status":"public","day":"01","author":[{"full_name":"Sugimoto, Yukihiko","last_name":"Sugimoto","first_name":"Yukihiko"},{"last_name":"Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi","orcid":"0000-0001-8761-9444","full_name":"Shigemoto, Ryuichi"},{"full_name":"Namba, Tsunehisa","last_name":"Namba","first_name":"Tsunehisa"},{"last_name":"Negishi","first_name":"Manabu","full_name":"Negishi, Manabu"},{"full_name":"Mizuno, Noboru","last_name":"Mizuno","first_name":"Noboru"},{"full_name":"Narumiya, Shuh","first_name":"Shuh","last_name":"Narumiya"},{"first_name":"Atsushi","last_name":"Ichikawa","full_name":"Ichikawa, Atsushi"}],"date_created":"2018-12-11T11:57:58Z","oa_version":"None","publication":"Neuroscience","issue":"3","_id":"2490","type":"journal_article","article_processing_charge":"No","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-06-09T11:56:23Z","publist_id":"4411","publisher":"Elsevier","article_type":"original","date_published":"1994-10-01T00:00:00Z","month":"10","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/0306452294904839?via%3Dihub"}],"intvolume":"        62","pmid":1,"year":"1994","publication_identifier":{"issn":["0306-4522"]},"language":[{"iso":"eng"}],"acknowledgement":"This work was supported in part by Grants-in-aid for Scientific Research 05404020, 04255103. 05771975, 05671816 and 05454568 from the Ministry of Education, Science and Culture of Japan and by grants from the Mitsubishi Foundation and the Takeda Science Foundation. We are grateful to Mr Akira Uesugi for photographic help. We also thank Drs Chihiro Akazawa, Hitoshi Ohishi and Masabumi Minami for helpful discussions. ","quality_controlled":"1","doi":"10.1016/0306-4522(94)90483-9","citation":{"ama":"Sugimoto Y, Shigemoto R, Namba T, et al. Distribution of the messenger rna for the prostaglandin e receptor subtype ep3 in the mouse nervous system. <i>Neuroscience</i>. 1994;62(3):919-928. doi:<a href=\"https://doi.org/10.1016/0306-4522(94)90483-9\">10.1016/0306-4522(94)90483-9</a>","apa":"Sugimoto, Y., Shigemoto, R., Namba, T., Negishi, M., Mizuno, N., Narumiya, S., &#38; Ichikawa, A. (1994). Distribution of the messenger rna for the prostaglandin e receptor subtype ep3 in the mouse nervous system. <i>Neuroscience</i>. Elsevier. <a href=\"https://doi.org/10.1016/0306-4522(94)90483-9\">https://doi.org/10.1016/0306-4522(94)90483-9</a>","chicago":"Sugimoto, Yukihiko, Ryuichi Shigemoto, Tsunehisa Namba, Manabu Negishi, Noboru Mizuno, Shuh Narumiya, and Atsushi Ichikawa. “Distribution of the Messenger Rna for the Prostaglandin e Receptor Subtype Ep3 in the Mouse Nervous System.” <i>Neuroscience</i>. Elsevier, 1994. <a href=\"https://doi.org/10.1016/0306-4522(94)90483-9\">https://doi.org/10.1016/0306-4522(94)90483-9</a>.","short":"Y. Sugimoto, R. Shigemoto, T. Namba, M. Negishi, N. Mizuno, S. Narumiya, A. Ichikawa, Neuroscience 62 (1994) 919–928.","ista":"Sugimoto Y, Shigemoto R, Namba T, Negishi M, Mizuno N, Narumiya S, Ichikawa A. 1994. Distribution of the messenger rna for the prostaglandin e receptor subtype ep3 in the mouse nervous system. Neuroscience. 62(3), 919–928.","ieee":"Y. Sugimoto <i>et al.</i>, “Distribution of the messenger rna for the prostaglandin e receptor subtype ep3 in the mouse nervous system,” <i>Neuroscience</i>, vol. 62, no. 3. Elsevier, pp. 919–928, 1994.","mla":"Sugimoto, Yukihiko, et al. “Distribution of the Messenger Rna for the Prostaglandin e Receptor Subtype Ep3 in the Mouse Nervous System.” <i>Neuroscience</i>, vol. 62, no. 3, Elsevier, 1994, pp. 919–28, doi:<a href=\"https://doi.org/10.1016/0306-4522(94)90483-9\">10.1016/0306-4522(94)90483-9</a>."},"extern":"1","abstract":[{"text":"Distribution of the messenger RNA for the prostaglandin E receptor subtype EP3 was investigated by in situ hybridization in the nervous system of the mouse. The hybridization signals for EP3 were widely distributed in the brain and sensory ganglia and specifically localized to neurons. In the dorsal root and trigeminal ganglia, about half of the neurons were labeled intensely. In the brain, intensely labeled neurons were found in Ammon's horn, the preoptic nuclei, lateral hypothalamic area, dorsomedial hypothalamic nucleus, lateral mammillary nucleus, entopeduncular nucleus, substantia nigra pars compacta, locus coeruleus and raphe nuclei. Moderately labeled neurons were seen in the mitral cell layer of the main olfactory bulb, layer V of the entorhinal and parasubicular cortices, layers V and VI of the cerebral neocortex, nuclei of the diagonal band, magnocellular preoptic nucleus, globus pallidus and lateral parabrachial nucleus. In the thalamus, moderately labeled neurons were distributed in the anterior, ventromedial, laterodorsal, paraventricular and central medial nuclei. Based on these distributions, we suggest that EP3 not only mediates prostaglandin E2 signals evoked by blood-borne cytokines in the areas poor in the blood-brain barrier, but also responds to those formed intrinsically within the brain to modulate various neuronal activities. Possible EP3 actions are discussed in relation to the reported neuronal activities of prostaglandin E2 in the brain.","lang":"eng"}],"page":"919 - 928","external_id":{"pmid":["7870313"]}},{"day":"01","status":"public","volume":71,"title":"Molecular diversity of glutamate receptors and their physiological functions","publication":"Experientia Supplementum","type":"book_chapter","_id":"2545","article_processing_charge":"No","date_created":"2018-12-11T11:58:18Z","oa_version":"None","author":[{"last_name":"Nakanishi","first_name":"Shigetada","full_name":"Nakanishi, Shigetada"},{"full_name":"Masu, Masayuki","first_name":"Masayuki","last_name":"Masu"},{"first_name":"Yasumasa","last_name":"Bessho","full_name":"Bessho, Yasumasa"},{"full_name":"Nakajima, Yoshiaki","last_name":"Nakajima","first_name":"Yoshiaki"},{"last_name":"Hayashi","first_name":"Yasunori","full_name":"Hayashi, Yasunori"},{"full_name":"Shigemoto, Ryuichi","orcid":"0000-0001-8761-9444","last_name":"Shigemoto","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87"}],"date_published":"1994-01-01T00:00:00Z","month":"01","date_updated":"2022-06-09T10:08:24Z","publist_id":"4352","publisher":"Birkhäuser","publication_status":"published","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/978-3-0348-7330-7_8"}],"scopus_import":"1","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783034873321"]},"year":"1994","intvolume":"        71","pmid":1,"extern":"1","quality_controlled":"1","doi":"10.1007/978-3-0348-7330-7_8","citation":{"apa":"Nakanishi, S., Masu, M., Bessho, Y., Nakajima, Y., Hayashi, Y., &#38; Shigemoto, R. (1994). Molecular diversity of glutamate receptors and their physiological functions. In <i>Experientia Supplementum</i> (Vol. 71, pp. 71–80). Birkhäuser. <a href=\"https://doi.org/10.1007/978-3-0348-7330-7_8\">https://doi.org/10.1007/978-3-0348-7330-7_8</a>","short":"S. Nakanishi, M. Masu, Y. Bessho, Y. Nakajima, Y. Hayashi, R. Shigemoto, in:, Experientia Supplementum, Birkhäuser, 1994, pp. 71–80.","chicago":"Nakanishi, Shigetada, Masayuki Masu, Yasumasa Bessho, Yoshiaki Nakajima, Yasunori Hayashi, and Ryuichi Shigemoto. “Molecular Diversity of Glutamate Receptors and Their Physiological Functions.” In <i>Experientia Supplementum</i>, 71:71–80. Birkhäuser, 1994. <a href=\"https://doi.org/10.1007/978-3-0348-7330-7_8\">https://doi.org/10.1007/978-3-0348-7330-7_8</a>.","ista":"Nakanishi S, Masu M, Bessho Y, Nakajima Y, Hayashi Y, Shigemoto R. 1994.Molecular diversity of glutamate receptors and their physiological functions. In: Experientia Supplementum. vol. 71, 71–80.","ieee":"S. Nakanishi, M. Masu, Y. Bessho, Y. Nakajima, Y. Hayashi, and R. Shigemoto, “Molecular diversity of glutamate receptors and their physiological functions,” in <i>Experientia Supplementum</i>, vol. 71, Birkhäuser, 1994, pp. 71–80.","mla":"Nakanishi, Shigetada, et al. “Molecular Diversity of Glutamate Receptors and Their Physiological Functions.” <i>Experientia Supplementum</i>, vol. 71, Birkhäuser, 1994, pp. 71–80, doi:<a href=\"https://doi.org/10.1007/978-3-0348-7330-7_8\">10.1007/978-3-0348-7330-7_8</a>.","ama":"Nakanishi S, Masu M, Bessho Y, Nakajima Y, Hayashi Y, Shigemoto R. Molecular diversity of glutamate receptors and their physiological functions. In: <i>Experientia Supplementum</i>. Vol 71. Birkhäuser; 1994:71-80. doi:<a href=\"https://doi.org/10.1007/978-3-0348-7330-7_8\">10.1007/978-3-0348-7330-7_8</a>"},"abstract":[{"text":"Glutamate receptors play an important role in many integrative brain functions and in neuronal development. We report the molecular diversity of NMDA receptors and metabotropic glutamate receptors on the basis of our studies of molecular cloning and characterization of the diverse members of these receptors. The NMDA receptors consist of two distinct types of subunits. NMDAR1 possesses all properties characteristic of the NMDA receptor-channel complex, whereas the four NMDAR2 subunits, termed NMDAR2A-2D, show no channel activity but potentiate the NMDAR1 activity and confer functional variability by different heteromeric formations. The NMDA receptor subunits are considerably divergent from the other ligand-gated ion channels, and the structural architecture of these subunits remains elusive. The mGluRs form a family of at least seven different subtypes termed mGluR1-mGluR7. These receptor subtypes have, seven transmembrane segments and possess a large extracellular domain at their N-terminal regions. The seven mGluR subtypes are classified into three subgroups according to their sequence similarities, signal transduction mechanisms and agonist selectivities: mGluR1/mGluR5, mGluR2/mGluR3 and mGluR4/mGluR6/mGluR7. On the basis of our knowledge of the molecular diversity of the NMDA receptors and mGluRs, we have studied the physiological roles of individual receptor subunits or subtypes. We have shown that K(+)-induced depolarization or NMDA treatment in primary cultures of neonatal cerebellar granule cells induces the functional NMDA receptor and specifically up-regulates NMDAR2A mRNA among the multiple NMDA receptor subunits through the increase in resting intracellular Ca2+ concentrations. Our study demonstrates that the regulation of the specific NMDA receptor subunit mRNA governs the NMDA receptor induction that is thought to play an important role in granule cell survival and death. Analysis of an agonist selectivity and an expression pattern of mGluR6 has indicated that mGluR6 is responsible for synaptic neurotransmission from photoreceptor cells to ON-bipolar cells in the visual system. We have also investigated the function of mGluR2 in granule cells of the accessory olfactory bulb by combining immunoelectron-microscopic analysis with slice-patch recordings on the basis of the identification of a new agonist selective for this receptor subtype. Our results demonstrate that mGluR2 is present at the presynaptic site of granule cells and modulates inhibitory GABA transmission from granule cells to mitral cells. This finding indicates that the mGluR2 activation relieves excited mitral cells from GABA inhibition but maintains the lateral inhibition of unexcited mitral cells, thus resulting in enhancement of the signal-to-noise ratio between the excited mitral cells and their neighboring unexcited mitral cells.","lang":"eng"}],"external_id":{"pmid":["8032174"]},"page":"71 - 80"}]