---
_id: '4298'
article_processing_charge: No
article_type: original
author:
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
citation:
  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>
  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>
  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>.
  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.
  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.
date_created: 2018-12-11T12:08:07Z
date_published: 1995-12-01T00:00:00Z
date_updated: 2022-06-28T07:47:30Z
day: '01'
doi: 10.1111/j.1558-5646.1995.tb04431.x
extern: '1'
intvolume: '        49'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1111/j.1558-5646.1995.tb04431.x
month: '12'
oa: 1
oa_version: Published Version
page: 1038 - 1045
publication: Evolution
publication_identifier:
  issn:
  - 1558-5646
publication_status: published
publisher: Wiley
publist_id: '1773'
quality_controlled: '1'
status: public
title: Appendix to "A simulation study of multilocus clines" by S J E Baird
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 49
year: '1995'
...
---
_id: '4428'
abstract:
- lang: eng
  text: "Hybrid systems are real-time systems that react to both discrete and continuous
    activities (such as analog signals, time, temperature, and speed). Typical examples
    of hybrid systems are embedded systems, timing-based communication protocols,
    and digital circuits at the transistor level. Due to the rapid development of
    microprocessor technology, hybrid systems directly control much of what we depend
    on in our daily lives. Consequently, the formal specification and verification
    of hybrid systems has become an active area of research. This dissertation presents
    the first general framework for the formal specification and verification of hybrid
    systems, as well as the first hybrid-system analysis tool--HyTech. The framework
    consists of a graphical finite-state-machine-like language for modeling hybrid
    systems, a temporal logic for modeling the requirements of hybrid systems, and
    a computer procedure that verifies modeled hybrid systems against modeled requirements.
    The tool HyTech is the implementation of the framework using C++ and Mathematica.\r\n\r\nMore
    specifically, our hybrid-system modeling language, Hybrid Automata, is an extension
    of timed automata with discrete and continuous variables whose dynamics are governed
    by differential equations. Our requirement modeling language, ICTL, is a branching-time
    temporal logic, and is an extension of TCTL with stop-watch variables. Our verification
    procedure is a symbolic model-checking procedure that verifies linear hybrid automata
    against ICTL formulas. To make HyTech more efficient and effective, we use model-checking
    strategies and abstract operators that can expedite the verification process.
    To enable HyTech to verify nonlinear hybrid automata, we introduce two translations
    from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech
    to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present
    the application of HyTech to three nontrivial hybrid systems taken from the literature."
article_processing_charge: No
author:
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
citation:
  ama: Ho P. Automatic analysis of hybrid systems. 1995:1-188.
  apa: Ho, P. (1995). <i>Automatic analysis of hybrid systems</i>. Cornell University.
  chicago: Ho, Pei. “Automatic Analysis of Hybrid Systems.” Cornell University, 1995.
  ieee: P. Ho, “Automatic analysis of hybrid systems,” Cornell University, 1995.
  ista: Ho P. 1995. Automatic analysis of hybrid systems. Cornell University.
  mla: Ho, Pei. <i>Automatic Analysis of Hybrid Systems</i>. Cornell University, 1995,
    pp. 1–188.
  short: P. Ho, Automatic Analysis of Hybrid Systems, Cornell University, 1995.
date_created: 2018-12-11T12:08:48Z
date_published: 1995-08-01T00:00:00Z
date_updated: 2022-06-28T07:30:34Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://hdl.handle.net/1813/7193
month: '08'
oa: 1
oa_version: Published Version
page: 1 - 188
publication_status: published
publisher: Cornell University
publist_id: '304'
status: public
supervisor:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
title: Automatic analysis of hybrid systems
type: dissertation
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...
---
_id: '4447'
abstract:
- lang: eng
  text: This paper is addressed to potential users of HyTech, the Cornell Hybrid Technology
    Tool, an automatic tool for analyzing hybrid systems. We review the formal technologies
    that have been incorporated into HyTech, and we illustrate the use of HyTech with
    three nontrivial case studies.
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
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>'
  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>'
  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>.'
  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.'
  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.'
  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>.'
  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.
conference:
  end_date: 1955-10-25
  location: ' New Brunswick, NJ, United States of America'
  name: Hybrid Systems III
  start_date: 1995-10-22
date_created: 2018-12-11T12:08:54Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T11:24:15Z
day: '01'
doi: 10.1007/3-540-60472-3_14
editor:
- first_name: Antsaklis
  full_name: Panos, Antsaklis
  last_name: Panos
