[{"extern":"1","quality_controlled":"1","oa":1,"month":"12","publication":"Evolution","doi":"10.1111/j.1558-5646.1995.tb04431.x","date_updated":"2022-06-28T07:47:30Z","publisher":"Wiley","article_processing_charge":"No","oa_version":"Published Version","article_type":"original","volume":49,"type":"journal_article","date_published":"1995-12-01T00:00:00Z","year":"1995","language":[{"iso":"eng"}],"publist_id":"1773","publication_status":"published","day":"01","date_created":"2018-12-11T12:08:07Z","page":"1038 - 1045","author":[{"full_name":"Barton, Nicholas H","id":"4880FE40-F248-11E8-B48F-1D18A9856A87","first_name":"Nicholas H","orcid":"0000-0002-8548-5240","last_name":"Barton"}],"_id":"4298","title":"Appendix to \"A simulation study of multilocus clines\" by S J E Baird","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"url":"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x","open_access":"1"}],"citation":{"chicago":"Barton, Nicholas H. “Appendix to ‘A Simulation Study of Multilocus Clines’ by S J E Baird.” <i>Evolution</i>. Wiley, 1995. <a href=\"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x\">https://doi.org/10.1111/j.1558-5646.1995.tb04431.x</a>.","ama":"Barton NH. Appendix to “A simulation study of multilocus clines” by S J E Baird. <i>Evolution</i>. 1995;49(6):1038-1045. doi:<a href=\"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x\">10.1111/j.1558-5646.1995.tb04431.x</a>","mla":"Barton, Nicholas H. “Appendix to ‘A Simulation Study of Multilocus Clines’ by S J E Baird.” <i>Evolution</i>, vol. 49, no. 6, Wiley, 1995, pp. 1038–45, doi:<a href=\"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x\">10.1111/j.1558-5646.1995.tb04431.x</a>.","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,” <i>Evolution</i>, 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. <i>Evolution</i>. Wiley. <a href=\"https://doi.org/10.1111/j.1558-5646.1995.tb04431.x\">https://doi.org/10.1111/j.1558-5646.1995.tb04431.x</a>"},"intvolume":"        49","status":"public","publication_identifier":{"issn":["1558-5646"]},"issue":"6"},{"language":[{"iso":"eng"}],"year":"1995","supervisor":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724"}],"page":"1 - 188","author":[{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"}],"publist_id":"304","publication_status":"published","day":"01","degree_awarded":"PhD","date_created":"2018-12-11T12:08:48Z","_id":"4428","date_updated":"2022-06-28T07:30:34Z","publisher":"Cornell University","title":"Automatic analysis of hybrid systems","abstract":[{"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.","lang":"eng"}],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","extern":"1","oa":1,"month":"08","status":"public","date_published":"1995-08-01T00:00:00Z","type":"dissertation","main_file_link":[{"open_access":"1","url":"https://hdl.handle.net/1813/7193"}],"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. <i>Automatic Analysis of Hybrid Systems</i>. Cornell University, 1995, pp. 1–188.","ieee":"P. Ho, “Automatic analysis of hybrid systems,” Cornell University, 1995.","short":"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). <i>Automatic analysis of hybrid systems</i>. Cornell University."},"oa_version":"Published Version"},{"publication":"4th International Hybrid Systems Workshop","date_updated":"2022-06-10T11:24:15Z","publisher":"Springer","doi":"10.1007/3-540-60472-3_14","article_processing_charge":"No","extern":"1","quality_controlled":"1","series_title":"LNCS","month":"01","volume":999,"date_published":"1995-01-01T00:00:00Z","type":"conference","oa_version":"None","language":[{"iso":"eng"}],"year":"1995","alternative_title":["LNCS"],"page":"265 - 293","conference":{"location":" New Brunswick, NJ, United States of America","end_date":"1955-10-25","start_date":"1995-10-22","name":"Hybrid Systems III"},"author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"}],"publist_id":"281","publication_status":"published","day":"01","date_created":"2018-12-11T12:08:54Z","_id":"4447","title":"HyTech: The Cornell Hybrid Technology Tool","abstract":[{"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.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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":[{"last_name":"Panos","full_name":"Panos, Antsaklis","first_name":"Antsaklis"},{"first_name":"Wolf","full_name":"Kohn, Wolf","last_name":"Kohn"},{"full_name":"Nerode, Anil","first_name":"Anil","last_name":"Nerode"},{"last_name":"Sastry","first_name":"Shankar","full_name":"Sastry, Shankar"}],"intvolume":"       999","citation":{"ama":"Henzinger TA, Ho P. HyTech: The Cornell Hybrid Technology Tool. In: Panos A, Kohn W, Nerode A, Sastry S, eds. <i>4th International Hybrid Systems Workshop</i>. Vol 999. LNCS. Springer; 1995:265-293. doi:<a href=\"https://doi.org/10.1007/3-540-60472-3_14\">10.1007/3-540-60472-3_14</a>","mla":"Henzinger, Thomas A., and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” <i>4th International Hybrid Systems Workshop</i>, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 265–93, doi:<a href=\"https://doi.org/10.1007/3-540-60472-3_14\">10.1007/3-540-60472-3_14</a>.","chicago":"Henzinger, Thomas A, and Pei Ho. “HyTech: The Cornell Hybrid Technology Tool.” In <i>4th International Hybrid Systems Workshop</i>, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:265–93. LNCS. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60472-3_14\">https://doi.org/10.1007/3-540-60472-3_14</a>.","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., &#38; Ho, P. (1995). HyTech: The Cornell Hybrid Technology Tool. In A. Panos, W. Kohn, A. Nerode, &#38; S. Sastry (Eds.), <i>4th International Hybrid Systems Workshop</i> (Vol. 999, pp. 265–293).  New Brunswick, NJ, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-60472-3_14\">https://doi.org/10.1007/3-540-60472-3_14</a>","ieee":"T. A. Henzinger and P. Ho, “HyTech: The Cornell Hybrid Technology Tool,” in <i>4th International Hybrid Systems Workshop</i>,  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."},"publication_identifier":{"isbn":["9783540683346"]}},{"publication_identifier":{"isbn":["9783540604723"]},"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.","abstract":[{"lang":"eng","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."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4448","title":"A note on abstract-interpretation strategies for hybrid automata","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60472-3_13"}],"editor":[{"last_name":"Panos","first_name":"Antsaklis","full_name":"Panos, Antsaklis"},{"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"}],"citation":{"chicago":"Henzinger, Thomas A, and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” In <i>3rd International Hybrid Systems Workshop</i>, edited by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:252–64. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60472-3_13\">https://doi.org/10.1007/3-540-60472-3_13</a>.","mla":"Henzinger, Thomas A., and Pei Ho. “A Note on Abstract-Interpretation Strategies for Hybrid Automata.” <i>3rd International Hybrid Systems Workshop</i>, edited by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 252–64, doi:<a href=\"https://doi.org/10.1007/3-540-60472-3_13\">10.1007/3-540-60472-3_13</a>.","ama":"Henzinger TA, Ho P. A note on abstract-interpretation strategies for hybrid automata. In: Panos A, Kohn W, Nerode A, Sastry S, eds. <i>3rd International Hybrid Systems Workshop</i>. Vol 999. Springer; 1995:252-264. doi:<a href=\"https://doi.org/10.1007/3-540-60472-3_13\">10.1007/3-540-60472-3_13</a>","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 <i>3rd International Hybrid Systems Workshop</i>, Ithaca, NY, United States of America, 1995, vol. 999, pp. 252–264.","apa":"Henzinger, T. A., &#38; Ho, P. (1995). A note on abstract-interpretation strategies for hybrid automata. In A. Panos, W. Kohn, A. Nerode, &#38; S. Sastry (Eds.), <i>3rd International Hybrid Systems Workshop</i> (Vol. 999, pp. 252–264). Ithaca, NY, United States of America: Springer. <a href=\"https://doi.org/10.1007/3-540-60472-3_13\">https://doi.org/10.1007/3-540-60472-3_13</a>","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."},"intvolume":"       999","status":"public","year":"1995","language":[{"iso":"eng"}],"date_created":"2018-12-11T12:08:54Z","publist_id":"282","publication_status":"published","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":"Ho","full_name":"Ho, Pei","first_name":"Pei"}],"alternative_title":["LNCS"],"page":"252 - 264","conference":{"start_date":"1994-10-28","name":"Hybrid Systems II","location":"Ithaca, NY, United States of America","end_date":"1994-10-30"},"month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"3rd International Hybrid Systems Workshop","doi":"10.1007/3-540-60472-3_13","publisher":"Springer","date_updated":"2022-06-10T11:48:59Z","oa_version":"None","volume":999,"type":"conference","date_published":"1995-01-01T00:00:00Z"},{"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60045-0_53"}],"citation":{"mla":"Henzinger, Thomas A., and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” <i>7th International Conference on Computer Aided Verification</i>, vol. 939, Springer, 1995, pp. 225–38, doi:<a href=\"https://doi.org/10.1007/3-540-60045-0_53\">10.1007/3-540-60045-0_53</a>.","ama":"Henzinger TA, Ho P. Algorithmic analysis of nonlinear hybrid systems. In: <i>7th International Conference on Computer Aided Verification</i>. Vol 939. Springer; 1995:225-238. doi:<a href=\"https://doi.org/10.1007/3-540-60045-0_53\">10.1007/3-540-60045-0_53</a>","chicago":"Henzinger, Thomas A, and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid Systems.” In <i>7th International Conference on Computer Aided Verification</i>, 939:225–38. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60045-0_53\">https://doi.org/10.1007/3-540-60045-0_53</a>.","apa":"Henzinger, T. A., &#38; Ho, P. (1995). Algorithmic analysis of nonlinear hybrid systems. In <i>7th International Conference on Computer Aided Verification</i> (Vol. 939, pp. 225–238). Liege, Belgium: Springer. <a href=\"https://doi.org/10.1007/3-540-60045-0_53\">https://doi.org/10.1007/3-540-60045-0_53</a>","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.","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 <i>7th International Conference on Computer Aided Verification</i>, Liege, Belgium, 1995, vol. 939, pp. 225–238."},"intvolume":"       939","status":"public","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.","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","publication_identifier":{"isbn":["9783540494133"]},"scopus_import":"1","oa_version":"None","volume":939,"type":"conference","date_published":"1995-01-01T00:00:00Z","month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"7th International Conference on Computer Aided Verification","publisher":"Springer","date_updated":"2022-06-10T09:48:52Z","doi":"10.1007/3-540-60045-0_53","date_created":"2018-12-11T12:08:55Z","publist_id":"280","publication_status":"published","day":"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":"Ho","full_name":"Ho, Pei","first_name":"Pei"}],"page":"225 - 238","alternative_title":["LNCS"],"conference":{"end_date":"1995-07-05","location":"Liege, Belgium","name":"CAV: Computer Aided Verification","start_date":"1995-07-03"},"language":[{"iso":"eng"}],"year":"1995"},{"status":"public","citation":{"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.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1995). A user guide to HyTech. In <i>1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 1019, pp. 41–71). Aarhus, Denmark: Springer. <a href=\"https://doi.org/10.1007/3-540-60630-0_3\">https://doi.org/10.1007/3-540-60630-0_3</a>","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 <i>1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems</i>, Aarhus, Denmark, 1995, vol. 1019, pp. 41–71.","ama":"Henzinger TA, Ho P, Wong Toi H. A user guide to HyTech. In: <i>1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 1019. Springer; 1995:41-71. doi:<a href=\"https://doi.org/10.1007/3-540-60630-0_3\">10.1007/3-540-60630-0_3</a>","mla":"Henzinger, Thomas A., et al. “A User Guide to HyTech.” <i>1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 1019, Springer, 1995, pp. 41–71, doi:<a href=\"https://doi.org/10.1007/3-540-60630-0_3\">10.1007/3-540-60630-0_3</a>.","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “A User Guide to HyTech.” In <i>1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems</i>, 1019:41–71. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60630-0_3\">https://doi.org/10.1007/3-540-60630-0_3</a>."},"intvolume":"      1019","main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60630-0_3"}],"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","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.","publication_identifier":{"isbn":["9783540606307"]},"scopus_import":"1","date_published":"1995-01-01T00:00:00Z","type":"conference","volume":1019,"oa_version":"None","article_processing_charge":"No","doi":"10.1007/3-540-60630-0_3","date_updated":"2022-06-10T09:00:05Z","publisher":"Springer","publication":"1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems","month":"01","quality_controlled":"1","extern":"1","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"},{"last_name":"Wong Toi","full_name":"Wong Toi, Howard","first_name":"Howard"}],"conference":{"end_date":"1995-05-20","location":"Aarhus, Denmark","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"1995-05-19"},"alternative_title":["LNCS"],"page":"41 - 71","date_created":"2018-12-11T12:09:09Z","day":"01","publication_status":"published","publist_id":"230","language":[{"iso":"eng"}],"year":"1995"},{"date_published":"1995-11-01T00:00:00Z","type":"conference","status":"public","oa_version":"None","citation":{"apa":"Henzinger, M. H., Henzinger, T. A., &#38; Kopke, P. (1995). Computing simulations on finite and infinite graphs. In <i>Proceedings of IEEE 36th Annual Foundations of Computer Science</i> (pp. 453–462). Milwaukee, WI, United States of America: IEEE. <a href=\"https://doi.org/10.1109/SFCS.1995.492576\">https://doi.org/10.1109/SFCS.1995.492576</a>","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.","ieee":"M. H. Henzinger, T. A. Henzinger, and P. Kopke, “Computing simulations on finite and infinite graphs,” in <i>Proceedings of IEEE 36th Annual Foundations of Computer Science</i>, Milwaukee, WI, United States of America, 1995, pp. 453–462.","short":"M.H. Henzinger, T.A. Henzinger, P. Kopke, in:, Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE, 1995, pp. 453–462.","mla":"Henzinger, Monika H., et al. “Computing Simulations on Finite and Infinite Graphs.” <i>Proceedings of IEEE 36th Annual Foundations of Computer Science</i>, IEEE, 1995, pp. 453–62, doi:<a href=\"https://doi.org/10.1109/SFCS.1995.492576\">10.1109/SFCS.1995.492576</a>.","ama":"Henzinger MH, Henzinger TA, Kopke P. Computing simulations on finite and infinite graphs. In: <i>Proceedings of IEEE 36th Annual Foundations of Computer Science</i>. IEEE; 1995:453-462. doi:<a href=\"https://doi.org/10.1109/SFCS.1995.492576\">10.1109/SFCS.1995.492576</a>","chicago":"Henzinger, Monika H, Thomas A Henzinger, and Peter Kopke. “Computing Simulations on Finite and Infinite Graphs.” In <i>Proceedings of IEEE 36th Annual Foundations of Computer Science</i>, 453–62. IEEE, 1995. <a href=\"https://doi.org/10.1109/SFCS.1995.492576\">https://doi.org/10.1109/SFCS.1995.492576</a>."},"article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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"}],"title":"Computing simulations on finite and infinite graphs","doi":"10.1109/SFCS.1995.492576","date_updated":"2023-02-09T08:43:48Z","publisher":"IEEE","_id":"4498","publication":"Proceedings of IEEE 36th Annual Foundations of Computer Science","month":"11","quality_controlled":"1","extern":"1","author":[{"last_name":"Henzinger","orcid":"0000-0002-5008-6530","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","first_name":"Monika H","full_name":"Henzinger, Monika H"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"},{"first_name":"Peter","full_name":"Kopke, Peter","last_name":"Kopke"}],"conference":{"end_date":"1995-10-25","location":"Milwaukee, WI, United States of America","name":"FOCS: Foundations of Computer Science","start_date":"1995-10-23"},"page":"453 - 462","publication_identifier":{"issn":["0272-5428"],"isbn":["0818671831"]},"date_created":"2018-12-11T12:09:10Z","day":"01","publication_status":"published","publist_id":"231","scopus_import":"1","year":"1995","language":[{"iso":"eng"}]},{"date_published":"1995-01-01T00:00:00Z","type":"conference","status":"public","oa_version":"None","main_file_link":[{"url":"https://ieeexplore.ieee.org/document/495196"}],"citation":{"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 <i>Proceedings 16th IEEE Real-Time Systems Symposium</i>, Pisa, Italy, 1995, pp. 56–65.","apa":"Henzinger, T. A., Ho, P., &#38; Wong Toi, H. (1995). HyTech: The next generation. In <i>Proceedings 16th IEEE Real-Time Systems Symposium</i> (pp. 56–65). Pisa, Italy: IEEE. <a href=\"https://doi.org/10.1109/REAL.1995.495196 \">https://doi.org/10.1109/REAL.1995.495196 </a>","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.","chicago":"Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: The next Generation.” In <i>Proceedings 16th IEEE Real-Time Systems Symposium</i>, 56–65. IEEE, 1995. <a href=\"https://doi.org/10.1109/REAL.1995.495196 \">https://doi.org/10.1109/REAL.1995.495196 </a>.","mla":"Henzinger, Thomas A., et al. “HyTech: The next Generation.” <i>Proceedings 16th IEEE Real-Time Systems Symposium</i>, IEEE, 1995, pp. 56–65, doi:<a href=\"https://doi.org/10.1109/REAL.1995.495196 \">10.1109/REAL.1995.495196 </a>.","ama":"Henzinger TA, Ho P, Wong Toi H. HyTech: The next generation. In: <i>Proceedings 16th IEEE Real-Time Systems Symposium</i>. IEEE; 1995:56-65. doi:<a href=\"https://doi.org/10.1109/REAL.1995.495196 \">10.1109/REAL.1995.495196 </a>"},"abstract":[{"lang":"eng","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"}],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","publication":"Proceedings 16th IEEE Real-Time Systems Symposium","_id":"4499","date_updated":"2022-06-10T09:33:19Z","publisher":"IEEE","doi":"10.1109/REAL.1995.495196 ","title":"HyTech: The next generation","month":"01","extern":"1","quality_controlled":"1","author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Ho","full_name":"Ho, Pei","first_name":"Pei"},{"full_name":"Wong Toi, Howard","first_name":"Howard","last_name":"Wong Toi"}],"page":"56 - 65","conference":{"start_date":"1995-12-05","name":"RTSS: Real-Time Systems Symposium","location":"Pisa, Italy","end_date":"1995-12-07"},"publication_identifier":{"isbn":["0818673370"]},"date_created":"2018-12-11T12:09:10Z","publist_id":"232","publication_status":"published","day":"01","scopus_import":"1","language":[{"iso":"eng"}],"year":"1995"},{"oa_version":"None","date_published":"1995-01-01T00:00:00Z","type":"conference","volume":944,"month":"01","quality_controlled":"1","extern":"1","article_processing_charge":"No","doi":"10.1007/3-540-60084-1_93","date_updated":"2022-06-09T14:58:31Z","publisher":"Springer","publication":"22nd International Colloquium on Automata, Languages and Programming ","date_created":"2018-12-11T12:09:10Z","day":"01","publist_id":"229","publication_status":"published","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":"Kopke","full_name":"Kopke, Peter","first_name":"Peter"},{"first_name":"Howard","full_name":"Wong Toi, Howard","last_name":"Wong Toi"}],"conference":{"end_date":"1995-07-14","location":"Szeged, Hungary","name":"ICALP: Automata, Languages and Programming","start_date":"1995-07-10"},"alternative_title":["LNCS"],"page":"417 - 428","year":"1995","language":[{"iso":"eng"}],"intvolume":"       944","citation":{"mla":"Henzinger, Thomas A., et al. “The Expressive Power of Clocks.” <i>22nd International Colloquium on Automata, Languages and Programming </i>, vol. 944, Springer, 1995, pp. 417–28, doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_93\">10.1007/3-540-60084-1_93</a>.","ama":"Henzinger TA, Kopke P, Wong Toi H. The expressive power of clocks. In: <i>22nd International Colloquium on Automata, Languages and Programming </i>. Vol 944. Springer; 1995:417-428. doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_93\">10.1007/3-540-60084-1_93</a>","chicago":"Henzinger, Thomas A, Peter Kopke, and Howard Wong Toi. “The Expressive Power of Clocks.” In <i>22nd International Colloquium on Automata, Languages and Programming </i>, 944:417–28. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60084-1_93\">https://doi.org/10.1007/3-540-60084-1_93</a>.","apa":"Henzinger, T. A., Kopke, P., &#38; Wong Toi, H. (1995). The expressive power of clocks. In <i>22nd International Colloquium on Automata, Languages and Programming </i> (Vol. 944, pp. 417–428). Szeged, Hungary: Springer. <a href=\"https://doi.org/10.1007/3-540-60084-1_93\">https://doi.org/10.1007/3-540-60084-1_93</a>","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.","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 <i>22nd International Colloquium on Automata, Languages and Programming </i>, Szeged, Hungary, 1995, vol. 944, pp. 417–428."},"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60084-1_93"}],"status":"public","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.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","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."}],"title":"The expressive power of clocks","_id":"4500","publication_identifier":{"isbn":["9783540600848"]}},{"author":[{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Kopke, Peter","first_name":"Peter","last_name":"Kopke"},{"first_name":"Anuj","full_name":"Puri, Anuj","last_name":"Puri"},{"first_name":"P.","full_name":"Varaiya, P.","last_name":"Varaiya"}],"conference":{"location":"Las Vegas, NV, United States of America","end_date":"1995-06-01","start_date":"1995-05-29","name":"STOC: Symposium on the Theory of Computing"},"page":"373 - 382","date_created":"2018-12-11T12:09:11Z","publication_identifier":{"isbn":["9780897917186"]},"day":"01","publication_status":"published","publist_id":"228","year":"1995","language":[{"iso":"eng"}],"type":"conference","date_published":"1995-01-01T00:00:00Z","status":"public","oa_version":"Published Version","citation":{"ieee":"T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about hybrid automata?,” in <i>Proceedings of the 27th annual ACM symposium on Theory of computing</i>, 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.","apa":"Henzinger, T. A., Kopke, P., Puri, A., &#38; Varaiya, P. (1995). What’s decidable about hybrid automata? In <i>Proceedings of the 27th annual ACM symposium on Theory of computing</i> (pp. 373–382). Las Vegas, NV, United States of America: ACM. <a href=\"https://doi.org/10.1145/225058.225162\">https://doi.org/10.1145/225058.225162</a>","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.","chicago":"Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable about Hybrid Automata?” In <i>Proceedings of the 27th Annual ACM Symposium on Theory of Computing</i>, 373–82. ACM, 1995. <a href=\"https://doi.org/10.1145/225058.225162\">https://doi.org/10.1145/225058.225162</a>.","mla":"Henzinger, Thomas A., et al. “What’s Decidable about Hybrid Automata?” <i>Proceedings of the 27th Annual ACM Symposium on Theory of Computing</i>, ACM, 1995, pp. 373–82, doi:<a href=\"https://doi.org/10.1145/225058.225162\">10.1145/225058.225162</a>.","ama":"Henzinger TA, Kopke P, Puri A, Varaiya P. What’s decidable about hybrid automata? In: <i>Proceedings of the 27th Annual ACM Symposium on Theory of Computing</i>. ACM; 1995:373-382. doi:<a href=\"https://doi.org/10.1145/225058.225162\">10.1145/225058.225162</a>"},"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/225058.225162","open_access":"1"}],"article_processing_charge":"No","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","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"}],"doi":"10.1145/225058.225162","date_updated":"2022-06-09T14:40:29Z","publisher":"ACM","title":"What's decidable about hybrid automata?","_id":"4502","publication":"Proceedings of the 27th annual ACM symposium on Theory of computing","month":"01","oa":1,"quality_controlled":"1","acknowledgement":"We thank Howard Wong-Toi for a careful reading.\r\n","extern":"1"},{"type":"conference","date_published":"1995-01-01T00:00:00Z","volume":944,"oa_version":"None","article_processing_charge":"No","doi":"10.1007/3-540-60084-1_85","publisher":"Springer","date_updated":"2022-06-09T14:21:08Z","publication":"22nd International Colloquium on Automata, Languages and Programming ","month":"01","quality_controlled":"1","extern":"1","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"conference":{"name":"ICALP: Automata, Languages and Programming","start_date":"1995-07-10","end_date":"1995-07-14","location":"Szeged, Hungary"},"alternative_title":["LNCS"],"page":"324 - 335","date_created":"2018-12-11T12:09:16Z","day":"01","publist_id":"212","publication_status":"published","year":"1995","language":[{"iso":"eng"}],"status":"public","intvolume":"       944","citation":{"chicago":"Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” In <i>22nd International Colloquium on Automata, Languages and Programming </i>, 944:324–35. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60084-1_85\">https://doi.org/10.1007/3-540-60084-1_85</a>.","ama":"Henzinger TA. Hybrid automata with finite bisimulations. In: <i>22nd International Colloquium on Automata, Languages and Programming </i>. Vol 944. Springer; 1995:324-335. doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_85\">10.1007/3-540-60084-1_85</a>","mla":"Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” <i>22nd International Colloquium on Automata, Languages and Programming </i>, vol. 944, Springer, 1995, pp. 324–35, doi:<a href=\"https://doi.org/10.1007/3-540-60084-1_85\">10.1007/3-540-60084-1_85</a>.","ieee":"T. A. Henzinger, “Hybrid automata with finite bisimulations,” in <i>22nd International Colloquium on Automata, Languages and Programming </i>, 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 <i>22nd International Colloquium on Automata, Languages and Programming </i> (Vol. 944, pp. 324–335). Szeged, Hungary: Springer. <a href=\"https://doi.org/10.1007/3-540-60084-1_85\">https://doi.org/10.1007/3-540-60084-1_85</a>"},"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60084-1_85"}],"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"}],"title":"Hybrid automata with finite bisimulations","_id":"4518","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","publication_identifier":{"isbn":["9783540600848"]}},{"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/3-540-60045-0_49"}],"citation":{"apa":"Alur, R., &#38; Henzinger, T. A. (1995). Local liveness for compositional modeling of fair reactive systems. In <i>7th International Conference on Computer Aided Verification</i> (Vol. 939, pp. 166–179). Liege, Belgium: Springer. <a href=\"https://doi.org/10.1007/3-540-60045-0_49\">https://doi.org/10.1007/3-540-60045-0_49</a>","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.","short":"R. Alur, T.A. Henzinger, in:, 7th International Conference on Computer Aided Verification, Springer, 1995, pp. 166–179.","ieee":"R. Alur and T. A. Henzinger, “Local liveness for compositional modeling of fair reactive systems,” in <i>7th International Conference on Computer Aided Verification</i>, Liege, Belgium, 1995, vol. 939, pp. 166–179.","mla":"Alur, Rajeev, and Thomas A. Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” <i>7th International Conference on Computer Aided Verification</i>, vol. 939, Springer, 1995, pp. 166–79, doi:<a href=\"https://doi.org/10.1007/3-540-60045-0_49\">10.1007/3-540-60045-0_49</a>.","ama":"Alur R, Henzinger TA. Local liveness for compositional modeling of fair reactive systems. In: <i>7th International Conference on Computer Aided Verification</i>. Vol 939. Springer; 1995:166-179. doi:<a href=\"https://doi.org/10.1007/3-540-60045-0_49\">10.1007/3-540-60045-0_49</a>","chicago":"Alur, Rajeev, and Thomas A Henzinger. “Local Liveness for Compositional Modeling of Fair Reactive Systems.” In <i>7th International Conference on Computer Aided Verification</i>, 939:166–79. Springer, 1995. <a href=\"https://doi.org/10.1007/3-540-60045-0_49\">https://doi.org/10.1007/3-540-60045-0_49</a>."},"intvolume":"       939","status":"public","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.","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","_id":"4587","title":"Local liveness for compositional modeling of fair reactive systems","publication_identifier":{"isbn":["978-3-540-60045-9"]},"oa_version":"None","volume":939,"date_published":"1995-01-01T00:00:00Z","type":"conference","month":"01","extern":"1","quality_controlled":"1","article_processing_charge":"No","publication":"7th International Conference on Computer Aided Verification","doi":"10.1007/3-540-60045-0_49","date_updated":"2022-06-09T14:05:04Z","publisher":"Springer","date_created":"2018-12-11T12:09:37Z","publist_id":"120","publication_status":"published","day":"01","author":[{"last_name":"Alur","full_name":"Alur, Rajeev","first_name":"Rajeev"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724"}],"alternative_title":["LNCS"],"page":"166 - 179","conference":{"name":"CAV: Computer Aided Verification","start_date":"1995-07-03","end_date":"1995-07-05","location":"Liege, Belgium"},"year":"1995","language":[{"iso":"eng"}]},{"issue":"1","publication_identifier":{"issn":["0304-3975"]},"status":"public","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/030439759400202T?via%3Dihub"}],"intvolume":"       138","citation":{"apa":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin, X., … Yovine, S. (1995). The algorithmic analysis of hybrid systems. <i>Theoretical Computer Science</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">https://doi.org/10.1016/0304-3975(94)00202-T</a>","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.","ieee":"R. Alur <i>et al.</i>, “The algorithmic analysis of hybrid systems,” <i>Theoretical Computer Science</i>, vol. 138, no. 1. Elsevier, pp. 3–34, 1995.","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.","mla":"Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” <i>Theoretical Computer Science</i>, vol. 138, no. 1, Elsevier, 1995, pp. 3–34, doi:<a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">10.1016/0304-3975(94)00202-T</a>.","ama":"Alur R, Courcoubetis C, Halbwachs N, et al. The algorithmic analysis of hybrid systems. <i>Theoretical Computer Science</i>. 1995;138(1):3-34. doi:<a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">10.1016/0304-3975(94)00202-T</a>","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.” <i>Theoretical Computer Science</i>. Elsevier, 1995. <a href=\"https://doi.org/10.1016/0304-3975(94)00202-T\">https://doi.org/10.1016/0304-3975(94)00202-T</a>."},"abstract":[{"lang":"eng","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."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4613","title":"The algorithmic analysis of hybrid systems","author":[{"last_name":"Alur","first_name":"Rajeev","full_name":"Alur, Rajeev"},{"last_name":"Courcoubetis","full_name":"Courcoubetis, Costas","first_name":"Costas"},{"full_name":"Halbwachs, Nicolas","first_name":"Nicolas","last_name":"Halbwachs"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","last_name":"Henzinger"},{"full_name":"Ho, Pei","first_name":"Pei","last_name":"Ho"},{"first_name":"Xavier","full_name":"Nicollin, Xavier","last_name":"Nicollin"},{"first_name":"Alfredo","full_name":"Olivero, Alfredo","last_name":"Olivero"},{"last_name":"Sifakis","full_name":"Sifakis, Joseph","first_name":"Joseph"},{"last_name":"Yovine","full_name":"Yovine, Sergio","first_name":"Sergio"}],"page":"3 - 34","date_created":"2018-12-11T12:09:45Z","publist_id":"94","publication_status":"published","day":"06","year":"1995","language":[{"iso":"eng"}],"volume":138,"date_published":"1995-02-06T00:00:00Z","type":"journal_article","article_type":"original","oa_version":"None","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","month":"02","extern":"1","quality_controlled":"1"},{"publication_status":"published","publist_id":"4438","day":"01","publication_identifier":{"isbn":["978-1-4020-2684-3"]},"date_created":"2018-12-11T11:57:49Z","page":"451 - 484","author":[{"last_name":"Morris","first_name":"David","full_name":"Morris, David"},{"id":"4159519E-F248-11E8-B48F-1D18A9856A87","first_name":"Jirí","full_name":"Friml, Jirí","last_name":"Friml","orcid":"0000-0002-8302-7596"},{"last_name":"Zažímalová","full_name":"Zažímalová, Eva","first_name":"Eva"}],"language":[{"iso":"eng"}],"year":"1995","scopus_import":"1","editor":[{"full_name":"Davies, Peter","first_name":"Peter","last_name":"Davies"}],"main_file_link":[{"url":"https://link.springer.com/chapter/10.1007/978-1-4020-2686-7_21"}],"citation":{"apa":"Morris, D., Friml, J., &#38; Zažímalová, E. (1995). Auxin transport. In P. Davies (Ed.), <i>Plant Hormones: Biosynthesis, Signal Transduction, Action!</i> (pp. 451–484). Kluwer. <a href=\"https://doi.org/10.1007/978-1-4020-2686-7_21\">https://doi.org/10.1007/978-1-4020-2686-7_21</a>","ista":"Morris D, Friml J, Zažímalová E. 1995.Auxin transport. In: Plant Hormones: Biosynthesis, Signal Transduction, Action! , 451–484.","short":"D. Morris, J. Friml, E. Zažímalová, in:, P. Davies (Ed.), Plant Hormones: Biosynthesis, Signal Transduction, Action!, Kluwer, 1995, pp. 451–484.","ieee":"D. Morris, J. Friml, and E. Zažímalová, “Auxin transport,” in <i>Plant Hormones: Biosynthesis, Signal Transduction, Action!</i>, P. Davies, Ed. Kluwer, 1995, pp. 451–484.","mla":"Morris, David, et al. “Auxin Transport.” <i>Plant Hormones: Biosynthesis, Signal Transduction, Action!</i>, edited by Peter Davies, Kluwer, 1995, pp. 451–84, doi:<a href=\"https://doi.org/10.1007/978-1-4020-2686-7_21\">10.1007/978-1-4020-2686-7_21</a>.","ama":"Morris D, Friml J, Zažímalová E. Auxin transport. In: Davies P, ed. <i>Plant Hormones: Biosynthesis, Signal Transduction, Action!</i>. Kluwer; 1995:451-484. doi:<a href=\"https://doi.org/10.1007/978-1-4020-2686-7_21\">10.1007/978-1-4020-2686-7_21</a>","chicago":"Morris, David, Jiří Friml, and Eva Zažímalová. “Auxin Transport.” In <i>Plant Hormones: Biosynthesis, Signal Transduction, Action!</i>, edited by Peter Davies, 451–84. Kluwer, 1995. <a href=\"https://doi.org/10.1007/978-1-4020-2686-7_21\">https://doi.org/10.1007/978-1-4020-2686-7_21</a>."},"oa_version":"None","status":"public","type":"book_chapter","date_published":"1995-01-01T00:00:00Z","extern":"1","quality_controlled":"1","month":"01","publication":"Plant Hormones: Biosynthesis, Signal Transduction, Action!","_id":"2465","title":"Auxin transport","date_updated":"2022-06-29T14:45:32Z","publisher":"Kluwer","doi":"10.1007/978-1-4020-2686-7_21","abstract":[{"lang":"eng","text":"Auxins play a crucial role in the regulation of spatial and temporal aspects of plant growth and development1. As well as being required for the division, enlargement and differentiation of individual plant cells, auxins also function as signals between cells, tissues and organs. In this way they contribute to the coordination and integration of growth and development in the whole plant and to physiological responses of plants to environmental cues (63). At the individual cell level, fast changes or pulses in hormone concentration may function to initiate or to terminate a developmental process. In contrast, the maintenance of a stable concentration of the hormone (homeostasis) may be necessary to maintain the progress of a developmental event that has already been initiated."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","article_processing_charge":"No"},{"scopus_import":"1","publication_identifier":{"issn":["0021-9967"]},"issue":"4","acknowledgement":"We are grateful  to Akira Uesugi for photographic help. This work has been supported in part by research grants from the Ministry of Education, Science and  Culture of Japan.","pmid":1,"_id":"2491","title":"Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain","abstract":[{"lang":"eng","text":"The distribution of mRNAs for metabotropic glutamate receptors, mGluR4 and mGluR7, which are highly sensitive for L-2-amino-4-phosphonobutyrate (L- AP4), was examined in the central nervous system of the rat by in situ hybridization. In general, the hybridization signals of mGluR7 mRNA were more widely distributed than those of mGluR4 mRNA, and differential expression of mGluR4 mRNA and mGluR7 mRNA was clearly indicated in some brain regions. Intense or moderate expression of mGluR4 mRNA was detected in the granule cells of the olfactory bulb and cerebellum, whereas no significant expression of mGluR7 mRNA was found in these cells. In other neurons or regions where mGluR7 mRNA was intensely or moderately expressed, no significant expression of mGluR4 mRNA was observed. Such were the mitral and tufted cells of the olfactory bulb; anterior olfactory nucleus; neocortical regions; cingulate cortex; retrosplenial cortex; piriform cortex; perirhinal cortex; CA1; CA3; granule cells of the dentate gyrus; superficial layers of the subicular cortex; deep layers of the entorhinal, parasubicular, and presubicular cortices; ventral part of the lateral septal nucleus; septohippocampal nucleus; triangular septal nucleus; nuclei of the diagonal band; bed nucleus of the stria terminalis; ventral pallidum; claustrum; amygdaloid nuclei other than the intercalated nuclei; preoptic region; hypothalamic nuclei other than the medial mammillary nucleus; ventral lateral geniculate nucleus; locus coeruleus; Purkinje cells; many nuclei of the lower brainstem other than the superior colliculus, periaqueductal gray, interpeduncular nucleus, pontine nuclei, and dorsal cochlear nucleus; and dorsal horn of the spinal cord. Both mGluR4 mRNA and mGluR7 mRNA were moderately or intensely expressed in the olfactory tubercle, superficial layers of the entorhinal cortex, CA4, septofimbrial nucleus, intercalated nuclei of the amygdala, medial mammillary nucleus, many thalamic nuclei, and pontine nuclei. Intense expression of both mGluR4 mRNA and mGluR7 mRNA was further detected in the trigeminal ganglion and dorsal root ganglia, whereas no significant expression of them was found in the pterygopalatine ganglion and superior cervical ganglion. The results indicate differential roles of the L-AP4-sensitive metabotropic glutamate receptors in the glutamatergic nervous system."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"url":"https://onlinelibrary.wiley.com/doi/abs/10.1002/cne.903600402"}],"intvolume":"       360","citation":{"ista":"Ohishi H, Akazawa C, Shigemoto R, Nakanishi S, Mizuno N. 1995. Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain. Journal of Comparative Neurology. 360(4), 555–570.","apa":"Ohishi, H., Akazawa, C., Shigemoto, R., Nakanishi, S., &#38; Mizuno, N. (1995). Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain. <i>Journal of Comparative Neurology</i>. Wiley-Blackwell. <a href=\"https://doi.org/10.1002/cne.903600402\">https://doi.org/10.1002/cne.903600402</a>","short":"H. Ohishi, C. Akazawa, R. Shigemoto, S. Nakanishi, N. Mizuno, Journal of Comparative Neurology 360 (1995) 555–570.","ieee":"H. Ohishi, C. Akazawa, R. Shigemoto, S. Nakanishi, and N. Mizuno, “Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain,” <i>Journal of Comparative Neurology</i>, vol. 360, no. 4. Wiley-Blackwell, pp. 555–570, 1995.","ama":"Ohishi H, Akazawa C, Shigemoto R, Nakanishi S, Mizuno N. Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic glutamate receptors, mGluR4 and mGluR7, in the rat brain. <i>Journal of Comparative Neurology</i>. 1995;360(4):555-570. doi:<a href=\"https://doi.org/10.1002/cne.903600402\">10.1002/cne.903600402</a>","mla":"Ohishi, Hitoshi, et al. “Distributions of the MRNAs for L-2-Amino-4-Phosphonobutyrate-Sensitive Metabotropic Glutamate Receptors, MGluR4 and MGluR7, in the Rat Brain.” <i>Journal of Comparative Neurology</i>, vol. 360, no. 4, Wiley-Blackwell, 1995, pp. 555–70, doi:<a href=\"https://doi.org/10.1002/cne.903600402\">10.1002/cne.903600402</a>.","chicago":"Ohishi, Hitoshi, Chihiro Akazawa, Ryuichi Shigemoto, Shigetada Nakanishi, and Noboru Mizuno. “Distributions of the MRNAs for L-2-Amino-4-Phosphonobutyrate-Sensitive Metabotropic Glutamate Receptors, MGluR4 and MGluR7, in the Rat Brain.” <i>Journal of Comparative Neurology</i>. Wiley-Blackwell, 1995. <a href=\"https://doi.org/10.1002/cne.903600402\">https://doi.org/10.1002/cne.903600402</a>."},"status":"public","year":"1995","language":[{"iso":"eng"}],"publication_status":"published","publist_id":"4410","day":"02","date_created":"2018-12-11T11:57:59Z","page":"555 - 570","author":[{"first_name":"Hitoshi","full_name":"Ohishi, Hitoshi","last_name":"Ohishi"},{"last_name":"Akazawa","first_name":"Chihiro","full_name":"Akazawa, Chihiro"},{"full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi","last_name":"Shigemoto","orcid":"0000-0001-8761-9444"},{"last_name":"Nakanishi","full_name":"Nakanishi, Shigetada","first_name":"Shigetada"},{"last_name":"Mizuno","full_name":"Mizuno, Noboru","first_name":"Noboru"}],"extern":"1","quality_controlled":"1","month":"10","publication":"Journal of Comparative Neurology","doi":"10.1002/cne.903600402","date_updated":"2022-06-29T13:08:19Z","publisher":"Wiley-Blackwell","article_processing_charge":"No","external_id":{"pmid":["8801249"]},"oa_version":"None","article_type":"original","volume":360,"date_published":"1995-10-02T00:00:00Z","type":"journal_article"},{"article_processing_charge":"No","publication":"Brain Research","date_updated":"2022-06-29T08:32:01Z","doi":"10.1016/0006-8993(95)00022-I","publisher":"Elsevier","month":"03","extern":"1","quality_controlled":"1","volume":674,"type":"journal_article","date_published":"1995-03-20T00:00:00Z","external_id":{"pmid":["7796113"]},"article_type":"original","oa_version":"None","language":[{"iso":"eng"}],"year":"1995","author":[{"last_name":"Ding","first_name":"Yu","full_name":"Ding, Yu"},{"first_name":"Masahiko","full_name":"Takada, Masahiko","last_name":"Takada"},{"orcid":"0000-0001-8761-9444","last_name":"Shigemoto","full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"},{"first_name":"Noboru","full_name":"Mizuno, Noboru","last_name":"Mizuno"}],"page":"336 - 340","date_created":"2018-12-11T11:58:22Z","publication_status":"published","publist_id":"4341","day":"20","abstract":[{"text":"By using substance P receptor (SPR) immunofluorescence histochemistry combined with fluorescent retrograde labeling, SPR-like immunoreactive (SPR-LI) neurons sending their axons to the lateral parabrachial region were observed in the lumbar spinal cord of the rat. After injection of Fluoro-Gold into the lateral parabrachial region, retrogradely labeled neurons with SPR-LI were seen frequently in lamina I and the lateral spinal nucleus, and occasionally in laminae IV and V, with a predominantly contralateral distribution. Some of these neurons, especially those in lamina I, may convey nociceptive information to the lateral parabrachial region.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"2556","title":"Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat","pmid":1,"acknowledgement":"The authors are grateful for photographic help of Mr. Akira Uesugi. This work was supported in part by Grants-in-Aid for Special Research on Priority Areas 05267104, Scientific Research (B) 05454658, and Scientific Research (C) 06680735 from the Ministry of Education, Science and Culture of Japan.","status":"public","main_file_link":[{"url":"sciencedirect.com/science/article/pii/000689939500022I?via%3Dihub"}],"intvolume":"       674","citation":{"chicago":"Ding, Yu, Masahiko Takada, Ryuichi Shigemoto, and Noboru Mizuno. “Spinoparabrachial Tract Neurons Showing Substance P Receptor-like Immunoreactivity in the Lumbar Spinal Cord of the Rat.” <i>Brain Research</i>. Elsevier, 1995. <a href=\"https://doi.org/10.1016/0006-8993(95)00022-I\">https://doi.org/10.1016/0006-8993(95)00022-I</a>.","ama":"Ding Y, Takada M, Shigemoto R, Mizuno N. Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat. <i>Brain Research</i>. 1995;674(2):336-340. doi:<a href=\"https://doi.org/10.1016/0006-8993(95)00022-I\">10.1016/0006-8993(95)00022-I</a>","mla":"Ding, Yu, et al. “Spinoparabrachial Tract Neurons Showing Substance P Receptor-like Immunoreactivity in the Lumbar Spinal Cord of the Rat.” <i>Brain Research</i>, vol. 674, no. 2, Elsevier, 1995, pp. 336–40, doi:<a href=\"https://doi.org/10.1016/0006-8993(95)00022-I\">10.1016/0006-8993(95)00022-I</a>.","short":"Y. Ding, M. Takada, R. Shigemoto, N. Mizuno, Brain Research 674 (1995) 336–340.","ieee":"Y. Ding, M. Takada, R. Shigemoto, and N. Mizuno, “Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat,” <i>Brain Research</i>, vol. 674, no. 2. Elsevier, pp. 336–340, 1995.","ista":"Ding Y, Takada M, Shigemoto R, Mizuno N. 1995. Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat. Brain Research. 674(2), 336–340.","apa":"Ding, Y., Takada, M., Shigemoto, R., &#38; Mizuno, N. (1995). Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity in the lumbar spinal cord of the rat. <i>Brain Research</i>. Elsevier. <a href=\"https://doi.org/10.1016/0006-8993(95)00022-I\">https://doi.org/10.1016/0006-8993(95)00022-I</a>"},"scopus_import":"1","issue":"2","publication_identifier":{"issn":["0006-8993"]}},{"pmid":1,"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"Brain areas involved in the genesis and control of daily rhythms receive a prominent neural input that contains the neurotransmitter substance P (SP), a peptide putatively involved in the synchronization of circadian rhythms by environmental light. We investigated the localization of receptors to SP in the suprachiasmatic nucleus of the hypothalamus (SCN) and in the intergeniculate leaflet of the thalamus (IGL) of the rat and hamster using in situ hybridization histochemistry and immunohistochemistry. Consistently with that previously described in the rat, a neuronal population distributed along the lateral margin and at the dorso-latero-caudal aspect of the hamster SCN expresses moderately the mRNA encoding the SP receptor. In both rat and hamster, immunohistochemical data confirm the previous finding and reveal an almost complete absence of SP receptors in the ventral part of the SCN, which receives a direct projection from the retina. In the IGL of both species, numerous neurons prominently express the mRNA encoding the SP receptor. The immunostaining shows a high density of SP receptors on perikarya and dendrites throughout the nucleus. A dense staining is also observed on individual cells and processes bordering the lumen of blood vessels in the SCN and IGL."}],"title":"Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents","_id":"2558","intvolume":"       318","citation":{"short":"G. Mick, R. Shigemoto, K. Kitahama, Comptes Rendus de l’Academie Des Sciences - Series III 318 (1995) 209–217.","ieee":"G. Mick, R. Shigemoto, and K. Kitahama, “Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents,” <i>Comptes Rendus de l’Academie des Sciences - Series III</i>, vol. 318, no. 2. Gauthier Villars Editeur, pp. 209–217, 1995.","apa":"Mick, G., Shigemoto, R., &#38; Kitahama, K. (1995). Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents. <i>Comptes Rendus de l’Academie Des Sciences - Series III</i>. Gauthier Villars Editeur.","ista":"Mick G, Shigemoto R, Kitahama K. 1995. Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents. Comptes Rendus de l’Academie des Sciences - Series III. 318(2), 209–217.","chicago":"Mick, Gérard, Ryuichi Shigemoto, and Kunio Kitahama. “Localization of Substance P Receptors in Central Neural Structures Controlling Daily Rhythms in Nocturnal Rodents.” <i>Comptes Rendus de l’Academie Des Sciences - Series III</i>. Gauthier Villars Editeur, 1995.","mla":"Mick, Gérard, et al. “Localization of Substance P Receptors in Central Neural Structures Controlling Daily Rhythms in Nocturnal Rodents.” <i>Comptes Rendus de l’Academie Des Sciences - Series III</i>, vol. 318, no. 2, Gauthier Villars Editeur, 1995, pp. 209–17.","ama":"Mick G, Shigemoto R, Kitahama K. Localization of substance P receptors in central neural structures controlling daily rhythms in nocturnal rodents. <i>Comptes Rendus de l’Academie des Sciences - Series III</i>. 1995;318(2):209-217."},"main_file_link":[{"url":"https://pubmed.ncbi.nlm.nih.gov/7757814/"}],"status":"public","scopus_import":"1","publication_identifier":{"issn":["0764-4469"]},"issue":"2","month":"02","quality_controlled":"1","extern":"1","article_processing_charge":"No","publisher":"Gauthier Villars Editeur","date_updated":"2022-06-29T08:18:48Z","publication":"Comptes Rendus de l'Academie des Sciences - Series III","oa_version":"None","article_type":"original","external_id":{"pmid":["7757814 "]},"type":"journal_article","date_published":"1995-02-01T00:00:00Z","volume":318,"year":"1995","language":[{"iso":"eng"}],"date_created":"2018-12-11T11:58:23Z","day":"01","publist_id":"4340","publication_status":"published","author":[{"last_name":"Mick","first_name":"Gérard","full_name":"Mick, Gérard"},{"full_name":"Shigemoto, Ryuichi","first_name":"Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0001-8761-9444","last_name":"Shigemoto"},{"first_name":"Kunio","full_name":"Kitahama, Kunio","last_name":"Kitahama"}],"page":"209 - 217"},{"publication_identifier":{"issn":["0092-8674"]},"issue":"5","acknowledgement":"We thank Drs. N. Mizuno, M. Iso, M. Tachibana, A. Kaneko, M. Tessier-Lavigne, and T. Hensch for useful advice and A. Uesugi for photographic assistance. This work is supported by grants in aid for specially promoted research, for scientific research on priority areas, and for scientific research (A) from the Ministry of Education, Science, and Culture in Japan and by grants from the Ministry of Health and Welfare of Japan, the Sankyo Foundation, and the Senri Life Science Foundation.","pmid":1,"title":"Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene","_id":"2559","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","abstract":[{"lang":"eng","text":"Taking advantage of the restricted expression of metabotropic glutamate receptor subtype 6 (mGIuR6) in retinal ON bipolar cells, we generated knockout mice lacking mGIuR6 expression. The homozygous mutant mice showed a loss of ON responses but unchanged OFF responses to light. The mutant mice displayed no obvious changes in retinal cell organization nor in the projection of optic fibers to the brain. Furthermore, the mGIuR6-deficient mice showed visual behavioral responses to light stimulation as examined by shuttle box avoidance behavior experiments using light exposure as a conditioned stimulus. The results demonstrate that mGIuR6 is essential in synaptic transmission to the ON bipolar cell and that the OFF response provides an important means for transmitting visual information."}],"intvolume":"        80","citation":{"ama":"Masu M, Iwakabe H, Tagawa Y, et al. Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene. <i>Cell</i>. 1995;80(5):757-765. doi:<a href=\"https://doi.org/10.1016/0092-8674(95)90354-2\">10.1016/0092-8674(95)90354-2</a>","mla":"Masu, Masayuki, et al. “Specific Deficit of the ON Response in Visual Transmission by Targeted Disruption of the MGIuR6 Gene.” <i>Cell</i>, vol. 80, no. 5, Cell Press, 1995, pp. 757–65, doi:<a href=\"https://doi.org/10.1016/0092-8674(95)90354-2\">10.1016/0092-8674(95)90354-2</a>.","chicago":"Masu, Masayuki, Hideki Iwakabe, Yoshiaki Tagawa, Tomomitsu Miyoshi, Masayuki Yamashita, Yutaka Fukuda, Hitoshi Sasaki, et al. “Specific Deficit of the ON Response in Visual Transmission by Targeted Disruption of the MGIuR6 Gene.” <i>Cell</i>. Cell Press, 1995. <a href=\"https://doi.org/10.1016/0092-8674(95)90354-2\">https://doi.org/10.1016/0092-8674(95)90354-2</a>.","ista":"Masu M, Iwakabe H, Tagawa Y, Miyoshi T, Yamashita M, Fukuda Y, Sasaki H, Hiroi K, Nakamura Y, Shigemoto R, Takada M, Nakamura K, Nakao K, Katsuki M, Nakanishi S. 1995. Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene. Cell. 80(5), 757–765.","apa":"Masu, M., Iwakabe, H., Tagawa, Y., Miyoshi, T., Yamashita, M., Fukuda, Y., … Nakanishi, S. (1995). Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene. <i>Cell</i>. Cell Press. <a href=\"https://doi.org/10.1016/0092-8674(95)90354-2\">https://doi.org/10.1016/0092-8674(95)90354-2</a>","short":"M. Masu, H. Iwakabe, Y. Tagawa, T. Miyoshi, M. Yamashita, Y. Fukuda, H. Sasaki, K. Hiroi, Y. Nakamura, R. Shigemoto, M. Takada, K. Nakamura, K. Nakao, M. Katsuki, S. Nakanishi, Cell 80 (1995) 757–765.","ieee":"M. Masu <i>et al.</i>, “Specific deficit of the ON response in visual transmission by targeted disruption of the mGIuR6 gene,” <i>Cell</i>, vol. 80, no. 5. Cell Press, pp. 757–765, 1995."},"main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/0092867495903542","open_access":"1"}],"status":"public","language":[{"iso":"eng"}],"year":"1995","day":"10","publist_id":"4339","publication_status":"published","date_created":"2018-12-11T11:58:23Z","page":"757 - 765","author":[{"last_name":"Masu","full_name":"Masu, Masayuki","first_name":"Masayuki"},{"last_name":"Iwakabe","first_name":"Hideki","full_name":"Iwakabe, Hideki"},{"last_name":"Tagawa","full_name":"Tagawa, Yoshiaki","first_name":"Yoshiaki"},{"first_name":"Tomomitsu","full_name":"Miyoshi, Tomomitsu","last_name":"Miyoshi"},{"full_name":"Yamashita, Masayuki","first_name":"Masayuki","last_name":"Yamashita"},{"full_name":"Fukuda, Yutaka","first_name":"Yutaka","last_name":"Fukuda"},{"last_name":"Sasaki","full_name":"Sasaki, Hitoshi","first_name":"Hitoshi"},{"full_name":"Hiroi, Kano","first_name":"Kano","last_name":"Hiroi"},{"last_name":"Nakamura","first_name":"Yasuhisa","full_name":"Nakamura, Yasuhisa"},{"full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi","last_name":"Shigemoto","orcid":"0000-0001-8761-9444"},{"full_name":"Takada, Masahiko","first_name":"Masahiko","last_name":"Takada"},{"last_name":"Nakamura","first_name":"Kenji","full_name":"Nakamura, Kenji"},{"first_name":"Kazuki","full_name":"Nakao, Kazuki","last_name":"Nakao"},{"last_name":"Katsuki","first_name":"Motoya","full_name":"Katsuki, Motoya"},{"last_name":"Nakanishi","full_name":"Nakanishi, Shigetada","first_name":"Shigetada"}],"quality_controlled":"1","oa":1,"extern":"1","month":"02","publisher":"Cell Press","doi":"10.1016/0092-8674(95)90354-2","date_updated":"2022-06-28T13:27:50Z","publication":"Cell","article_processing_charge":"No","oa_version":"Published Version","external_id":{"pmid":["7889569"]},"article_type":"original","type":"journal_article","date_published":"1995-02-10T00:00:00Z","volume":80},{"status":"public","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/0304394095119915?via%3Dihub"}],"citation":{"mla":"Lü, Yan, et al. “Expression of C-Fos Protein in Substance P Receptor-like Immunoreactive Neurons in Response to Noxious Stimuli on the Urinary Bladder: An Observation in the Lumbosacral Cord Segments of the Rat.” <i>Neuroscience Letters</i>, vol. 198, no. 2, Elsevier, 1995, pp. 139–42, doi:<a href=\"https://doi.org/10.1016/0304-3940(95)11991-5\">10.1016/0304-3940(95)11991-5</a>.","ama":"Lü Y, Jin S, Xu T, et al. Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat. <i>Neuroscience Letters</i>. 1995;198(2):139-142. doi:<a href=\"https://doi.org/10.1016/0304-3940(95)11991-5\">10.1016/0304-3940(95)11991-5</a>","chicago":"Lü, Yan, Shan Jin, Tian Xu, Bing Qin, Ji Li, Yu Ding, Ryuichi Shigemoto, and Noboru Mizuno. “Expression of C-Fos Protein in Substance P Receptor-like Immunoreactive Neurons in Response to Noxious Stimuli on the Urinary Bladder: An Observation in the Lumbosacral Cord Segments of the Rat.” <i>Neuroscience Letters</i>. Elsevier, 1995. <a href=\"https://doi.org/10.1016/0304-3940(95)11991-5\">https://doi.org/10.1016/0304-3940(95)11991-5</a>.","apa":"Lü, Y., Jin, S., Xu, T., Qin, B., Li, J., Ding, Y., … Mizuno, N. (1995). Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat. <i>Neuroscience Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3940(95)11991-5\">https://doi.org/10.1016/0304-3940(95)11991-5</a>","ista":"Lü Y, Jin S, Xu T, Qin B, Li J, Ding Y, Shigemoto R, Mizuno N. 1995. Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat. Neuroscience Letters. 198(2), 139–142.","ieee":"Y. Lü <i>et al.</i>, “Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat,” <i>Neuroscience Letters</i>, vol. 198, no. 2. Elsevier, pp. 139–142, 1995.","short":"Y. Lü, S. Jin, T. Xu, B. Qin, J. Li, Y. Ding, R. Shigemoto, N. Mizuno, Neuroscience Letters 198 (1995) 139–142."},"intvolume":"       198","abstract":[{"text":"Chemical irritation of the urinary bladder with formalin in the rat induced c-fos protein-like immunoreactivity in more than 80% of substance P receptor-like immunoreactive (SPR-LI) neurons of the dorsal commissural nucleus, sacral parasympathetic nucleus and lamina I in the 6th lumbar and 1st sacral cord segments. These neurons with SPR-LI may receive noxious information from the urinary bladder through the primary afferent fibers with substance P.","lang":"eng"}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"2560","title":"Expression of c-fos protein in substance P receptor-like immunoreactive neurons in response to noxious stimuli on the urinary bladder: an observation in the lumbosacral cord segments of the rat","pmid":1,"issue":"2","publication_identifier":{"issn":["0304-3940"]},"volume":198,"type":"journal_article","date_published":"1995-09-29T00:00:00Z","external_id":{"pmid":["8592640"]},"oa_version":"None","article_type":"original","article_processing_charge":"No","publication":"Neuroscience Letters","doi":"10.1016/0304-3940(95)11991-5","publisher":"Elsevier","date_updated":"2022-06-28T12:54:14Z","month":"09","extern":"1","quality_controlled":"1","author":[{"last_name":"Lü","full_name":"Lü, Yan","first_name":"Yan"},{"last_name":"Jin","first_name":"Shan","full_name":"Jin, Shan"},{"last_name":"Xu","full_name":"Xu, Tian","first_name":"Tian"},{"full_name":"Qin, Bing","first_name":"Bing","last_name":"Qin"},{"full_name":"Li, Ji","first_name":"Ji","last_name":"Li"},{"last_name":"Ding","first_name":"Yu","full_name":"Ding, Yu"},{"full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi","last_name":"Shigemoto","orcid":"0000-0001-8761-9444"},{"full_name":"Mizuno, Noboru","first_name":"Noboru","last_name":"Mizuno"}],"page":"139 - 142","date_created":"2018-12-11T11:58:23Z","publication_status":"published","publist_id":"4338","day":"29","language":[{"iso":"eng"}],"year":"1995"},{"extern":"1","quality_controlled":"1","month":"12","publication":"Neuroscience Letters","doi":"10.1016/0304-3940(95)12207-9","publisher":"Elsevier","date_updated":"2022-06-28T12:44:57Z","article_processing_charge":"No","external_id":{"pmid":["8787837"]},"oa_version":"None","article_type":"original","volume":202,"date_published":"1995-12-01T00:00:00Z","type":"journal_article","language":[{"iso":"eng"}],"year":"1995","publication_status":"published","publist_id":"4337","day":"01","date_created":"2018-12-11T11:58:24Z","page":"85 - 88","author":[{"full_name":"Ohishi, Hitoshi","first_name":"Hitoshi","last_name":"Ohishi"},{"full_name":"Nomura, Sakashi","first_name":"Sakashi","last_name":"Nomura"},{"full_name":"Ding, Yu","first_name":"Yu","last_name":"Ding"},{"orcid":"0000-0001-8761-9444","last_name":"Shigemoto","full_name":"Shigemoto, Ryuichi","id":"499F3ABC-F248-11E8-B48F-1D18A9856A87","first_name":"Ryuichi"},{"full_name":"Wada, Eiki","first_name":"Eiki","last_name":"Wada"},{"full_name":"Kinoshita, Ayae","first_name":"Ayae","last_name":"Kinoshita"},{"first_name":"Jin","full_name":"Li, Jin","last_name":"Li"},{"first_name":"Akio","full_name":"Neki, Akio","last_name":"Neki"},{"full_name":"Nakanishi, Shigetada","first_name":"Shigetada","last_name":"Nakanishi"},{"last_name":"Mizuno","full_name":"Mizuno, Noboru","first_name":"Noboru"}],"acknowledgement":"We are grateful to Mr. Akira Uesugi for photographic help.","pmid":1,"_id":"2561","title":"Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat","abstract":[{"lang":"eng","text":"An antibody which recognizes specifically a metabotropic glutamate receptor, mGluR7, was produced by using a trpE fusion protein containing a C-terminal sequence of rat mGluR7. Neuropil in laminae I and II of the dorsal horn of the rat, as well as many neuronal cell bodies in the dorsal root ganglion, showed mGluR7-like immunoreactivity; the immunoreactivity in neuropil was seen in axon terminals, which were filled with round synaptic vesicles and constituted axodendritic and axosomatic asymmetric synapses. The mGluR7-like immunoreactivity in laminae I and II in the dorsal horn was reduced after dorsal rhizotomy. The results indicate that some axon terminals of the primary afferent fibers to laminae I and II of the dorsal horn are provided with mGluR7."}],"user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","main_file_link":[{"url":"https://www.sciencedirect.com/science/article/pii/0304394095122079?via%3Dihub"}],"citation":{"mla":"Ohishi, Hitoshi, et al. “Presynaptic Localization of a Metabotropic Glutamate Receptor, MGluR7, in the Primary Afferent Neurons: An Immunohistochemical Study in the Rat.” <i>Neuroscience Letters</i>, vol. 202, no. 1–2, Elsevier, 1995, pp. 85–88, doi:<a href=\"https://doi.org/10.1016/0304-3940(95)12207-9\">10.1016/0304-3940(95)12207-9</a>.","ama":"Ohishi H, Nomura S, Ding Y, et al. Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat. <i>Neuroscience Letters</i>. 1995;202(1-2):85-88. doi:<a href=\"https://doi.org/10.1016/0304-3940(95)12207-9\">10.1016/0304-3940(95)12207-9</a>","chicago":"Ohishi, Hitoshi, Sakashi Nomura, Yu Ding, Ryuichi Shigemoto, Eiki Wada, Ayae Kinoshita, Jin Li, Akio Neki, Shigetada Nakanishi, and Noboru Mizuno. “Presynaptic Localization of a Metabotropic Glutamate Receptor, MGluR7, in the Primary Afferent Neurons: An Immunohistochemical Study in the Rat.” <i>Neuroscience Letters</i>. Elsevier, 1995. <a href=\"https://doi.org/10.1016/0304-3940(95)12207-9\">https://doi.org/10.1016/0304-3940(95)12207-9</a>.","apa":"Ohishi, H., Nomura, S., Ding, Y., Shigemoto, R., Wada, E., Kinoshita, A., … Mizuno, N. (1995). Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat. <i>Neuroscience Letters</i>. Elsevier. <a href=\"https://doi.org/10.1016/0304-3940(95)12207-9\">https://doi.org/10.1016/0304-3940(95)12207-9</a>","ista":"Ohishi H, Nomura S, Ding Y, Shigemoto R, Wada E, Kinoshita A, Li J, Neki A, Nakanishi S, Mizuno N. 1995. Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat. Neuroscience Letters. 202(1–2), 85–88.","ieee":"H. Ohishi <i>et al.</i>, “Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study in the rat,” <i>Neuroscience Letters</i>, vol. 202, no. 1–2. Elsevier, pp. 85–88, 1995.","short":"H. Ohishi, S. Nomura, Y. Ding, R. Shigemoto, E. Wada, A. Kinoshita, J. Li, A. Neki, S. Nakanishi, N. Mizuno, Neuroscience Letters 202 (1995) 85–88."},"intvolume":"       202","status":"public","publication_identifier":{"issn":["0304-3940"]},"issue":"1-2"}]