[{"quality_controlled":"1","publication":"Protein Science","intvolume":"         7","status":"public","publisher":"Wiley-Blackwell","extern":"1","month":"09","date_created":"2018-12-11T12:06:27Z","page":"1884 - 1897","language":[{"iso":"eng"}],"doi":"10.1002/pro.5560070905","pmid":1,"day":"01","author":[{"full_name":"Liang, Jie","first_name":"Jie","last_name":"Liang"},{"first_name":"Herbert","full_name":"Edelsbrunner, Herbert","last_name":"Edelsbrunner","orcid":"0000-0002-9823-6833","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Clare","full_name":"Woodward, Clare","last_name":"Woodward"}],"type":"journal_article","citation":{"mla":"Liang, Jie, et al. “Anatomy of Protein Pockets and Cavities: Measurement of Binding Site Geometry and Implications for Ligand Design.” <i>Protein Science</i>, vol. 7, no. 9, Wiley-Blackwell, 1998, pp. 1884–97, doi:<a href=\"https://doi.org/10.1002/pro.5560070905\">10.1002/pro.5560070905</a>.","chicago":"Liang, Jie, Herbert Edelsbrunner, and Clare Woodward. “Anatomy of Protein Pockets and Cavities: Measurement of Binding Site Geometry and Implications for Ligand Design.” <i>Protein Science</i>. Wiley-Blackwell, 1998. <a href=\"https://doi.org/10.1002/pro.5560070905\">https://doi.org/10.1002/pro.5560070905</a>.","ista":"Liang J, Edelsbrunner H, Woodward C. 1998. Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design. Protein Science. 7(9), 1884–1897.","ieee":"J. Liang, H. Edelsbrunner, and C. Woodward, “Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design,” <i>Protein Science</i>, vol. 7, no. 9. Wiley-Blackwell, pp. 1884–1897, 1998.","ama":"Liang J, Edelsbrunner H, Woodward C. Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design. <i>Protein Science</i>. 1998;7(9):1884-1897. doi:<a href=\"https://doi.org/10.1002/pro.5560070905\">10.1002/pro.5560070905</a>","apa":"Liang, J., Edelsbrunner, H., &#38; Woodward, C. (1998). Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design. <i>Protein Science</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/pro.5560070905\">https://doi.org/10.1002/pro.5560070905</a>","short":"J. Liang, H. Edelsbrunner, C. Woodward, Protein Science 7 (1998) 1884–1897."},"title":"Anatomy of protein pockets and cavities: Measurement of binding site geometry and implications for ligand design","volume":7,"publication_status":"published","oa":1,"main_file_link":[{"url":"http://www.ncbi.nlm.nih.gov/pmc/articles/PMC2144175/","open_access":"1"}],"_id":"4017","date_published":"1998-09-01T00:00:00Z","abstract":[{"text":"Identification and size characterization of surface pockets and occluded cavities are initial steps in protein structure-based ligand design. A new program, CAST, for automatically locating and measuring protein pockets and cavities, is based on precise computational geometry methods, including alpha shape and discrete flow theory. CAST identifies and measures pockets and pocket mouth openings, as well as cavities. The program specifies the atoms lining pockets, pocket openings. and buried cavities; the volume and area of pockets and cavities; and the area and circumference of mouth openings. CAST analysis of over 100 proteins has been carried out; proteins examined include a set of 51 monomeric enzyme-ligand structures, several elastase-inhibitor complexes, the FK506 binding protein, 30 HIV-1 protease-inhibitor complexes, and a number of small and large protein inhibitors, Medium-sized globular proteins typically have 10-20 pockets/cavities. Most often, binding sites are pockets with 1-2 mouth openings; much less frequently they are cavities. Ligand binding pockets vary widely in size, most within the range 10(2)-10(3) Angstrom(3). Statistical analysis reveals that the number of pockets and cavities is correlated with protein size, but there is no correlation between the size of the protein and the size of binding sites. Most frequently, the largest pocket/cavity is thp active site, but there are a number of instructive exceptions. Ligand volume and binding site volume are somewhat correlated when binding site volume is less than or equal to 700 Angstrom(3), but the ligand seldom occupies the entire site. Auxiliary pockets near the active site have been suggested as additional binding surface for designed ligands (Mattos C ct al., 1993, Nat Struct Biol 1:55-58). Analysis of elastase-inhibitor complexes suggests that CAST can identify ancillary pockets, suitable for recruitment in ligand design strategies. Analysis of the FK506 binding protein, and of compounds developed in SAR by NMR (Shuker SE et al.. 1996, Science 274:1531-1534), indicates that CAST pocket computation may provide a priori identification of target proteins for Linked-fragment design. CAST analysis of 30 HIV-1 protease-inhibitor complexes shows that the flexible active site pocket can vary over a range of 853-1,566 Angstrom(3), and that there are two pockets near or adjoining the active site that may be recruited for ligand design.","lang":"eng"}],"issue":"9","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-08-25T12:49:41Z","external_id":{"pmid":["9761470 "]},"scopus_import":"1","publication_identifier":{"issn":["0961-8368"]},"publist_id":"2111","article_type":"original","oa_version":"Published Version","year":"1998"},{"page":"104 - 113","article_processing_charge":"No","extern":"1","month":"10","_id":"4019","abstract":[{"lang":"eng","text":"The construction of shape spaces is studied from a mathematical and a computational viewpoint. A program is outlined reducing the problem to four tasks: the representation of geometry, the canonical deformation of geometry, the measuring of distance in shape space, and the selection of base shapes. The technical part of this paper focuses on the second task: the specification of a deformation mixing two or more shapes in continuously, changing proportions."}],"date_created":"2018-12-11T12:06:28Z","date_published":"1998-10-01T00:00:00Z","publication_status":"published","publisher":"IEEE","quality_controlled":"1","publication":"Proceedings of the 6th Pacific Conference on Computer Graphics and Applications","status":"public","citation":{"ista":"Cheng H, Edelsbrunner H, Fu P. 1998. Shape space from deformation. Proceedings of the 6th Pacific Conference on Computer Graphics and Applications. CGA: Conference on Computer Graphics and Applications , 104–113.","ieee":"H. Cheng, H. Edelsbrunner, and P. Fu, “Shape space from deformation,” in <i>Proceedings of the 6th Pacific Conference on Computer Graphics and Applications</i>, Singapore, 1998, pp. 104–113.","chicago":"Cheng, Ho, Herbert Edelsbrunner, and Ping Fu. “Shape Space from Deformation.” In <i>Proceedings of the 6th Pacific Conference on Computer Graphics and Applications</i>, 104–13. IEEE, 1998. <a href=\"https://doi.org/10.1109/PCCGA.1998.732056\">https://doi.org/10.1109/PCCGA.1998.732056</a>.","mla":"Cheng, Ho, et al. “Shape Space from Deformation.” <i>Proceedings of the 6th Pacific Conference on Computer Graphics and Applications</i>, IEEE, 1998, pp. 104–13, doi:<a href=\"https://doi.org/10.1109/PCCGA.1998.732056\">10.1109/PCCGA.1998.732056</a>.","short":"H. Cheng, H. Edelsbrunner, P. Fu, in:, Proceedings of the 6th Pacific Conference on Computer Graphics and Applications, IEEE, 1998, pp. 104–113.","apa":"Cheng, H., Edelsbrunner, H., &#38; Fu, P. (1998). Shape space from deformation. In <i>Proceedings of the 6th Pacific Conference on Computer Graphics and Applications</i> (pp. 104–113). Singapore: IEEE. <a href=\"https://doi.org/10.1109/PCCGA.1998.732056\">https://doi.org/10.1109/PCCGA.1998.732056</a>","ama":"Cheng H, Edelsbrunner H, Fu P. Shape space from deformation. In: <i>Proceedings of the 6th Pacific Conference on Computer Graphics and Applications</i>. IEEE; 1998:104-113. doi:<a href=\"https://doi.org/10.1109/PCCGA.1998.732056\">10.1109/PCCGA.1998.732056</a>"},"conference":{"start_date":"1998-10-26","end_date":"1998-10-29","name":"CGA: Conference on Computer Graphics and Applications ","location":"Singapore"},"title":"Shape space from deformation","publist_id":"2107","day":"01","year":"1998","oa_version":"None","author":[{"full_name":"Cheng, Ho","first_name":"Ho","last_name":"Cheng"},{"last_name":"Edelsbrunner","full_name":"Edelsbrunner, Herbert","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833"},{"last_name":"Fu","first_name":"Ping","full_name":"Fu, Ping"}],"type":"conference","acknowledgement":"This research is partially supported by the National Science Foundation under grants CCR-96-19542 and CCR-97-12088, and by the Army Research O*ce under grant DAAG55-98-1-0177.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-08-25T12:06:20Z","language":[{"iso":"eng"}],"doi":"10.1109/PCCGA.1998.732056","publication_identifier":{"isbn":["0818686200"]}},{"publication":"Robotics: The Algorithmic Perspective","quality_controlled":"1","status":"public","publication_status":"published","publisher":"AK Peters","month":"10","extern":"1","abstract":[{"text":"Space Filing diagrams are geometric models of molecular conformations in three-dimensional space. Each atom is a location is space and a quantitative expression of influence on the immediate surrounding. This paper surveys the basic types of space filling diagrams with a focus on the dual alpha shape. Properties of those diagrams that relate to questions of connectivity, size, shape and symmetry, and metamorphosis are discussed.","lang":"eng"}],"_id":"4020","date_created":"2018-12-11T12:06:28Z","date_published":"1998-10-01T00:00:00Z","page":"265 - 277","article_processing_charge":"No","language":[{"iso":"eng"}],"date_updated":"2022-08-25T12:12:04Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9781568810812"]},"publist_id":"2108","day":"01","author":[{"full_name":"Edelsbrunner, Herbert","first_name":"Herbert","last_name":"Edelsbrunner","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-9823-6833"}],"type":"book_chapter","year":"1998","oa_version":"None","citation":{"short":"H. Edelsbrunner, in:, Robotics: The Algorithmic Perspective, AK Peters, 1998, pp. 265–277.","ama":"Edelsbrunner H. Geometry for modeling biomolecules. In: <i>Robotics: The Algorithmic Perspective</i>. AK Peters; 1998:265-277.","apa":"Edelsbrunner, H. (1998). Geometry for modeling biomolecules. In <i>Robotics: The Algorithmic Perspective</i> (pp. 265–277). AK Peters.","chicago":"Edelsbrunner, Herbert. “Geometry for Modeling Biomolecules.” In <i>Robotics: The Algorithmic Perspective</i>, 265–77. AK Peters, 1998.","ieee":"H. Edelsbrunner, “Geometry for modeling biomolecules,” in <i>Robotics: The Algorithmic Perspective</i>, AK Peters, 1998, pp. 265–277.","ista":"Edelsbrunner H. 1998.Geometry for modeling biomolecules. In: Robotics: The Algorithmic Perspective. , 265–277.","mla":"Edelsbrunner, Herbert. “Geometry for Modeling Biomolecules.” <i>Robotics: The Algorithmic Perspective</i>, AK Peters, 1998, pp. 265–77."},"title":"Geometry for modeling biomolecules"},{"day":"01","type":"journal_article","author":[{"last_name":"Ritchie","full_name":"Ritchie, Mike","first_name":"Mike"},{"orcid":"0000-0002-8548-5240","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","full_name":"Barton, Nicholas H","first_name":"Nicholas H"}],"citation":{"short":"M. Ritchie, N.H. Barton, Trends in Ecology and Evolution 13 (1998) 282–283.","apa":"Ritchie, M., &#38; Barton, N. H. (1998). Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton. <i>Trends in Ecology and Evolution</i>. Cell Press. <a href=\"https://doi.org/10.1016/S0169-5347(98)01396-2\">https://doi.org/10.1016/S0169-5347(98)01396-2</a>","ama":"Ritchie M, Barton NH. Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton. <i>Trends in Ecology and Evolution</i>. 1998;13(7):282-283. doi:<a href=\"https://doi.org/10.1016/S0169-5347(98)01396-2\">10.1016/S0169-5347(98)01396-2</a>","ista":"Ritchie M, Barton NH. 1998. Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton. Trends in Ecology and Evolution. 13(7), 282–283.","ieee":"M. Ritchie and N. H. Barton, “Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton,” <i>Trends in Ecology and Evolution</i>, vol. 13, no. 7. Cell Press, pp. 282–283, 1998.","chicago":"Ritchie, Mike, and Nicholas H Barton. “Hybrids and Hybrid Zones: Reply from M.G. Ritchie and N.H. Barton.” <i>Trends in Ecology and Evolution</i>. Cell Press, 1998. <a href=\"https://doi.org/10.1016/S0169-5347(98)01396-2\">https://doi.org/10.1016/S0169-5347(98)01396-2</a>.","mla":"Ritchie, Mike, and Nicholas H. Barton. “Hybrids and Hybrid Zones: Reply from M.G. Ritchie and N.H. Barton.” <i>Trends in Ecology and Evolution</i>, vol. 13, no. 7, Cell Press, 1998, pp. 282–83, doi:<a href=\"https://doi.org/10.1016/S0169-5347(98)01396-2\">10.1016/S0169-5347(98)01396-2</a>."},"title":"Hybrids and hybrid zones: Reply from M.G. Ritchie and N.H. Barton","language":[{"iso":"eng"}],"doi":"10.1016/S0169-5347(98)01396-2","pmid":1,"extern":"1","month":"07","date_created":"2018-12-11T12:08:01Z","page":"282 - 283","quality_controlled":"1","publication":"Trends in Ecology and Evolution","status":"public","intvolume":"        13","publisher":"Cell Press","publist_id":"1806","article_type":"original","oa_version":"None","year":"1998","date_updated":"2022-08-25T11:56:08Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","external_id":{"pmid":["21238302"]},"publication_identifier":{"issn":["0169-5347"]},"_id":"4280","date_published":"1998-07-01T00:00:00Z","issue":"7","article_processing_charge":"No","volume":13,"publication_status":"published"},{"day":"25","type":"journal_article","author":[{"last_name":"Barton","first_name":"Nicholas H","full_name":"Barton, Nicholas H","orcid":"0000-0002-8548-5240","id":"4880FE40-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Charlesworth, Brian","first_name":"Brian","last_name":"Charlesworth"}],"citation":{"mla":"Barton, Nicholas H., and Brian Charlesworth. “Why Sex and Recombination?” <i>Science</i>, vol. 281, no. 5385, American Association for the Advancement of Science, 1998, pp. 1986–90, doi:<a href=\"https://doi.org/10.1126/science.281.5385.1986\">10.1126/science.281.5385.1986</a>.","ieee":"N. H. Barton and B. Charlesworth, “Why sex and recombination?,” <i>Science</i>, vol. 281, no. 5385. American Association for the Advancement of Science, pp. 1986–1990, 1998.","ista":"Barton NH, Charlesworth B. 1998. Why sex and recombination? Science. 281(5385), 1986–1990.","chicago":"Barton, Nicholas H, and Brian Charlesworth. “Why Sex and Recombination?” <i>Science</i>. American Association for the Advancement of Science, 1998. <a href=\"https://doi.org/10.1126/science.281.5385.1986\">https://doi.org/10.1126/science.281.5385.1986</a>.","apa":"Barton, N. H., &#38; Charlesworth, B. (1998). Why sex and recombination? <i>Science</i>. American Association for the Advancement of Science. <a href=\"https://doi.org/10.1126/science.281.5385.1986\">https://doi.org/10.1126/science.281.5385.1986</a>","ama":"Barton NH, Charlesworth B. Why sex and recombination? <i>Science</i>. 1998;281(5385):1986-1990. doi:<a href=\"https://doi.org/10.1126/science.281.5385.1986\">10.1126/science.281.5385.1986</a>","short":"N.H. Barton, B. Charlesworth, Science 281 (1998) 1986–1990."},"title":"Why sex and recombination?","language":[{"iso":"eng"}],"doi":"10.1126/science.281.5385.1986","pmid":1,"extern":"1","month":"09","date_created":"2018-12-11T12:08:01Z","page":"1986 - 1990","quality_controlled":"1","publication":"Science","status":"public","intvolume":"       281","publisher":"American Association for the Advancement of Science","publist_id":"1804","article_type":"original","oa_version":"None","year":"1998","date_updated":"2022-08-25T11:53:29Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","external_id":{"pmid":["9748151"]},"scopus_import":"1","publication_identifier":{"issn":["0036-8075"]},"_id":"4281","date_published":"1998-09-25T00:00:00Z","abstract":[{"lang":"eng","text":"Most higher organisms reproduce sexually, despite the automatic reproductive advantage experienced by asexual variants. This implies the operation of selective forces that confer an advantage to sexuality and genetic recombination, at either the population or individual level. The effect of sex and recombination in breaking down negative correlations between favorable variants at different genetic loci, which increases the efficiency of natural selection, is likely to be a major factor favoring their evolution and maintenance. Various processes that can cause such an effect have been studied theoretically. It has, however, so far proved hard to discriminate among them empirically. "}],"issue":"5385","article_processing_charge":"No","volume":281,"publication_status":"published"},{"citation":{"short":"N.H. Barton, Genetical Research 72 (1998) 73–73.","apa":"Barton, N. H. (1998). Genetics and analysis of quantitative traits. <i>Genetical Research</i>. Cambridge University Press. <a href=\"https://doi.org/10.1017/S0016672398219732\">https://doi.org/10.1017/S0016672398219732</a>","ama":"Barton NH. Genetics and analysis of quantitative traits. <i>Genetical Research</i>. 1998;72(1):73-73. doi:<a href=\"https://doi.org/10.1017/S0016672398219732\">10.1017/S0016672398219732</a>","ieee":"N. H. Barton, “Genetics and analysis of quantitative traits,” <i>Genetical Research</i>, vol. 72, no. 1. Cambridge University Press, pp. 73–73, 1998.","ista":"Barton NH. 1998. Genetics and analysis of quantitative traits. Genetical Research. 72(1), 73–73.","chicago":"Barton, Nicholas H. “Genetics and Analysis of Quantitative Traits.” <i>Genetical Research</i>. Cambridge University Press, 1998. <a href=\"https://doi.org/10.1017/S0016672398219732\">https://doi.org/10.1017/S0016672398219732</a>.","mla":"Barton, Nicholas H. “Genetics and Analysis of Quantitative Traits.” <i>Genetical Research</i>, vol. 72, no. 1, Cambridge University Press, 1998, pp. 73–73, doi:<a href=\"https://doi.org/10.1017/S0016672398219732\">10.1017/S0016672398219732</a>."},"title":"Genetics and analysis of quantitative traits","day":"01","publist_id":"1801","year":"1998","oa_version":"None","author":[{"orcid":"0000-0002-8548-5240","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","full_name":"Barton, Nicholas H","first_name":"Nicholas H"}],"type":"review","date_updated":"2022-08-24T13:36:46Z","language":[{"iso":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","doi":"10.1017/S0016672398219732","publication_identifier":{"issn":["0016-6723"]},"page":"73 - 73","issue":"1","article_processing_charge":"No","extern":"1","month":"08","date_published":"1998-08-01T00:00:00Z","_id":"4282","date_created":"2018-12-11T12:08:01Z","publisher":"Cambridge University Press","publication_status":"published","publication":"Genetical Research","volume":72,"status":"public","intvolume":"        72"},{"type":"review","author":[{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H","first_name":"Nicholas H","last_name":"Barton"}],"oa_version":"None","year":"1998","day":"01","publist_id":"1802","title":"The geometry of adaptation","citation":{"ama":"Barton NH. The geometry of adaptation. <i>Nature</i>. 1998;395(6704):751-752. doi:<a href=\"https://doi.org/10.1038/27338\">10.1038/27338</a>","apa":"Barton, N. H. (1998). The geometry of adaptation. <i>Nature</i>. Nature Publishing Group. <a href=\"https://doi.org/10.1038/27338\">https://doi.org/10.1038/27338</a>","short":"N.H. Barton, Nature 395 (1998) 751–752.","mla":"Barton, Nicholas H. “The Geometry of Adaptation.” <i>Nature</i>, vol. 395, no. 6704, Nature Publishing Group, 1998, pp. 751–52, doi:<a href=\"https://doi.org/10.1038/27338\">10.1038/27338</a>.","chicago":"Barton, Nicholas H. “The Geometry of Adaptation.” <i>Nature</i>. Nature Publishing Group, 1998. <a href=\"https://doi.org/10.1038/27338\">https://doi.org/10.1038/27338</a>.","ieee":"N. H. Barton, “The geometry of adaptation,” <i>Nature</i>, vol. 395, no. 6704. Nature Publishing Group, pp. 751–752, 1998.","ista":"Barton NH. 1998. The geometry of adaptation. Nature. 395(6704), 751–752."},"publication_identifier":{"issn":["0028-0836"]},"doi":"10.1038/27338","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-08-24T13:50:49Z","language":[{"iso":"eng"}],"_id":"4283","date_created":"2018-12-11T12:08:02Z","date_published":"1998-10-01T00:00:00Z","month":"10","extern":"1","article_processing_charge":"No","issue":"6704","page":"751 - 752","status":"public","intvolume":"       395","volume":395,"publication":"Nature","quality_controlled":"1","publication_status":"published","publisher":"Nature Publishing Group"},{"publist_id":"323","oa_version":"None","year":"1998","date_updated":"2022-08-24T12:15:17Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"isbn":["9783540648963"]},"article_processing_charge":"No","_id":"4408","date_published":"1998-01-01T00:00:00Z","abstract":[{"text":"This paper presents a complete axiomatization of fully decidable propositional real-time linear temporal logics with past: the Event Clock Logic (ECL) and the Metric Interval Temporal Logic with past (MITL). The completeness proof consists of an effective proof building procedure for ECL. From this result we obtain a complete axiomatization of MITL by providing axioms translating MITL formulae into ECL formulae, the two logics being equally expressive. Our proof is structured to yield a similar axiomatization and procedure for interesting fragments of these logics, such as the linear temporal logic of the real numbers (LTR).","lang":"eng"}],"publication_status":"published","volume":1466,"citation":{"short":"J. Raskin, P. Schobbens, T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 219–236.","ama":"Raskin J, Schobbens P, Henzinger TA. Axioms for real-time logics. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:219-236. doi:<a href=\"https://doi.org/10.1007/BFb0055625\">10.1007/BFb0055625</a>","apa":"Raskin, J., Schobbens, P., &#38; Henzinger, T. A. (1998). Axioms for real-time logics. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 219–236). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055625\">https://doi.org/10.1007/BFb0055625</a>","chicago":"Raskin, Jean, Pierre Schobbens, and Thomas A Henzinger. “Axioms for Real-Time Logics.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:219–36. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055625\">https://doi.org/10.1007/BFb0055625</a>.","ista":"Raskin J, Schobbens P, Henzinger TA. 1998. Axioms for real-time logics. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 219–236.","ieee":"J. Raskin, P. Schobbens, and T. A. Henzinger, “Axioms for real-time logics,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 219–236.","mla":"Raskin, Jean, et al. “Axioms for Real-Time Logics.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 219–36, doi:<a href=\"https://doi.org/10.1007/BFb0055625\">10.1007/BFb0055625</a>."},"conference":{"end_date":"1998-09-11","start_date":"1998-09-08","name":"CONCUR: Concurrency Theory","location":"Nice, France"},"title":"Axioms for real-time logics","day":"01","alternative_title":["LNCS"],"author":[{"first_name":"Jean","full_name":"Raskin, Jean","last_name":"Raskin"},{"first_name":"Pierre","full_name":"Schobbens, Pierre","last_name":"Schobbens"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"type":"conference","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, by the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.","language":[{"iso":"eng"}],"doi":"10.1007/BFb0055625","page":"219 - 236","extern":"1","month":"01","date_created":"2018-12-11T12:08:42Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","quality_controlled":"1","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","intvolume":"      1466","status":"public"},{"conference":{"location":"Lyngby, Denmark","start_date":"1998-09-14","end_date":"1998-09-18","name":"FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems"},"title":"An algorithm for the approximative analysis of rectangular automata","citation":{"ista":"Preußig J, Kowalewski S, Wong Toi H, Henzinger TA. 1998. An algorithm for the approximative analysis of rectangular automata. Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS, vol. 1486, 228–240.","ieee":"J. Preußig, S. Kowalewski, H. Wong Toi, and T. A. Henzinger, “An algorithm for the approximative analysis of rectangular automata,” in <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, Lyngby, Denmark, 1998, vol. 1486, pp. 228–240.","chicago":"Preußig, Jörg, Stefan Kowalewski, Howard Wong Toi, and Thomas A Henzinger. “An Algorithm for the Approximative Analysis of Rectangular Automata.” In <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, 1486:228–40. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0055350\">https://doi.org/10.1007/BFb0055350</a>.","mla":"Preußig, Jörg, et al. “An Algorithm for the Approximative Analysis of Rectangular Automata.” <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>, vol. 1486, Springer, 1998, pp. 228–40, doi:<a href=\"https://doi.org/10.1007/BFb0055350\">10.1007/BFb0055350</a>.","short":"J. Preußig, S. Kowalewski, H. Wong Toi, T.A. Henzinger, in:, Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1998, pp. 228–240.","apa":"Preußig, J., Kowalewski, S., Wong Toi, H., &#38; Henzinger, T. A. (1998). An algorithm for the approximative analysis of rectangular automata. In <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i> (Vol. 1486, pp. 228–240). Lyngby, Denmark: Springer. <a href=\"https://doi.org/10.1007/BFb0055350\">https://doi.org/10.1007/BFb0055350</a>","ama":"Preußig J, Kowalewski S, Wong Toi H, Henzinger TA. An algorithm for the approximative analysis of rectangular automata. In: <i>Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems</i>. Vol 1486. Springer; 1998:228-240. doi:<a href=\"https://doi.org/10.1007/BFb0055350\">10.1007/BFb0055350</a>"},"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Preußig","first_name":"Jörg","full_name":"Preußig, Jörg"},{"full_name":"Kowalewski, Stefan","first_name":"Stefan","last_name":"Kowalewski"},{"last_name":"Wong Toi","first_name":"Howard","full_name":"Wong Toi, Howard"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"day":"01","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the DARPA/NASA grant NAG2-1214, by the ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","doi":"10.1007/BFb0055350","language":[{"iso":"eng"}],"page":"228 - 240","date_created":"2018-12-11T12:08:43Z","extern":"1","month":"01","publisher":"Springer","intvolume":"      1486","status":"public","quality_controlled":"1","publication":"Proceedings of the 5th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems","year":"1998","oa_version":"None","publist_id":"320","publication_identifier":{"isbn":["9783540650034"]},"date_updated":"2022-08-24T12:01:57Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","article_processing_charge":"No","_id":"4410","abstract":[{"text":"Rectangular automata are well suited for approximate modeling of continuous-discrete systems. The exact analysis of these automata is feasible for small examples but can encounter severe numerical problems for even medium-sized systems. This paper presents an analysis algorithm that uses conservative overapproximation to avoid these numerical problems. The algorithm is demonstrated on a simple benchmark system consisting of two connected tanks.\r\nSupported by the German Research Council (DFG) under grant Ko1430/3 in the special program KONDISK (‘Continuous-discrete dynamics of technical systems’).","lang":"eng"}],"date_published":"1998-01-01T00:00:00Z","publication_status":"published","volume":1486},{"citation":{"apa":"Henzinger, T. A., &#38; Rusu, V. (1998). Reachability verification for hybrid automata. In <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i> (Vol. 1386, pp. 190–204). Berkely, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-64358-3_40\">https://doi.org/10.1007/3-540-64358-3_40</a>","ama":"Henzinger TA, Rusu V. Reachability verification for hybrid automata. In: <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>. Vol 1386. Springer; 1998:190-204. doi:<a href=\"https://doi.org/10.1007/3-540-64358-3_40\">10.1007/3-540-64358-3_40</a>","short":"T.A. Henzinger, V. Rusu, in:, Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control, Springer, 1998, pp. 190–204.","mla":"Henzinger, Thomas A., and Vlad Rusu. “Reachability Verification for Hybrid Automata.” <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, vol. 1386, Springer, 1998, pp. 190–204, doi:<a href=\"https://doi.org/10.1007/3-540-64358-3_40\">10.1007/3-540-64358-3_40</a>.","ista":"Henzinger TA, Rusu V. 1998. Reachability verification for hybrid automata. Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 1386, 190–204.","ieee":"T. A. Henzinger and V. Rusu, “Reachability verification for hybrid automata,” in <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, Berkely, CA, United States of America, 1998, vol. 1386, pp. 190–204.","chicago":"Henzinger, Thomas A, and Vlad Rusu. “Reachability Verification for Hybrid Automata.” In <i>Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control</i>, 1386:190–204. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-64358-3_40\">https://doi.org/10.1007/3-540-64358-3_40</a>."},"title":"Reachability verification for hybrid automata","conference":{"location":"Berkely, CA, United States of America","name":"HSCC: Hybrid Systems - Computation and Control","end_date":"1998-04-15","start_date":"1998-04-13"},"day":"01","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Vlad","full_name":"Rusu, Vlad","last_name":"Rusu"}],"type":"conference","alternative_title":["LNCS"],"acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.\r\nSupported by Lavoisier grant of the French Foreign Affairs Ministry and by SRI.","language":[{"iso":"eng"}],"doi":"10.1007/3-540-64358-3_40","page":"190 - 204","month":"01","extern":"1","date_created":"2018-12-11T12:08:48Z","publisher":"Springer","publication":"Proceedings of the 1st International Workshop on Hybrid Systems: Computation and Control","quality_controlled":"1","intvolume":"      1386","status":"public","publist_id":"299","oa_version":"None","year":"1998","scopus_import":"1","date_updated":"2022-08-24T11:29:14Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["9783540643586"]},"article_processing_charge":"No","abstract":[{"lang":"eng","text":"We study the reachability problem for hybrid automata. Automatic approaches, which attempt to construct the reachable region by symbolic execution, often do not terminate. In these cases, we require the user to guess the reachable region, and we use a theorem prover (Pvs) to verify the guess. We classify hybrid automata according to the theory in which their reachable region can be defined finitely. This is the theory in which the prover needs to operate in order to verify the guess. The approach is interesting, because an appropriate guess can often be deduced by extrapolating from the first few steps of symbolic execution."}],"_id":"4429","date_published":"1998-01-01T00:00:00Z","publication_status":"published","volume":1386},{"citation":{"short":"T.A. Henzinger, ed., HSCC: Hybrid Systems—Computation and Control, Springer, 1998.","apa":"Henzinger, T. A. (Ed.). (1998). <i>HSCC: Hybrid Systems—Computation and Control</i> (Vol. 1386). Presented at the HSCC: Hybrid Systems: Computation and Control, Berkeley, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-64358-3\">https://doi.org/10.1007/3-540-64358-3</a>","ama":"Henzinger TA, ed. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol 1386. Springer; 1998. doi:<a href=\"https://doi.org/10.1007/3-540-64358-3\">10.1007/3-540-64358-3</a>","ieee":"T. A. Henzinger, Ed., <i>HSCC: Hybrid Systems—Computation and Control</i>, vol. 1386. Springer, 1998.","ista":"Henzinger TA ed. 1998. HSCC: Hybrid Systems—Computation and Control, Springer,p.","chicago":"Henzinger, Thomas A, ed. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol. 1386. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-64358-3\">https://doi.org/10.1007/3-540-64358-3</a>.","mla":"Henzinger, Thomas A., editor. <i>HSCC: Hybrid Systems—Computation and Control</i>. Vol. 1386, Springer, 1998, doi:<a href=\"https://doi.org/10.1007/3-540-64358-3\">10.1007/3-540-64358-3</a>."},"title":"HSCC: Hybrid Systems—Computation and Control","editor":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"conference":{"end_date":"1998-04-15","start_date":"1998-04-13","name":"HSCC: Hybrid Systems: Computation and Control","location":"Berkeley, CA, United States of America"},"day":"01","publist_id":"300","type":"conference_editor","oa_version":"None","year":"1998","alternative_title":["LNCS"],"language":[{"iso":"eng"}],"date_updated":"2022-08-24T11:36:03Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication_identifier":{"isbn":["978-3-540-64358-6"]},"doi":"10.1007/3-540-64358-3","article_processing_charge":"No","month":"01","extern":"1","date_created":"2018-12-11T12:08:49Z","_id":"4430","date_published":"1998-01-01T00:00:00Z","publisher":"Springer","publication_status":"published","status":"public","intvolume":"      1386","volume":1386},{"doi":"10.1007/3-540-49519-3_27","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","type":"conference","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"},{"last_name":"Tasiran","full_name":"Tasiran, Serdar","first_name":"Serdar"}],"alternative_title":["LNCS"],"day":"01","title":"An assume-guarantee rule for checking simulation","conference":{"name":"FMCAD: Formal Methods in Computer-Aided Design","start_date":"1998-11-04","end_date":"1998-11-06","location":"Palo Alto, CA, United States of America"},"citation":{"short":"T.A. Henzinger, S. Qadeer, S. Rajamani, S. Tasiran, in:, Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design, Springer, 1998, pp. 421–432.","ama":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. An assume-guarantee rule for checking simulation. In: <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>. Vol 1522. Springer; 1998:421-432. doi:<a href=\"https://doi.org/10.1007/3-540-49519-3_27\">10.1007/3-540-49519-3_27</a>","apa":"Henzinger, T. A., Qadeer, S., Rajamani, S., &#38; Tasiran, S. (1998). An assume-guarantee rule for checking simulation. In <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i> (Vol. 1522, pp. 421–432). Palo Alto, CA, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-49519-3_27\">https://doi.org/10.1007/3-540-49519-3_27</a>","chicago":"Henzinger, Thomas A, Shaz Qadeer, Sriram Rajamani, and Serdar Tasiran. “An Assume-Guarantee Rule for Checking Simulation.” In <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, 1522:421–32. Springer, 1998. <a href=\"https://doi.org/10.1007/3-540-49519-3_27\">https://doi.org/10.1007/3-540-49519-3_27</a>.","ista":"Henzinger TA, Qadeer S, Rajamani S, Tasiran S. 1998. An assume-guarantee rule for checking simulation. Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, LNCS, vol. 1522, 421–432.","ieee":"T. A. Henzinger, S. Qadeer, S. Rajamani, and S. Tasiran, “An assume-guarantee rule for checking simulation,” in <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, Palo Alto, CA, United States of America, 1998, vol. 1522, pp. 421–432.","mla":"Henzinger, Thomas A., et al. “An Assume-Guarantee Rule for Checking Simulation.” <i>Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design</i>, vol. 1522, Springer, 1998, pp. 421–32, doi:<a href=\"https://doi.org/10.1007/3-540-49519-3_27\">10.1007/3-540-49519-3_27</a>."},"status":"public","intvolume":"      1522","publication":"Proceedings of the 2nd International Conference on Formal Methods in Computer-Aided Design","quality_controlled":"1","publisher":"Springer","date_created":"2018-12-11T12:09:06Z","month":"01","extern":"1","page":"421 - 432","publication_identifier":{"isbn":["9783540651918"]},"scopus_import":"1","date_updated":"2022-08-24T10:00:50Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","year":"1998","publist_id":"242","volume":1522,"publication_status":"published","_id":"4486","date_published":"1998-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"The simulation preorder on state transition systems is widely accepted as a useful notion of refinement, both in its own right and as an efficiently checkable sufficient condition for trace containment. For composite systems, due to the exponential explosion of the state space, there is a need for decomposing a simulation check of the form P&lt; s Q into simpler simulation checks on the components of P and Q. We present an assume-guarantee rule that enables such a decomposition. To the best of our knowledge, this is the first assume-guarantee rule that applies to a refinement relation different from trace containment. Our rule is circular, and its soundness proof requires induction on trace trees. The proof is constructive: given simulation relations that witness the simulation preorder between corresponding components of P and Q, we provide a procedure for constructing a witness relation for P&lt; s Q. We also extend our assume-guarantee rule to account for fairness assumptions on transition systems"}],"article_processing_charge":"No"},{"acknowledgement":"This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","doi":"10.1007/BFb0028765","language":[{"iso":"eng"}],"conference":{"name":"CAV: Computer Aided Verification","end_date":"1998-07-02","start_date":"1998-06-28","location":"Vancouver, Canada"},"title":"You assume, we guarantee: Methodology and case studies","citation":{"short":"T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 440–451.","apa":"Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1998). You assume, we guarantee: Methodology and case studies. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 440–451). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028765\">https://doi.org/10.1007/BFb0028765</a>","ama":"Henzinger TA, Qadeer S, Rajamani S. You assume, we guarantee: Methodology and case studies. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:440-451. doi:<a href=\"https://doi.org/10.1007/BFb0028765\">10.1007/BFb0028765</a>","ista":"Henzinger TA, Qadeer S, Rajamani S. 1998. You assume, we guarantee: Methodology and case studies. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 440–451.","ieee":"T. A. Henzinger, S. Qadeer, and S. Rajamani, “You assume, we guarantee: Methodology and case studies,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 440–451.","chicago":"Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “You Assume, We Guarantee: Methodology and Case Studies.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:440–51. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028765\">https://doi.org/10.1007/BFb0028765</a>.","mla":"Henzinger, Thomas A., et al. “You Assume, We Guarantee: Methodology and Case Studies.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 440–51, doi:<a href=\"https://doi.org/10.1007/BFb0028765\">10.1007/BFb0028765</a>."},"alternative_title":["LNCS"],"type":"conference","author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"}],"day":"01","publisher":"Springer","intvolume":"      1427","status":"public","quality_controlled":"1","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","page":"440 - 451","date_created":"2018-12-11T12:09:06Z","extern":"1","month":"01","publication_identifier":{"isbn":["9783540646082"]},"date_updated":"2022-09-05T07:31:52Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","year":"1998","oa_version":"None","publist_id":"239","publication_status":"published","volume":1427,"article_processing_charge":"No","_id":"4488","date_published":"1998-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"Assume-guarantee reasoning has long been advertised as an important method for decomposing proof obligations in system verification. Refinement mappings (homomorphisms) have long been advertised as an important method for solving the language-inclusion problem in practice. When confronted with large verification problems, we therefore attempted to make use of both techniques. We soon found that rather than offering instant solutions, the success of assume-guarantee reasoning depends critically on the construction of suitable abstraction modules, and the success of refinement checking depends critically on the construction of suitable witness modules. Moreover, as abstractions need to be witnessed, and witnesses abstracted, the process must be iterated. We present here the main lessons we learned from our experiments, in limn of a systematic and structured discipline for the compositional verification of reactive modules. An infrastructure to support this discipline, and automate parts of the verification, has been implemented in the tool Mocha."}]},{"publist_id":"240","oa_version":"None","year":"1998","scopus_import":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","date_updated":"2022-08-24T09:19:53Z","publication_identifier":{"isbn":["9783540646082"]},"article_processing_charge":"No","date_published":"1998-01-01T00:00:00Z","_id":"4489","abstract":[{"text":"Symbolic model checking, which enables the automatic verification of large systems, proceeds by calculating with expressions that represent state sets. Traditionally, symbolic model-checking tools arc based on backward state traversal; their basic operation is the function pre, which given a set of states, returns the set of all predecessor states. This is because specifiers usally employ formalisms with future-time modalities. which are naturally evaluated by iterating applications of pre. It has been recently shown experimentally that symbolic model checking can perform significantly better if it is based, instead, on forward state traversal; in this case, the basic operation is the function post, which given a set of states, returns the set of all successor states. This is because forward state traversal can ensure that only those parts of the state space are explored which are reachable from an initial state and relevant for satisfaction or violation of the specification; that is, errors can be detected as soon as possible.\r\nIn this paper, we investigate which specifications can be checked by symbolic forward state traversal. We formulate the problems of symbolic backward and forward model checking by means of two -calculi. The pre- calculus is based on the pre operation; the post- calculus, on the post operation. These two -calculi induce query logics, which augment fixpoint expressions with a boolean emptiness query. Using query logics, we are able to relate and compare the symbolic backward and forward approaches. In particular, we prove that all -regular (linear-time) specifications can be expressed as post- queries, and therefore checked using symbolic forward state traversal. On the other hand, we show that there are simple branching-time specifications that cannot be checked in this way.","lang":"eng"}],"publication_status":"published","volume":1427,"citation":{"short":"T.A. Henzinger, O. Kupferman, S. Qadeer, in:, Proceedings of the 10th International Conference on Computer Aided Verification, Springer, 1998, pp. 195–206.","ama":"Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic model checking. In: <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>. Vol 1427. Springer; 1998:195-206. doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>","apa":"Henzinger, T. A., Kupferman, O., &#38; Qadeer, S. (1998). From pre-historic to post-modern symbolic model checking. In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i> (Vol. 1427, pp. 195–206). Vancouver, Canada: Springer. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic to Post-Modern Symbolic Model Checking.” In <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, 1427:195–206. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0028745\">https://doi.org/10.1007/BFb0028745</a>.","ieee":"T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern symbolic model checking,” in <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, Vancouver, Canada, 1998, vol. 1427, pp. 195–206.","ista":"Henzinger TA, Kupferman O, Qadeer S. 1998. From pre-historic to post-modern symbolic model checking. Proceedings of the 10th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1427, 195–206.","mla":"Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model Checking.” <i>Proceedings of the 10th International Conference on Computer Aided Verification</i>, vol. 1427, Springer, 1998, pp. 195–206, doi:<a href=\"https://doi.org/10.1007/BFb0028745\">10.1007/BFb0028745</a>."},"title":"From pre-historic to post-modern symbolic model checking","conference":{"location":"Vancouver, Canada","name":"CAV: Computer Aided Verification","start_date":"1998-06-28","end_date":"1998-07-02"},"day":"01","type":"conference","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"},{"full_name":"Qadeer, Shaz","first_name":"Shaz","last_name":"Qadeer"}],"alternative_title":["LNCS"],"acknowledgement":"This work is supported in part by ONR YIP award N00014-95-1-0520, by NSF CAREER award CCR-9501708, by NSF grant CCR-9504469, by ARO MURI grant DAAH-04-96-1-0341, and by the SRC contract 97-DC-324.041.","language":[{"iso":"eng"}],"doi":"10.1007/BFb0028745","page":"195 - 206","month":"01","extern":"1","date_created":"2018-12-11T12:09:07Z","publisher":"Springer","publication":"Proceedings of the 10th International Conference on Computer Aided Verification","quality_controlled":"1","status":"public","intvolume":"      1427"},{"publication_status":"published","volume":1443,"article_processing_charge":"No","_id":"4490","date_published":"1998-01-01T00:00:00Z","abstract":[{"text":"A specification formalism for reactive systems defines a class of Ω-languages. We call a specification formalism fully decidable if it is constructively closed under boolean operations and has a decidable satisfiability (nonemptiness) problem. There are two important, robust classes of Ω-languages that are definable by fully decidable formalisms. The Ω -reqular languages are definable by finite automata, or equivalcntly, by the Sequential Calculus. The counter-free Ω-regular languages are definable by temporal logic, or equivalcntly, by the first-order fragment of the Sequential Calculus. The gap between both classes can be closed by finite counting (using automata connectives), or equivalently, by projection (existential second-order quantification over letters).\r\nA specification formalism for real-time systems defines a class of timed Ω-langnages, whose letters have real-numbered time stamps. Two popular ways of specifying timing constraints rely on the use of clocks, and on the use of time bounds for temporal operators. However, temporal logics with clocks or time bounds have undecidable satisfiability problems, and finite automata with clocks (so-called timed automata) are not closed under complement. Therefore, two fully decidable restrictions of these formalisms have been proposed. In the first case, clocks are restricted to event clocks, which measure distances to immediately preceding or succeeding events only. In the second case, time bounds are restricted to nonsingular intervals, which cannot specify the exact punctuality of events. We show that the resulting classes of timed Ω-languages are robust, and we explain their relationship.\r\nFirst, we show that temporal logic with event clocks defines the same class of timed Ω-languages as temporal logic with nonsingular time bounds, and we identify a first-order monadic theory that also defines this class. Second, we show that if the ability of finite counting is added to these formalisms, we obtain the class of timed Ω-languages that are definable by finite automata with event clocks, or equivalently, by a restricted second-order extension of the monadic theory. Third, we show that if projection is added, we obtain the class of timed Ω-languages that are definable by timed automata, or equivalently, by a richer second-order extension of the monadic theory. These results identify three robust classes of timed Ω-languages, of which the third, while popular, is not definable by a, fully decidable formalism. By contrast, the first two classes are definable by fully decidable formalisms from temporal logic, from automata theory, and from monadic logic. Since the gap between these two classes can be closed by finite counting, we dub them the timed Ω-regular languages and the timed counter-free Ω-rcgular languages, respectively.","lang":"eng"}],"date_updated":"2022-08-24T09:30:11Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","publication_identifier":{"isbn":["9783540647812"]},"publist_id":"241","year":"1998","oa_version":"None","publisher":"Springer","quality_controlled":"1","publication":"Proceedings of the 25th International Colloqium on Automata, Languages and Programming","status":"public","intvolume":"      1443","page":"580 - 591","extern":"1","month":"01","date_created":"2018-12-11T12:09:07Z","acknowledgement":"This work is supported in part by the ONR YIP award N00014-95-1-0520, the NSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the ARO MURI grant DAAH-04-96-1-0341, the SRC contract 97-DC-324.041, the Belgian National Fund for Scientific Research (FNRS), the European Commission under WGs Aspire and Fireworks, the Portuguese FCT, and by Belgacom.","language":[{"iso":"eng"}],"doi":"10.1007/BFb0055086","citation":{"chicago":"Henzinger, Thomas A, Jean Raskin, and Pierre Schobbens. “The Regular Real-Time Languages.” In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, 1443:580–91. Springer, 1998. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>.","ieee":"T. A. Henzinger, J. Raskin, and P. Schobbens, “The regular real-time languages,” in <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, Aalborg, Denmark, 1998, vol. 1443, pp. 580–591.","ista":"Henzinger TA, Raskin J, Schobbens P. 1998. The regular real-time languages. Proceedings of the 25th International Colloqium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 1443, 580–591.","mla":"Henzinger, Thomas A., et al. “The Regular Real-Time Languages.” <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>, vol. 1443, Springer, 1998, pp. 580–91, doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>.","short":"T.A. Henzinger, J. Raskin, P. Schobbens, in:, Proceedings of the 25th International Colloqium on Automata, Languages and Programming, Springer, 1998, pp. 580–591.","ama":"Henzinger TA, Raskin J, Schobbens P. The regular real-time languages. In: <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i>. Vol 1443. Springer; 1998:580-591. doi:<a href=\"https://doi.org/10.1007/BFb0055086\">10.1007/BFb0055086</a>","apa":"Henzinger, T. A., Raskin, J., &#38; Schobbens, P. (1998). The regular real-time languages. In <i>Proceedings of the 25th International Colloqium on Automata, Languages and Programming</i> (Vol. 1443, pp. 580–591). Aalborg, Denmark: Springer. <a href=\"https://doi.org/10.1007/BFb0055086\">https://doi.org/10.1007/BFb0055086</a>"},"conference":{"name":"ICALP: Automata, Languages and Programming","end_date":"1998-07-17","start_date":"1998-07-13","location":"Aalborg, Denmark"},"title":"The regular real-time languages","day":"01","alternative_title":["LNCS"],"type":"conference","author":[{"orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Raskin, Jean","first_name":"Jean","last_name":"Raskin"},{"last_name":"Schobbens","first_name":"Pierre","full_name":"Schobbens, Pierre"}]},{"publication_status":"published","publisher":"IEEE","volume":43,"status":"public","intvolume":"        43","quality_controlled":"1","publication":"IEEE Transactions on Automatic Control","issue":"4","article_processing_charge":"No","page":"540 - 554","_id":"4491","date_published":"1998-01-01T00:00:00Z","abstract":[{"lang":"eng","text":"We present two methods for translating nonlinear hybrid systems into linear hybrid automata. Properties of the nonlinear systems can then be inferred from the automatic analysis of the translated linear hybrid automata. The first method, called clock translation, replaces constraints on nonlinear variables by constraints on clock variables. The second method, called linear phase-portrait approximation, conservatively overapproximates the phase portrait of a hybrid automaton using piecewise-constant polyhedral differential inclusions. Both methods are sound for safety properties. We illustrate both methods by using HYTECH, a symbolic model checker for linear hybrid automata, to automatically check properties of a nonlinear temperature controller and of a predator-prey ecology"}],"date_created":"2018-12-11T12:09:07Z","extern":"1","month":"01","doi":"10.1109/9.664156 ","publication_identifier":{"issn":["0018-9162"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","language":[{"iso":"eng"}],"date_updated":"2022-08-23T14:34:35Z","title":"Algorithmic analysis of nonlinear hybrid systems","citation":{"apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1998). Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. IEEE. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>","ama":"Henzinger TA, Ho P, Wong Toi H. Algorithmic analysis of nonlinear hybrid systems. <i>IEEE Transactions on Automatic Control</i>. 1998;43(4):540-554. doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>","short":"T.A. Henzinger, P. Ho, H. Wong Toi, IEEE Transactions on Automatic Control 43 (1998) 540–554.","mla":"Henzinger, Thomas A., et al. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4, IEEE, 1998, pp. 540–54, doi:<a href=\"https://doi.org/10.1109/9.664156 \">10.1109/9.664156 </a>.","ista":"Henzinger TA, Ho P, Wong Toi H. 1998. Algorithmic analysis of nonlinear hybrid systems. IEEE Transactions on Automatic Control. 43(4), 540–554.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “Algorithmic analysis of nonlinear hybrid systems,” <i>IEEE Transactions on Automatic Control</i>, vol. 43, no. 4. IEEE, pp. 540–554, 1998.","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>IEEE Transactions on Automatic Control</i>. IEEE, 1998. <a href=\"https://doi.org/10.1109/9.664156 \">https://doi.org/10.1109/9.664156 </a>."},"oa_version":"None","year":"1998","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Ho","first_name":"Pei","full_name":"Ho, Pei"},{"full_name":"Wong Toi, Howard","first_name":"Howard","last_name":"Wong Toi"}],"type":"journal_article","day":"01","publist_id":"238","article_type":"original"},{"acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator Award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation Grant CCR-9504469, by the Air Force Office of Scientific Research Contract F49620-93-1-0056, by the Army Research Office MURI Grant DAAH-04-96-1-0341, by the Army Research Office Contract DAAH-04-94-G-0026, by the Defense Advanced Research Projects Agency Grant NAG2-892, and by the California PATH program.","doi":"10.1006/jcss.1998.1581","language":[{"iso":"eng"}],"title":"What's decidable about hybrid automata?","citation":{"short":"T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, Journal of Computer and System Sciences 57 (1998) 94–124.","ama":"Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. 1998;57(1):94-124. doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>","apa":"Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1998). What’s decidable about hybrid automata? <i>Journal of Computer and System Sciences</i>. Elsevier. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>","chicago":"Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>. Elsevier, 1998. <a href=\"https://doi.org/10.1006/jcss.1998.1581\">https://doi.org/10.1006/jcss.1998.1581</a>.","ista":"Henzinger TA, Kopke P, Puri A, Varaiya P. 1998. What’s decidable about hybrid automata? Journal of Computer and System Sciences. 57(1), 94–124.","ieee":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1. Elsevier, pp. 94–124, 1998.","mla":"Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Journal of Computer and System Sciences</i>, vol. 57, no. 1, Elsevier, 1998, pp. 94–124, doi:<a href=\"https://doi.org/10.1006/jcss.1998.1581\">10.1006/jcss.1998.1581</a>."},"author":[{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"first_name":"Peter","full_name":"Kopke, Peter","last_name":"Kopke"},{"first_name":"Anuj","full_name":"Puri, Anuj","last_name":"Puri"},{"last_name":"Varaiya","full_name":"Varaiya, P.","first_name":"P."}],"type":"journal_article","day":"01","publisher":"Elsevier","intvolume":"        57","status":"public","publication":"Journal of Computer and System Sciences","quality_controlled":"1","page":"94 - 124","date_created":"2018-12-11T12:09:08Z","month":"01","extern":"1","publication_identifier":{"isbn":["0022-0000"]},"date_updated":"2022-08-23T14:29:15Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"Published Version","year":"1998","article_type":"original","publist_id":"237","oa":1,"main_file_link":[{"open_access":"1","url":"https://www.sciencedirect.com/science/article/pii/S0022000098915811"}],"publication_status":"published","volume":57,"article_processing_charge":"No","issue":"1","_id":"4492","abstract":[{"lang":"eng","text":"Hybrid automata model systems with both digital and analog components, such as embedded control programs. Many verification tasks for such programs can be expressed as reachability problems for hybrid automata. By improving on previous decidability and undecidability results, we identify a boundary between decidability and undecidability for the reachability problem of hybrid automata. On the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow independent trajectories within piecewise-linear envelopes and are reinitialized whenever the envelope changes. Our algorithm is based on the construction of a timed automaton that contains all reachability information about a given initialized rectangular automaton. The translation has practical significance for verification, because it guarantees the termination of symbolic procedures for the reachability analysis of initialized rectangular automata. The translation also preserves theω-languages of initialized rectangular automata with bounded nondeterminism. On the negative side, we show that several slight generalizations of initialized rectangular automata lead to an undecidable reachability problem. In particular, we prove that the reachability problem is undecidable for timed automata augmented with a single stopwatch."}],"date_published":"1998-01-01T00:00:00Z"},{"date_created":"2018-12-11T12:09:15Z","month":"01","extern":"1","page":"439 - 454","status":"public","intvolume":"      1466","publication":"Proceedings of the 9th Interantional Conference on Concurrency Theory","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"}],"type":"conference","alternative_title":["LNCS"],"day":"01","title":"It's about time: Real-time logics reviewed","conference":{"location":"Nice, France","name":"CONCUR: Concurrency Theory","start_date":"1998-09-08","end_date":"1998-09-11"},"citation":{"ista":"Henzinger TA. 1998. It’s about time: Real-time logics reviewed. Proceedings of the 9th Interantional Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1466, 439–454.","ieee":"T. A. Henzinger, “It’s about time: Real-time logics reviewed,” in <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, Nice, France, 1998, vol. 1466, pp. 439–454.","chicago":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, 1466:439–54. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>.","mla":"Henzinger, Thomas A. “It’s about Time: Real-Time Logics Reviewed.” <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>, vol. 1466, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–54, doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>.","short":"T.A. Henzinger, in:, Proceedings of the 9th Interantional Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1998, pp. 439–454.","apa":"Henzinger, T. A. (1998). It’s about time: Real-time logics reviewed. In <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i> (Vol. 1466, pp. 439–454). Nice, France: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/BFb0055640\">https://doi.org/10.1007/BFb0055640</a>","ama":"Henzinger TA. It’s about time: Real-time logics reviewed. In: <i>Proceedings of the 9th Interantional Conference on Concurrency Theory</i>. Vol 1466. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1998:439-454. doi:<a href=\"https://doi.org/10.1007/BFb0055640\">10.1007/BFb0055640</a>"},"doi":"10.1007/BFb0055640","language":[{"iso":"eng"}],"acknowledgement":"This research was supported in part by the Office of Naval Research Young Investigator award N00014-95-1-0520, by the National Science Foundation CAREER award CCR-9501708, by the National Science Foundation grant CCR-9504469, by the Defense Advanced Research Projects Agency grant NAG2-1214, by the Army Research Office MURI grant DAAH-04-96-1-0341, and by the Semiconductor Research Corporation contract 97-DC-324.041.","date_published":"1998-01-01T00:00:00Z","_id":"4515","abstract":[{"lang":"eng","text":"We summarize and reorganize some of the last decade's research on real-time extensions of temporal logic. Our main focus is on tableau constructions for model checking linear temporal formulas with timing constraints. In particular, we find that a great deal of real-time verification can be performed in polynomial space, but also that considerable care must be exercised in order to keep the real-time verification problem in polynomial space, or even decidable."}],"article_processing_charge":"No","volume":1466,"publication_status":"published","year":"1998","oa_version":"None","publist_id":"214","publication_identifier":{"isbn":["978-3-540-64896-3"]},"scopus_import":"1","date_updated":"2022-08-23T14:24:08Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17"},{"page":"320 - 336","date_created":"2018-12-11T11:57:59Z","extern":"1","month":"02","publisher":"Wiley-Blackwell","status":"public","intvolume":"       378","quality_controlled":"1","publication":"Journal of Comparative Neurology","title":"Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus","citation":{"chicago":"Acsády, László, István Katona, Attila Gulyás, Ryuichi Shigemoto, and Tamás Freund. “Immunostaining for Substance P Receptor Labels GABAergic Cells with Distinct Termination Patterns in the Hippocampus.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 1997. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>.","ieee":"L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, and T. Freund, “Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus,” <i>Journal of Comparative Neurology</i>, vol. 378, no. 3. Wiley-Blackwell, pp. 320–336, 1997.","ista":"Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. 1997. Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. Journal of Comparative Neurology. 378(3), 320–336.","mla":"Acsády, László, et al. “Immunostaining for Substance P Receptor Labels GABAergic Cells with Distinct Termination Patterns in the Hippocampus.” <i>Journal of Comparative Neurology</i>, vol. 378, no. 3, Wiley-Blackwell, 1997, pp. 320–36, doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>.","short":"L. Acsády, I. Katona, A. Gulyás, R. Shigemoto, T. Freund, Journal of Comparative Neurology 378 (1997) 320–336.","ama":"Acsády L, Katona I, Gulyás A, Shigemoto R, Freund T. Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. <i>Journal of Comparative Neurology</i>. 1997;378(3):320-336. doi:<a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>","apa":"Acsády, L., Katona, I., Gulyás, A., Shigemoto, R., &#38; Freund, T. (1997). Immunostaining for substance P receptor labels GABAergic cells with distinct termination patterns in the hippocampus. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5\">https://doi.org/10.1002/(SICI)1096-9861(19970217)378:3&#38;lt;320::AID-CNE2&#38;gt;3.0.CO;2-5</a>"},"type":"journal_article","author":[{"first_name":"László","full_name":"Acsády, László","last_name":"Acsády"},{"full_name":"Katona, István","first_name":"István","last_name":"Katona"},{"full_name":"Gulyás, Attila","first_name":"Attila","last_name":"Gulyás"},{"id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","last_name":"Shigemoto","first_name":"Ryuichi","full_name":"Shigemoto, Ryuichi"},{"first_name":"Tamás","full_name":"Freund, Tamás","last_name":"Freund"}],"day":"17","acknowledgement":"This sudy was supported by grants from the Human Frontier Science Program Organisation, the Howard Hughes Medical Institute, and OTKA (T 16942) Hungary.We are grateful to Dr. K.G. Baimbridge and to Dr. M.R.Celio (calbindin and parvalbumin), Dr. T. Go ̈rcs (CCK, VIP,NPY, and somatostatin), Dr. J.H. Rogers (calretinin), andDr. C.G. Beaulieau (GABA) for kind gifts of antisera. The excellent technical assistance of Mrs. E. Borok, Mrs. A.Z.Szabo, and Mr. G. Terstyanszky is also acknowledged","pmid":1,"doi":"10.1002/(SICI)1096-9861(19970217)378:3&lt;320::AID-CNE2&gt;3.0.CO;2-5","language":[{"iso":"eng"}],"issue":"3","article_processing_charge":"No","_id":"2493","date_published":"1997-02-17T00:00:00Z","abstract":[{"text":"A specific antiserum against substance P receptor (SPR) labels nonprincipal neurons in the cerebral cortex of the rat (T. Kaneko et al. [1994], Neuroscience 60:199-211; Y. Nakaya et al. [1994], J. Comp. Neurol. 347:249-274). In the present study, we aimed to identify the types of SPR- immunoreactive neurons in the hippocampus according to their content of neurochemical markers, which label interneuron populations with distinct termination patterns. Markers for perisomatic inhibitory cells, parvalbumin and cholecystokinin (CCK), colocalized with SPR in pyramidallike basket cells in the dentate gyrus and in large multipolar or bitufted cells within all hippocampal subfields respectively. A dense meshwork of SPR-immunoreactive spiny dendrites in the hilus and stratum lucidum of the CA3 region belonged largely to inhibitory cells terminating in the distal dendritic region of granule cells, as indicated by the somatostatin and neuropeptide Y (NPY) content. In addition, SPR and NPY were colocalized in numerous multipolar interneurons with dendrites branching close to the soma. Twenty-five percent of the SPR-immunoreactive cells overlapped with calretinin-positive neurons in all hippocampal subfields, showing that interneurons specialized to contact other gamma-aminobutyric acid-ergic cells may also contain SPR. On the basis of the known termination pattern of the colocalized markers, we conclude that SPR-positive interneurons are functionally heterogeneous and participate in different inhibitory processes: (1) perisomatic inhibition of principal cells (CCK-containing cells, and parvalbumin-positive cells in the dentate gyrus), (2) feedback dendritic inhibition in the entorhinal termination zone (somatostatin and NPY-containing cells), and (3) innervation of other interneurons (calretinin-containing cells).","lang":"eng"}],"publication_status":"published","volume":378,"year":"1997","oa_version":"None","publist_id":"4408","article_type":"original","publication_identifier":{"issn":["0021-9967"]},"date_updated":"2022-08-22T13:43:18Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","external_id":{"pmid":["9034894"]}},{"publist_id":"4322","article_type":"original","year":"1997","oa_version":"None","date_updated":"2022-08-22T13:06:30Z","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","scopus_import":"1","external_id":{"pmid":["9080455"]},"publication_identifier":{"issn":["0304-3940"]},"issue":"3","article_processing_charge":"No","abstract":[{"text":"It was examined electron microscopically in the rat if a metabotropic glutamate receptor, mGluR7, might be localized in axon terminals of nociceptive, primary afferent fibers in laminae I and II of the spinal dorsal horn. Nociceptive nature of axon terminals showing mGluR7-like immunoreactivity (mGluR7-LI) was indicated by binding to the isolectin I-B4 from Griffonia simplicifolia (I-B4), or by substance P-like immunoreactivity (SP-LI). Axon terminals labeled with immunogold particles indicating mGluR7-LI were usually filled with round synaptic vesicles and were in asymmetric synaptic contact with dendritic or somatic profiles; occasionally they contained pleomorphic vesicles and were in symmetric synaptic contact with somatic profiles in lamina II. The double-labeling studies revealed that most of axon terminals with I-B4 labeling as well as a small population of axon terminals with SP-LI, showed mGluR7-LI. About one-third or much smaller population of axon terminals with mGluR7-LI in laminae I and II were labeled, respectively, with I-B4 or SP-LI; these were in asymmetric synaptic contact with dendritic profiles.","lang":"eng"}],"_id":"2575","date_published":"1997-02-28T00:00:00Z","publication_status":"published","volume":223,"citation":{"mla":"Li, He, et al. “Localization of a Metabotropic Glutamate Receptor, MGluR7, in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” <i>Neuroscience Letters</i>, vol. 223, no. 3, Elsevier, 1997, pp. 153–56, doi:<a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">10.1016/S0304-3940(97)13429-2</a>.","ieee":"H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, and N. Mizuno, “Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat,” <i>Neuroscience Letters</i>, vol. 223, no. 3. Elsevier, pp. 153–156, 1997.","ista":"Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. 1997. Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. Neuroscience Letters. 223(3), 153–156.","chicago":"Li, He, Hitoshi Ohishi, Ayae Kinoshita, Ryuichi Shigemoto, Sakashi Nomura, and Noboru Mizuno. “Localization of a Metabotropic Glutamate Receptor, MGluR7, in Axon Terminals of Presumed Nociceptive, Primary Afferent Fibers in the Superficial Layers of the Spinal Dorsal Horn: An Electron Microscope Study in the Rat.” <i>Neuroscience Letters</i>. Elsevier, 1997. <a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">https://doi.org/10.1016/S0304-3940(97)13429-2</a>.","apa":"Li, H., Ohishi, H., Kinoshita, A., Shigemoto, R., Nomura, S., &#38; Mizuno, N. (1997). Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. <i>Neuroscience Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">https://doi.org/10.1016/S0304-3940(97)13429-2</a>","ama":"Li H, Ohishi H, Kinoshita A, Shigemoto R, Nomura S, Mizuno N. Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat. <i>Neuroscience Letters</i>. 1997;223(3):153-156. doi:<a href=\"https://doi.org/10.1016/S0304-3940(97)13429-2\">10.1016/S0304-3940(97)13429-2</a>","short":"H. Li, H. Ohishi, A. Kinoshita, R. Shigemoto, S. Nomura, N. Mizuno, Neuroscience Letters 223 (1997) 153–156."},"title":"Localization of a metabotropic glutamate receptor, mGluR7, in axon terminals of presumed nociceptive, primary afferent fibers in the superficial layers of the spinal dorsal horn: An electron microscope study in the rat","day":"28","author":[{"last_name":"Li","first_name":"He","full_name":"Li, He"},{"first_name":"Hitoshi","full_name":"Ohishi, Hitoshi","last_name":"Ohishi"},{"full_name":"Kinoshita, Ayae","first_name":"Ayae","last_name":"Kinoshita"},{"first_name":"Ryuichi","full_name":"Shigemoto, Ryuichi","last_name":"Shigemoto","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444"},{"last_name":"Nomura","full_name":"Nomura, Sakashi","first_name":"Sakashi"},{"last_name":"Mizuno","first_name":"Noboru","full_name":"Mizuno, Noboru"}],"type":"journal_article","acknowledgement":"We are grateful for photographic help of Mr. Akira Uesugi. We also express our gratitude for the support of Drs. Satoru Fukuchi, Ritsu Hayashi, Sohzaburo Hayashi, Mizuho Katsurada, Hitoshi Kawai, Yutaka Kitani, Toshihiko Kuroda, Keiko Kumagai, Hiroshi Matsubara, Hiroshi Matsushima, Chisato Minakuchi, Gonpei Niwa, Hajime Oda, Masahiko Ohbayashi, Sei-ichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, Eizo Watanabe, Kazuo Yoshino, and Toshiaki Yoshino. This work was supported in part by Grant-in-Aid from Ministry of Education, Science, Culture and Sports of Japan.","pmid":1,"language":[{"iso":"eng"}],"doi":"10.1016/S0304-3940(97)13429-2","page":"153 - 156","extern":"1","month":"02","date_created":"2018-12-11T11:58:28Z","publisher":"Elsevier","quality_controlled":"1","publication":"Neuroscience Letters","intvolume":"       223","status":"public"}]