- first_name: Wolf
  full_name: Kohn, Wolf
  last_name: Kohn
- first_name: Anil
  full_name: Nerode, Anil
  last_name: Nerode
- first_name: Shankar
  full_name: Sastry, Shankar
  last_name: Sastry
extern: '1'
intvolume: '       999'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60472-3_14
month: '01'
oa_version: None
page: 265 - 293
publication: 4th International Hybrid Systems Workshop
publication_identifier:
  isbn:
  - '9783540683346'
publication_status: published
publisher: Springer
publist_id: '281'
quality_controlled: '1'
series_title: LNCS
status: public
title: 'HyTech: The Cornell Hybrid Technology Tool'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 999
year: '1995'
...
---
_id: '4448'
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.
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.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
citation:
  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>'
  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>'
  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>.
  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.
  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.
  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>.
  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.
conference:
  end_date: 1994-10-30
  location: Ithaca, NY, United States of America
  name: Hybrid Systems II
  start_date: 1994-10-28
date_created: 2018-12-11T12:08:54Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T11:48:59Z
day: '01'
doi: 10.1007/3-540-60472-3_13
editor:
- first_name: Antsaklis
  full_name: Panos, Antsaklis
  last_name: Panos
- first_name: Wolf
  full_name: Kohn, Wolf
  last_name: Kohn
- first_name: Anil
  full_name: Nerode, Anil
  last_name: Nerode
- first_name: Shankar
  full_name: Sastry, Shankar
  last_name: Sastry
extern: '1'
intvolume: '       999'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60472-3_13
month: '01'
oa_version: None
page: 252 - 264
publication: 3rd International Hybrid Systems Workshop
publication_identifier:
  isbn:
  - '9783540604723'
publication_status: published
publisher: Springer
publist_id: '282'
quality_controlled: '1'
status: public
title: A note on abstract-interpretation strategies for hybrid automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 999
year: '1995'
...
---
_id: '4450'
abstract:
- lang: eng
  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."
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  short: T.A. Henzinger, P. Ho, in:, 7th International Conference on Computer Aided
    Verification, Springer, 1995, pp. 225–238.
conference:
  end_date: 1995-07-05
  location: Liege, Belgium
  name: 'CAV: Computer Aided Verification'
  start_date: 1995-07-03
date_created: 2018-12-11T12:08:55Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T09:48:52Z
day: '01'
doi: 10.1007/3-540-60045-0_53
extern: '1'
intvolume: '       939'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60045-0_53
month: '01'
oa_version: None
page: 225 - 238
publication: 7th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540494133'
publication_status: published
publisher: Springer
publist_id: '280'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Algorithmic analysis of nonlinear hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 939
year: '1995'
...
---
_id: '4497'
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."
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
- first_name: Howard
  full_name: Wong Toi, Howard
  last_name: Wong Toi
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  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.
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
date_created: 2018-12-11T12:09:09Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T09:00:05Z
day: '01'
doi: 10.1007/3-540-60630-0_3
extern: '1'
intvolume: '      1019'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60630-0_3
month: '01'
oa_version: None
page: 41 - 71
publication: 1st International Workshop on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  isbn:
  - '9783540606307'
publication_status: published
publisher: Springer
publist_id: '230'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A user guide to HyTech
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1019
year: '1995'
...
---
_id: '4498'
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
article_processing_charge: No
author:
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Peter
  full_name: Kopke, Peter
  last_name: Kopke
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  short: M.H. Henzinger, T.A. Henzinger, P. Kopke, in:, Proceedings of IEEE 36th Annual
    Foundations of Computer Science, IEEE, 1995, pp. 453–462.
conference:
  end_date: 1995-10-25
  location: Milwaukee, WI, United States of America
  name: 'FOCS: Foundations of Computer Science'
  start_date: 1995-10-23
date_created: 2018-12-11T12:09:10Z
date_published: 1995-11-01T00:00:00Z
date_updated: 2023-02-09T08:43:48Z
day: '01'
doi: 10.1109/SFCS.1995.492576
extern: '1'
language:
- iso: eng
month: '11'
oa_version: None
page: 453 - 462
publication: Proceedings of IEEE 36th Annual Foundations of Computer Science
publication_identifier:
  isbn:
  - '0818671831'
  issn:
  - 0272-5428
publication_status: published
publisher: IEEE
publist_id: '231'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing simulations on finite and infinite graphs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1995'
...
---
_id: '4499'
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
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
- first_name: Howard
  full_name: Wong Toi, Howard
  last_name: Wong Toi
