---
_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. Neuroscience Letters.
1995;198(2):139-142. doi:10.1016/0304-3940(95)11991-5'
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. Neuroscience Letters. Elsevier. https://doi.org/10.1016/0304-3940(95)11991-5'
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.” Neuroscience Letters. Elsevier,
1995. https://doi.org/10.1016/0304-3940(95)11991-5.'
ieee: 'Y. Lü 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,” Neuroscience Letters,
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.” Neuroscience Letters,
vol. 198, no. 2, Elsevier, 1995, pp. 139–42, doi:10.1016/0304-3940(95)11991-5.'
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. Neuroscience Letters. 1995;202(1-2):85-88. doi:10.1016/0304-3940(95)12207-9'
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.
Neuroscience Letters. Elsevier. https://doi.org/10.1016/0304-3940(95)12207-9'
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.” Neuroscience Letters.
Elsevier, 1995. https://doi.org/10.1016/0304-3940(95)12207-9.'
ieee: 'H. Ohishi et al., “Presynaptic localization of a metabotropic glutamate
receptor, mGluR7, in the primary afferent neurons: An immunohistochemical study
in the rat,” Neuroscience Letters, 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.” Neuroscience Letters, vol. 202, no. 1–2, Elsevier, 1995, pp.
85–88, doi:10.1016/0304-3940(95)12207-9.'
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'
...
---
_id: '2563'
abstract:
- lang: eng
text: By means of substance P receptor (SPR) immunofluorescence histochemistry combined
with Fluoro-Gold fluorescent retrograde labeling, SPR-like immunoreactive neurons
in the caudal subnucleus of the spinal trigeminal nucleus of the rat were observed
to send their axons to the nucleus of Kolliker-Fuse and ventrolateral part of
the lateral parabrachial nucleus bilaterally with a clear ipsilateral dominance.
These neurons were distributed mainly in lamina I, and additionally in lamina
III.
acknowledgement: 'The authors are grateful for photographic help of Ms. Miao-Li Zhang
and 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. Trigeminoparabrachial projection neurons
showing substance P receptor-like immunoreactivity in the rat. Neuroscience
Research. 1995;23(4):415-418. doi:10.1016/0168-0102(95)00961-R
apa: Ding, Y., Takada, M., Shigemoto, R., & Mizuno, N. (1995). Trigeminoparabrachial
projection neurons showing substance P receptor-like immunoreactivity in the rat.
Neuroscience Research. Elsevier. https://doi.org/10.1016/0168-0102(95)00961-R
chicago: Ding, Yu, Masahiko Takada, Ryuichi Shigemoto, and Noboru Mizuno. “Trigeminoparabrachial
Projection Neurons Showing Substance P Receptor-like Immunoreactivity in the Rat.”
Neuroscience Research. Elsevier, 1995. https://doi.org/10.1016/0168-0102(95)00961-R.
ieee: Y. Ding, M. Takada, R. Shigemoto, and N. Mizuno, “Trigeminoparabrachial projection
neurons showing substance P receptor-like immunoreactivity in the rat,” Neuroscience
Research, vol. 23, no. 4. Elsevier, pp. 415–418, 1995.
ista: Ding Y, Takada M, Shigemoto R, Mizuno N. 1995. Trigeminoparabrachial projection
neurons showing substance P receptor-like immunoreactivity in the rat. Neuroscience
Research. 23(4), 415–418.
mla: Ding, Yu, et al. “Trigeminoparabrachial Projection Neurons Showing Substance
P Receptor-like Immunoreactivity in the Rat.” Neuroscience Research, vol.
23, no. 4, Elsevier, 1995, pp. 415–18, doi:10.1016/0168-0102(95)00961-R.
short: Y. Ding, M. Takada, R. Shigemoto, N. Mizuno, Neuroscience Research 23 (1995)
415–418.
date_created: 2018-12-11T11:58:24Z
date_published: 1995-11-01T00:00:00Z
date_updated: 2022-06-28T09:50:42Z
day: '01'
doi: 10.1016/0168-0102(95)00961-R
extern: '1'
external_id:
pmid:
- '8602281'
intvolume: ' 23'
issue: '4'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/016801029500961R?via%3Dihub
month: '11'
oa_version: None
page: 415 - 418
pmid: 1
publication: Neuroscience Research
publication_identifier:
issn:
- 0168-0102
publication_status: published
publisher: Elsevier
publist_id: '4336'
quality_controlled: '1'
status: public
title: Trigeminoparabrachial projection neurons showing substance P receptor-like
immunoreactivity in the rat
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 23
year: '1995'
...
---
_id: '2712'
abstract:
- lang: eng
text: We study the generalizations of the well-known Lieb-Thirring inequality for
the magnetic Schrödinger operator with a nonconstant magnetic field. We use stochastic
methods to prove estimates on the moments of the negative eigenvalues.
acknowledgement: Work supported by the NSF grant PHY90-19433 A02, by the Alfred Sloan
Foundation dissertation Fellowship and by the Erwin Schrödinger Institute for Mathematical
Physics in Vienna.
alternative_title:
- 'Operator Theory: Advances and Applications'
article_processing_charge: No
author:
- first_name: László
full_name: Erdös, László
id: 4DBD5372-F248-11E8-B48F-1D18A9856A87
last_name: Erdös
orcid: 0000-0001-5366-9603
citation:
ama: 'Erdös L. Magnetic Lieb-Thirring inequalities and stochastic oscillatory integrals.
In: Vol 78. Birkhäuser; 1995:127-132. doi:10.1007/978-3-0348-9092-2_13'
apa: 'Erdös, L. (1995). Magnetic Lieb-Thirring inequalities and stochastic oscillatory
integrals (Vol. 78, pp. 127–132). Presented at the International Conference on
Partial Differential Operators and Mathematical Physics, Holzhau, Germany: Birkhäuser.
https://doi.org/10.1007/978-3-0348-9092-2_13'
chicago: Erdös, László. “Magnetic Lieb-Thirring Inequalities and Stochastic Oscillatory
Integrals,” 78:127–32. Birkhäuser, 1995. https://doi.org/10.1007/978-3-0348-9092-2_13.
ieee: L. Erdös, “Magnetic Lieb-Thirring inequalities and stochastic oscillatory
integrals,” presented at the International Conference on Partial Differential
Operators and Mathematical Physics, Holzhau, Germany, 1995, vol. 78, pp. 127–132.
ista: 'Erdös L. 1995. Magnetic Lieb-Thirring inequalities and stochastic oscillatory
integrals. International Conference on Partial Differential Operators and Mathematical
Physics, Operator Theory: Advances and Applications, vol. 78, 127–132.'
mla: Erdös, László. Magnetic Lieb-Thirring Inequalities and Stochastic Oscillatory
Integrals. Vol. 78, Birkhäuser, 1995, pp. 127–32, doi:10.1007/978-3-0348-9092-2_13.
short: L. Erdös, in:, Birkhäuser, 1995, pp. 127–132.
conference:
end_date: 1995-07-09
location: Holzhau, Germany
name: International Conference on Partial Differential Operators and Mathematical
Physics
start_date: 1995-07-03
date_created: 2018-12-11T11:59:12Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-28T09:31:20Z
day: '01'
doi: 10.1007/978-3-0348-9092-2_13
extern: '1'
intvolume: ' 78'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/978-3-0348-9092-2_13
month: '01'
oa_version: None
page: 127 - 132
publication_status: published
publisher: Birkhäuser
publist_id: '4184'
quality_controlled: '1'
status: public
title: Magnetic Lieb-Thirring inequalities and stochastic oscillatory integrals
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 78
year: '1995'
...
---
_id: '2724'
abstract:
- lang: eng
text: We study the generalizations of the well-known Lieb-Thirring inequality for
the magnetic Schrödinger operator with nonconstant magnetic field. Our main result
is the naturally expected magnetic Lieb-Thirring estimate on the moments of the
negative eigenvalues for a certain class of magnetic fields (including even some
unbounded ones). We develop a localization technique in path space of the stochastic
Feynman-Kac representation of the heat kernel which effectively estimates the
oscillatory effect due to the magnetic phase factor.
article_processing_charge: No
article_type: original
author:
- first_name: László
full_name: Erdös, László
id: 4DBD5372-F248-11E8-B48F-1D18A9856A87
last_name: Erdös
orcid: 0000-0001-5366-9603
citation:
ama: Erdös L. Magnetic Lieb-Thirring inequalities. Communications in Mathematical
Physics. 1995;170(3):629-668. doi:10.1007/BF02099152
apa: Erdös, L. (1995). Magnetic Lieb-Thirring inequalities. Communications in
Mathematical Physics. Springer. https://doi.org/10.1007/BF02099152
chicago: Erdös, László. “Magnetic Lieb-Thirring Inequalities.” Communications
in Mathematical Physics. Springer, 1995. https://doi.org/10.1007/BF02099152.
ieee: L. Erdös, “Magnetic Lieb-Thirring inequalities,” Communications in Mathematical
Physics, vol. 170, no. 3. Springer, pp. 629–668, 1995.
ista: Erdös L. 1995. Magnetic Lieb-Thirring inequalities. Communications in Mathematical
Physics. 170(3), 629–668.
mla: Erdös, László. “Magnetic Lieb-Thirring Inequalities.” Communications in
Mathematical Physics, vol. 170, no. 3, Springer, 1995, pp. 629–68, doi:10.1007/BF02099152.
short: L. Erdös, Communications in Mathematical Physics 170 (1995) 629–668.
date_created: 2018-12-11T11:59:16Z
date_published: 1995-06-01T00:00:00Z
date_updated: 2022-06-28T09:19:36Z
day: '01'
doi: 10.1007/BF02099152
extern: '1'
intvolume: ' 170'
issue: '3'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/article/10.1007/BF02099152
month: '06'
oa_version: None
page: 629 - 668
publication: Communications in Mathematical Physics
publication_identifier:
issn:
- 0010-3616
publication_status: published
publisher: Springer
publist_id: '4168'
quality_controlled: '1'
status: public
title: Magnetic Lieb-Thirring inequalities
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 170
year: '1995'
...
---
_id: '1943'
abstract:
- lang: eng
text: Transhydrogenase from beef-heart mitochondria was solubilised with Triton
X-100 and purified by column chromatography. The detergent-dispersed enzyme catalysed
the reduction of acetylpyridine adenine dinucleotide (AcPdAD+) by NADH, but only
in the presence of NADP+. Experiments showed that this reaction was cyclic; NADP(H),
whilst remaining bound to the enzyme, was alternately reduced by NADH and oxidised
by AcPdAD+. A period of incubation of the enzyme with NADPH at pH 6.0 led to inhibition
of the simple transhydrogenation reaction between AcPdAD+ and NADPH. However,
after such treatment, transhydrogenase acquired the ability to catalyse the (NADPH-dependent)
reduction of AcPdAD+ by NADH. It is suggested that this is a similar cycle to
the one described above. Evidently, the binding affinity for NADP+ increases as
a consequence of the inhibition process resulting from prolonged incubation with
NADPH. The pH dependences of simple and cyclic transhydrogenation reactions are
described. Though more complex than those in Escherichia coli transhydrogenase,
they are consistent with the view [Hutton, M., Day, J.M., Bizouarn, T. and Jackson,
J.B. (1994) Eur. J. Biochem. 219, 1041–10511] that, also in the mitochondrial
enzyme, binding the release of NADP+ and NADP are accompanied by binding and release
of a proton. The enzyme was successfully reconstituted into liposomes by a cholate
dilution procedure. The proteoliposomes catalysed cyclic NADPH-dependent reduction
of AcPdAD+ by NADH only when they were tightly coupled. However, they catalysed
cyclic NADP+-dependent reduction of AcPdAD+ by NADH only when they were uncoupled
eg. by addition of carbonylcyanide-p-trifluoromethoxyphenyl hydrazone. These observations
are evidence that the proton binding and release which accompany NADP+ binding
and release, respectively, take place on the inside of the vesicle, and that they
are components of the electrogenic processes of the enzyme.
acknowledgement: 'L.A.S. is grateful to the Wellcome Trust for a Research Fellowship.
Support from the Biotechnology and Biological Sciences Research Council is also
acknowledged. We thank our colleagues. Tania Bizouarn, Mike Hutton and Nick Cotton,
for advice and valuable discussion. '
article_processing_charge: No
article_type: original
author:
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
- first_name: Baz
full_name: Jackson, Baz
last_name: Jackson
citation:
ama: Sazanov LA, Jackson B. Cyclic reactions catalysed by detergent-dispersed and
reconstituted transhydrogenase from beef heart mitochondria; implications for
the mechanism of proton translocation. Biochimica et Biophysica Acta - Bioenergetics.
1995;1231(3):304-312. doi:10.1016/0005-2728(95)00096-2
apa: Sazanov, L. A., & Jackson, B. (1995). Cyclic reactions catalysed by detergent-dispersed
and reconstituted transhydrogenase from beef heart mitochondria; implications
for the mechanism of proton translocation. Biochimica et Biophysica Acta -
Bioenergetics. Elsevier. https://doi.org/10.1016/0005-2728(95)00096-2
chicago: Sazanov, Leonid A, and Baz Jackson. “Cyclic Reactions Catalysed by Detergent-Dispersed
and Reconstituted Transhydrogenase from Beef Heart Mitochondria; Implications
for the Mechanism of Proton Translocation.” Biochimica et Biophysica Acta -
Bioenergetics. Elsevier, 1995. https://doi.org/10.1016/0005-2728(95)00096-2.
ieee: L. A. Sazanov and B. Jackson, “Cyclic reactions catalysed by detergent-dispersed
and reconstituted transhydrogenase from beef heart mitochondria; implications
for the mechanism of proton translocation,” Biochimica et Biophysica Acta -
Bioenergetics, vol. 1231, no. 3. Elsevier, pp. 304–312, 1995.
ista: Sazanov LA, Jackson B. 1995. Cyclic reactions catalysed by detergent-dispersed
and reconstituted transhydrogenase from beef heart mitochondria; implications
for the mechanism of proton translocation. Biochimica et Biophysica Acta - Bioenergetics.
1231(3), 304–312.
mla: Sazanov, Leonid A., and Baz Jackson. “Cyclic Reactions Catalysed by Detergent-Dispersed
and Reconstituted Transhydrogenase from Beef Heart Mitochondria; Implications
for the Mechanism of Proton Translocation.” Biochimica et Biophysica Acta -
Bioenergetics, vol. 1231, no. 3, Elsevier, 1995, pp. 304–12, doi:10.1016/0005-2728(95)00096-2.
short: L.A. Sazanov, B. Jackson, Biochimica et Biophysica Acta - Bioenergetics 1231
(1995) 304–312.
date_created: 2018-12-11T11:54:50Z
date_published: 1995-10-10T00:00:00Z
date_updated: 2022-06-29T15:04:47Z
day: '10'
doi: 10.1016/0005-2728(95)00096-2
extern: '1'
external_id:
pmid:
- '7578218'
intvolume: ' 1231'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/0005272895000962?via%3Dihub
month: '10'
oa: 1
oa_version: Published Version
page: 304 - 312
pmid: 1
publication: Biochimica et Biophysica Acta - Bioenergetics
publication_identifier:
issn:
- 0005-2728
publication_status: published
publisher: Elsevier
publist_id: '5142'
quality_controlled: '1'
status: public
title: Cyclic reactions catalysed by detergent-dispersed and reconstituted transhydrogenase
from beef heart mitochondria; implications for the mechanism of proton translocation
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1231
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). Automatic analysis of hybrid systems. 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. Automatic Analysis of Hybrid Systems. 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. 4th International Hybrid Systems Workshop.
Vol 999. LNCS. Springer; 1995:265-293. doi:10.1007/3-540-60472-3_14'
apa: 'Henzinger, T. A., & Ho, P. (1995). HyTech: The Cornell Hybrid Technology
Tool. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.), 4th International
Hybrid Systems Workshop (Vol. 999, pp. 265–293). New Brunswick, NJ, United
States of America: Springer. https://doi.org/10.1007/3-540-60472-3_14'
chicago: 'Henzinger, Thomas A, and Pei Ho. “HyTech: The Cornell Hybrid Technology
Tool.” In 4th International Hybrid Systems Workshop, edited by Antsaklis
Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:265–93. LNCS. Springer,
1995. https://doi.org/10.1007/3-540-60472-3_14.'
ieee: 'T. A. Henzinger and P. Ho, “HyTech: The Cornell Hybrid Technology Tool,”
in 4th International Hybrid Systems Workshop, New Brunswick, NJ, United
States of America, 1995, vol. 999, pp. 265–293.'
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.”
4th International Hybrid Systems Workshop, edited by Antsaklis Panos et
al., vol. 999, Springer, 1995, pp. 265–93, doi:10.1007/3-540-60472-3_14.'
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. 3rd International Hybrid
Systems Workshop. Vol 999. Springer; 1995:252-264. doi:10.1007/3-540-60472-3_13'
apa: 'Henzinger, T. A., & Ho, P. (1995). A note on abstract-interpretation strategies
for hybrid automata. In A. Panos, W. Kohn, A. Nerode, & S. Sastry (Eds.),
3rd International Hybrid Systems Workshop (Vol. 999, pp. 252–264). Ithaca,
NY, United States of America: Springer. https://doi.org/10.1007/3-540-60472-3_13'
chicago: Henzinger, Thomas A, and Pei Ho. “A Note on Abstract-Interpretation Strategies
for Hybrid Automata.” In 3rd International Hybrid Systems Workshop, edited
by Antsaklis Panos, Wolf Kohn, Anil Nerode, and Shankar Sastry, 999:252–64. Springer,
1995. https://doi.org/10.1007/3-540-60472-3_13.
ieee: T. A. Henzinger and P. Ho, “A note on abstract-interpretation strategies for
hybrid automata,” in 3rd International Hybrid Systems Workshop, Ithaca,
NY, United States of America, 1995, vol. 999, pp. 252–264.
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.” 3rd International Hybrid Systems Workshop, edited
by Antsaklis Panos et al., vol. 999, Springer, 1995, pp. 252–64, doi:10.1007/3-540-60472-3_13.
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:
7th International Conference on Computer Aided Verification. Vol 939. Springer;
1995:225-238. doi:10.1007/3-540-60045-0_53'
apa: 'Henzinger, T. A., & Ho, P. (1995). Algorithmic analysis of nonlinear hybrid
systems. In 7th International Conference on Computer Aided Verification
(Vol. 939, pp. 225–238). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_53'
chicago: Henzinger, Thomas A, and Pei Ho. “Algorithmic Analysis of Nonlinear Hybrid
Systems.” In 7th International Conference on Computer Aided Verification,
939:225–38. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_53.
ieee: T. A. Henzinger and P. Ho, “Algorithmic analysis of nonlinear hybrid systems,”
in 7th International Conference on Computer Aided Verification, Liege,
Belgium, 1995, vol. 939, pp. 225–238.
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.” 7th International Conference on Computer Aided Verification,
vol. 939, Springer, 1995, pp. 225–38, doi:10.1007/3-540-60045-0_53.
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: 1st International
Workshop on Tools and Algorithms for the Construction and Analysis of Systems.
Vol 1019. Springer; 1995:41-71. doi:10.1007/3-540-60630-0_3'
apa: 'Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). A user guide to HyTech.
In 1st International Workshop on Tools and Algorithms for the Construction
and Analysis of Systems (Vol. 1019, pp. 41–71). Aarhus, Denmark: Springer.
https://doi.org/10.1007/3-540-60630-0_3'
chicago: Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “A User Guide to HyTech.”
In 1st International Workshop on Tools and Algorithms for the Construction
and Analysis of Systems, 1019:41–71. Springer, 1995. https://doi.org/10.1007/3-540-60630-0_3.
ieee: T. A. Henzinger, P. Ho, and H. Wong Toi, “A user guide to HyTech,” in 1st
International Workshop on Tools and Algorithms for the Construction and Analysis
of Systems, Aarhus, Denmark, 1995, vol. 1019, pp. 41–71.
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.” 1st International
Workshop on Tools and Algorithms for the Construction and Analysis of Systems,
vol. 1019, Springer, 1995, pp. 41–71, doi:10.1007/3-540-60630-0_3.
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 M, Henzinger TA, Kopke P. Computing simulations on finite and infinite
graphs. In: Proceedings of IEEE 36th Annual Foundations of Computer Science.
IEEE; 1995:453-462. doi:10.1109/SFCS.1995.492576'
apa: 'Henzinger, M., Henzinger, T. A., & Kopke, P. (1995). Computing simulations
on finite and infinite graphs. In Proceedings of IEEE 36th Annual Foundations
of Computer Science (pp. 453–462). Milwaukee, WI, United States of America:
IEEE. https://doi.org/10.1109/SFCS.1995.492576'
chicago: Henzinger, Monika, Thomas A Henzinger, and Peter Kopke. “Computing Simulations
on Finite and Infinite Graphs.” In Proceedings of IEEE 36th Annual Foundations
of Computer Science, 453–62. IEEE, 1995. https://doi.org/10.1109/SFCS.1995.492576.
ieee: M. Henzinger, T. A. Henzinger, and P. Kopke, “Computing simulations on finite
and infinite graphs,” in Proceedings of IEEE 36th Annual Foundations of Computer
Science, Milwaukee, WI, United States of America, 1995, pp. 453–462.
ista: 'Henzinger M, 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, et al. “Computing Simulations on Finite and Infinite Graphs.”
Proceedings of IEEE 36th Annual Foundations of Computer Science, IEEE,
1995, pp. 453–62, doi:10.1109/SFCS.1995.492576.
short: M. 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: 2024-11-06T12:02:08Z
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: Proceedings
16th IEEE Real-Time Systems Symposium. IEEE; 1995:56-65. doi:10.1109/REAL.1995.495196 '
apa: 'Henzinger, T. A., Ho, P., & Wong Toi, H. (1995). HyTech: The next generation.
In Proceedings 16th IEEE Real-Time Systems Symposium (pp. 56–65). Pisa,
Italy: IEEE. https://doi.org/10.1109/REAL.1995.495196
'
chicago: 'Henzinger, Thomas A, Pei Ho, and Howard Wong Toi. “HyTech: The next Generation.”
In Proceedings 16th IEEE Real-Time Systems Symposium, 56–65. IEEE, 1995.
https://doi.org/10.1109/REAL.1995.495196
.'
ieee: 'T. A. Henzinger, P. Ho, and H. Wong Toi, “HyTech: The next generation,” in
Proceedings 16th IEEE Real-Time Systems Symposium, Pisa, Italy, 1995, pp.
56–65.'
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.” Proceedings
16th IEEE Real-Time Systems Symposium, IEEE, 1995, pp. 56–65, doi:10.1109/REAL.1995.495196 .'
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: 22nd
International Colloquium on Automata, Languages and Programming . Vol 944.
Springer; 1995:417-428. doi:10.1007/3-540-60084-1_93'
apa: 'Henzinger, T. A., Kopke, P., & Wong Toi, H. (1995). The expressive power
of clocks. In 22nd International Colloquium on Automata, Languages and Programming
(Vol. 944, pp. 417–428). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_93'
chicago: Henzinger, Thomas A, Peter Kopke, and Howard Wong Toi. “The Expressive
Power of Clocks.” In 22nd International Colloquium on Automata, Languages and
Programming , 944:417–28. Springer, 1995. https://doi.org/10.1007/3-540-60084-1_93.
ieee: T. A. Henzinger, P. Kopke, and H. Wong Toi, “The expressive power of clocks,”
in 22nd International Colloquium on Automata, Languages and Programming ,
Szeged, Hungary, 1995, vol. 944, pp. 417–428.
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.” 22nd International
Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995,
pp. 417–28, doi:10.1007/3-540-60084-1_93.
short: T.A. Henzinger, P. Kopke, H. Wong Toi, in:, 22nd International Colloquium
on Automata, Languages and Programming , Springer, 1995, pp. 417–428.
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: Proceedings of the 27th Annual ACM Symposium on Theory of Computing.
ACM; 1995:373-382. doi:10.1145/225058.225162'
apa: 'Henzinger, T. A., Kopke, P., Puri, A., & Varaiya, P. (1995). What’s decidable
about hybrid automata? In Proceedings of the 27th annual ACM symposium on Theory
of computing (pp. 373–382). Las Vegas, NV, United States of America: ACM.
https://doi.org/10.1145/225058.225162'
chicago: Henzinger, Thomas A, Peter Kopke, Anuj Puri, and P. Varaiya. “What’s Decidable
about Hybrid Automata?” In Proceedings of the 27th Annual ACM Symposium on
Theory of Computing, 373–82. ACM, 1995. https://doi.org/10.1145/225058.225162.
ieee: T. A. Henzinger, P. Kopke, A. Puri, and P. Varaiya, “What’s decidable about
hybrid automata?,” in Proceedings of the 27th annual ACM symposium on Theory
of computing, Las Vegas, NV, United States of America, 1995, pp. 373–382.
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?” Proceedings
of the 27th Annual ACM Symposium on Theory of Computing, ACM, 1995, pp. 373–82,
doi:10.1145/225058.225162.
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: 22nd International
Colloquium on Automata, Languages and Programming . Vol 944. Springer; 1995:324-335.
doi:10.1007/3-540-60084-1_85'
apa: 'Henzinger, T. A. (1995). Hybrid automata with finite bisimulations. In 22nd
International Colloquium on Automata, Languages and Programming (Vol. 944,
pp. 324–335). Szeged, Hungary: Springer. https://doi.org/10.1007/3-540-60084-1_85'
chicago: Henzinger, Thomas A. “Hybrid Automata with Finite Bisimulations.” In 22nd
International Colloquium on Automata, Languages and Programming , 944:324–35.
Springer, 1995. https://doi.org/10.1007/3-540-60084-1_85.
ieee: T. A. Henzinger, “Hybrid automata with finite bisimulations,” in 22nd International
Colloquium on Automata, Languages and Programming , Szeged, Hungary, 1995,
vol. 944, pp. 324–335.
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.” 22nd International
Colloquium on Automata, Languages and Programming , vol. 944, Springer, 1995,
pp. 324–35, doi:10.1007/3-540-60084-1_85.
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: 2025-06-26T08:47:29Z
day: '01'
doi: 10.1007/3-540-60084-1_85
extern: '1'
intvolume: ' 944'
language:
- iso: eng
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
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: 7th International Conference on Computer Aided Verification.
Vol 939. Springer; 1995:166-179. doi:10.1007/3-540-60045-0_49'
apa: 'Alur, R., & Henzinger, T. A. (1995). Local liveness for compositional
modeling of fair reactive systems. In 7th International Conference on Computer
Aided Verification (Vol. 939, pp. 166–179). Liege, Belgium: Springer. https://doi.org/10.1007/3-540-60045-0_49'
chicago: Alur, Rajeev, and Thomas A Henzinger. “Local Liveness for Compositional
Modeling of Fair Reactive Systems.” In 7th International Conference on Computer
Aided Verification, 939:166–79. Springer, 1995. https://doi.org/10.1007/3-540-60045-0_49.
ieee: R. Alur and T. A. Henzinger, “Local liveness for compositional modeling of
fair reactive systems,” in 7th International Conference on Computer Aided Verification,
Liege, Belgium, 1995, vol. 939, pp. 166–179.
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.” 7th International Conference on Computer Aided Verification,
vol. 939, Springer, 1995, pp. 166–79, doi:10.1007/3-540-60045-0_49.
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. Theoretical Computer Science. 1995;138(1):3-34. doi:10.1016/0304-3975(94)00202-T
apa: Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T. A., Ho, P., Nicollin,
X., … Yovine, S. (1995). The algorithmic analysis of hybrid systems. Theoretical
Computer Science. Elsevier. https://doi.org/10.1016/0304-3975(94)00202-T
chicago: Alur, Rajeev, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger,
Pei Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The
Algorithmic Analysis of Hybrid Systems.” Theoretical Computer Science.
Elsevier, 1995. https://doi.org/10.1016/0304-3975(94)00202-T.
ieee: R. Alur et al., “The algorithmic analysis of hybrid systems,” Theoretical
Computer Science, 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.” Theoretical
Computer Science, vol. 138, no. 1, Elsevier, 1995, pp. 3–34, doi:10.1016/0304-3975(94)00202-T.
short: R. Alur, C. Courcoubetis, N. Halbwachs, T.A. Henzinger, P. Ho, X. Nicollin,
A. Olivero, J. Sifakis, S. Yovine, Theoretical Computer Science 138 (1995) 3–34.
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: '6162'
abstract:
- lang: eng
text: 'The tra-1 gene is the terminal global selector of somatic sex in Caenorhabditis
elegans: High tra-1 activity elicits female somatic development while low tra-1
activity elicits male development. Previous genetic studies defined a cascade
of negatively interacting genes that regulates tra-1 activity in response to the
primary sex-determining signal. Here, we investigate the last step in this regulatory
cascade, by studying rare gain-of-function (gf) mutations of tra-1 that direct
female somatic development irrespective of the upstream sex-determining signal.
These mutations appear to abolish negative regulation of tra-1 in male tissues.
We identify the lesions associated with 29 of these mutations and find that all
affect a short stretch of amino acid residues present in both protein products
of the tra-1 gene. Twenty-six alleles are associated with single nonconservative
amino acid substitutions. Two alleles affect tra-1 RNA splicing and generate messages
that omit part or all of the exon encoding this short stretch. These results suggest
that sexual regulation of tra-1 is achieved post-translationally, by an inhibitory
protein-protein interaction. The amino acid stretch altered by the tra-1(gf) mutations
may define a site of interaction for negative regulators of tra-1. The stretch
includes a potential phosphorylation site for glycogen synthase kinase 3 and may
be conserved in the human gene GLI3, a homolog of tra-1 identified previously.'
author:
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
- first_name: D.
full_name: Zarkower, D.
last_name: Zarkower
- first_name: J.
full_name: Hodgkin, J.
last_name: Hodgkin
citation:
ama: de Bono M, Zarkower D, Hodgkin J. Dominant feminizing mutations implicate protein-protein
interactions as the main mode of regulation of the nematode sex-determining gene
tra-1. Genes and Development. 1995;9(2):155-167. doi:10.1101/gad.9.2.155
apa: de Bono, M., Zarkower, D., & Hodgkin, J. (1995). Dominant feminizing mutations
implicate protein-protein interactions as the main mode of regulation of the nematode
sex-determining gene tra-1. Genes and Development. CSH Press. https://doi.org/10.1101/gad.9.2.155
chicago: Bono, Mario de, D. Zarkower, and J. Hodgkin. “Dominant Feminizing Mutations
Implicate Protein-Protein Interactions as the Main Mode of Regulation of the Nematode
Sex-Determining Gene Tra-1.” Genes and Development. CSH Press, 1995. https://doi.org/10.1101/gad.9.2.155.
ieee: M. de Bono, D. Zarkower, and J. Hodgkin, “Dominant feminizing mutations implicate
protein-protein interactions as the main mode of regulation of the nematode sex-determining
gene tra-1,” Genes and Development, vol. 9, no. 2. CSH Press, pp. 155–167,
1995.
ista: de Bono M, Zarkower D, Hodgkin J. 1995. Dominant feminizing mutations implicate
protein-protein interactions as the main mode of regulation of the nematode sex-determining
gene tra-1. Genes and Development. 9(2), 155–167.
mla: de Bono, Mario, et al. “Dominant Feminizing Mutations Implicate Protein-Protein
Interactions as the Main Mode of Regulation of the Nematode Sex-Determining Gene
Tra-1.” Genes and Development, vol. 9, no. 2, CSH Press, 1995, pp. 155–67,
doi:10.1101/gad.9.2.155.
short: M. de Bono, D. Zarkower, J. Hodgkin, Genes and Development 9 (1995) 155–167.
date_created: 2019-03-21T11:57:40Z
date_published: 1995-01-15T00:00:00Z
date_updated: 2021-01-12T08:06:29Z
day: '15'
doi: 10.1101/gad.9.2.155
extern: '1'
external_id:
pmid:
- '7851791'
intvolume: ' 9'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 155-167
pmid: 1
publication: Genes and Development
publication_identifier:
issn:
- '08909369'
publication_status: published
publisher: CSH Press
quality_controlled: '1'
status: public
title: Dominant feminizing mutations implicate protein-protein interactions as the
main mode of regulation of the nematode sex-determining gene tra-1
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '1995'
...
---
_id: '3454'
abstract:
- lang: eng
text: The study of gene expression and regulation in the central nervous system
(CNS) is a daunting task because of the diversity of neuronal phenotypes and the
complexity of many protein classes. Molecular cloning revealed the presence of
a large number of different protein families in the CNS, each comprising several
members. Ligand-gated ion channels may serve as an example to illustrate this
point (for review, see Unwin, 1993). Heterologous expression combined with electrophysiological
analysis suggests that ligand-gated channels are multimeric proteins with functional
properties depending on the subunit composition. Very little is known, however,
about how the functional properties of the recombinant and native receptors relate
to each other. Thus, it is of eminent importance to elucidate the subunit expression
profile in different types of neurons in the CNS and to correlate this with the
functional properties of the native receptors.
article_processing_charge: No
author:
- first_name: Hannah
full_name: Monyer, Hannah
last_name: Monyer
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
citation:
ama: 'Monyer H, Jonas PM. Polymerase chain reaction analysis of ion channel expression
in single neurons of brain slices. In: Sakmann B, Neher E, eds. Single-Channel
Recording. Plenum; 1995:357-373. doi:10.1007/978-1-4419-1229-9_16'
apa: Monyer, H., & Jonas, P. M. (1995). Polymerase chain reaction analysis of
ion channel expression in single neurons of brain slices. In B. Sakmann &
E. Neher (Eds.), Single-channel recording (pp. 357–373). Plenum. https://doi.org/10.1007/978-1-4419-1229-9_16
chicago: Monyer, Hannah, and Peter M Jonas. “Polymerase Chain Reaction Analysis
of Ion Channel Expression in Single Neurons of Brain Slices.” In Single-Channel
Recording, edited by Bert Sakmann and Erwin Neher, 357–73. Plenum, 1995. https://doi.org/10.1007/978-1-4419-1229-9_16.
ieee: H. Monyer and P. M. Jonas, “Polymerase chain reaction analysis of ion channel
expression in single neurons of brain slices,” in Single-channel recording,
B. Sakmann and E. Neher, Eds. Plenum, 1995, pp. 357–373.
ista: 'Monyer H, Jonas PM. 1995.Polymerase chain reaction analysis of ion channel
expression in single neurons of brain slices. In: Single-channel recording. ,
357–373.'
mla: Monyer, Hannah, and Peter M. Jonas. “Polymerase Chain Reaction Analysis of
Ion Channel Expression in Single Neurons of Brain Slices.” Single-Channel Recording,
edited by Bert Sakmann and Erwin Neher, Plenum, 1995, pp. 357–73, doi:10.1007/978-1-4419-1229-9_16.
short: H. Monyer, P.M. Jonas, in:, B. Sakmann, E. Neher (Eds.), Single-Channel Recording,
Plenum, 1995, pp. 357–373.
date_created: 2018-12-11T12:03:25Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2022-06-28T09:13:01Z
day: '01'
doi: 10.1007/978-1-4419-1229-9_16
editor:
- first_name: Bert
full_name: Sakmann, Bert
last_name: Sakmann
- first_name: Erwin
full_name: Neher, Erwin
last_name: Neher
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/978-1-4419-1229-9_16
month: '01'
oa_version: None
page: 357 - 373
publication: Single-channel recording
publication_identifier:
isbn:
- 978-0-306-44870-6
publication_status: published
publisher: Plenum
publist_id: '2933'
quality_controlled: '1'
status: public
title: Polymerase chain reaction analysis of ion channel expression in single neurons
of brain slices
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1995'
...