[{"language":[{"iso":"eng"}],"year":"1997","page":"178 - 180","issue":"2","author":[{"full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","last_name":"Barton","orcid":"0000-0002-8548-5240"}],"publist_id":"1789","publication_status":"published","day":"01","date_created":"2018-12-11T12:08:04Z","publication_identifier":{"issn":["0016-6723"]},"_id":"4290","publication":"Genetical Research","publisher":"Cambridge University Press","date_updated":"2022-08-17T14:10:20Z","title":"Natural hybridization and evolution","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","extern":"1","month":"10","status":"public","volume":70,"date_published":"1997-10-01T00:00:00Z","type":"review","citation":{"ista":"Barton NH. 1997. Natural hybridization and evolution. Genetical Research. 70(2), 178–180.","apa":"Barton, N. H. (1997). Natural hybridization and evolution. <i>Genetical Research</i>. Cambridge University Press.","ieee":"N. H. Barton, “Natural hybridization and evolution,” <i>Genetical Research</i>, vol. 70, no. 2. Cambridge University Press, pp. 178–180, 1997.","short":"N.H. Barton, Genetical Research 70 (1997) 178–180.","ama":"Barton NH. Natural hybridization and evolution. <i>Genetical Research</i>. 1997;70(2):178-180.","mla":"Barton, Nicholas H. “Natural Hybridization and Evolution.” <i>Genetical Research</i>, vol. 70, no. 2, Cambridge University Press, 1997, pp. 178–80.","chicago":"Barton, Nicholas H. “Natural Hybridization and Evolution.” <i>Genetical Research</i>. Cambridge University Press, 1997."},"intvolume":"        70","oa_version":"None"},{"date_created":"2018-12-11T12:08:04Z","publication_identifier":{"issn":["0016-6723"]},"publist_id":"1790","publication_status":"published","day":"01","issue":"2","author":[{"full_name":"Barton, Nicholas H","first_name":"Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","last_name":"Barton","orcid":"0000-0002-8548-5240"}],"page":"180 - 181","year":"1997","language":[{"iso":"eng"}],"oa_version":"None","main_file_link":[{"url":"https://www.cambridge.org/core/journals/genetics-research/article/ecological-detective-confronting-models-with-data-by-ray-hilborn-and-marc-mangel-princeton-university-press-1997-315xvii-pages-price-3000-cloth-1695-paper-isbn-0-691-03496-6-0-691-03497-4-pbk/AA6FCD668DFFAEF537C2674ECCFC8966"}],"intvolume":"        70","citation":{"ama":"Barton NH. The ecological detective: Confronting models with data. <i>Genetical Research</i>. 1997;70(2):180-181.","mla":"Barton, Nicholas H. “The Ecological Detective: Confronting Models with Data.” <i>Genetical Research</i>, vol. 70, no. 2, Cambridge University Press, 1997, pp. 180–81.","chicago":"Barton, Nicholas H. “The Ecological Detective: Confronting Models with Data.” <i>Genetical Research</i>. Cambridge University Press, 1997.","ista":"Barton NH. 1997. The ecological detective: Confronting models with data. Genetical Research. 70(2), 180–181.","apa":"Barton, N. H. (1997). The ecological detective: Confronting models with data. <i>Genetical Research</i>. Cambridge University Press.","short":"N.H. Barton, Genetical Research 70 (1997) 180–181.","ieee":"N. H. Barton, “The ecological detective: Confronting models with data,” <i>Genetical Research</i>, vol. 70, no. 2. Cambridge University Press, pp. 180–181, 1997."},"volume":70,"type":"review","date_published":"1997-10-01T00:00:00Z","status":"public","month":"10","extern":"1","quality_controlled":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","_id":"4291","publication":"Genetical Research","title":"The ecological detective: Confronting models with data","date_updated":"2022-08-18T09:36:25Z","publisher":"Cambridge University Press"},{"extern":"1","quality_controlled":"1","month":"03","_id":"4293","publication":"Metapopulation Biology","title":"The evolution of metapopulations","publisher":"Academic Press","doi":"10.1016/B978-012323445-2/50012-2","date_updated":"2022-08-17T12:47:42Z","abstract":[{"lang":"eng","text":"Natural populations differ from the simplest models in ways which can significantly affect their evolution. Real populations are rarely all of the same size; the rates of migration into and out of populations vary in space and time; some populations go extinct, and new ones are established, while all populations fluctuate in size. Furthermore, the genetic properties of real species are not like those assumed in simple models. Alleles are exposed to a wide variety of selection mutation rarely creates novel genotypes with each mutation event, generations overlap, and environments vary from place to place. Evolution in a metapopulation can be substantially different from the predictions of single-population models and, indeed, very different from the simplest models of subdivided species."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","editor":[{"full_name":"Hanski, Illka","first_name":"Illka","last_name":"Hanski"},{"full_name":"Gilpin, Michael E.","first_name":"Michael E.","last_name":"Gilpin"}],"citation":{"apa":"Barton, N. H., &#38; Whitlock, M. (1997). The evolution of metapopulations. In I. Hanski &#38; M. E. Gilpin (Eds.), <i>Metapopulation Biology</i> (pp. 183–210). Academic Press. <a href=\"https://doi.org/10.1016/B978-012323445-2/50012-2\">https://doi.org/10.1016/B978-012323445-2/50012-2</a>","ista":"Barton NH, Whitlock M. 1997.The evolution of metapopulations. In: Metapopulation Biology. , 183–210.","short":"N.H. Barton, M. Whitlock, in:, I. Hanski, M.E. Gilpin (Eds.), Metapopulation Biology, Academic Press, 1997, pp. 183–210.","ieee":"N. H. Barton and M. Whitlock, “The evolution of metapopulations,” in <i>Metapopulation Biology</i>, I. Hanski and M. E. Gilpin, Eds. Academic Press, 1997, pp. 183–210.","mla":"Barton, Nicholas H., and Michael Whitlock. “The Evolution of Metapopulations.” <i>Metapopulation Biology</i>, edited by Illka Hanski and Michael E. Gilpin, Academic Press, 1997, pp. 183–210, doi:<a href=\"https://doi.org/10.1016/B978-012323445-2/50012-2\">10.1016/B978-012323445-2/50012-2</a>.","ama":"Barton NH, Whitlock M. The evolution of metapopulations. In: Hanski I, Gilpin ME, eds. <i>Metapopulation Biology</i>. Academic Press; 1997:183-210. doi:<a href=\"https://doi.org/10.1016/B978-012323445-2/50012-2\">10.1016/B978-012323445-2/50012-2</a>","chicago":"Barton, Nicholas H, and Michael Whitlock. “The Evolution of Metapopulations.” In <i>Metapopulation Biology</i>, edited by Illka Hanski and Michael E. Gilpin, 183–210. Academic Press, 1997. <a href=\"https://doi.org/10.1016/B978-012323445-2/50012-2\">https://doi.org/10.1016/B978-012323445-2/50012-2</a>."},"oa_version":"None","status":"public","type":"book_chapter","date_published":"1997-03-12T00:00:00Z","language":[{"iso":"eng"}],"year":"1997","publist_id":"1782","publication_status":"published","day":"12","date_created":"2018-12-11T12:08:05Z","publication_identifier":{"isbn":["9780123234452"]},"page":"183 - 210","author":[{"id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","full_name":"Barton, Nicholas H","last_name":"Barton","orcid":"0000-0002-8548-5240"},{"last_name":"Whitlock","full_name":"Whitlock, Michael","first_name":"Michael"}]},{"type":"conference","date_published":"1997-01-01T00:00:00Z","volume":1201,"oa_version":"None","article_processing_charge":"No","doi":"10.1007/BFb0014712","publisher":"Springer","date_updated":"2022-08-17T12:29:48Z","publication":"Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems","month":"01","quality_controlled":"1","extern":"1","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Kupferman","first_name":"Orna","full_name":"Kupferman, Orna"}],"conference":{"location":"Grenoble, France","end_date":"1997-03-28","start_date":"1997-03-26","name":"HART: Hybrid and Real-Time Systems"},"alternative_title":["LNCS"],"page":"48 - 62","date_created":"2018-12-11T12:08:51Z","day":"01","publist_id":"291","publication_status":"published","year":"1997","language":[{"iso":"eng"}],"status":"public","citation":{"chicago":"Henzinger, Thomas A, and Orna Kupferman. “From Quantity to Quality.” In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, 1201:48–62. Springer, 1997. <a href=\"https://doi.org/10.1007/BFb0014712\">https://doi.org/10.1007/BFb0014712</a>.","mla":"Henzinger, Thomas A., and Orna Kupferman. “From Quantity to Quality.” <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, vol. 1201, Springer, 1997, pp. 48–62, doi:<a href=\"https://doi.org/10.1007/BFb0014712\">10.1007/BFb0014712</a>.","ama":"Henzinger TA, Kupferman O. From quantity to quality. In: <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201. Springer; 1997:48-62. doi:<a href=\"https://doi.org/10.1007/BFb0014712\">10.1007/BFb0014712</a>","ieee":"T. A. Henzinger and O. Kupferman, “From quantity to quality,” in <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, Grenoble, France, 1997, vol. 1201, pp. 48–62.","short":"T.A. Henzinger, O. Kupferman, in:, Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 48–62.","apa":"Henzinger, T. A., &#38; Kupferman, O. (1997). From quantity to quality. In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i> (Vol. 1201, pp. 48–62). Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/BFb0014712\">https://doi.org/10.1007/BFb0014712</a>","ista":"Henzinger TA, Kupferman O. 1997. From quantity to quality. Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and Real-Time Systems, LNCS, vol. 1201, 48–62."},"intvolume":"      1201","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"In temporal-logic model checking, we verify the correctness of a program with respect to a desired behavior by checking whether a structure that models the program satisfies a temporal-logic formula that specifies the behavior. The model-checking problem for the branching-time temporal logic CTL can be solved in linear running time, and model-checking tools for CTL are used successfully in industrial applications. The development of programs that must meet rigid real-time constraints has brought with it a need for real-time temporal logics that enable quantitative reference to time. Early research on real-time temporal logics uses the discrete domain of the integers to model time. Present research on real-time temporal logics focuses on continuous time and uses the dense domain of the reals to model time. There, model checking becomes significantly more complicated. For example, the model-checking problem for TCTL, a continuous-time extension of the logic CTL, is PSPACE-complete.\r\nIn this paper we suggest a reduction from TCTL model checking to CTL model checking. The contribution of such a reduction is twofold. Theoretically, while it has long been known that model-checking methods for untimed temporal logics can be extended quite easily to handle discrete time, it was not clear whether and how untimed methods can handle the reset quantifier of TCTL, which resets a realvalued clock. Practically, our reduction enables anyone who has a tool for CTL model checking to use it for TCTL model checking. The TCTL model-checking algorithm that follows from our reduction is in PSPACE, matching the known bound for this problem. In addition, it enjoys the wide distribution of CTL model-checking tools and the extensive and fruitful research efforts and heuristics that have been put into these tools.","lang":"eng"}],"title":"From quantity to quality","_id":"4438","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.","publication_identifier":{"isbn":["9783540626008"]},"scopus_import":"1"},{"publication_identifier":{"isbn":["9783540631651"]},"scopus_import":"1","status":"public","intvolume":"      1256","citation":{"ieee":"T. A. Henzinger and P. Kopke, “Discrete-time control for rectangular hybrid automata,” in <i>Proceedings of the 24th International Colloquium on Automata, Languages and Programming</i>, Bologna, Italy, 1997, vol. 1256, pp. 582–593.","short":"T.A. Henzinger, P. Kopke, in:, Proceedings of the 24th International Colloquium on Automata, Languages and Programming, Springer, 1997, pp. 582–593.","apa":"Henzinger, T. A., &#38; Kopke, P. (1997). Discrete-time control for rectangular hybrid automata. In <i>Proceedings of the 24th International Colloquium on Automata, Languages and Programming</i> (Vol. 1256, pp. 582–593). Bologna, Italy: Springer. <a href=\"https://doi.org/10.1007/3-540-63165-8_213\">https://doi.org/10.1007/3-540-63165-8_213</a>","ista":"Henzinger TA, Kopke P. 1997. Discrete-time control for rectangular hybrid automata. Proceedings of the 24th International Colloquium on Automata, Languages and Programming. ICALP: Automata, Languages and Programming, LNCS, vol. 1256, 582–593.","chicago":"Henzinger, Thomas A, and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” In <i>Proceedings of the 24th International Colloquium on Automata, Languages and Programming</i>, 1256:582–93. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63165-8_213\">https://doi.org/10.1007/3-540-63165-8_213</a>.","mla":"Henzinger, Thomas A., and Peter Kopke. “Discrete-Time Control for Rectangular Hybrid Automata.” <i>Proceedings of the 24th International Colloquium on Automata, Languages and Programming</i>, vol. 1256, Springer, 1997, pp. 582–93, doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_213\">10.1007/3-540-63165-8_213</a>.","ama":"Henzinger TA, Kopke P. Discrete-time control for rectangular hybrid automata. In: <i>Proceedings of the 24th International Colloquium on Automata, Languages and Programming</i>. Vol 1256. Springer; 1997:582-593. doi:<a href=\"https://doi.org/10.1007/3-540-63165-8_213\">10.1007/3-540-63165-8_213</a>"},"_id":"4441","title":"Discrete-time control for rectangular hybrid automata","abstract":[{"lang":"eng","text":"Rectangular hybrid automata model digital control programs of analog plant environments. We study rectangular hybrid automata where the plant state evolves continuously in real-numbered time, and the controller samples the plant state and changes the control state discretely, only at the integer points in time. We prove that rectangular hybrid automata have finite bisimilarity quotients when all control transitions happen at integer times, even if the constraints on the derivatives of the variables vary between control states. This is sharply in contrast with the conventional model where control transitions may happen at any real time, and already the reachability problem is undecidable. Based on the finite bisimilarity quotients, we give an exponential algorithm for the symbolic sampling-controller synthesis of rectangular automata. We show our algorithm to be optimal by proving the problem to be EXPTIME-hard. We also show that rectangular automata form a maximal class of systems for which the sampling-controller synthesis problem can be solved algorithmically."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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 contract DAAH-04-96-1-0341, by the ARO contract DAAL03-91-C-0027 through the MSI at Cornell University, by the ARPA grant NAG2-892, and by the SRC contract 95-DC-324.036.","page":"582 - 593","alternative_title":["LNCS"],"conference":{"end_date":"1997-07-11","location":"Bologna, Italy","name":"ICALP: Automata, Languages and Programming","start_date":"1997-07-07"},"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"}],"publist_id":"289","publication_status":"published","day":"01","date_created":"2018-12-11T12:08:52Z","year":"1997","language":[{"iso":"eng"}],"volume":1256,"date_published":"1997-01-01T00:00:00Z","type":"conference","oa_version":"None","publication":"Proceedings of the 24th International Colloquium on Automata, Languages and Programming","date_updated":"2022-08-17T12:04:15Z","doi":"10.1007/3-540-63165-8_213","publisher":"Springer","article_processing_charge":"No","extern":"1","quality_controlled":"1","month":"01"},{"intvolume":"         1","citation":{"chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker for Hybrid Systems.” <i>Software Tools For Technology Transfer</i>. Springer, 1997. <a href=\"https://doi.org/10.1007/s100090050008\">https://doi.org/10.1007/s100090050008</a>.","mla":"Henzinger, Thomas A., et al. “HyTech: A Model Checker for Hybrid Systems.” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2, Springer, 1997, pp. 110–22, doi:<a href=\"https://doi.org/10.1007/s100090050008\">10.1007/s100090050008</a>.","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems. <i>Software Tools For Technology Transfer</i>. 1997;1(1-2):110-122. doi:<a href=\"https://doi.org/10.1007/s100090050008\">10.1007/s100090050008</a>","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid systems,” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2. Springer, pp. 110–122, 1997.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, Software Tools For Technology Transfer 1 (1997) 110–122.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1997). HyTech: A model checker for hybrid systems. <i>Software Tools For Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s100090050008\">https://doi.org/10.1007/s100090050008</a>","ista":"Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid systems. Software Tools For Technology Transfer. 1(1–2), 110–122."},"status":"public","acknowledgement":"This research was supported in part by the ONR YIP award N00014-95-1-0520, the NSF CAREER award CCR-501708, NSF grant CCR-9504469, AFOSR contract F49620-93-1-0056, ARO MURI grant DAAH-04-96-1-0341, ARPA grant  AG2-892, and SRC contract 95-DC-324.036.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. HyTech is a symbolic model checker for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically by computing with polyhedral state sets. A key feature of HyTech is its ability to perform parametric analysis, i.e., to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal-logic requirement."}],"title":"HyTech: A model checker for hybrid systems","_id":"4493","publication_identifier":{"issn":["1433-2779"]},"issue":"1-2","scopus_import":"1","article_type":"original","oa_version":"None","type":"journal_article","date_published":"1997-01-01T00:00:00Z","volume":1,"month":"01","quality_controlled":"1","extern":"1","article_processing_charge":"No","date_updated":"2022-08-17T11:14:15Z","publisher":"Springer","doi":"10.1007/s100090050008","publication":"Software Tools For Technology Transfer","date_created":"2018-12-11T12:09:08Z","day":"01","publication_status":"published","publist_id":"236","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"page":"110 - 122","year":"1997","language":[{"iso":"eng"}]},{"language":[{"iso":"eng"}],"year":"1997","author":[{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Pei","full_name":"Ho, Pei","last_name":"Ho"},{"full_name":"Wong Toi, Howard","first_name":"Howard","last_name":"Wong Toi"}],"page":"460 - 463","alternative_title":["LNCS"],"conference":{"name":"CAV: Computer Aided Verification","start_date":"1997-06-22","end_date":"1997-06-25","location":"Haifa, Israel"},"date_created":"2018-12-11T12:09:08Z","publication_status":"published","publist_id":"235","day":"01","article_processing_charge":"No","date_updated":"2022-08-17T11:06:13Z","doi":"10.1007/3-540-63166-6_48","publisher":"Springer","month":"01","extern":"1","quality_controlled":"1","volume":1254,"date_published":"1997-01-01T00:00:00Z","type":"conference","oa_version":"None","scopus_import":"1","publication_identifier":{"isbn":["9783540631668"]},"abstract":[{"text":"A hybrid system consists of a collection of digital programs that interact with each other and with an analog environment. Examples of hybrid systems include medical equipment, manufacturing controllers, automotive controllers, and robots. The formal analysis of the mixed digital-analog nature of these systems requires a model that incorporates the discrete behavior of computer programs with the continuous behavior of environment variables, such as temperature and pressure. Hybrid automata capture both types of behavior by combining finite automata with differential inclusions (i.e. differential inequalities). HyTech is a symbolic model checker for linear hybrid automata, an expressive, yet automatically analyzable, subclass of hybrid automata. A key feature of HyTech is its ability to perform parametric analysis, i.e. to determine the values of design parameters for which a linear hybrid automaton satisfies a temporal requirement.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4494","title":"HyTech: A model checker for hybrid systems","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.","status":"public","citation":{"chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: A Model Checker for Hybrid Systems,” 1254:460–63. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63166-6_48\">https://doi.org/10.1007/3-540-63166-6_48</a>.","mla":"Henzinger, Thomas A., et al. <i>HyTech: A Model Checker for Hybrid Systems</i>. Vol. 1254, Springer, 1997, pp. 460–63, doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_48\">10.1007/3-540-63166-6_48</a>.","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: A model checker for hybrid systems. In: Vol 1254. Springer; 1997:460-463. doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_48\">10.1007/3-540-63166-6_48</a>","ieee":"T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: A model checker for hybrid systems,” presented at the CAV: Computer Aided Verification, Haifa, Israel, 1997, vol. 1254, pp. 460–463.","short":"T.A. Henzinger, P. Ho, H. Wong Toi, in:, Springer, 1997, pp. 460–463.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1997). HyTech: A model checker for hybrid systems (Vol. 1254, pp. 460–463). Presented at the CAV: Computer Aided Verification, Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/3-540-63166-6_48\">https://doi.org/10.1007/3-540-63166-6_48</a>","ista":"Henzinger TA, Ho P, Wong Toi H. 1997. HyTech: A model checker for hybrid systems. CAV: Computer Aided Verification, LNCS, vol. 1254, 460–463."},"intvolume":"      1254"},{"language":[{"iso":"eng"}],"year":"1997","author":[{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"},{"first_name":"Sriram","full_name":"Rajamani, Sriram","last_name":"Rajamani"}],"conference":{"location":"Warsaw, Poland","end_date":"1997-07-04","start_date":"1997-07-01","name":"CONCUR: Concurrency Theory"},"alternative_title":["LNCS"],"page":"273 - 287","date_created":"2018-12-11T12:09:09Z","day":"01","publist_id":"234","publication_status":"published","article_processing_charge":"No","doi":"10.1007/3-540-63141-0_19","publisher":"Springer","date_updated":"2022-08-17T09:09:13Z","publication":"Proceedings of the 8th International Conference on Concurrency Theory","month":"01","quality_controlled":"1","extern":"1","type":"conference","date_published":"1997-01-01T00:00:00Z","volume":1243,"oa_version":"None","scopus_import":"1","publication_identifier":{"isbn":["9783540631415"]},"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"text":"The simulation preorder for labeled transition systems is defined locally as a game that relates states with their immediate successor states. Liveness assumptions about transition systems are typically modeled using fairness constraints. Existing notions of simulation for fair transition systems, however, are not local, and as a result, many appealing properties of the simulation preorder are lost. We extend the local definition of simulation to account for fairness: system S fairly simulates system I iff in the simulation game, there is a strategy that matches with each fair computation of I a fair computation of S. Our definition enjoys a fully abstract semantics and has a logical characterization: S fairly simulates I iff every fair computation tree embedded in the unrolling of I can be embedded also in the unrolling of S or, equivalently, iff every Fair-AFMC formula satisfied by I is satisfied also by S (AFMC is the universal fragment of the alternation-free -calculus). The locality of the definition leads us to a polynomial-time algorithm for checking fair simulation for finite-state systems with weak and strong fairness constraints. Finally, fair simulation implies fair trace-containment, and is therefore useful as an efficientlycomputable local criterion for proving linear-time abstraction hierarchies.","lang":"eng"}],"title":"Fair simulation","_id":"4496","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.","status":"public","citation":{"mla":"Henzinger, Thomas A., et al. “Fair Simulation.” <i>Proceedings of the 8th International Conference on Concurrency Theory</i>, vol. 1243, Springer, 1997, pp. 273–87, doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_19\">10.1007/3-540-63141-0_19</a>.","ama":"Henzinger TA, Kupferman O, Rajamani S. Fair simulation. In: <i>Proceedings of the 8th International Conference on Concurrency Theory</i>. Vol 1243. Springer; 1997:273-287. doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_19\">10.1007/3-540-63141-0_19</a>","chicago":"Henzinger, Thomas A, Orna Kupferman, and Sriram Rajamani. “Fair Simulation.” In <i>Proceedings of the 8th International Conference on Concurrency Theory</i>, 1243:273–87. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63141-0_19\">https://doi.org/10.1007/3-540-63141-0_19</a>.","apa":"Henzinger, T. A., Kupferman, O., &#38; Rajamani, S. (1997). Fair simulation. In <i>Proceedings of the 8th International Conference on Concurrency Theory</i> (Vol. 1243, pp. 273–287). Warsaw, Poland: Springer. <a href=\"https://doi.org/10.1007/3-540-63141-0_19\">https://doi.org/10.1007/3-540-63141-0_19</a>","ista":"Henzinger TA, Kupferman O, Rajamani S. 1997. Fair simulation. Proceedings of the 8th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1243, 273–287.","short":"T.A. Henzinger, O. Kupferman, S. Rajamani, in:, Proceedings of the 8th International Conference on Concurrency Theory, Springer, 1997, pp. 273–287.","ieee":"T. A. Henzinger, O. Kupferman, and S. Rajamani, “Fair simulation,” in <i>Proceedings of the 8th International Conference on Concurrency Theory</i>, Warsaw, Poland, 1997, vol. 1243, pp. 273–287."},"intvolume":"      1243"},{"year":"1997","language":[{"iso":"eng"}],"publication_status":"published","publist_id":"207","day":"01","date_created":"2018-12-11T12:09:17Z","alternative_title":["LNCS"],"page":"331 - 345","conference":{"location":"Grenoble, France","end_date":"1997-03-28","start_date":"1997-03-26","name":"HART: Hybrid and Real-Time Systems"},"author":[{"last_name":"Gupta","first_name":"Vineet","full_name":"Gupta, Vineet"},{"orcid":"0000−0002−2985−7724","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Jagadeesan","first_name":"Radha","full_name":"Jagadeesan, Radha"}],"extern":"1","quality_controlled":"1","month":"01","publication":"Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems","date_updated":"2022-08-17T09:04:39Z","publisher":"Springer","doi":"10.1007/BFb0014736","article_processing_charge":"No","oa_version":"None","volume":1201,"date_published":"1997-01-01T00:00:00Z","type":"conference","scopus_import":"1","publication_identifier":{"isbn":["9783540626008"]},"acknowledgement":"The first and third author were supported in part by grants from ARPA and ONR. The second author 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. The third author was also supported by the NSF.","_id":"4520","title":"Robust timed automata","abstract":[{"text":"We define robust timed automata, which are timed automata that accept all trajectories robustly: if a robust timed automaton accepts a trajectory, then it must accept neighboring trajectories also; and if a robust timed automaton rejects a trajectory, then it must reject neighboring trajectories also. We show that the emptiness problem for robust timed automata is still decidable, by modifying the region construction for timed automata. We then show that, like timed automata, robust timed automata cannot be determinized. This result is somewhat unexpected, given that in temporal logic, the removal of realtime equality constraints is known to lead to a decidable theory that is closed under all boolean operations.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"ista":"Gupta V, Henzinger TA, Jagadeesan R. 1997. Robust timed automata. Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems. HART: Hybrid and Real-Time Systems, LNCS, vol. 1201, 331–345.","apa":"Gupta, V., Henzinger, T. A., &#38; Jagadeesan, R. (1997). Robust timed automata. In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i> (Vol. 1201, pp. 331–345). Grenoble, France: Springer. <a href=\"https://doi.org/10.1007/BFb0014736\">https://doi.org/10.1007/BFb0014736</a>","ieee":"V. Gupta, T. A. Henzinger, and R. Jagadeesan, “Robust timed automata,” in <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, Grenoble, France, 1997, vol. 1201, pp. 331–345.","short":"V. Gupta, T.A. Henzinger, R. Jagadeesan, in:, Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems, Springer, 1997, pp. 331–345.","ama":"Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In: <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>. Vol 1201. Springer; 1997:331-345. doi:<a href=\"https://doi.org/10.1007/BFb0014736\">10.1007/BFb0014736</a>","mla":"Gupta, Vineet, et al. “Robust Timed Automata.” <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, vol. 1201, Springer, 1997, pp. 331–45, doi:<a href=\"https://doi.org/10.1007/BFb0014736\">10.1007/BFb0014736</a>.","chicago":"Gupta, Vineet, Thomas A Henzinger, and Radha Jagadeesan. “Robust Timed Automata.” In <i>Proceedings of the 5th International Workshop on Hybrid and Real-Time Systems</i>, 1201:331–45. Springer, 1997. <a href=\"https://doi.org/10.1007/BFb0014736\">https://doi.org/10.1007/BFb0014736</a>."},"intvolume":"      1201","status":"public"},{"scopus_import":"1","publication_identifier":{"isbn":["9783540691884"]},"title":"Modularity for timed and hybrid systems","_id":"4583","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"In a trace-based world, the modular specification, verification, and control of live systems require each module to be receptive; that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves. We study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We define the receptiveness of such a module as the existence of a winning strategy in a game of the module against its environment. By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of prepositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. Finally, we present an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules."}],"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.","status":"public","intvolume":"      1243","citation":{"short":"R. Alur, T.A. Henzinger, in:, 8th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88.","ieee":"R. Alur and T. A. Henzinger, “Modularity for timed and hybrid systems,” in <i>8th International Conference on Concurrency Theory</i>, Warsaw, Poland, 1997, vol. 1243, pp. 74–88.","ista":"Alur R, Henzinger TA. 1997. Modularity for timed and hybrid systems. 8th International Conference on Concurrency Theory. CONCUR: Concurrency Theory, LNCS, vol. 1243, 74–88.","apa":"Alur, R., &#38; Henzinger, T. A. (1997). Modularity for timed and hybrid systems. In <i>8th International Conference on Concurrency Theory</i> (Vol. 1243, pp. 74–88). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.1007/3-540-63141-0_6\">https://doi.org/10.1007/3-540-63141-0_6</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Modularity for Timed and Hybrid Systems.” In <i>8th International Conference on Concurrency Theory</i>, 1243:74–88. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997. <a href=\"https://doi.org/10.1007/3-540-63141-0_6\">https://doi.org/10.1007/3-540-63141-0_6</a>.","ama":"Alur R, Henzinger TA. Modularity for timed and hybrid systems. In: <i>8th International Conference on Concurrency Theory</i>. Vol 1243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1997:74-88. doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_6\">10.1007/3-540-63141-0_6</a>","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Modularity for Timed and Hybrid Systems.” <i>8th International Conference on Concurrency Theory</i>, vol. 1243, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1997, pp. 74–88, doi:<a href=\"https://doi.org/10.1007/3-540-63141-0_6\">10.1007/3-540-63141-0_6</a>."},"language":[{"iso":"eng"}],"year":"1997","conference":{"location":"Warsaw, Poland","end_date":"1997-07-04","start_date":"1997-07-01","name":"CONCUR: Concurrency Theory"},"alternative_title":["LNCS"],"page":"74 - 88","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"day":"01","publist_id":"124","publication_status":"published","date_created":"2018-12-11T12:09:36Z","date_updated":"2022-08-17T08:47:55Z","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","doi":"10.1007/3-540-63141-0_6","publication":"8th International Conference on Concurrency Theory","article_processing_charge":"No","quality_controlled":"1","extern":"1","month":"01","date_published":"1997-01-01T00:00:00Z","type":"conference","volume":1243,"oa_version":"None"},{"year":"1997","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:36Z","publication_status":"published","publist_id":"123","day":"01","author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"page":"86 - 109","month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Software Tools For Technology Transfer","publisher":"Springer","date_updated":"2022-08-17T08:27:20Z","doi":"10.1007/s100090050007","oa_version":"None","article_type":"original","volume":1,"date_published":"1997-01-01T00:00:00Z","type":"journal_article","scopus_import":"1","publication_identifier":{"issn":["1433-2779"]},"issue":"1-2","acknowledgement":"The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.","abstract":[{"text":"This paper introduces, gently but rigorously, the clock approach to real-time programming. We present with mathematical precision, assuming no prerequisites other than familiarity with logical and programming notations, the concepts that are necessary for understanding, writing, and executing clock programs. In keeping with an expository style, all references are clustered in bibliographic remarks at the end of each section. The first appendix presents proof rules for verifying temporal properties of clock programs. The second appendix points to selected literature on formal methods and tools for programming with clocks. In particular, the timed automaton, which is a finite-state machine equipped with clocks, has become a standard paradigm for real-time model checking; it underlies the tools HyTech, Kronos, and Uppaal, which are discussed elsewhere in this volume.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4584","title":"Real-time system = discrete system + clock variables","intvolume":"         1","citation":{"mla":"Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2, Springer, 1997, pp. 86–109, doi:<a href=\"https://doi.org/10.1007/s100090050007\">10.1007/s100090050007</a>.","ama":"Alur R, Henzinger TA. Real-time system = discrete system + clock variables. <i>Software Tools For Technology Transfer</i>. 1997;1(1-2):86-109. doi:<a href=\"https://doi.org/10.1007/s100090050007\">10.1007/s100090050007</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System + Clock Variables.” <i>Software Tools For Technology Transfer</i>. Springer, 1997. <a href=\"https://doi.org/10.1007/s100090050007\">https://doi.org/10.1007/s100090050007</a>.","apa":"Alur, R., &#38; Henzinger, T. A. (1997). Real-time system = discrete system + clock variables. <i>Software Tools For Technology Transfer</i>. Springer. <a href=\"https://doi.org/10.1007/s100090050007\">https://doi.org/10.1007/s100090050007</a>","ista":"Alur R, Henzinger TA. 1997. Real-time system = discrete system + clock variables. Software Tools For Technology Transfer. 1(1–2), 86–109.","ieee":"R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,” <i>Software Tools For Technology Transfer</i>, vol. 1, no. 1–2. Springer, pp. 86–109, 1997.","short":"R. Alur, T.A. Henzinger, Software Tools For Technology Transfer 1 (1997) 86–109."},"status":"public"},{"abstract":[{"lang":"eng","text":"A hybrid system is a dynamical system whose behavior exhibits both discrete and continuous change. A hybrid automaton is a mathematical model for hybrid systems, which combines, in a single formalism, automaton transitions for capturing discrete change with differential equations for capturing continuous change. In this survey, we demonstrate symbolic algorithms for the verification of and controller synthesis for linear hybrid automata, a subclass of hybrid automata that can be analyzed automatically"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","_id":"4605","publication":"Proceedings of the 36th IEEE Conference on Decision and Control","title":"Symbolic analysis of hybrid systems","publisher":"IEEE","date_updated":"2022-08-17T08:08:36Z","doi":"10.1109/CDC.1997.650717  ","month":"12","extern":"1","quality_controlled":"1","type":"conference","date_published":"1997-12-01T00:00:00Z","status":"public","oa_version":"None","citation":{"ista":"Alur R, Henzinger TA, Wong Toi H. 1997. Symbolic analysis of hybrid systems. Proceedings of the 36th IEEE Conference on Decision and Control. CDC: Decision and Control, 702–707.","apa":"Alur, R., Henzinger, T. A., &#38; Wong Toi, H. (1997). Symbolic analysis of hybrid systems. In <i>Proceedings of the 36th IEEE Conference on Decision and Control</i> (pp. 702–707). San Diego, CA, USA: IEEE. <a href=\"https://doi.org/10.1109/CDC.1997.650717  \">https://doi.org/10.1109/CDC.1997.650717  </a>","short":"R. Alur, T.A. Henzinger, H. Wong Toi, in:, Proceedings of the 36th IEEE Conference on Decision and Control, IEEE, 1997, pp. 702–707.","ieee":"R. Alur, T. A. Henzinger, and H. Wong Toi, “Symbolic analysis of hybrid systems,” in <i>Proceedings of the 36th IEEE Conference on Decision and Control</i>, San Diego, CA, USA, 1997, pp. 702–707.","ama":"Alur R, Henzinger TA, Wong Toi H. Symbolic analysis of hybrid systems. In: <i>Proceedings of the 36th IEEE Conference on Decision and Control</i>. IEEE; 1997:702-707. doi:<a href=\"https://doi.org/10.1109/CDC.1997.650717  \">10.1109/CDC.1997.650717  </a>","mla":"Alur, Rajeev, et al. “Symbolic Analysis of Hybrid Systems.” <i>Proceedings of the 36th IEEE Conference on Decision and Control</i>, IEEE, 1997, pp. 702–07, doi:<a href=\"https://doi.org/10.1109/CDC.1997.650717  \">10.1109/CDC.1997.650717  </a>.","chicago":"Alur, Rajeev, Thomas A Henzinger, and Howard Wong Toi. “Symbolic Analysis of Hybrid Systems.” In <i>Proceedings of the 36th IEEE Conference on Decision and Control</i>, 702–7. IEEE, 1997. <a href=\"https://doi.org/10.1109/CDC.1997.650717  \">https://doi.org/10.1109/CDC.1997.650717  </a>."},"scopus_import":"1","language":[{"iso":"eng"}],"year":"1997","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Wong Toi","first_name":"Howard","full_name":"Wong Toi, Howard"}],"page":"702 - 707","conference":{"start_date":"1997-12-12","name":"CDC: Decision and Control","location":"San Diego, CA, USA","end_date":"1997-12-12"},"publication_identifier":{"isbn":["0780341872"]},"date_created":"2018-12-11T12:09:43Z","publication_status":"published","publist_id":"101","day":"01"},{"scopus_import":"1","issue":"2","publication_identifier":{"issn":["0925-9856"]},"abstract":[{"lang":"eng","text":"We present a verification algorithm for duration properties of real-time systems. While simple real-time properties constrain the total elapsed time between events, duration properties constrain the accumulated satisfaction time of state predicates. We formalize the concept of durations by introducing duration measures for timed automata. A duration measure assigns to each finite run of a timed automaton a real number —the duration of the run— which may be the accumulated satisfaction time of a state predicate along the run. Given a timed automaton with a duration measure, an initial and a final state, and an arithmetic constraint, the duration-bounded reachability problem asks if there is a run of the automaton from the initial state to the final state such that the duration of the run satisfies the constraint. Our main result is an (optimal) PSPACE decision procedure for the duration-bounded reachability problem."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4607","title":"Computing accumulated delays in real-time systems","acknowledgement":"A preliminary version of this paper appeared in the Proceedings of the Fifth International Conference on Computer-Aided Verification (CAV 93), Springer-Verlag LNCS 818, pp. 181–193, 1993. We thank Sergio Yovine for a careful reading of the manuscript. This reaserch was partially supported by the BRA ESPRIT project REACT, by the ONR YIP\r\naward 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.","status":"public","citation":{"apa":"Alur, R., Courcoubetis, C., &#38; Henzinger, T. A. (1997). Computing accumulated delays in real-time systems. <i>Formal Methods in System Design</i>. Springer. <a href=\"https://doi.org/10.1023/A:1008626013578\">https://doi.org/10.1023/A:1008626013578</a>","ista":"Alur R, Courcoubetis C, Henzinger TA. 1997. Computing accumulated delays in real-time systems. Formal Methods in System Design. 11(2), 137–156.","ieee":"R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays in real-time systems,” <i>Formal Methods in System Design</i>, vol. 11, no. 2. Springer, pp. 137–156, 1997.","short":"R. Alur, C. Courcoubetis, T.A. Henzinger, Formal Methods in System Design 11 (1997) 137–156.","mla":"Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” <i>Formal Methods in System Design</i>, vol. 11, no. 2, Springer, 1997, pp. 137–56, doi:<a href=\"https://doi.org/10.1023/A:1008626013578\">10.1023/A:1008626013578</a>.","ama":"Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time systems. <i>Formal Methods in System Design</i>. 1997;11(2):137-156. doi:<a href=\"https://doi.org/10.1023/A:1008626013578\">10.1023/A:1008626013578</a>","chicago":"Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated Delays in Real-Time Systems.” <i>Formal Methods in System Design</i>. Springer, 1997. <a href=\"https://doi.org/10.1023/A:1008626013578\">https://doi.org/10.1023/A:1008626013578</a>."},"intvolume":"        11","year":"1997","language":[{"iso":"eng"}],"author":[{"first_name":"Rajeev","full_name":"Alur, Rajeev","last_name":"Alur"},{"full_name":"Courcoubetis, Costas","first_name":"Costas","last_name":"Courcoubetis"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"page":"137 - 156","date_created":"2018-12-11T12:09:43Z","publication_status":"published","publist_id":"98","day":"01","article_processing_charge":"No","publication":"Formal Methods in System Design","doi":"10.1023/A:1008626013578","date_updated":"2022-08-16T13:43:41Z","publisher":"Springer","month":"01","extern":"1","quality_controlled":"1","volume":11,"type":"journal_article","date_published":"1997-01-01T00:00:00Z","article_type":"original","oa_version":"None"},{"status":"public","intvolume":"      1254","citation":{"chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” In <i>9th International Conference on Computer Aided Verification</i>, 1254:340–51. Springer, 1997. <a href=\"https://doi.org/10.1007/3-540-63166-6_34\">https://doi.org/10.1007/3-540-63166-6_34</a>.","ama":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction in symbolic state-space exploration. In: <i>9th International Conference on Computer Aided Verification</i>. Vol 1254. Springer; 1997:340-351. doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_34\">10.1007/3-540-63166-6_34</a>","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” <i>9th International Conference on Computer Aided Verification</i>, vol. 1254, Springer, 1997, pp. 340–51, doi:<a href=\"https://doi.org/10.1007/3-540-63166-6_34\">10.1007/3-540-63166-6_34</a>.","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, in:, 9th International Conference on Computer Aided Verification, Springer, 1997, pp. 340–351.","ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” in <i>9th International Conference on Computer Aided Verification</i>, Haifa, Israel, 1997, vol. 1254, pp. 340–351.","ista":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 1997. Partial-order reduction in symbolic state-space exploration. 9th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1254, 340–351.","apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1997). Partial-order reduction in symbolic state-space exploration. In <i>9th International Conference on Computer Aided Verification</i> (Vol. 1254, pp. 340–351). Haifa, Israel: Springer. <a href=\"https://doi.org/10.1007/3-540-63166-6_34\">https://doi.org/10.1007/3-540-63166-6_34</a>"},"title":"Partial-order reduction in symbolic state-space exploration","_id":"4608","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"State space explosion is a fundamental obstacle in formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reductions and symbolic state space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy."}],"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 Semiconductor Research Corporation contracts DC-324.036 and DC-324.005.","publication_identifier":{"isbn":["9783540631668"]},"scopus_import":"1","type":"conference","date_published":"1997-01-01T00:00:00Z","volume":1254,"oa_version":"None","publisher":"Springer","date_updated":"2022-08-16T14:09:54Z","doi":"10.1007/3-540-63166-6_34","publication":"9th International Conference on Computer Aided Verification","article_processing_charge":"No","quality_controlled":"1","extern":"1","month":"01","conference":{"name":"CAV: Computer Aided Verification","start_date":"1997-06-22","end_date":"1997-06-25","location":"Haifa, Israel"},"alternative_title":["LNCS"],"page":"340 - 351","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"last_name":"Brayton","first_name":"Robert","full_name":"Brayton, Robert"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"first_name":"Shaz","full_name":"Qadeer, Shaz","last_name":"Qadeer"},{"last_name":"Rajamani","first_name":"Sriram","full_name":"Rajamani, Sriram"}],"day":"01","publist_id":"99","publication_status":"published","date_created":"2018-12-11T12:09:44Z","year":"1997","language":[{"iso":"eng"}]},{"month":"01","quality_controlled":"1","acknowledgement":"We thank Luca de Alfaro, Kousha Etessami, Salvatore La Torre, P. Madhusudan, Amir Pnueli, Moshe Vardi, Thomas Wilke, and Mihalis Yannakakis for helpful discussions. We also thank Freddy Mang for comments on a draft of this manuscript.","extern":"1","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No","abstract":[{"lang":"eng","text":"Temporal logic comes in two varieties: linear-time temporal logic assumes implicit universal quantification over all paths that are generated by system moves; branching-time temporal logic allows explicit existential and universal quantification over all paths. We introduce a third, more general variety of temporal logic: alternating-time temporal logic offers selective quantification over those paths that are possible outcomes of games, such as the game in which the system and the environment alternate moves. While linear-time and branching-time logics are natural specification languages for closed systems, alternating-time logics are natural specification languages for open systems. For example, by preceding the temporal operator “eventually” with a selective path quantifier, we can specify that in the game between the system and the environment, the system has a strategy to reach a certain state. Also the problems of receptiveness, realizability, and controllability can be formulated as model-checking problems for alternating-time formulas"}],"date_updated":"2022-09-05T07:32:05Z","publisher":"Association for Computing Machinery (ACM)","doi":"10.1145/585265.585270","title":"Alternating-time temporal logic","publication":"Proceedings of the 38th Annual Symposium on Foundations of Computer Science","_id":"4609","oa_version":"None","citation":{"ama":"Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i>. Association for Computing Machinery (ACM); 1997:100-109. doi:<a href=\"https://doi.org/10.1145/585265.585270\">10.1145/585265.585270</a>","mla":"Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i>, Association for Computing Machinery (ACM), 1997, pp. 100–09, doi:<a href=\"https://doi.org/10.1145/585265.585270\">10.1145/585265.585270</a>.","chicago":"Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time Temporal Logic.” In <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i>, 100–109. Association for Computing Machinery (ACM), 1997. <a href=\"https://doi.org/10.1145/585265.585270\">https://doi.org/10.1145/585265.585270</a>.","ista":"Alur R, Henzinger TA, Kupferman O. 1997. Alternating-time temporal logic. Proceedings of the 38th Annual Symposium on Foundations of Computer Science. FOCS: Foundations of Computer Science, 100–109.","apa":"Alur, R., Henzinger, T. A., &#38; Kupferman, O. (1997). Alternating-time temporal logic. In <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i> (pp. 100–109). Washington, DC, United States: Association for Computing Machinery (ACM). <a href=\"https://doi.org/10.1145/585265.585270\">https://doi.org/10.1145/585265.585270</a>","short":"R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the 38th Annual Symposium on Foundations of Computer Science, Association for Computing Machinery (ACM), 1997, pp. 100–109.","ieee":"R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,” in <i>Proceedings of the 38th Annual Symposium on Foundations of Computer Science</i>, Washington, DC, United States, 1997, pp. 100–109."},"type":"conference","date_published":"1997-01-01T00:00:00Z","status":"public","scopus_import":"1","year":"1997","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:09:44Z","publication_identifier":{"issn":["0004-5411"]},"day":"01","publist_id":"100","publication_status":"published","author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"last_name":"Kupferman","full_name":"Kupferman, Orna","first_name":"Orna"}],"conference":{"start_date":"1997-10-19","name":"FOCS: Foundations of Computer Science","location":"Washington, DC, United States","end_date":"1997-10-22"},"page":"100 - 109"},{"volume":2,"date_published":"1996-01-01T00:00:00Z","type":"conference","status":"public","citation":{"chicago":"Sazanov, Leonid A, P Burrows, and P J Nixon. “Presence of a Large Protein Complex Containing the NdhK Gene Product and Possessing NADH-Specific Dehydrogenase Activity in Thylakoid Membranes of Higher Plant Chloroplasts,” 2:705–8. Kluwer, 1996.","ama":"Sazanov LA, Burrows P, Nixon PJ. Presence of a large protein complex containing the ndhK gene product and possessing NADH-specific dehydrogenase activity in thylakoid membranes of higher plant chloroplasts. In: Vol 2. Kluwer; 1996:705-708.","mla":"Sazanov, Leonid A., et al. <i>Presence of a Large Protein Complex Containing the NdhK Gene Product and Possessing NADH-Specific Dehydrogenase Activity in Thylakoid Membranes of Higher Plant Chloroplasts</i>. Vol. 2, Kluwer, 1996, pp. 705–08.","short":"L.A. Sazanov, P. Burrows, P.J. Nixon, in:, Kluwer, 1996, pp. 705–708.","ieee":"L. A. Sazanov, P. Burrows, and P. J. Nixon, “Presence of a large protein complex containing the ndhK gene product and possessing NADH-specific dehydrogenase activity in thylakoid membranes of higher plant chloroplasts,” presented at the IPC: International Photosynthesis Congress, 1996, vol. 2, pp. 705–708.","ista":"Sazanov LA, Burrows P, Nixon PJ. 1996. Presence of a large protein complex containing the ndhK gene product and possessing NADH-specific dehydrogenase activity in thylakoid membranes of higher plant chloroplasts. IPC: International Photosynthesis Congress, Photosynthesis: from light to biosphere, vol. 2, 705–708.","apa":"Sazanov, L. A., Burrows, P., &#38; Nixon, P. J. (1996). Presence of a large protein complex containing the ndhK gene product and possessing NADH-specific dehydrogenase activity in thylakoid membranes of higher plant chloroplasts (Vol. 2, pp. 705–708). Presented at the IPC: International Photosynthesis Congress, Kluwer."},"intvolume":"         2","_id":"1942","publisher":"Kluwer","date_updated":"2021-01-12T06:54:14Z","title":"Presence of a large protein complex containing the ndhK gene product and possessing NADH-specific dehydrogenase activity in thylakoid membranes of higher plant chloroplasts","month":"01","extern":1,"quality_controlled":0,"author":[{"orcid":"0000-0002-0977-7989","last_name":"Sazanov","first_name":"Leonid A","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","full_name":"Leonid Sazanov"},{"first_name":"P","full_name":"Burrows, P","last_name":"Burrows"},{"last_name":"Nixon","full_name":"Nixon, P J","first_name":"P J"}],"page":"705 - 708","alternative_title":["Photosynthesis: from light to biosphere"],"conference":{"name":"IPC: International Photosynthesis Congress"},"date_created":"2018-12-11T11:54:50Z","publist_id":"5143","publication_status":"published","day":"01","year":"1996"},{"scopus_import":"1","publication_identifier":{"issn":["0300-5127"]},"issue":"3","pmid":1,"title":"Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids","_id":"1951","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","citation":{"apa":"Sazanov, L. A., Burrows, P., &#38; Nixon, P. (1996). Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids. <i>Biochemical Society Transactions</i>. Portland Press. <a href=\"https://doi.org/10.1042/bst0240739\">https://doi.org/10.1042/bst0240739</a>","ista":"Sazanov LA, Burrows P, Nixon P. 1996. Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids. Biochemical Society Transactions. 24(3), 739–743.","ieee":"L. A. Sazanov, P. Burrows, and P. Nixon, “Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids,” <i>Biochemical Society Transactions</i>, vol. 24, no. 3. Portland Press, pp. 739–743, 1996.","short":"L.A. Sazanov, P. Burrows, P. Nixon, Biochemical Society Transactions 24 (1996) 739–743.","mla":"Sazanov, Leonid A., et al. “Detection and Characterization of a Complex I-like NADH-Specific Dehydrogenase from Pea Thylakoids.” <i>Biochemical Society Transactions</i>, vol. 24, no. 3, Portland Press, 1996, pp. 739–43, doi:<a href=\"https://doi.org/10.1042/bst0240739\">10.1042/bst0240739</a>.","ama":"Sazanov LA, Burrows P, Nixon P. Detection and characterization of a complex I-like NADH-specific dehydrogenase from pea thylakoids. <i>Biochemical Society Transactions</i>. 1996;24(3):739-743. doi:<a href=\"https://doi.org/10.1042/bst0240739\">10.1042/bst0240739</a>","chicago":"Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “Detection and Characterization of a Complex I-like NADH-Specific Dehydrogenase from Pea Thylakoids.” <i>Biochemical Society Transactions</i>. Portland Press, 1996. <a href=\"https://doi.org/10.1042/bst0240739\">https://doi.org/10.1042/bst0240739</a>."},"intvolume":"        24","status":"public","year":"1996","language":[{"iso":"eng"}],"day":"01","publication_status":"published","publist_id":"5131","date_created":"2018-12-11T11:54:53Z","page":"739 - 743","author":[{"id":"338D39FE-F248-11E8-B48F-1D18A9856A87","first_name":"Leonid A","full_name":"Sazanov, Leonid A","last_name":"Sazanov","orcid":"0000-0002-0977-7989"},{"full_name":"Burrows, Paul","first_name":"Paul","last_name":"Burrows"},{"last_name":"Nixon","full_name":"Nixon, Peter","first_name":"Peter"}],"quality_controlled":"1","extern":"1","month":"01","date_updated":"2022-08-16T08:25:02Z","doi":"10.1042/bst0240739","publisher":"Portland Press","publication":"Biochemical Society Transactions","article_processing_charge":"No","external_id":{"pmid":["8878837"]},"oa_version":"None","article_type":"original","type":"journal_article","date_published":"1996-01-01T00:00:00Z","volume":24},{"date_created":"2018-12-11T11:54:53Z","publication_status":"published","publist_id":"5132","day":"11","author":[{"last_name":"Bizouarn","full_name":"Bizouarn, Tania","first_name":"Tania"},{"full_name":"Sazanov, Leonid A","first_name":"Leonid A","id":"338D39FE-F248-11E8-B48F-1D18A9856A87","last_name":"Sazanov","orcid":"0000-0002-0977-7989"},{"first_name":"Sébastien","full_name":"Aubourg, Sébastien","last_name":"Aubourg"},{"full_name":"Jackson, Julie","first_name":"Julie","last_name":"Jackson"}],"page":"4 - 12","year":"1996","language":[{"iso":"eng"}],"oa_version":"None","article_type":"original","external_id":{"pmid":["8573594 "]},"volume":1273,"date_published":"1996-01-11T00:00:00Z","type":"journal_article","month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"Biochimica et Biophysica Acta - Bioenergetics","date_updated":"2022-08-16T12:35:22Z","publisher":"Elsevier","doi":"10.1016/0005-2728(95)00125-5","publication_identifier":{"issn":["0005-2728"]},"issue":"1","citation":{"apa":"Bizouarn, T., Sazanov, L. A., Aubourg, S., &#38; Jackson, J. (1996). Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme. <i>Biochimica et Biophysica Acta - Bioenergetics</i>. Elsevier. <a href=\"https://doi.org/10.1016/0005-2728(95)00125-5\">https://doi.org/10.1016/0005-2728(95)00125-5</a>","ista":"Bizouarn T, Sazanov LA, Aubourg S, Jackson J. 1996. Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme. Biochimica et Biophysica Acta - Bioenergetics. 1273(1), 4–12.","short":"T. Bizouarn, L.A. Sazanov, S. Aubourg, J. Jackson, Biochimica et Biophysica Acta - Bioenergetics 1273 (1996) 4–12.","ieee":"T. Bizouarn, L. A. Sazanov, S. Aubourg, and J. Jackson, “Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme,” <i>Biochimica et Biophysica Acta - Bioenergetics</i>, vol. 1273, no. 1. Elsevier, pp. 4–12, 1996.","mla":"Bizouarn, Tania, et al. “Estimation of the H+/H- Ratio of the Reaction Catalysed by the Nicotinamide Nucleotide Transhydrogenase in Chromatophores from over-Expressing Strains of Rhodospirillum Rubrum and in Liposomes Inlaid with the Purified Bovine Enzyme.” <i>Biochimica et Biophysica Acta - Bioenergetics</i>, vol. 1273, no. 1, Elsevier, 1996, pp. 4–12, doi:<a href=\"https://doi.org/10.1016/0005-2728(95)00125-5\">10.1016/0005-2728(95)00125-5</a>.","ama":"Bizouarn T, Sazanov LA, Aubourg S, Jackson J. Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme. <i>Biochimica et Biophysica Acta - Bioenergetics</i>. 1996;1273(1):4-12. doi:<a href=\"https://doi.org/10.1016/0005-2728(95)00125-5\">10.1016/0005-2728(95)00125-5</a>","chicago":"Bizouarn, Tania, Leonid A Sazanov, Sébastien Aubourg, and Julie Jackson. “Estimation of the H+/H- Ratio of the Reaction Catalysed by the Nicotinamide Nucleotide Transhydrogenase in Chromatophores from over-Expressing Strains of Rhodospirillum Rubrum and in Liposomes Inlaid with the Purified Bovine Enzyme.” <i>Biochimica et Biophysica Acta - Bioenergetics</i>. Elsevier, 1996. <a href=\"https://doi.org/10.1016/0005-2728(95)00125-5\">https://doi.org/10.1016/0005-2728(95)00125-5</a>."},"intvolume":"      1273","status":"public","pmid":1,"acknowledgement":"L.A.S. would like to thank the Wellcome Trust, and T.B., the Biotechnology and Biological Sciences Research Council, for financial support. We are very grateful to Nick Cotton for helpful advice.","abstract":[{"text":"Two strains of Rhodospirillum rubrum were constructed in which, by a gene dosage effect, the transhydrogenase activity of isolated chromatophores was increased 7-10-fold and 15-20-fold, respectively. The H+/H- ratio (the ratio of protons translocated per hydride ion equivalent transferred from NADPH to an NAD+ analogue, acetyl pyridine adenine dinucleotide), determined by a spectroscopic technique, was approximately 1.0 for chromatophores from the over-expressing strains, but was only approximately 0.6 for wild-type chromatophores. Highly-coupled proteoliposomes were prepared containing purified transhydrogenase from beef-heart mitochondria. Using the same technique, the H+/H- ratio was close to 1.0 for these proteoliposomes. It is suggested that the mechanistic H+/H- ratio is indeed unity, but that a low ratio is obtained in wild-type chromatophores because of inhomogeneity in the vesicle population.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"1952","title":"Estimation of the H+/H- ratio of the reaction catalysed by the nicotinamide nucleotide transhydrogenase in chromatophores from over-expressing strains of Rhodospirillum rubrum and in liposomes inlaid with the purified bovine enzyme"},{"issue":"2","publication_identifier":{"issn":["00166731"]},"status":"public","main_file_link":[{"url":"https://www.ncbi.nlm.nih.gov/pmc/articles/PMC1207552/","open_access":"1"}],"citation":{"ista":"de Bono M, Hodgkin J. 1996. Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences. Genetics. 144(2), 587–595.","apa":"de Bono, M., &#38; Hodgkin, J. (1996). Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences. <i>Genetics</i>. Genetics Society of America.","short":"M. de Bono, J. Hodgkin, Genetics 144 (1996) 587–595.","ieee":"M. de Bono and J. Hodgkin, “Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences,” <i>Genetics</i>, vol. 144, no. 2. Genetics Society of America, pp. 587–595, 1996.","ama":"de Bono M, Hodgkin J. Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences. <i>Genetics</i>. 1996;144(2):587-595.","mla":"de Bono, Mario, and J. Hodgkin. “Evolution of Sex Determination in Caenorhabditis: Unusually High Divergence of Tra-1 and Its Functional Consequences.” <i>Genetics</i>, vol. 144, no. 2, Genetics Society of America, 1996, pp. 587–95.","chicago":"Bono, Mario de, and J. Hodgkin. “Evolution of Sex Determination in Caenorhabditis: Unusually High Divergence of Tra-1 and Its Functional Consequences.” <i>Genetics</i>. Genetics Society of America, 1996."},"intvolume":"       144","_id":"6161","title":"Evolution of sex determination in Caenorhabditis: Unusually high divergence of tra-1 and its functional consequences","abstract":[{"lang":"eng","text":"The tra-1 gene is a terminal regulator of somatic sex in Caenorhabditis elegans: high tra-1 activity elicits female development, low tra-1 activity elicits male development. To investigate the function and evolution of tra- 1, we examined the tra-1 gene from the closely related nematode C. briggsae. Ce-tra-1 and Cb-tra-1 are unusually divergent. Each gene generates two transcripts, but only one of these is present in both species. This common transcript encodes TRA-1A, which shows only 44% amino acid identity between the species, a figure much lower than that for previously compared genes. A Cb-tra-1 transgene rescues many tissues of tra-1(null) mutants of C. elegans but not the somatic gonad or germ line. This transgene also causes nongonadal feminization of XO animals, indicating incorrect sexual regulation. Alignment of Ce-TRA-1A and Cb-TRA-1A defined several conserved regions likely to be important for tra-1 function. The phenotype differences between Ce-tra- 1(null) mutants rescued by Cb-tra-1 transgenes and wild-type C. elegans indicate significant divergence of regulatory regions. These molecular and functional studies suggest that evolution of sex determination in nematodes is rapid and genetically complex."}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","pmid":1,"page":"587-595","author":[{"orcid":"0000-0001-8347-0443","last_name":"de Bono","full_name":"de Bono, Mario","first_name":"Mario","id":"4E3FF80E-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Hodgkin","full_name":"Hodgkin, J.","first_name":"J."}],"keyword":["amino acid sequence","article","caenorhabditis elegans","evolution","genetic variability","nonhuman","priority journal","sex determination","Amino Acid Sequence","Animals","Animals","Genetically Modified","Base Sequence","Caenorhabditis","Caenorhabditis elegans","Caenorhabditis elegans Proteins","DNA","Helminth","DNA-Binding Proteins","Evolution","Molecular","Female","Helminth Proteins","Membrane Proteins","Molecular Sequence Data","Mutagenesis","RNA","Messenger","Sequence Homology","Amino Acid","Sex Determination (Analysis)","Transcription Factors","Transgenes","Turner Syndrome","Animalia","Caenorhabditis","Caenorhabditis briggsae","Caenorhabditis elegans","Nematoda"],"publication_status":"published","day":"01","date_created":"2019-03-21T11:50:37Z","year":"1996","language":[{"iso":"eng"}],"volume":144,"date_published":"1996-10-01T00:00:00Z","type":"journal_article","oa_version":"Published Version","external_id":{"pmid":["8889522"]},"publication":"Genetics","publisher":"Genetics Society of America","date_updated":"2021-01-12T08:06:28Z","extern":"1","quality_controlled":"1","oa":1,"month":"10"},{"issue":"1","author":[{"orcid":"0000-0002-5008-6530","last_name":"Henzinger","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H"},{"full_name":"Williamson, David P.","first_name":"David P.","last_name":"Williamson"}],"page":"41-44","date_created":"2022-08-08T11:49:48Z","publication_identifier":{"issn":["0020-0190"]},"publication_status":"published","day":"08","scopus_import":"1","year":"1996","language":[{"iso":"eng"}],"volume":59,"type":"journal_article","date_published":"1996-07-08T00:00:00Z","status":"public","article_type":"original","oa_version":"None","citation":{"mla":"Henzinger, Monika H., and David P. Williamson. “On the Number of Small Cuts in a Graph.” <i>Information Processing Letters</i>, vol. 59, no. 1, Elsevier, 1996, pp. 41–44, doi:<a href=\"https://doi.org/10.1016/0020-0190(96)00079-8\">10.1016/0020-0190(96)00079-8</a>.","ama":"Henzinger MH, Williamson DP. On the number of small cuts in a graph. <i>Information Processing Letters</i>. 1996;59(1):41-44. doi:<a href=\"https://doi.org/10.1016/0020-0190(96)00079-8\">10.1016/0020-0190(96)00079-8</a>","chicago":"Henzinger, Monika H, and David P. Williamson. “On the Number of Small Cuts in a Graph.” <i>Information Processing Letters</i>. Elsevier, 1996. <a href=\"https://doi.org/10.1016/0020-0190(96)00079-8\">https://doi.org/10.1016/0020-0190(96)00079-8</a>.","apa":"Henzinger, M. H., &#38; Williamson, D. P. (1996). On the number of small cuts in a graph. <i>Information Processing Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/0020-0190(96)00079-8\">https://doi.org/10.1016/0020-0190(96)00079-8</a>","ista":"Henzinger MH, Williamson DP. 1996. On the number of small cuts in a graph. Information Processing Letters. 59(1), 41–44.","ieee":"M. H. Henzinger and D. P. Williamson, “On the number of small cuts in a graph,” <i>Information Processing Letters</i>, vol. 59, no. 1. Elsevier, pp. 41–44, 1996.","short":"M.H. Henzinger, D.P. Williamson, Information Processing Letters 59 (1996) 41–44."},"intvolume":"        59","abstract":[{"lang":"eng","text":"We prove that in an undirected graph there are at most O(n²) cuts of size strictly less than of the size of the minimum cut."}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","_id":"11761","publication":"Information Processing Letters","date_updated":"2022-09-12T09:39:51Z","publisher":"Elsevier","doi":"10.1016/0020-0190(96)00079-8","title":"On the number of small cuts in a graph","month":"07","extern":"1","quality_controlled":"1"}]