citation:
  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>'
  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>'
  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>.'
  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.'
  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.'
  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>.'
  short: T.A. Henzinger, P. Ho, H. Wong Toi, in:, Proceedings 16th IEEE Real-Time
    Systems Symposium, IEEE, 1995, pp. 56–65.
conference:
  end_date: 1995-12-07
  location: Pisa, Italy
  name: 'RTSS: Real-Time Systems Symposium'
  start_date: 1995-12-05
date_created: 2018-12-11T12:09:10Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-10T09:33:19Z
day: '01'
doi: '10.1109/REAL.1995.495196 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/495196
month: '01'
oa_version: None
page: 56 - 65
publication: Proceedings 16th IEEE Real-Time Systems Symposium
publication_identifier:
  isbn:
  - '0818673370'
publication_status: published
publisher: IEEE
publist_id: '232'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'HyTech: The next generation'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...
---
_id: '4500'
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.'
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."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Peter
  full_name: Kopke, Peter
  last_name: Kopke
- first_name: Howard
  full_name: Wong Toi, Howard
  last_name: Wong Toi
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  short: T.A. Henzinger, P. Kopke, H. Wong Toi, in:, 22nd International Colloquium
    on Automata, Languages and Programming , Springer, 1995, pp. 417–428.
conference:
  end_date: 1995-07-14
  location: Szeged, Hungary
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 1995-07-10
date_created: 2018-12-11T12:09:10Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:58:31Z
day: '01'
doi: 10.1007/3-540-60084-1_93
extern: '1'
intvolume: '       944'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60084-1_93
month: '01'
oa_version: None
page: 417 - 428
publication: '22nd International Colloquium on Automata, Languages and Programming '
publication_identifier:
  isbn:
  - '9783540600848'
publication_status: published
publisher: Springer
publist_id: '229'
quality_controlled: '1'
status: public
title: The expressive power of clocks
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 944
year: '1995'
...
---
_id: '4502'
abstract:
- lang: eng
  text: "Hybrid automata model systems with both digital and analog components, such
    as embedded control programs. Many verification tasks for such programs can be
    expressed as reachability problems for hybrid automata. By improving on previous
    decidability and undecidability results, we identify 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."
acknowledgement: "We thank Howard Wong-Toi for a careful reading.\r\n"
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Peter
  full_name: Kopke, Peter
  last_name: Kopke
- first_name: Anuj
  full_name: Puri, Anuj
  last_name: Puri
- first_name: P.
  full_name: Varaiya, P.
  last_name: Varaiya
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  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.
conference:
  end_date: 1995-06-01
  location: Las Vegas, NV, United States of America
  name: 'STOC: Symposium on the Theory of Computing'
  start_date: 1995-05-29
date_created: 2018-12-11T12:09:11Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:40:29Z
day: '01'
doi: 10.1145/225058.225162
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://dl.acm.org/doi/10.1145/225058.225162
month: '01'
oa: 1
oa_version: Published Version
page: 373 - 382
publication: Proceedings of the 27th annual ACM symposium on Theory of computing
publication_identifier:
  isbn:
  - '9780897917186'
publication_status: published
publisher: ACM
publist_id: '228'
quality_controlled: '1'
status: public
title: What's decidable about hybrid automata?
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...
---
_id: '4518'
abstract:
- lang: eng
  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.
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"
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  short: T.A. Henzinger, in:, 22nd International Colloquium on Automata, Languages
    and Programming , Springer, 1995, pp. 324–335.
conference:
  end_date: 1995-07-14
  location: Szeged, Hungary
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 1995-07-10
date_created: 2018-12-11T12:09:16Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:21:08Z
day: '01'
doi: 10.1007/3-540-60084-1_85
extern: '1'
intvolume: '       944'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60084-1_85
month: '01'
oa_version: None
page: 324 - 335
publication: '22nd International Colloquium on Automata, Languages and Programming '
publication_identifier:
  isbn:
  - '9783540600848'
publication_status: published
publisher: Springer
publist_id: '212'
quality_controlled: '1'
status: public
title: Hybrid automata with finite bisimulations
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 944
year: '1995'
...
---
_id: '4587'
abstract:
- lang: eng
  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.
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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  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>'
  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>'
  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>.
  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.
  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.'
  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>.
  short: R. Alur, T.A. Henzinger, in:, 7th International Conference on Computer Aided
    Verification, Springer, 1995, pp. 166–179.
