[{"language":[{"iso":"eng"}],"year":"1995","author":[{"full_name":"Edelsbrunner, Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","first_name":"Herbert","orcid":"0000-0002-9823-6833","last_name":"Edelsbrunner"}],"page":"248 - 257","conference":{"start_date":"1995-10-23","name":"FOCS: Foundations of Computer Science","location":"Milwaukee, WI, United States of America","end_date":"1995-10-25"},"date_created":"2018-12-11T12:06:33Z","publication_identifier":{"issn":["0272-5428"]},"publist_id":"2093","publication_status":"published","day":"01","abstract":[{"text":"Any arbitrary polyhedron P contained as a subset within Rd can be written as algebraic sum of simple terms, each an integer multiple of the intersection of d or fewer half-spaces defined by facets of P. P can be non-convex and can have holes of any kind. Among the consequences of this result are a short boolean formula for P, a fast parallel algorithm for point classification, and a new proof of the Gram-Sommerville angle relation.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","publication":"Proceedings of IEEE 36th Annual Foundations of Computer Science","_id":"4034","publisher":"IEEE","date_updated":"2022-06-13T12:27:11Z","title":"Algebraic decomposition of non-convex polyhedra","month":"10","acknowledgement":"The author thanks Bei-Fang Chen, Siu-Wing Cheng, David Dobkin, Nikolai Dolbilin, Ping Fu, Sergei Ryshkov, and Vadim Shapiro for discussions on the topic of this paper.","extern":"1","quality_controlled":"1","date_published":"1995-10-01T00:00:00Z","type":"conference","status":"public","oa_version":"None","main_file_link":[{"url":"https://ieeexplore.ieee.org/abstract/document/492480"}],"citation":{"apa":"Edelsbrunner, H. (1995). Algebraic decomposition of non-convex polyhedra. In Proceedings of IEEE 36th Annual Foundations of Computer Science (pp. 248–257). Milwaukee, WI, United States of America: IEEE.","ista":"Edelsbrunner H. 1995. Algebraic decomposition of non-convex polyhedra. Proceedings of IEEE 36th Annual Foundations of Computer Science. FOCS: Foundations of Computer Science, 248–257.","ieee":"H. Edelsbrunner, “Algebraic decomposition of non-convex polyhedra,” in Proceedings of IEEE 36th Annual Foundations of Computer Science, Milwaukee, WI, United States of America, 1995, pp. 248–257.","short":"H. Edelsbrunner, in:, Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 248–257.","mla":"Edelsbrunner, Herbert. “Algebraic Decomposition of Non-Convex Polyhedra.” Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 248–57.","ama":"Edelsbrunner H. Algebraic decomposition of non-convex polyhedra. In: Proceedings of IEEE 36th Annual Foundations of Computer Science. IEEE; 1995:248-257.","chicago":"Edelsbrunner, Herbert. “Algebraic Decomposition of Non-Convex Polyhedra.” In Proceedings of IEEE 36th Annual Foundations of Computer Science, 248–57. IEEE, 1995."}},{"publication_identifier":{"issn":["0179-5376"]},"issue":"1","main_file_link":[{"url":"https://link.springer.com/article/10.1007/BF02574025"}],"citation":{"mla":"Chazelle, Bernard, et al. “Improved Bounds on Weak ε-Nets for Convex Sets.” Discrete & Computational Geometry, vol. 13, no. 1, Springer, 1995, pp. 1–15, doi:10.1007/BF02574025.","ama":"Chazelle B, Edelsbrunner H, Grigni M, Guibas L, Sharir M, Welzl E. Improved bounds on weak ε-nets for convex sets. Discrete & Computational Geometry. 1995;13(1):1-15. doi:10.1007/BF02574025","chicago":"Chazelle, Bernard, Herbert Edelsbrunner, Michelangelo Grigni, Leonidas Guibas, Micha Sharir, and Emo Welzl. “Improved Bounds on Weak ε-Nets for Convex Sets.” Discrete & Computational Geometry. Springer, 1995. https://doi.org/10.1007/BF02574025.","apa":"Chazelle, B., Edelsbrunner, H., Grigni, M., Guibas, L., Sharir, M., & Welzl, E. (1995). Improved bounds on weak ε-nets for convex sets. Discrete & Computational Geometry. Springer. https://doi.org/10.1007/BF02574025","ista":"Chazelle B, Edelsbrunner H, Grigni M, Guibas L, Sharir M, Welzl E. 1995. Improved bounds on weak ε-nets for convex sets. Discrete & Computational Geometry. 13(1), 1–15.","ieee":"B. Chazelle, H. Edelsbrunner, M. Grigni, L. Guibas, M. Sharir, and E. Welzl, “Improved bounds on weak ε-nets for convex sets,” Discrete & Computational Geometry, vol. 13, no. 1. Springer, pp. 1–15, 1995.","short":"B. Chazelle, H. Edelsbrunner, M. Grigni, L. Guibas, M. Sharir, E. Welzl, Discrete & Computational Geometry 13 (1995) 1–15."},"intvolume":" 13","status":"public","acknowledgement":"The authors wish to express their gratitude for the support and hospitality of the DEC Palo Alto Systems Research Center.","abstract":[{"text":"Let S be a set of n points in ℝd . A set W is a weak ε-net for (convex ranges of)S if, for any T⊆S containing εn points, the convex hull of T intersects W. We show the existence of weak ε-nets of size {Mathematical expression}, where β2=0, β3=1, and βd ≈0.149·2d-1(d-1)!, improving a previous bound of Alon et al. Such a net can be computed effectively. We also consider two special cases: when S is a planar point set in convex position, we prove the existence of a net of size O((1/ε) log1.6(1/ε)). In the case where S consists of the vertices of a regular polygon, we use an argument from hyperbolic geometry to exhibit an optimal net of size O(1/ε), which improves a previous bound of Capoyleas.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4035","title":"Improved bounds on weak ε-nets for convex sets","date_created":"2018-12-11T12:06:33Z","publication_status":"published","publist_id":"2094","day":"01","author":[{"first_name":"Bernard","full_name":"Chazelle, Bernard","last_name":"Chazelle"},{"full_name":"Edelsbrunner, Herbert","first_name":"Herbert","id":"3FB178DA-F248-11E8-B48F-1D18A9856A87","last_name":"Edelsbrunner","orcid":"0000-0002-9823-6833"},{"last_name":"Grigni","full_name":"Grigni, Michelangelo","first_name":"Michelangelo"},{"last_name":"Guibas","full_name":"Guibas, Leonidas","first_name":"Leonidas"},{"full_name":"Sharir, Micha","first_name":"Micha","last_name":"Sharir"},{"first_name":"Emo","full_name":"Welzl, Emo","last_name":"Welzl"}],"page":"1 - 15","language":[{"iso":"eng"}],"year":"1995","oa_version":"None","article_type":"original","volume":13,"type":"journal_article","date_published":"1995-12-01T00:00:00Z","month":"12","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Discrete & Computational Geometry","doi":"10.1007/BF02574025","publisher":"Springer","date_updated":"2022-06-13T12:37:06Z"},{"_id":"4153","publication":"Blood","date_updated":"2022-06-13T12:02:52Z","publisher":"American Society of Hematology","title":"Hematopoietic mutants identified in a saturation screen of the zebrafish genome","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"01","status":"public","volume":86,"type":"journal_article","date_published":"1995-01-01T00:00:00Z","intvolume":" 86","citation":{"apa":"Ransom, D., Brownlie, A., Haffter, P., Odenthal, J., Kelsh, R., Brand, M., … Zon, L. (1995). Hematopoietic mutants identified in a saturation screen of the zebrafish genome. Blood. American Society of Hematology.","ista":"Ransom D, Brownlie A, Haffter P, Odenthal J, Kelsh R, Brand M, Furutani Seiki M, Granato M, Hammerschmidt M, Heisenberg C-PJ, Jiang Y, Kane D, Mullins M, Van Eden F, Warga R, Nüsslein Volhard C, Zon L. 1995. Hematopoietic mutants identified in a saturation screen of the zebrafish genome. Blood. 86(10), 1912–1912.","short":"D. Ransom, A. Brownlie, P. Haffter, J. Odenthal, R. Kelsh, M. Brand, M. Furutani Seiki, M. Granato, M. Hammerschmidt, C.-P.J. Heisenberg, Y. Jiang, D. Kane, M. Mullins, F. Van Eden, R. Warga, C. Nüsslein Volhard, L. Zon, Blood 86 (1995) 1912–1912.","ieee":"D. Ransom et al., “Hematopoietic mutants identified in a saturation screen of the zebrafish genome,” Blood, vol. 86, no. 10. American Society of Hematology, pp. 1912–1912, 1995.","mla":"Ransom, D., et al. “Hematopoietic Mutants Identified in a Saturation Screen of the Zebrafish Genome.” Blood, vol. 86, no. 10, American Society of Hematology, 1995, pp. 1912–1912.","ama":"Ransom D, Brownlie A, Haffter P, et al. Hematopoietic mutants identified in a saturation screen of the zebrafish genome. Blood. 1995;86(10):1912-1912.","chicago":"Ransom, D., Alison Brownlie, Pascal Haffter, Jörg Odenthal, Robert Kelsh, Michael Brand, Makoto Furutani Seiki, et al. “Hematopoietic Mutants Identified in a Saturation Screen of the Zebrafish Genome.” Blood. American Society of Hematology, 1995."},"oa_version":"None","article_type":"original","language":[{"iso":"eng"}],"year":"1995","page":"1912 - 1912","issue":"10","author":[{"full_name":"Ransom, D.","first_name":"D.","last_name":"Ransom"},{"last_name":"Brownlie","first_name":"Alison","full_name":"Brownlie, Alison"},{"full_name":"Haffter, Pascal","first_name":"Pascal","last_name":"Haffter"},{"first_name":"Jörg","full_name":"Odenthal, Jörg","last_name":"Odenthal"},{"last_name":"Kelsh","full_name":"Kelsh, Robert","first_name":"Robert"},{"first_name":"Michael","full_name":"Brand, Michael","last_name":"Brand"},{"first_name":"Makoto","full_name":"Furutani Seiki, Makoto","last_name":"Furutani Seiki"},{"full_name":"Granato, Michael","first_name":"Michael","last_name":"Granato"},{"first_name":"Matthias","full_name":"Hammerschmidt, Matthias","last_name":"Hammerschmidt"},{"full_name":"Heisenberg, Carl-Philipp J","first_name":"Carl-Philipp J","id":"39427864-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-0912-4566","last_name":"Heisenberg"},{"last_name":"Jiang","full_name":"Jiang, Yunjin","first_name":"Yunjin"},{"first_name":"David","full_name":"Kane, David","last_name":"Kane"},{"first_name":"Mary","full_name":"Mullins, Mary","last_name":"Mullins"},{"last_name":"Van Eden","full_name":"Van Eden, Fredericus","first_name":"Fredericus"},{"last_name":"Warga","full_name":"Warga, Rachel","first_name":"Rachel"},{"first_name":"Christiane","full_name":"Nüsslein Volhard, Christiane","last_name":"Nüsslein Volhard"},{"first_name":"L.","full_name":"Zon, L.","last_name":"Zon"}],"publist_id":"1965","publication_status":"published","day":"01","publication_identifier":{"issn":["0006-4971"]},"date_created":"2018-12-11T12:07:16Z"},{"citation":{"chicago":"Partridge, Linda, Brian Barrie, Nicholas H Barton, Kevin Fowler, and Vernon French. “Rapid Laboratory Evolution of Adult Life History Traits in Drosophila Melanogaster in Response to Temperature.” Evolution. Wiley-Blackwell, 1995. https://doi.org/10.1111/j.1558-5646.1995.tb02285.x.","mla":"Partridge, Linda, et al. “Rapid Laboratory Evolution of Adult Life History Traits in Drosophila Melanogaster in Response to Temperature.” Evolution, vol. 49, no. 3, Wiley-Blackwell, 1995, pp. 538–44, doi:10.1111/j.1558-5646.1995.tb02285.x.","ama":"Partridge L, Barrie B, Barton NH, Fowler K, French V. Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature. Evolution. 1995;49(3):538-544. doi:10.1111/j.1558-5646.1995.tb02285.x","short":"L. Partridge, B. Barrie, N.H. Barton, K. Fowler, V. French, Evolution 49 (1995) 538–544.","ieee":"L. Partridge, B. Barrie, N. H. Barton, K. Fowler, and V. French, “Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature,” Evolution, vol. 49, no. 3. Wiley-Blackwell, pp. 538–544, 1995.","apa":"Partridge, L., Barrie, B., Barton, N. H., Fowler, K., & French, V. (1995). Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature. Evolution. Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.1995.tb02285.x","ista":"Partridge L, Barrie B, Barton NH, Fowler K, French V. 1995. Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature. Evolution. 49(3), 538–544."},"intvolume":" 49","main_file_link":[{"open_access":"1","url":"https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1558-5646.1995.tb02285.x"}],"status":"public","acknowledgement":"We thank Natural Environment Research Council and the Royal Society for financial support.","pmid":1,"title":"Rapid laboratory evolution of adult life history traits in Drosophila melanogaster in response to temperature","_id":"4296","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"Three replicate lines of Drosophila melanogaster were cultured at each of two temperatures (16.5⚬C and 25⚬C) in population cages for 4 yr. The lifespans of both sexes and the fecundity and fertility of the females were then measured at both experimental temperatures. The characters showed evidence of adaptation; flies of both sexes from each selection regime showed higher longevity, and females showed higher fecundity and fertility, than flies from the other selection regime when they were tested at the experimental temperature at which they had evolved. Calculation of intrinsic rates of increase under different assumptions about the rate of population increase showed that the difference between the lines from the two selection regimes became less the higher the rate of population increase, because the lines were more similar in early adulthood than they were later. Despite the increased adaptation of the low-temperature lines to the low temperature, like the high temperature lines they produced progeny at a higher rate at the higher temperature. The lines may have independently evolved adaptations to their respective thermal regimes during the experiment, or there may have been a trade-off between adaptation to the two temperatures, or mutation pressure may have lowered adaptation to the temperature that the flies no longer encountered."}],"publication_identifier":{"issn":["0014-3820"]},"issue":"3","scopus_import":"1","oa_version":"Published Version","external_id":{"pmid":["28565092 "]},"article_type":"original","type":"journal_article","date_published":"1995-06-01T00:00:00Z","volume":49,"oa":1,"quality_controlled":"1","extern":"1","month":"06","date_updated":"2022-06-13T08:42:11Z","doi":"10.1111/j.1558-5646.1995.tb02285.x","publisher":"Wiley-Blackwell","publication":"Evolution","article_processing_charge":"No","day":"01","publication_status":"published","publist_id":"1778","date_created":"2018-12-11T12:08:06Z","page":"538 - 544","author":[{"last_name":"Partridge","first_name":"Linda","full_name":"Partridge, Linda"},{"last_name":"Barrie","full_name":"Barrie, Brian","first_name":"Brian"},{"last_name":"Barton","orcid":"0000-0002-8548-5240","full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H"},{"first_name":"Kevin","full_name":"Fowler, Kevin","last_name":"Fowler"},{"last_name":"French","full_name":"French, Vernon","first_name":"Vernon"}],"language":[{"iso":"eng"}],"year":"1995"},{"external_id":{"pmid":["28593667"]},"article_type":"original","oa_version":"Published Version","date_published":"1995-02-01T00:00:00Z","type":"journal_article","volume":49,"quality_controlled":"1","oa":1,"extern":"1","month":"02","doi":"10.1111/j.1558-5646.1995.tb05955.x","date_updated":"2022-06-13T09:24:40Z","publisher":"Wiley-Blackwell","publication":"Evolution","article_processing_charge":"No","day":"01","publication_status":"published","publist_id":"1779","date_created":"2018-12-11T12:08:06Z","page":"9 - 36","author":[{"last_name":"Sites","full_name":"Sites, Jack","first_name":"Jack"},{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","full_name":"Barton, Nicholas H","orcid":"0000-0002-8548-5240","last_name":"Barton"},{"first_name":"Kent","full_name":"Reed, Kent","last_name":"Reed"}],"language":[{"iso":"eng"}],"year":"1995","intvolume":" 49","citation":{"ama":"Sites J, Barton NH, Reed K. The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico. Evolution. 1995;49(1):9-36. doi:10.1111/j.1558-5646.1995.tb05955.x","mla":"Sites, Jack, et al. “The Genetic Structure of a Mosaic Hybrid Zone between Two Chromosome Races of the Sceloporus Grammicus Complex (Sauria, Phrynosomatidae) in Central Mexico.” Evolution, vol. 49, no. 1, Wiley-Blackwell, 1995, pp. 9–36, doi:10.1111/j.1558-5646.1995.tb05955.x.","chicago":"Sites, Jack, Nicholas H Barton, and Kent Reed. “The Genetic Structure of a Mosaic Hybrid Zone between Two Chromosome Races of the Sceloporus Grammicus Complex (Sauria, Phrynosomatidae) in Central Mexico.” Evolution. Wiley-Blackwell, 1995. https://doi.org/10.1111/j.1558-5646.1995.tb05955.x.","ista":"Sites J, Barton NH, Reed K. 1995. The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico. Evolution. 49(1), 9–36.","apa":"Sites, J., Barton, N. H., & Reed, K. (1995). The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico. Evolution. Wiley-Blackwell. https://doi.org/10.1111/j.1558-5646.1995.tb05955.x","ieee":"J. Sites, N. H. Barton, and K. Reed, “The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico,” Evolution, vol. 49, no. 1. Wiley-Blackwell, pp. 9–36, 1995.","short":"J. Sites, N.H. Barton, K. Reed, Evolution 49 (1995) 9–36."},"main_file_link":[{"url":"https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1558-5646.1995.tb05955.x","open_access":"1"}],"status":"public","acknowledgement":"For field assistance in collecting and mapping of the zone, we thank E. Arevalo, I. Goyenechea, D. Hutchison, M. Man- cilia, F. Mendoza, D. Mink, and J. and H. Sites. The mark- recapture work was carried out by M. Mancilla, F Mendoza, and A. Gonzales. J.W.S. also thanks T. Hinckley and D. Ste­vens of the Brigham Young University Department of Ge­ography for lessons in surveying and map making and use of the field equipment and planimeter. B. Nürnberger pro­vided the digitized coordinates for individual lizards and as­sisted with the analysis of spatial structure and viability. B. Nürnberger, C. MacCallum, J. Mallet, and J. Searle also pro­vided helpful comments on the manuscript. This work was supported by National Science Foundation grants BSR 85- 09092 and 88-22751 to J.W.S., and grants from the Science and Engineering Research Council (GR/H09929) and Natural Environment Research Council (GR3/8002) and the DarwinTrust to N.H.B. The Mexican agency Secretaria de DesarrolloUrbano y Ecologia (now Secretaria de Desarrollo Social) kindly provided scientific collecting permits (to E. Arévalo) for field work in 1989 and 1991.","pmid":1,"title":"The genetic structure of a mosaic hybrid zone between two chromosome races of the Sceloporus grammicus complex (Sauria, Phrynosomatidae) in central Mexico","_id":"4297","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"The F5 (2n = 34) and FM2 (2n = 44-46) chromosome races of the Sceloporus grammicus complex form a parapatric hybrid zone in the Mexican state of Hidalgo, characterized by steep concordant clines among three diagnostic chromosome markers across a straight-line distance of about 2 km. Here, we show that this zone is actually structured into local patches in which hybridization extends over an extremely irregular front. The distribution of hybrid-index (HI) scores across the transect reveals some hybridization at almost all localities mapped in a central 7 km x 3 km area. Pooling the central samples produces both a strong heterozygote deficit for all diagnostic markers and strong linkage disequilibria between all pairwise combinations of these (unlinked) markers. Moreover, a highly significant association exists between the habitat on which each individual was caught and its karyotype (F5 chromosomes are more likely to be found on oak). Analysis of genotype frequencies over a range of spatial scales shows that there is no significant heterozygote deficit or habitat association within local areas of less than about 200 m; however, there is significant linkage disequilibrium over the smallest scales (R = D (pquv)1/2 = 0.29, support limits, 0.18-0.36) over 100 m. These patterns suggest that lizards mate and choose habitats randomly within local patches. This conclusion is supported by mark-recapture estimates of dispersal (≈ 80 m in a generation) and by inference of matings from embryo and maternal karyotypes. Closer examination of the two-dimensional pattern reveals a convoluted cline for all three markers, with a width of 830 m (support limits 770 m-930 m). This cline width, combined with the strength of local linkage disequilibrium, implies a dispersal rate of σ = 160 m in a generation and an effective selection pressure of 30% on each chromosome marker. The proportion of inviable embryos is greater in females from the center of the hybrid zone; this is caused by effects associated with both karyotype and location. The hybrid zone is likely to be maintained by selection against chromosomal heterozygotes, by other kinds of selection against hybrids, and by selection adapting the chromosome races to different habitats. The structure of the contact may be caused by both random drift and by selection in relation to habitat.","lang":"eng"}],"publication_identifier":{"issn":["0014-3820"]},"issue":"1","scopus_import":"1"},{"intvolume":" 49","citation":{"chicago":"Barton, Nicholas H. “Appendix to ‘A Simulation Study of Multilocus Clines’ by S J E Baird.” Evolution. Wiley, 1995. https://doi.org/10.1111/j.1558-5646.1995.tb04431.x.","ama":"Barton NH. Appendix to “A simulation study of multilocus clines” by S J E Baird. Evolution. 1995;49(6):1038-1045. doi:10.1111/j.1558-5646.1995.tb04431.x","mla":"Barton, Nicholas H. “Appendix to ‘A Simulation Study of Multilocus Clines’ by S J E Baird.” Evolution, vol. 49, no. 6, Wiley, 1995, pp. 1038–45, doi:10.1111/j.1558-5646.1995.tb04431.x.","short":"N.H. Barton, Evolution 49 (1995) 1038–1045.","ieee":"N. H. Barton, “Appendix to ‘A simulation study of multilocus clines’ by S J E Baird,” Evolution, vol. 49, no. 6. Wiley, pp. 1038–1045, 1995.","ista":"Barton NH. 1995. Appendix to ‘A simulation study of multilocus clines’ by S J E Baird. Evolution. 49(6), 1038–1045.","apa":"Barton, N. H. (1995). Appendix to “A simulation study of multilocus clines” by S J E Baird. Evolution. Wiley. https://doi.org/10.1111/j.1558-5646.1995.tb04431.x"},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x"}],"status":"public","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","title":"Appendix to \"A simulation study of multilocus clines\" by S J E Baird","_id":"4298","publication_identifier":{"issn":["1558-5646"]},"issue":"6","article_type":"original","oa_version":"Published Version","type":"journal_article","date_published":"1995-12-01T00:00:00Z","volume":49,"month":"12","quality_controlled":"1","oa":1,"extern":"1","article_processing_charge":"No","publisher":"Wiley","doi":"10.1111/j.1558-5646.1995.tb04431.x","date_updated":"2022-06-28T07:47:30Z","publication":"Evolution","date_created":"2018-12-11T12:08:07Z","day":"01","publication_status":"published","publist_id":"1773","author":[{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","full_name":"Barton, Nicholas H","orcid":"0000-0002-8548-5240","last_name":"Barton"}],"page":"1038 - 1045","language":[{"iso":"eng"}],"year":"1995"},{"supervisor":[{"last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"year":"1995","language":[{"iso":"eng"}],"publist_id":"304","publication_status":"published","day":"01","degree_awarded":"PhD","date_created":"2018-12-11T12:08:48Z","page":"1 - 188","author":[{"first_name":"Pei","full_name":"Ho, Pei","last_name":"Ho"}],"extern":"1","oa":1,"month":"08","_id":"4428","publisher":"Cornell University","title":"Automatic analysis of hybrid systems","date_updated":"2022-06-28T07:30:34Z","abstract":[{"lang":"eng","text":"Hybrid systems are real-time systems that react to both discrete and continuous activities (such as analog signals, time, temperature, and speed). Typical examples of hybrid systems are embedded systems, timing-based communication protocols, and digital circuits at the transistor level. Due to the rapid development of microprocessor technology, hybrid systems directly control much of what we depend on in our daily lives. Consequently, the formal specification and verification of hybrid systems has become an active area of research. This dissertation presents the first general framework for the formal specification and verification of hybrid systems, as well as the first hybrid-system analysis tool--HyTech. The framework consists of a graphical finite-state-machine-like language for modeling hybrid systems, a temporal logic for modeling the requirements of hybrid systems, and a computer procedure that verifies modeled hybrid systems against modeled requirements. The tool HyTech is the implementation of the framework using C++ and Mathematica.\r\n\r\nMore specifically, our hybrid-system modeling language, Hybrid Automata, is an extension of timed automata with discrete and continuous variables whose dynamics are governed by differential equations. Our requirement modeling language, ICTL, is a branching-time temporal logic, and is an extension of TCTL with stop-watch variables. Our verification procedure is a symbolic model-checking procedure that verifies linear hybrid automata against ICTL formulas. To make HyTech more efficient and effective, we use model-checking strategies and abstract operators that can expedite the verification process. To enable HyTech to verify nonlinear hybrid automata, we introduce two translations from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present the application of HyTech to three nontrivial hybrid systems taken from the literature."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","main_file_link":[{"url":"https://hdl.handle.net/1813/7193","open_access":"1"}],"citation":{"chicago":"Ho, Pei. “Automatic Analysis of Hybrid Systems.” Cornell University, 1995.","ama":"Ho P. Automatic analysis of hybrid systems. 1995:1-188.","mla":"Ho, Pei. Automatic Analysis of Hybrid Systems. Cornell University, 1995, pp. 1–188.","short":"P. Ho, Automatic Analysis of Hybrid Systems, Cornell University, 1995.","ieee":"P. Ho, “Automatic analysis of hybrid systems,” Cornell University, 1995.","ista":"Ho P. 1995. Automatic analysis of hybrid systems. Cornell University.","apa":"Ho, P. (1995). Automatic analysis of hybrid systems. Cornell University."},"oa_version":"Published Version","status":"public","type":"dissertation","date_published":"1995-08-01T00:00:00Z"},{"abstract":[{"lang":"eng","text":"This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies that have been incorporated into HyTech, and we illustrate the use of HyTech with three nontrivial case studies."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4447","title":"HyTech: The Cornell Hybrid Technology Tool","acknowledgement":"This research was supported in part by the National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","status":"public","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60472-3_14"}],"editor":[{"first_name":"Antsaklis","full_name":"Panos, Antsaklis","last_name":"Panos"},{"last_name":"Kohn","first_name":"Wolf","full_name":"Kohn, Wolf"},{"last_name":"Nerode","first_name":"Anil","full_name":"Nerode, Anil"},{"last_name":"Sastry","first_name":"Shankar","full_name":"Sastry, Shankar"}],"intvolume":" 999","citation":{"ista":"Henzinger TA, Ho P. 1995. HyTech: The Cornell Hybrid Technology Tool. 4th International Hybrid Systems Workshop. Hybrid Systems IIILNCS, LNCS, vol. 999, 265–293.","apa":"Henzinger, T. A., & Ho, P. (1995). HyTech: The Cornell Hybrid Technology Tool. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.), 4th International Hybrid Systems Workshop (Vol. 999, pp. 265–293). New Brunswick, NJ, United States of America: Springer. https://doi.org/10.1007/3-540-60472-3_14","ieee":"T. A. Henzinger and P. Ho, “HyTech: The Cornell Hybrid Technology Tool,” in 4th International Hybrid Systems Workshop, New Brunswick, NJ, United States of America, 1995, vol. 999, pp. 265–293.","short":"T.A. Henzinger, P. Ho, in:, A. Panos, W. Kohn, A. Nerode, S. Sastry (Eds.), 4th International Hybrid Systems Workshop, Springer, 1995, pp. 265–293.","ama":"Henzinger TA, Ho P. HyTech: The Cornell Hybrid Technology Tool. In: Panos A, Kohn W, Nerode A, Sastry S, eds. 4th International Hybrid Systems Workshop. Vol 999. LNCS. Springer; 1995:265-293. doi:10.1007/3-540-60472-3_14","mla":"Henzinger, Thomas A., and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” 4th International Hybrid Systems Workshop, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 265–93, doi:10.1007/3-540-60472-3_14.","chicago":"Henzinger, Thomas A, and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” In 4th International Hybrid Systems Workshop, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:265–93. LNCS. Springer, 1995. https://doi.org/10.1007/3-540-60472-3_14."},"publication_identifier":{"isbn":["9783540683346"]},"article_processing_charge":"No","publication":"4th International Hybrid Systems Workshop","doi":"10.1007/3-540-60472-3_14","date_updated":"2022-06-10T11:24:15Z","publisher":"Springer","month":"01","extern":"1","quality_controlled":"1","series_title":"LNCS","volume":999,"type":"conference","date_published":"1995-01-01T00:00:00Z","oa_version":"None","language":[{"iso":"eng"}],"year":"1995","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"}],"alternative_title":["LNCS"],"page":"265 - 293","conference":{"start_date":"1995-10-22","name":"Hybrid Systems III","location":" New Brunswick, NJ, United States of America","end_date":"1955-10-25"},"date_created":"2018-12-11T12:08:54Z","publist_id":"281","publication_status":"published","day":"01"},{"article_processing_charge":"No","publication":"3rd International Hybrid Systems Workshop","publisher":"Springer","date_updated":"2022-06-10T11:48:59Z","doi":"10.1007/3-540-60472-3_13","month":"01","extern":"1","quality_controlled":"1","volume":999,"date_published":"1995-01-01T00:00:00Z","type":"conference","oa_version":"None","year":"1995","language":[{"iso":"eng"}],"author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ho","first_name":"Pei","full_name":"Ho, Pei"}],"page":"252 - 264","alternative_title":["LNCS"],"conference":{"name":"Hybrid Systems II","start_date":"1994-10-28","end_date":"1994-10-30","location":"Ithaca, NY, United States of America"},"date_created":"2018-12-11T12:08:54Z","publist_id":"282","publication_status":"published","day":"01","abstract":[{"text":"We report on several abstract interpretation strategies that are designed to improve the performance of HyTech, a symbolic model checker for linear hybrid systems. We (1) simultaneously compute the target region from different directions, (2) conservatively approximate the target region by dropping constraints, and (3) iteratively refine the approximation until sufficient precision is obtained. We consider the standard abstract convex-hull operator and a novel abstract extrapolation operator.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4448","title":"A note on abstract-interpretation strategies for hybrid automata","acknowledgement":" National Science Foundation under grant CCR-9200794, by the Air Force Office of Scientific Research under contract F49620-93-1-0056, by the Office of Naval Research under YIP grant N00014-95-1-0520, and by the Defense Advanced Research Projects Agency under grant NAG2-892.","status":"public","editor":[{"first_name":"Antsaklis","full_name":"Panos, Antsaklis","last_name":"Panos"},{"last_name":"Kohn","full_name":"Kohn, Wolf","first_name":"Wolf"},{"last_name":"Nerode","first_name":"Anil","full_name":"Nerode, Anil"},{"full_name":"Sastry, Shankar","first_name":"Shankar","last_name":"Sastry"}],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60472-3_13"}],"citation":{"apa":"Henzinger, T. A., & Ho, P. (1995). A note on abstract-interpretation strategies for hybrid automata. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.), 3rd International Hybrid Systems Workshop (Vol. 999, pp. 252–264). Ithaca, NY, United States of America: Springer. https://doi.org/10.1007/3-540-60472-3_13","ista":"Henzinger TA, Ho P. 1995. A note on abstract-interpretation strategies for hybrid automata. 3rd International Hybrid Systems Workshop. Hybrid Systems II, LNCS, vol. 999, 252–264.","short":"T.A. Henzinger, P. Ho, in:, A. Panos, W. Kohn, A. Nerode, S. Sastry (Eds.), 3rd International Hybrid Systems Workshop, Springer, 1995, pp. 252–264.","ieee":"T. A. Henzinger and P. Ho, “A note on abstract-interpretation strategies for hybrid automata,” in 3rd International Hybrid Systems Workshop, Ithaca, NY, United States of America, 1995, vol. 999, pp. 252–264.","mla":"Henzinger, Thomas A., and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” 3rd International Hybrid Systems Workshop, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 252–64, doi:10.1007/3-540-60472-3_13.","ama":"Henzinger TA, Ho P. A note on abstract-interpretation strategies for hybrid automata. In: Panos A, Kohn W, Nerode A, Sastry S, eds. 3rd International Hybrid Systems Workshop. Vol 999. Springer; 1995:252-264. doi:10.1007/3-540-60472-3_13","chicago":"Henzinger, Thomas A, and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” In 3rd International Hybrid Systems Workshop, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:252–64. Springer, 1995. https://doi.org/10.1007/3-540-60472-3_13."},"intvolume":" 999","publication_identifier":{"isbn":["9783540604723"]}},{"publication_identifier":{"isbn":["9783540494133"]},"scopus_import":"1","status":"public","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60045-0_53"}],"intvolume":" 939","citation":{"short":"T.A. Henzinger, P. Ho, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 225–238.","ieee":"T. A. Henzinger and P. Ho, “Algorithmic analysis of nonlinear hybrid systems,” in 7th International Conference on Computer Aided Verification, Liege, Belgium, 1995, vol. 939, pp. 225–238.","apa":"Henzinger, T. A., & Ho, P. (1995). Algorithmic analysis of nonlinear hybrid systems. In 7th International Conference on Computer Aided Verification (Vol. 939, pp. 225–238). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_53","ista":"Henzinger TA, Ho P. 1995. Algorithmic analysis of nonlinear hybrid systems. 7th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 939, 225–238.","chicago":"Henzinger, Thomas A, and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” In 7th International Conference on Computer Aided Verification, 939:225–38. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_53.","mla":"Henzinger, Thomas A., and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” 7th International Conference on Computer Aided Verification, vol. 939, Springer, 1995, pp. 225–38, doi:10.1007/3-540-60045-0_53.","ama":"Henzinger TA, Ho P. Algorithmic analysis of nonlinear hybrid systems. In: 7th International Conference on Computer Aided Verification. Vol 939. Springer; 1995:225-238. doi:10.1007/3-540-60045-0_53"},"abstract":[{"text":"Hybrid systems model discrete programs that are embedded in continuous environments. Model-checking tools are available for the analysis of linear hybrid systems, whose continuous variables are bounded by piecewise-linear trajectories. Most embedded programs, however, operate in nonlinear environments. We present, analyze, and apply two algorithms for translating nonlinear hybrid systems into linear hybrid systems.\r\nThe clock translation replaces nonlinear variables by clock variables; the rate translation approximates nonlinear variables by piecewise-linear envelopes. Both translations are sound for reachability; that is, if we establish a safety property of the translated linear system, we may conclude that the original nonlinear system satisfies the property. The clock translation is also complete for reachability; that is, the original system and the translated system satisfy the same safety properties. The two translations apply to incomparable classes of nonlinear hybrid systems. From the clock translation we obtain a new decidability result for hybrid systems.\r\nWith the help of Hytech, a symbolic model checker for linear hybrid systems, we automatically verify a nonlinear railroad gate control program using the clock translation, and a nonlinear temperature control program using the rate translation.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4450","title":"Algorithmic analysis of nonlinear hybrid systems","acknowledgement":"This research was supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"}],"alternative_title":["LNCS"],"page":"225 - 238","conference":{"name":"CAV: Computer Aided Verification","start_date":"1995-07-03","end_date":"1995-07-05","location":"Liege, Belgium"},"date_created":"2018-12-11T12:08:55Z","publication_status":"published","publist_id":"280","day":"01","language":[{"iso":"eng"}],"year":"1995","volume":939,"type":"conference","date_published":"1995-01-01T00:00:00Z","oa_version":"None","article_processing_charge":"No","publication":"7th International Conference on Computer Aided Verification","date_updated":"2022-06-10T09:48:52Z","publisher":"Springer","doi":"10.1007/3-540-60045-0_53","month":"01","extern":"1","quality_controlled":"1"},{"date_created":"2018-12-11T12:09:09Z","day":"01","publist_id":"230","publication_status":"published","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Pei","full_name":"Ho, Pei","last_name":"Ho"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"1995-05-19","end_date":"1995-05-20","location":"Aarhus, Denmark"},"alternative_title":["LNCS"],"page":"41 - 71","language":[{"iso":"eng"}],"year":"1995","oa_version":"None","date_published":"1995-01-01T00:00:00Z","type":"conference","volume":1019,"month":"01","quality_controlled":"1","extern":"1","article_processing_charge":"No","date_updated":"2022-06-10T09:00:05Z","publisher":"Springer","doi":"10.1007/3-540-60630-0_3","publication":"1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems","publication_identifier":{"isbn":["9783540606307"]},"scopus_import":"1","intvolume":" 1019","citation":{"apa":"Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). A user guide to HyTech. In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 1019, pp. 41–71). Aarhus, Denmark: Springer. https://doi.org/10.1007/3-540-60630-0_3","ista":"Henzinger TA, Ho P, Wong Toi H. 1995. A user guide to HyTech. 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 1019, 41–71.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 1995, pp. 41–71.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “A user guide to HyTech,” in 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, 1995, vol. 1019, pp. 41–71.","mla":"Henzinger, Thomas A., et al. “A User Guide to HyTech.” 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, vol. 1019, Springer, 1995, pp. 41–71, doi:10.1007/3-540-60630-0_3.","ama":"Henzinger TA, Ho P, Wong Toi H. A user guide to HyTech. In: 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems. Vol 1019. Springer; 1995:41-71. doi:10.1007/3-540-60630-0_3","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “A User Guide to HyTech.” In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, 1019:41–71. Springer, 1995. https://doi.org/10.1007/3-540-60630-0_3."},"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60630-0_3"}],"status":"public","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 grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056, and by the ARPA grant NAG2-892.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"HyTech is a tool for the automated analysis of embedded systems. This document, designed for the first-time user of HyTech, guides the reader through the underlying system model, and through the input language for describing and analyzing systems. The guide gives several examples of usage, and some hints for gaining maximal computational efficiency from the tool.\r\nThe version of HyTech described in this guide was released in August 1995, and is available through anonymous ftp from ftp.cs.cornell.edu in the directory pub/tah/HyTech, and through the World-Wide Web via HyTech's home page http:/www.cs.cornell.edu/Info/People/tah/hytech.html."}],"title":"A user guide to HyTech","_id":"4497"},{"status":"public","date_published":"1995-11-01T00:00:00Z","type":"conference","citation":{"short":"M.H. Henzinger, T.A. Henzinger, P. Kopke, in:, Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 453–462.","ieee":"M. H. Henzinger, T. A. Henzinger, and P. Kopke, “Computing simulations on finite and infinite graphs,” in Proceedings of IEEE 36th Annual Foundations of Computer Science, Milwaukee, WI, United States of America, 1995, pp. 453–462.","ista":"Henzinger MH, Henzinger TA, Kopke P. 1995. Computing simulations on finite and infinite graphs. Proceedings of IEEE 36th Annual Foundations of Computer Science. FOCS: Foundations of Computer Science, 453–462.","apa":"Henzinger, M. H., Henzinger, T. A., & Kopke, P. (1995). Computing simulations on finite and infinite graphs. In Proceedings of IEEE 36th Annual Foundations of Computer Science (pp. 453–462). Milwaukee, WI, United States of America: IEEE. https://doi.org/10.1109/SFCS.1995.492576","chicago":"Henzinger, Monika H, Thomas A Henzinger, and Peter Kopke. “Computing Simulations on Finite and Infinite Graphs.” In Proceedings of IEEE 36th Annual Foundations of Computer Science, 453–62. IEEE, 1995. https://doi.org/10.1109/SFCS.1995.492576.","ama":"Henzinger MH, Henzinger TA, Kopke P. Computing simulations on finite and infinite graphs. In: Proceedings of IEEE 36th Annual Foundations of Computer Science. IEEE; 1995:453-462. doi:10.1109/SFCS.1995.492576","mla":"Henzinger, Monika H., et al. “Computing Simulations on Finite and Infinite Graphs.” Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 453–62, doi:10.1109/SFCS.1995.492576."},"oa_version":"None","_id":"4498","publication":"Proceedings of IEEE 36th Annual Foundations of Computer Science","doi":"10.1109/SFCS.1995.492576","publisher":"IEEE","date_updated":"2023-02-09T08:43:48Z","title":"Computing simulations on finite and infinite graphs","abstract":[{"lang":"eng","text":"We present algorithms for computing similarity relations of labeled graphs. Similarity relations have applications for the refinement and verification of reactive systems. For finite graphs, we present an O(mn) algorithm for computing the similarity relation of a graph with n vertices and m edges (assuming m⩾n). For effectively presented infinite graphs, we present a symbolic similarity-checking procedure that terminates if a finite similarity relation exists. We show that 2D rectangular automata, which model discrete reactive systems with continuous environments, define effectively presented infinite graphs with finite similarity relations. It follows that the refinement problem and the ∀CTL* model-checking problem are decidable for 2D rectangular automata"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"11","page":"453 - 462","conference":{"start_date":"1995-10-23","name":"FOCS: Foundations of Computer Science","location":"Milwaukee, WI, United States of America","end_date":"1995-10-25"},"author":[{"full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","last_name":"Henzinger","orcid":"0000-0002-5008-6530"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Kopke","full_name":"Kopke, Peter","first_name":"Peter"}],"publication_status":"published","publist_id":"231","day":"01","publication_identifier":{"issn":["0272-5428"],"isbn":["0818671831"]},"date_created":"2018-12-11T12:09:10Z","language":[{"iso":"eng"}],"year":"1995","scopus_import":"1"},{"scopus_import":"1","language":[{"iso":"eng"}],"year":"1995","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Ho","first_name":"Pei","full_name":"Ho, Pei"},{"last_name":"Wong Toi","first_name":"Howard","full_name":"Wong Toi, Howard"}],"conference":{"name":"RTSS: Real-Time Systems Symposium","start_date":"1995-12-05","end_date":"1995-12-07","location":"Pisa, Italy"},"page":"56 - 65","publication_identifier":{"isbn":["0818673370"]},"date_created":"2018-12-11T12:09:10Z","day":"01","publication_status":"published","publist_id":"232","article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"We describe a new implementation of HYTECH, a symbolic model checker for hybrid systems. Given a parametric description of an embedded system as a collection of communicating automata, HYTECH automatically computes the conditions on the parameters under which the system satisfies its safety and timing requirements. While the original HYTECH prototype was based on the symbolic algebra tool Mathematica, the new implementation is written in C++ and builds on geometric algorithms instead of formula manipulation. The new HYTECH offers a cleaner and more expressive input language, greater portability, superior performance (typically two to three orders of magnitude), and new features such as diagnostic error-trace generation. We illustrate the effectiveness of the new implementation by applying HYTECH to the automatic parametric analysis of the generic railroad crossing benchmark problem and to an active structure control algorithm","lang":"eng"}],"publisher":"IEEE","date_updated":"2022-06-10T09:33:19Z","doi":"10.1109/REAL.1995.495196 ","title":"HyTech: The next generation","publication":"Proceedings 16th IEEE Real-Time Systems Symposium","_id":"4499","month":"01","quality_controlled":"1","extern":"1","date_published":"1995-01-01T00:00:00Z","type":"conference","status":"public","oa_version":"None","citation":{"mla":"Henzinger, Thomas A., et al. “HyTech: The next Generation.” Proceedings 16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65, doi:10.1109/REAL.1995.495196 .","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: The next generation. In: Proceedings 16th IEEE Real-Time Systems Symposium. IEEE; 1995:56-65. doi:10.1109/REAL.1995.495196 ","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: The next Generation.” In Proceedings 16th IEEE Real-Time Systems Symposium, 56–65. IEEE, 1995. https://doi.org/10.1109/REAL.1995.495196 .","apa":"Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). HyTech: The next generation. In Proceedings 16th IEEE Real-Time Systems Symposium (pp. 56–65). Pisa, Italy: IEEE. https://doi.org/10.1109/REAL.1995.495196 ","ista":"Henzinger TA, Ho P, Wong Toi H. 1995. HyTech: The next generation. Proceedings 16th IEEE Real-Time Systems Symposium. RTSS: Real-Time Systems Symposium, 56–65.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, Proceedings 16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65.","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: The next generation,” in Proceedings 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 1995, pp. 56–65."},"main_file_link":[{"url":"https://ieeexplore.ieee.org/document/495196"}]},{"language":[{"iso":"eng"}],"year":"1995","date_created":"2018-12-11T12:09:10Z","publication_status":"published","publist_id":"229","day":"01","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"last_name":"Kopke","full_name":"Kopke, Peter","first_name":"Peter"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"alternative_title":["LNCS"],"page":"417 - 428","conference":{"start_date":"1995-07-10","name":"ICALP: Automata, Languages and Programming","location":"Szeged, Hungary","end_date":"1995-07-14"},"month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"22nd International Colloquium on Automata, Languages and Programming ","doi":"10.1007/3-540-60084-1_93","publisher":"Springer","date_updated":"2022-06-09T14:58:31Z","oa_version":"None","volume":944,"date_published":"1995-01-01T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9783540600848"]},"acknowledgement":"This research was 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, by the Defense Advanced Research Projects Agency under grant NAG2-892, and by the U.S. Army Research Office through the Mathematical Sciences Institute of Cornell University, Contract Number DAAL03-91-C-0027.\r\nThe full version of this paper is available from the Department of Computer Science, Cornell University, Ithaca, NY 14853, as Technical Report TR95-1496.","abstract":[{"text":"We investigate the expressive power of timing restrictions on labeled transition systems. In particular, we show how constraints on clock variables together with a uniform liveness condition—the divergence of time—can express Büchi, Muller, Streett, Rabin, and weak and strong fairness conditions on a given labeled transition system. We then consider the effect, on both timed and time-abstract expressiveness, of varying the following parameters: time domain (discrete or dense), number of clocks, number of states, and size of constants used in timing restrictions.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4500","title":"The expressive power of clocks","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60084-1_93"}],"intvolume":" 944","citation":{"ama":"Henzinger TA, Kopke P, Wong Toi H. The expressive power of clocks. In: 22nd International Colloquium on Automata, Languages and Programming . Vol 944. Springer; 1995:417-428. doi:10.1007/3-540-60084-1_93","mla":"Henzinger, Thomas A., et al. “The Expressive Power of Clocks.” 22nd International Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995, pp. 417–28, doi:10.1007/3-540-60084-1_93.","chicago":"Henzinger, Thomas A, Peter Kopke, and Howard Wong Toi. “The Expressive Power of Clocks.” In 22nd International Colloquium on Automata, Languages and Programming , 944:417–28. Springer, 1995. https://doi.org/10.1007/3-540-60084-1_93.","ista":"Henzinger TA, Kopke P, Wong Toi H. 1995. The expressive power of clocks. 22nd International Colloquium on Automata, Languages and Programming . ICALP: Automata, Languages and Programming, LNCS, vol. 944, 417–428.","apa":"Henzinger, T. A., Kopke, P., & Wong Toi, H. (1995). The expressive power of clocks. In 22nd International Colloquium on Automata, Languages and Programming (Vol. 944, pp. 417–428). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_93","short":"T.A. Henzinger, P. Kopke, H. Wong Toi, in:, 22nd International Colloquium on Automata, Languages and Programming , Springer, 1995, pp. 417–428.","ieee":"T. A. Henzinger, P. Kopke, and H. Wong Toi, “The expressive power of clocks,” in 22nd International Colloquium on Automata, Languages and Programming , Szeged, Hungary, 1995, vol. 944, pp. 417–428."},"status":"public"},{"year":"1995","language":[{"iso":"eng"}],"page":"373 - 382","conference":{"start_date":"1995-05-29","name":"STOC: Symposium on the Theory of Computing","location":"Las Vegas, NV, United States of America","end_date":"1995-06-01"},"author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Kopke","first_name":"Peter","full_name":"Kopke, Peter"},{"last_name":"Puri","first_name":"Anuj","full_name":"Puri, Anuj"},{"last_name":"Varaiya","full_name":"Varaiya, P.","first_name":"P."}],"publist_id":"228","publication_status":"published","day":"01","publication_identifier":{"isbn":["9780897917186"]},"date_created":"2018-12-11T12:09:11Z","publication":"Proceedings of the 27th annual ACM symposium on Theory of computing","_id":"4502","doi":"10.1145/225058.225162","date_updated":"2022-06-09T14:40:29Z","publisher":"ACM","title":"What's decidable about hybrid automata?","abstract":[{"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 the precise boundary between decidability and undecidability of the reachability problem for hybrid automata.\r\n\r\nOn the positive side, we give an (optimal) PSPACE reachability algorithm for the case of initialized rectangular automata, where all analog variables follow 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 omega-languages of initialized rectangular automata with bounded nondeterminism.\r\n\r\nOn 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.","lang":"eng"}],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"We thank Howard Wong-Toi for a careful reading.\r\n","extern":"1","oa":1,"quality_controlled":"1","month":"01","status":"public","date_published":"1995-01-01T00:00:00Z","type":"conference","main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/225058.225162","open_access":"1"}],"citation":{"ieee":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” in Proceedings of the 27th annual ACM symposium on Theory of computing, Las Vegas, NV, United States of America, 1995, pp. 373–382.","short":"T.A. Henzinger, P. Kopke, A. Puri, P. Varaiya, in:, Proceedings of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–382.","ista":"Henzinger TA, Kopke P, Puri A, Varaiya P. 1995. What’s decidable about hybrid automata? Proceedings of the 27th annual ACM symposium on Theory of computing. STOC: Symposium on the Theory of Computing, 373–382.","apa":"Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1995). What’s decidable about hybrid automata? In Proceedings of the 27th annual ACM symposium on Theory of computing (pp. 373–382). Las Vegas, NV, United States of America: ACM. https://doi.org/10.1145/225058.225162","chicago":"Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” In Proceedings of the 27th Annual ACM Symposium on Theory of Computing, 373–82. ACM, 1995. https://doi.org/10.1145/225058.225162.","ama":"Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? In: Proceedings of the 27th Annual ACM Symposium on Theory of Computing. ACM; 1995:373-382. doi:10.1145/225058.225162","mla":"Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” Proceedings of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–82, doi:10.1145/225058.225162."},"oa_version":"Published Version"},{"acknowledgement":"This research was supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.\r\n","title":"Hybrid automata with finite bisimulations","_id":"4518","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"The analysis, verification, and control of hybrid automata with finite bisimulations can be reduced to finite-state problems. We advocate a time-abstract, phase-based methodology for checking if a given hybrid automaton has a finite bisimulation. First, we factor the automaton into two components, a boolean automaton with a discrete dynamics on the finite state space B m and a euclidean automaton with a continuous dynamics on the infinite state space n . Second, we investigate the phase portrait of the euclidean component. In this fashion, we obtain new decidability results for hybrid systems as well as new, uniform proofs of known decidability results.","lang":"eng"}],"citation":{"chicago":"Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” In 22nd International Colloquium on Automata, Languages and Programming , 944:324–35. Springer, 1995. https://doi.org/10.1007/3-540-60084-1_85.","ama":"Henzinger TA. Hybrid automata with finite bisimulations. In: 22nd International Colloquium on Automata, Languages and Programming . Vol 944. Springer; 1995:324-335. doi:10.1007/3-540-60084-1_85","mla":"Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” 22nd International Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995, pp. 324–35, doi:10.1007/3-540-60084-1_85.","ieee":"T. A. Henzinger, “Hybrid automata with finite bisimulations,” in 22nd International Colloquium on Automata, Languages and Programming , Szeged, Hungary, 1995, vol. 944, pp. 324–335.","short":"T.A. Henzinger, in:, 22nd International Colloquium on Automata, Languages and Programming , Springer, 1995, pp. 324–335.","ista":"Henzinger TA. 1995. Hybrid automata with finite bisimulations. 22nd International Colloquium on Automata, Languages and Programming . ICALP: Automata, Languages and Programming, LNCS, vol. 944, 324–335.","apa":"Henzinger, T. A. (1995). Hybrid automata with finite bisimulations. In 22nd International Colloquium on Automata, Languages and Programming (Vol. 944, pp. 324–335). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_85"},"intvolume":" 944","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60084-1_85"}],"status":"public","publication_identifier":{"isbn":["9783540600848"]},"quality_controlled":"1","extern":"1","month":"01","publisher":"Springer","date_updated":"2022-06-09T14:21:08Z","doi":"10.1007/3-540-60084-1_85","publication":"22nd International Colloquium on Automata, Languages and Programming ","article_processing_charge":"No","oa_version":"None","date_published":"1995-01-01T00:00:00Z","type":"conference","volume":944,"year":"1995","language":[{"iso":"eng"}],"day":"01","publication_status":"published","publist_id":"212","date_created":"2018-12-11T12:09:16Z","conference":{"start_date":"1995-07-10","name":"ICALP: Automata, Languages and Programming","location":"Szeged, Hungary","end_date":"1995-07-14"},"alternative_title":["LNCS"],"page":"324 - 335","author":[{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"}]},{"publication":"7th International Conference on Computer Aided Verification","publisher":"Springer","doi":"10.1007/3-540-60045-0_49","date_updated":"2022-06-09T14:05:04Z","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"01","volume":939,"date_published":"1995-01-01T00:00:00Z","type":"conference","oa_version":"None","language":[{"iso":"eng"}],"year":"1995","page":"166 - 179","alternative_title":["LNCS"],"conference":{"start_date":"1995-07-03","name":"CAV: Computer Aided Verification","location":"Liege, Belgium","end_date":"1995-07-05"},"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"publist_id":"120","publication_status":"published","day":"01","date_created":"2018-12-11T12:09:37Z","_id":"4587","title":"Local liveness for compositional modeling of fair reactive systems","abstract":[{"text":"We argue that the standard constraints on liveness conditions in nonblocking trace models—machine closure for closed systems, and receptiveness for open systems—are unnecessarily weak and complex, and that liveness should, instead, be specified by augmenting transition systems with acceptance conditions that satisfy a locality constraint. First, locality implies machine closure and receptiveness, and thus permits the composition and modular verification of live transition systems. Second, while machine closure and receptiveness are based on infinite games, locality is based on repeated finite games, and thus easier to check. Third, no expressive power is lost by the restriction to local liveness conditions. We illustrate the appeal of local liveness using the model of Fair Reactive Systems, a nonblocking trace model of communicating processes.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","acknowledgement":"Supported in part by the NSF grant CCR-9200794, by the AFOSR contract F49620-93-1-0056, and by the DARPA grant NAG2-892.","status":"public","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60045-0_49"}],"intvolume":" 939","citation":{"chicago":"Alur, Rajeev, and Thomas A Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” In 7th International Conference on Computer Aided Verification, 939:166–79. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_49.","ama":"Alur R, Henzinger TA. Local liveness for compositional modeling of fair reactive systems. In: 7th International Conference on Computer Aided Verification. Vol 939. Springer; 1995:166-179. doi:10.1007/3-540-60045-0_49","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” 7th International Conference on Computer Aided Verification, vol. 939, Springer, 1995, pp. 166–79, doi:10.1007/3-540-60045-0_49.","ieee":"R. Alur and T. A. Henzinger, “Local liveness for compositional modeling of fair reactive systems,” in 7th International Conference on Computer Aided Verification, Liege, Belgium, 1995, vol. 939, pp. 166–179.","short":"R. Alur, T.A. Henzinger, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 166–179.","ista":"Alur R, Henzinger TA. 1995. Local liveness for compositional modeling of fair reactive systems. 7th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 939, 166–179.","apa":"Alur, R., & Henzinger, T. A. (1995). Local liveness for compositional modeling of fair reactive systems. In 7th International Conference on Computer Aided Verification (Vol. 939, pp. 166–179). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_49"},"publication_identifier":{"isbn":["978-3-540-60045-9"]}},{"language":[{"iso":"eng"}],"year":"1995","date_created":"2018-12-11T12:09:45Z","publication_status":"published","publist_id":"94","day":"06","author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"last_name":"Courcoubetis","first_name":"Costas","full_name":"Courcoubetis, Costas"},{"full_name":"Halbwachs, Nicolas","first_name":"Nicolas","last_name":"Halbwachs"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"},{"full_name":"Nicollin, Xavier","first_name":"Xavier","last_name":"Nicollin"},{"first_name":"Alfredo","full_name":"Olivero, Alfredo","last_name":"Olivero"},{"last_name":"Sifakis","first_name":"Joseph","full_name":"Sifakis, Joseph"},{"first_name":"Sergio","full_name":"Yovine, Sergio","last_name":"Yovine"}],"page":"3 - 34","month":"02","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Theoretical Computer Science","date_updated":"2022-06-09T13:40:48Z","doi":"10.1016/0304-3975(94)00202-T","publisher":"Elsevier","oa_version":"None","article_type":"original","volume":138,"date_published":"1995-02-06T00:00:00Z","type":"journal_article","publication_identifier":{"issn":["0304-3975"]},"issue":"1","abstract":[{"text":"We present a general framework for the formal specification and algorithmic analysis of hybrid systems. A hybrid system consists of a discrete program with an analog environment. We model hybrid systems as finite automata equipped with variables that evolve continuously with time according to dynamical laws. For verification purposes, we restrict ourselves to linear hybrid systems, where all variables follow piecewise-linear trajectories. We provide decidability and undecidability results for classes of linear hybrid systems, and we show that standard program-analysis techniques can be adapted to linear hybrid systems. In particular, we consider symbolic model-checking and minimization procedures that are based on the reachability analysis of an infinite state space. The procedures iteratively compute state sets that are definable as unions of convex polyhedra in multidimensional real space. We also present approximation techniques for dealing with systems for which the iterative procedures do not converge.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4613","title":"The algorithmic analysis of hybrid systems","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/030439759400202T?via%3Dihub"}],"citation":{"ista":"Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis J, Yovine S. 1995. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 138(1), 3–34.","apa":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin, X., … Yovine, S. (1995). The algorithmic analysis of hybrid systems. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/0304-3975(94)00202-T","short":"R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, Theoretical Computer Science 138 (1995) 3–34.","ieee":"R. Alur et al., “The algorithmic analysis of hybrid systems,” Theoretical Computer Science, vol. 138, no. 1. Elsevier, pp. 3–34, 1995.","ama":"Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. Theoretical Computer Science. 1995;138(1):3-34. doi:10.1016/0304-3975(94)00202-T","mla":"Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” Theoretical Computer Science, vol. 138, no. 1, Elsevier, 1995, pp. 3–34, doi:10.1016/0304-3975(94)00202-T.","chicago":"Alur, Rajeev, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, Pei Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis of Hybrid Systems.” Theoretical Computer Science. Elsevier, 1995. https://doi.org/10.1016/0304-3975(94)00202-T."},"intvolume":" 138","status":"public"},{"date_published":"1994-05-16T00:00:00Z","type":"journal_article","volume":344,"article_type":"original","external_id":{"pmid":["8187868"]},"oa_version":"Published Version","article_processing_charge":"No","publisher":"Elsevier","date_updated":"2022-06-09T13:21:50Z","doi":"10.1016/0014-5793(94)00370-X","publication":"FEBS Letters","month":"05","oa":1,"quality_controlled":"1","extern":"1","author":[{"orcid":"0000-0002-0977-7989","last_name":"Sazanov","full_name":"Sazanov, Leonid A","first_name":"Leonid A","id":"338D39FE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Jackson, Julie","first_name":"Julie","last_name":"Jackson"}],"page":"109 - 116","date_created":"2018-12-11T11:54:52Z","day":"16","publist_id":"5134","publication_status":"published","year":"1994","language":[{"iso":"eng"}],"status":"public","citation":{"apa":"Sazanov, L. A., & Jackson, J. (1994). Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria. FEBS Letters. Elsevier. https://doi.org/10.1016/0014-5793(94)00370-X","ista":"Sazanov LA, Jackson J. 1994. Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria. FEBS Letters. 344(2–3), 109–116.","short":"L.A. Sazanov, J. Jackson, FEBS Letters 344 (1994) 109–116.","ieee":"L. A. Sazanov and J. Jackson, “Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria,” FEBS Letters, vol. 344, no. 2–3. Elsevier, pp. 109–116, 1994.","mla":"Sazanov, Leonid A., and Julie Jackson. “Proton Translocating Transhydrogenase and NAD- and NADP-Linked Isocitrate Dehydrogenases Operate in a Substrate Cycle Which Contributes to Fine Regulation of the Tricarboxylic Acid Cycle Activity in Mitochondria.” FEBS Letters, vol. 344, no. 2–3, Elsevier, 1994, pp. 109–16, doi:10.1016/0014-5793(94)00370-X.","ama":"Sazanov LA, Jackson J. Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria. FEBS Letters. 1994;344(2-3):109-116. doi:10.1016/0014-5793(94)00370-X","chicago":"Sazanov, Leonid A, and Julie Jackson. “Proton Translocating Transhydrogenase and NAD- and NADP-Linked Isocitrate Dehydrogenases Operate in a Substrate Cycle Which Contributes to Fine Regulation of the Tricarboxylic Acid Cycle Activity in Mitochondria.” FEBS Letters. Elsevier, 1994. https://doi.org/10.1016/0014-5793(94)00370-X."},"intvolume":" 344","main_file_link":[{"url":"https://febs.onlinelibrary.wiley.com/doi/abs/10.1016/0014-5793%2894%2900370-X","open_access":"1"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"H+-transhydrogenase (H+-Thase) and NADP-linked isocitrate dehydrogenase (NADP-ICDH) are very active in animal mitochondria but their physiological function is only poorly understood. This is especially so in the case of the heart and muscle, where there are no major consumers of NADPH. We propose here that H+-Thase and NADP-ICDH have a combined function in the fine regulation of the activity of the tricarboxylic acid (TCA) cycle, providing enhanced sensitivy to changes in energy demand. This is achieved through cycling of substrates by NAD-linked ICDH, NADP-linked ICDH and H+-Thase. It is proposed that NAD-ICDH operates in the forward direction of the TCA cycle, but NADP-ICDH is driven in reverse by elevated levels of NADPH resulting from the action of the transmembrane proton electrochemical potential gradient (Δp) on H+-Thase. This has the effect of increasing the sensitivity to allosteric modifiers of NAD-ICDH (NADH, ADP, ATP, Ca2+ etc), potentially giving rise to large changes in the net flux from iso-citrate to α-ketoglutarate. Furthermore, changes in the level of Δp resulting from changes in the demand for ATP would, via H+-Thase, shift the redox state of the NADP pool and this, in turn, would lead to a change in the rate of the reaction catalysed by NADP-ICDH and hence to an additional and complementary effect on the net metabolic flux from isocitrate to α-ketoglutarate. Other consequences of this substrate cycle are, (i) the production of heat at the expense of Δp, which may contribute to thermoregulation in the animal, and (ii) an increased rate of dissipation of Δp (leak).","lang":"eng"}],"title":"Proton translocating transhydrogenase and NAD- and NADP-linked isocitrate dehydrogenases operate in a substrate cycle which contributes to fine regulation of the tricarboxylic acid cycle activity in mitochondria","_id":"1949","pmid":1,"acknowledgement":"LAS is grateful to the Wellcome Trust for a fellowship. We should like to thank Prof. R.M. Denton for discussion.","issue":"2-3","publication_identifier":{"issn":["0014-5793"]}},{"oa_version":"Published Version","article_type":"original","external_id":{"pmid":["7982481"]},"type":"journal_article","date_published":"1994-11-28T00:00:00Z","volume":355,"month":"11","oa":1,"quality_controlled":"1","extern":"1","article_processing_charge":"No","publisher":"Elsevier","date_updated":"2022-06-09T12:58:57Z","doi":"10.1016/0014-5793(94)01109-5","publication":"FEBS Letters","date_created":"2018-12-11T11:54:53Z","day":"28","publication_status":"published","publist_id":"5133","author":[{"last_name":"Efanov","first_name":"Alexander","full_name":"Efanov, Alexander"},{"first_name":"Aleksei","full_name":"Koshkin, Aleksei","last_name":"Koshkin"},{"orcid":"0000-0002-0977-7989","last_name":"Sazanov","first_name":"Leonid A","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","full_name":"Sazanov, Leonid A"},{"last_name":"Borodulina","first_name":"O I","full_name":"Borodulina, O I"},{"last_name":"Varfolomeev","full_name":"Varfolomeev, Sergei","first_name":"Sergei"},{"last_name":"Zaǐtsev","full_name":"Zaǐtsev, Sergei","first_name":"Sergei"}],"page":"114 - 116","year":"1994","language":[{"iso":"eng"}],"citation":{"chicago":"Efanov, Alexander, Aleksei Koshkin, Leonid A Sazanov, O I Borodulina, Sergei Varfolomeev, and Sergei Zaǐtsev. “Inhibition of the Respiratory Burst in Mouse Macrophages by Ultra-Low Doses of an Opioid Peptide Is Consistent with a Possible Adaptation Mechanism.” FEBS Letters. Elsevier, 1994. https://doi.org/10.1016/0014-5793(94)01109-5.","mla":"Efanov, Alexander, et al. “Inhibition of the Respiratory Burst in Mouse Macrophages by Ultra-Low Doses of an Opioid Peptide Is Consistent with a Possible Adaptation Mechanism.” FEBS Letters, vol. 355, no. 2, Elsevier, 1994, pp. 114–16, doi:10.1016/0014-5793(94)01109-5.","ama":"Efanov A, Koshkin A, Sazanov LA, Borodulina OI, Varfolomeev S, Zaǐtsev S. Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism. FEBS Letters. 1994;355(2):114-116. doi:10.1016/0014-5793(94)01109-5","short":"A. Efanov, A. Koshkin, L.A. Sazanov, O.I. Borodulina, S. Varfolomeev, S. Zaǐtsev, FEBS Letters 355 (1994) 114–116.","ieee":"A. Efanov, A. Koshkin, L. A. Sazanov, O. I. Borodulina, S. Varfolomeev, and S. Zaǐtsev, “Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism,” FEBS Letters, vol. 355, no. 2. Elsevier, pp. 114–116, 1994.","apa":"Efanov, A., Koshkin, A., Sazanov, L. A., Borodulina, O. I., Varfolomeev, S., & Zaǐtsev, S. (1994). Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism. FEBS Letters. Elsevier. https://doi.org/10.1016/0014-5793(94)01109-5","ista":"Efanov A, Koshkin A, Sazanov LA, Borodulina OI, Varfolomeev S, Zaǐtsev S. 1994. Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism. FEBS Letters. 355(2), 114–116."},"intvolume":" 355","main_file_link":[{"open_access":"1","url":"https://febs.onlinelibrary.wiley.com/doi/abs/10.1016/0014-5793%2894%2901109-5"}],"status":"public","pmid":1,"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"The respiratory burst induced by phorbol myristate acetate in mouse macrophages was inhibited by ultra-low doses (10-15 -10-13 M) of an opioid peptide [d-Ala2] methionine enkephalinamide. The effect disappeared at concentrations above and below this range. The inhibition approached 50% and was statistically significant (P < 0.001). Increasing the time of the opioid incubation with cells brought about a shift in the maximal effect to lower concentrations of the opioid (from 10-13 to 5 · 10-15 M) and led to a decrease in the value of the effect, fully in accord with the previously proposed adaptation mechanism of the action of ultra-low doses.","lang":"eng"}],"title":"Inhibition of the respiratory burst in mouse macrophages by ultra-low doses of an opioid peptide is consistent with a possible adaptation mechanism","_id":"1953","publication_identifier":{"issn":["0014-5793"]},"issue":"2"}]