conference:
  end_date: 1995-07-05
  location: Liege, Belgium
  name: 'CAV: Computer Aided Verification'
  start_date: 1995-07-03
date_created: 2018-12-11T12:09:37Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-09T14:05:04Z
day: '01'
doi: 10.1007/3-540-60045-0_49
extern: '1'
intvolume: '       939'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-60045-0_49
month: '01'
oa_version: None
page: 166 - 179
publication: 7th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - 978-3-540-60045-9
publication_status: published
publisher: Springer
publist_id: '120'
quality_controlled: '1'
status: public
title: Local liveness for compositional modeling of fair reactive systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 939
year: '1995'
...
---
_id: '4613'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Costas
  full_name: Courcoubetis, Costas
  last_name: Courcoubetis
- first_name: Nicolas
  full_name: Halbwachs, Nicolas
  last_name: Halbwachs
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Pei
  full_name: Ho, Pei
  last_name: Ho
- first_name: Xavier
  full_name: Nicollin, Xavier
  last_name: Nicollin
- first_name: Alfredo
  full_name: Olivero, Alfredo
  last_name: Olivero
- first_name: Joseph
  full_name: Sifakis, Joseph
  last_name: Sifakis
- first_name: Sergio
  full_name: Yovine, Sergio
  last_name: Yovine
citation:
  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>
  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>
  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>.
  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.
  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.
  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>.
  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.
date_created: 2018-12-11T12:09:45Z
date_published: 1995-02-06T00:00:00Z
date_updated: 2022-06-09T13:40:48Z
day: '06'
doi: 10.1016/0304-3975(94)00202-T
extern: '1'
intvolume: '       138'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/030439759400202T?via%3Dihub
month: '02'
oa_version: None
page: 3 - 34
publication: Theoretical Computer Science
publication_identifier:
  issn:
  - 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '94'
quality_controlled: '1'
status: public
title: The algorithmic analysis of hybrid systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 138
year: '1995'
...
---
_id: '2465'
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.
article_processing_charge: No
author:
- first_name: David
  full_name: Morris, David
  last_name: Morris
- first_name: Jirí
  full_name: Friml, Jirí
  id: 4159519E-F248-11E8-B48F-1D18A9856A87
  last_name: Friml
  orcid: 0000-0002-8302-7596
- first_name: Eva
  full_name: Zažímalová, Eva
  last_name: Zažímalová
citation:
  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>'
  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>'
  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>.'
  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.'
  ista: 'Morris D, Friml J, Zažímalová E. 1995.Auxin transport. In: Plant Hormones:
    Biosynthesis, Signal Transduction, Action! , 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>.'
  short: 'D. Morris, J. Friml, E. Zažímalová, in:, P. Davies (Ed.), Plant Hormones:
    Biosynthesis, Signal Transduction, Action!, Kluwer, 1995, pp. 451–484.'
date_created: 2018-12-11T11:57:49Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-29T14:45:32Z
day: '01'
doi: 10.1007/978-1-4020-2686-7_21
editor:
- first_name: Peter
  full_name: Davies, Peter
  last_name: Davies
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/978-1-4020-2686-7_21
month: '01'
oa_version: None
page: 451 - 484
publication: 'Plant Hormones: Biosynthesis, Signal Transduction, Action!'
publication_identifier:
  isbn:
  - 978-1-4020-2684-3
publication_status: published
publisher: Kluwer
publist_id: '4438'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Auxin transport
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...
---
_id: '2491'
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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Hitoshi
  full_name: Ohishi, Hitoshi
  last_name: Ohishi
- first_name: Chihiro
  full_name: Akazawa, Chihiro
  last_name: Akazawa
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Shigetada
  full_name: Nakanishi, Shigetada
  last_name: Nakanishi
- first_name: Noboru
  full_name: Mizuno, Noboru
  last_name: Mizuno
citation:
  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>
  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>
  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>.
  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.
  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.
  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>.
  short: H. Ohishi, C. Akazawa, R. Shigemoto, S. Nakanishi, N. Mizuno, Journal of
    Comparative Neurology 360 (1995) 555–570.
date_created: 2018-12-11T11:57:59Z
date_published: 1995-10-02T00:00:00Z
date_updated: 2022-06-29T13:08:19Z
day: '02'
doi: 10.1002/cne.903600402
extern: '1'
external_id:
  pmid:
  - '8801249'
intvolume: '       360'
issue: '4'
language:
- iso: eng
main_file_link:
- url: https://onlinelibrary.wiley.com/doi/abs/10.1002/cne.903600402
month: '10'
oa_version: None
page: 555 - 570
pmid: 1
publication: Journal of Comparative Neurology
publication_identifier:
  issn:
  - 0021-9967
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4410'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Distributions of the mRNAs for L-2-amino-4-phosphonobutyrate-sensitive metabotropic
  glutamate receptors, mGluR4 and mGluR7, in the rat brain
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 360
year: '1995'
...
---
_id: '2556'
abstract:
- lang: eng
  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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Yu
  full_name: Ding, Yu
  last_name: Ding
- first_name: Masahiko
  full_name: Takada, Masahiko
  last_name: Takada
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Noboru
  full_name: Mizuno, Noboru
  last_name: Mizuno
citation:
  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>
  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>
  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>.
  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.
  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.
date_created: 2018-12-11T11:58:22Z
date_published: 1995-03-20T00:00:00Z
date_updated: 2022-06-29T08:32:01Z
day: '20'
doi: 10.1016/0006-8993(95)00022-I
extern: '1'
external_id:
  pmid:
  - '7796113'
intvolume: '       674'
issue: '2'
language:
- iso: eng
main_file_link:
- url: sciencedirect.com/science/article/pii/000689939500022I?via%3Dihub
month: '03'
oa_version: None
page: 336 - 340
pmid: 1
publication: Brain Research
publication_identifier:
  issn:
  - 0006-8993
publication_status: published
publisher: Elsevier
publist_id: '4341'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Spinoparabrachial tract neurons showing substance P receptor-like immunoreactivity
  in the lumbar spinal cord of the rat
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 674
year: '1995'
...
---
_id: '2558'
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.
article_processing_charge: No
article_type: original
author:
- first_name: Gérard
  full_name: Mick, Gérard
  last_name: Mick
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Kunio
  full_name: Kitahama, Kunio
  last_name: Kitahama
citation:
  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.
  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.
  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.
  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.
  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.
  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.
  short: G. Mick, R. Shigemoto, K. Kitahama, Comptes Rendus de l’Academie Des Sciences
    - Series III 318 (1995) 209–217.
date_created: 2018-12-11T11:58:23Z
date_published: 1995-02-01T00:00:00Z
date_updated: 2022-06-29T08:18:48Z
day: '01'
extern: '1'
external_id:
  pmid:
  - '7757814 '
intvolume: '       318'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://pubmed.ncbi.nlm.nih.gov/7757814/
month: '02'
oa_version: None
page: 209 - 217
pmid: 1
publication: Comptes Rendus de l'Academie des Sciences - Series III
publication_identifier:
  issn:
  - 0764-4469
publication_status: published
publisher: Gauthier Villars Editeur
publist_id: '4340'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Localization of substance P receptors in central neural structures controlling
  daily rhythms in nocturnal rodents
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 318
year: '1995'
...
---
_id: '2559'
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.
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.
article_processing_charge: No
article_type: original
author:
- first_name: Masayuki
  full_name: Masu, Masayuki
  last_name: Masu
- first_name: Hideki
  full_name: Iwakabe, Hideki
  last_name: Iwakabe
- first_name: Yoshiaki
  full_name: Tagawa, Yoshiaki
  last_name: Tagawa
- first_name: Tomomitsu
  full_name: Miyoshi, Tomomitsu
  last_name: Miyoshi
- first_name: Masayuki
  full_name: Yamashita, Masayuki
  last_name: Yamashita
- first_name: Yutaka
  full_name: Fukuda, Yutaka
  last_name: Fukuda
- first_name: Hitoshi
  full_name: Sasaki, Hitoshi
  last_name: Sasaki
- first_name: Kano
  full_name: Hiroi, Kano
  last_name: Hiroi
- first_name: Yasuhisa
  full_name: Nakamura, Yasuhisa
  last_name: Nakamura
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Masahiko
  full_name: Takada, Masahiko
  last_name: Takada
- first_name: Kenji
  full_name: Nakamura, Kenji
  last_name: Nakamura
- first_name: Kazuki
  full_name: Nakao, Kazuki
  last_name: Nakao
- first_name: Motoya
  full_name: Katsuki, Motoya
  last_name: Katsuki
- first_name: Shigetada
  full_name: Nakanishi, Shigetada
  last_name: Nakanishi
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>
  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>
  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>.
  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.
  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.
  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>.
  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.
date_created: 2018-12-11T11:58:23Z
date_published: 1995-02-10T00:00:00Z
date_updated: 2022-06-28T13:27:50Z
day: '10'
doi: 10.1016/0092-8674(95)90354-2
extern: '1'
external_id:
  pmid:
  - '7889569'
intvolume: '        80'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.sciencedirect.com/science/article/pii/0092867495903542
month: '02'
oa: 1
oa_version: Published Version
page: 757 - 765
pmid: 1
publication: Cell
publication_identifier:
  issn:
  - 0092-8674
publication_status: published
publisher: Cell Press
publist_id: '4339'
quality_controlled: '1'
status: public
title: Specific deficit of the ON response in visual transmission by targeted disruption
  of the mGIuR6 gene
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 80
year: '1995'
...
---
_id: '2560'
abstract:
- lang: eng
  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.
article_processing_charge: No
article_type: original
author:
- first_name: Yan
  full_name: Lü, Yan
  last_name: Lü
- first_name: Shan
  full_name: Jin, Shan
  last_name: Jin
- first_name: Tian
  full_name: Xu, Tian
  last_name: Xu
- first_name: Bing
  full_name: Qin, Bing
  last_name: Qin
- first_name: Ji
  full_name: Li, Ji
  last_name: Li
- first_name: Yu
  full_name: Ding, Yu
  last_name: Ding
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Noboru
  full_name: Mizuno, Noboru
  last_name: Mizuno
citation:
  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>'
  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>'
  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>.'
  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.'
  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.'
  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>.'
  short: Y. Lü, S. Jin, T. Xu, B. Qin, J. Li, Y. Ding, R. Shigemoto, N. Mizuno, Neuroscience
    Letters 198 (1995) 139–142.
date_created: 2018-12-11T11:58:23Z
date_published: 1995-09-29T00:00:00Z
date_updated: 2022-06-28T12:54:14Z
day: '29'
doi: 10.1016/0304-3940(95)11991-5
extern: '1'
external_id:
  pmid:
  - '8592640'
intvolume: '       198'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/0304394095119915?via%3Dihub
month: '09'
oa_version: None
page: 139 - 142
pmid: 1
publication: Neuroscience Letters
publication_identifier:
  issn:
  - 0304-3940
publication_status: published
publisher: Elsevier
publist_id: '4338'
quality_controlled: '1'
status: public
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'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 198
year: '1995'
...
---
_id: '2561'
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.
acknowledgement: We are grateful to Mr. Akira Uesugi for photographic help.
article_processing_charge: No
article_type: original
author:
- first_name: Hitoshi
  full_name: Ohishi, Hitoshi
  last_name: Ohishi
- first_name: Sakashi
  full_name: Nomura, Sakashi
  last_name: Nomura
- first_name: Yu
  full_name: Ding, Yu
  last_name: Ding
- first_name: Ryuichi
  full_name: Shigemoto, Ryuichi
  id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
  last_name: Shigemoto
  orcid: 0000-0001-8761-9444
- first_name: Eiki
  full_name: Wada, Eiki
  last_name: Wada
- first_name: Ayae
  full_name: Kinoshita, Ayae
  last_name: Kinoshita
- first_name: Jin
  full_name: Li, Jin
  last_name: Li
- first_name: Akio
  full_name: Neki, Akio
  last_name: Neki
- first_name: Shigetada
  full_name: Nakanishi, Shigetada
  last_name: Nakanishi
- first_name: Noboru
  full_name: Mizuno, Noboru
  last_name: Mizuno
citation:
  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>'
  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>'
  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>.'
  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.'
  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.'
  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>.'
  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.
date_created: 2018-12-11T11:58:24Z
date_published: 1995-12-01T00:00:00Z
date_updated: 2022-06-28T12:44:57Z
day: '01'
doi: 10.1016/0304-3940(95)12207-9
extern: '1'
external_id:
  pmid:
  - '8787837'
intvolume: '       202'
issue: 1-2
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/0304394095122079?via%3Dihub
month: '12'
oa_version: None
page: 85 - 88
pmid: 1
publication: Neuroscience Letters
publication_identifier:
  issn:
  - 0304-3940
publication_status: published
publisher: Elsevier
publist_id: '4337'
quality_controlled: '1'
status: public
title: 'Presynaptic localization of a metabotropic glutamate receptor, mGluR7, in
  the primary afferent neurons: An immunohistochemical study in the rat'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 202
year: '1995'
...
