---
_id: '4033'
abstract:
- lang: eng
text: 'A collection of geometric selection lemmas is proved, such as the following:
For any set P of n points in three-dimensional space and any set S of m spheres,
where each sphere passes through a distinct point pair in P. there exists a point
x, not necessarily in P, that is enclosed by Ω(m2/(n2 log6 n2/m)) of the spheres
in S. Similar results apply in arbitrary fixed dimensions, and for geometric bodies
other than spheres. The results have applications in reducing the size of geometric
structures, such as three-dimensional Delaunay triangulations and Gabriel graphs,
by adding extra points to their defining sets.'
article_processing_charge: No
article_type: original
author:
- first_name: Bernard
full_name: Chazelle, Bernard
last_name: Chazelle
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Leonidas
full_name: Guibas, Leonidas
last_name: Guibas
- first_name: John
full_name: Hershberger, John
last_name: Hershberger
- first_name: Raimund
full_name: Seidel, Raimund
last_name: Seidel
- first_name: Micha
full_name: Sharir, Micha
last_name: Sharir
citation:
ama: Chazelle B, Edelsbrunner H, Guibas L, Hershberger J, Seidel R, Sharir M. Selecting
heavily covered points. SIAM Journal on Computing. 1994;23(6):1138-1151.
doi:10.1137/S0097539790179919
apa: Chazelle, B., Edelsbrunner, H., Guibas, L., Hershberger, J., Seidel, R., &
Sharir, M. (1994). Selecting heavily covered points. SIAM Journal on Computing.
SIAM. https://doi.org/10.1137/S0097539790179919
chicago: Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, John Hershberger,
Raimund Seidel, and Micha Sharir. “Selecting Heavily Covered Points.” SIAM
Journal on Computing. SIAM, 1994. https://doi.org/10.1137/S0097539790179919 .
ieee: B. Chazelle, H. Edelsbrunner, L. Guibas, J. Hershberger, R. Seidel, and M.
Sharir, “Selecting heavily covered points,” SIAM Journal on Computing,
vol. 23, no. 6. SIAM, pp. 1138–1151, 1994.
ista: Chazelle B, Edelsbrunner H, Guibas L, Hershberger J, Seidel R, Sharir M. 1994.
Selecting heavily covered points. SIAM Journal on Computing. 23(6), 1138–1151.
mla: Chazelle, Bernard, et al. “Selecting Heavily Covered Points.” SIAM Journal
on Computing, vol. 23, no. 6, SIAM, 1994, pp. 1138–51, doi:10.1137/S0097539790179919 .
short: B. Chazelle, H. Edelsbrunner, L. Guibas, J. Hershberger, R. Seidel, M. Sharir,
SIAM Journal on Computing 23 (1994) 1138–1151.
date_created: 2018-12-11T12:06:33Z
date_published: 1994-12-01T00:00:00Z
date_updated: 2022-06-03T06:41:56Z
day: '01'
doi: '10.1137/S0097539790179919 '
extern: '1'
intvolume: ' 23'
issue: '6'
language:
- iso: eng
main_file_link:
- url: https://epubs.siam.org/doi/10.1137/S0097539790179919
month: '12'
oa_version: None
page: 1138 - 1151
publication: SIAM Journal on Computing
publication_identifier:
issn:
- 0097-5397
publication_status: published
publisher: SIAM
publist_id: '2092'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Selecting heavily covered points
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 23
year: '1994'
...
---
_id: '4037'
abstract:
- lang: eng
text: Frequently, data in scientific computing is in its abstract form a finite
point set in space, and it is sometimes useful or required to compute what one
might call the `'shape” of the set. For that purpose, this article introduces
the formal notion of the family of alpha-shapes of a finite point set in R3. Each
shape is a well-defined polytope, derived from the Delaunay triangulation of the
point set, with a parameter alpha is-an-element-of R controlling the desired level
of detail. An algorithm is presented that constructs the entire family of shapes
for a given set of size n in time O(n2), worst case. A robust implementation of
the algorithm is discussed, and several applications in the area of scientific
computing are mentioned.
acknowledgement: National Science Foundation under grant CCR-8921421 and Alan T.
Waterman award, grant CCR-9118874.
article_processing_charge: No
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Ernst
full_name: Mücke, Ernst
last_name: Mücke
citation:
ama: Edelsbrunner H, Mücke E. Three-dimensional alpha shapes. ACM Transactions
on Graphics. 1994;13(1):43-72. doi:10.1145/174462.156635
apa: Edelsbrunner, H., & Mücke, E. (1994). Three-dimensional alpha shapes. ACM
Transactions on Graphics. ACM. https://doi.org/10.1145/174462.156635
chicago: Edelsbrunner, Herbert, and Ernst Mücke. “Three-Dimensional Alpha Shapes.”
ACM Transactions on Graphics. ACM, 1994. https://doi.org/10.1145/174462.156635.
ieee: H. Edelsbrunner and E. Mücke, “Three-dimensional alpha shapes,” ACM Transactions
on Graphics, vol. 13, no. 1. ACM, pp. 43–72, 1994.
ista: Edelsbrunner H, Mücke E. 1994. Three-dimensional alpha shapes. ACM Transactions
on Graphics. 13(1), 43–72.
mla: Edelsbrunner, Herbert, and Ernst Mücke. “Three-Dimensional Alpha Shapes.” ACM
Transactions on Graphics, vol. 13, no. 1, ACM, 1994, pp. 43–72, doi:10.1145/174462.156635.
short: H. Edelsbrunner, E. Mücke, ACM Transactions on Graphics 13 (1994) 43–72.
date_created: 2018-12-11T12:06:34Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T12:00:42Z
day: '01'
doi: 10.1145/174462.156635
extern: '1'
intvolume: ' 13'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://dl.acm.org/doi/10.1145/174462.156635
month: '01'
oa: 1
oa_version: None
page: 43 - 72
publication: ACM Transactions on Graphics
publication_status: published
publisher: ACM
publist_id: '2088'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Three-dimensional alpha shapes
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 13
year: '1994'
...
---
_id: '4038'
abstract:
- lang: eng
text: We consider a variety of problems on the interaction between two sets of line
segments in two and three dimensions. These problems range from counting the number
of intersecting pairs between m blue segments and n red segments in the plane
(assuming that two line segments are disjoint if they have the same color) to
finding the smallest vertical distance between two nonintersecting polyhedral
terrains in three-dimensional space. We solve these problems efficiently by using
a variant of the segment tree. For the three-dimensional problems we also apply
a variety of recent combinatorial and algorithmic techniques involving arrangements
of lines in three-dimensional space, as developed in a companion paper.
acknowledgement: Supported in part by the National Science Foundation under Grant
CCR-8714565.
article_processing_charge: No
article_type: original
author:
- first_name: Bernard
full_name: Chazelle, Bernard
last_name: Chazelle
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Leonidas
full_name: Guibas, Leonidas
last_name: Guibas
- first_name: Micha
full_name: Sharir, Micha
last_name: Sharir
citation:
ama: Chazelle B, Edelsbrunner H, Guibas L, Sharir M. Algorithms for bichromatic
line-segment problems and polyhedral terrains. Algorithmica. 1994;11(2):116-132.
doi:10.1007/BF01182771
apa: Chazelle, B., Edelsbrunner, H., Guibas, L., & Sharir, M. (1994). Algorithms
for bichromatic line-segment problems and polyhedral terrains. Algorithmica.
Springer. https://doi.org/10.1007/BF01182771
chicago: Chazelle, Bernard, Herbert Edelsbrunner, Leonidas Guibas, and Micha Sharir.
“Algorithms for Bichromatic Line-Segment Problems and Polyhedral Terrains.” Algorithmica.
Springer, 1994. https://doi.org/10.1007/BF01182771.
ieee: B. Chazelle, H. Edelsbrunner, L. Guibas, and M. Sharir, “Algorithms for bichromatic
line-segment problems and polyhedral terrains,” Algorithmica, vol. 11,
no. 2. Springer, pp. 116–132, 1994.
ista: Chazelle B, Edelsbrunner H, Guibas L, Sharir M. 1994. Algorithms for bichromatic
line-segment problems and polyhedral terrains. Algorithmica. 11(2), 116–132.
mla: Chazelle, Bernard, et al. “Algorithms for Bichromatic Line-Segment Problems
and Polyhedral Terrains.” Algorithmica, vol. 11, no. 2, Springer, 1994,
pp. 116–32, doi:10.1007/BF01182771.
short: B. Chazelle, H. Edelsbrunner, L. Guibas, M. Sharir, Algorithmica 11 (1994)
116–132.
date_created: 2018-12-11T12:06:34Z
date_published: 1994-02-01T00:00:00Z
date_updated: 2022-06-02T12:25:29Z
day: '01'
doi: 10.1007/BF01182771
extern: '1'
intvolume: ' 11'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/article/10.1007/BF01182771
month: '02'
oa_version: None
page: 116 - 132
publication: Algorithmica
publication_identifier:
issn:
- 0178-4617
publication_status: published
publisher: Springer
publist_id: '2089'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Algorithms for bichromatic line-segment problems and polyhedral terrains
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 11
year: '1994'
...
---
_id: '4039'
abstract:
- lang: eng
text: Let P be a simple polygon with n vertices. We present a simple decomposition
scheme that partitions the interior of P into O(n) so-called geodesic triangles,
so that any line segment interior to P crosses at most 2 log n of these triangles.
This decomposition can be used to preprocess P in a very simple manner, so that
any ray-shooting query can be answered in time O(log n). The data structure requires
O(n) storage and O(n log n) preprocessing time. By using more sophisticated techniques,
we can reduce the preprocessing time to O(n). We also extend our general technique
to the case of ray shooting amidst k polygonal obstacles with a total of n edges,
so that a query can be answered in O(√ log n) time.
acknowledgement: Work by Bernard Chazelle has been supported by NSF Grant CCR-87-00917.
Work by Herbert Edelsbrunner has been supported by NSF Grant CCR-89-21421. Work
by Micha Sharir has been supported by ONR Grants N00014-89-J-3042 and N00014-90-J-1284,
by NSF Grant CCR-89-01484, and by grants from the U.S.-Israeli Binational Science
Foundation, the Fund for Basic Research administered by the Israeli Academy of Sciences,
and the G.I.F., the German-Israeli Foundation for Scientific Research and Development.
article_processing_charge: No
article_type: original
author:
- first_name: Bernard
full_name: Chazelle, Bernard
last_name: Chazelle
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Michelangelo
full_name: Grigni, Michelangelo
last_name: Grigni
- first_name: Leonidas
full_name: Guibas, Leonidas
last_name: Guibas
- first_name: John
full_name: Hershberger, John
last_name: Hershberger
- first_name: Micha
full_name: Sharir, Micha
last_name: Sharir
- first_name: Jack
full_name: Snoeyink, Jack
last_name: Snoeyink
citation:
ama: Chazelle B, Edelsbrunner H, Grigni M, et al. Ray shooting in polygons using
geodesic triangulations. Algorithmica. 1994;12(1):54-68. doi:10.1007/BF01377183
apa: Chazelle, B., Edelsbrunner, H., Grigni, M., Guibas, L., Hershberger, J., Sharir,
M., & Snoeyink, J. (1994). Ray shooting in polygons using geodesic triangulations.
Algorithmica. Springer. https://doi.org/10.1007/BF01377183
chicago: Chazelle, Bernard, Herbert Edelsbrunner, Michelangelo Grigni, Leonidas
Guibas, John Hershberger, Micha Sharir, and Jack Snoeyink. “Ray Shooting in Polygons
Using Geodesic Triangulations.” Algorithmica. Springer, 1994. https://doi.org/10.1007/BF01377183.
ieee: B. Chazelle et al., “Ray shooting in polygons using geodesic triangulations,”
Algorithmica, vol. 12, no. 1. Springer, pp. 54–68, 1994.
ista: Chazelle B, Edelsbrunner H, Grigni M, Guibas L, Hershberger J, Sharir M, Snoeyink
J. 1994. Ray shooting in polygons using geodesic triangulations. Algorithmica.
12(1), 54–68.
mla: Chazelle, Bernard, et al. “Ray Shooting in Polygons Using Geodesic Triangulations.”
Algorithmica, vol. 12, no. 1, Springer, 1994, pp. 54–68, doi:10.1007/BF01377183.
short: B. Chazelle, H. Edelsbrunner, M. Grigni, L. Guibas, J. Hershberger, M. Sharir,
J. Snoeyink, Algorithmica 12 (1994) 54–68.
date_created: 2018-12-11T12:06:35Z
date_published: 1994-07-01T00:00:00Z
date_updated: 2022-06-02T12:41:07Z
day: '01'
doi: 10.1007/BF01377183
extern: '1'
intvolume: ' 12'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/article/10.1007/BF01377183
month: '07'
oa_version: None
page: 54 - 68
publication: Algorithmica
publication_identifier:
issn:
- 0178-4617
publication_status: published
publisher: Springer
publist_id: '2090'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Ray shooting in polygons using geodesic triangulations
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 12
year: '1994'
...
---
_id: '4179'
abstract:
- lang: eng
text: Neurotrophin-3 (NT-3) is a member of the neurotrophin gene family and is highly
expressed in the developing rat cerebellum. Here we show that brain-derived neurotrophic
factor (BDNF) increased by approximately 10-fold the NT-3 mRNA levels in cultured
cerebellar granule neurons isolated from postnatal rats, whereas nerve growth
factor (NGF) and NT-3 itself had no effect. The effect of BDNF was additive to
that of triiodothyronine (T3), which also increased NT-3 mRNA in these neurons.
The drug K252a inhibited the BDNF-mediated stimulation of NT-3 expression, suggesting
an involvement of trkB receptors. Nuclear run-on experiments showed that BDNF
enhanced NT-3 transcription, whereas the stability of NT-3 mRNA remained unchanged.
The data presented are the first demonstration that one neurotrophin regulates
the expression of another and provide evidence that NT-3 production in granule
neurons is regulated by both BDNF and T3.
acknowledgement: We thank Dorothea Stratmann and Karin Angermayer for skillful technical
assistance.
article_processing_charge: No
article_type: original
author:
- first_name: Axel
full_name: Leingärtner, Axel
last_name: Leingärtner
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
- first_name: Roland
full_name: Kolbeck, Roland
last_name: Kolbeck
- first_name: Hans
full_name: Thoenen, Hans
last_name: Thoenen
- first_name: Dan
full_name: Lindholm, Dan
last_name: Lindholm
citation:
ama: Leingärtner A, Heisenberg C-PJ, Kolbeck R, Thoenen H, Lindholm D. Brain-derived
neurotrophic factor increases neurotrophin-3 expression in cerebellar granule
neurons. Journal of Biological Chemistry. 1994;269(2):828-830. doi:10.1016/s0021-9258(17)42186-7
apa: Leingärtner, A., Heisenberg, C.-P. J., Kolbeck, R., Thoenen, H., & Lindholm,
D. (1994). Brain-derived neurotrophic factor increases neurotrophin-3 expression
in cerebellar granule neurons. Journal of Biological Chemistry. American
Society for Biochemistry and Molecular Biology. https://doi.org/10.1016/s0021-9258(17)42186-7
chicago: Leingärtner, Axel, Carl-Philipp J Heisenberg, Roland Kolbeck, Hans Thoenen,
and Dan Lindholm. “Brain-Derived Neurotrophic Factor Increases Neurotrophin-3
Expression in Cerebellar Granule Neurons.” Journal of Biological Chemistry.
American Society for Biochemistry and Molecular Biology, 1994. https://doi.org/10.1016/s0021-9258(17)42186-7.
ieee: A. Leingärtner, C.-P. J. Heisenberg, R. Kolbeck, H. Thoenen, and D. Lindholm,
“Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar
granule neurons,” Journal of Biological Chemistry, vol. 269, no. 2. American
Society for Biochemistry and Molecular Biology, pp. 828–830, 1994.
ista: Leingärtner A, Heisenberg C-PJ, Kolbeck R, Thoenen H, Lindholm D. 1994. Brain-derived
neurotrophic factor increases neurotrophin-3 expression in cerebellar granule
neurons. Journal of Biological Chemistry. 269(2), 828–830.
mla: Leingärtner, Axel, et al. “Brain-Derived Neurotrophic Factor Increases Neurotrophin-3
Expression in Cerebellar Granule Neurons.” Journal of Biological Chemistry,
vol. 269, no. 2, American Society for Biochemistry and Molecular Biology, 1994,
pp. 828–30, doi:10.1016/s0021-9258(17)42186-7.
short: A. Leingärtner, C.-P.J. Heisenberg, R. Kolbeck, H. Thoenen, D. Lindholm,
Journal of Biological Chemistry 269 (1994) 828–830.
date_created: 2018-12-11T12:07:25Z
date_published: 1994-01-14T00:00:00Z
date_updated: 2022-06-02T10:23:48Z
day: '14'
doi: 10.1016/s0021-9258(17)42186-7
extern: '1'
intvolume: ' 269'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0021925817421867?via%3Dihub
month: '01'
oa: 1
oa_version: None
page: 828 - 830
publication: Journal of Biological Chemistry
publication_identifier:
eissn:
- 1083-351X
issn:
- 0021-9258
publication_status: published
publisher: American Society for Biochemistry and Molecular Biology
publist_id: '1941'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Brain-derived neurotrophic factor increases neurotrophin-3 expression in cerebellar
granule neurons
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 269
year: '1994'
...
---
_id: '4202'
abstract:
- lang: eng
text: NERVE growth factor (NGF) injected into the otherwise unlesioned adult rat
septum induced sprouting of presumptive cholinergic fibres positive for p75(NGFR)
and acetylcholinesterase (AChE). These fibres did not stain for tyrosine hydroxylase
and therefore did not represent sympathetic ingrowth. Neurofilament staining on
adjacent sections revealed fibres with similar morphology, suggesting new outgrowth
in the form of sprouting rather than the upregulation of p75(NGFR) and AChE in
pre-existing fibres. Simultaneous injections of subneurotoxic doses of N-methyl-D-aspartate
(NMDA) significantly potentiated the effect of NGF on cholinergic fibre sprouting
and caused pronounced glial fibrillary acidic protein (GFAP)positive astrocytosis.
Application of NMDA alone did not elicit sprouting of this type. These findings
indicate that NGF can induce the sprouting of uninjured adult rat septal cholinergic
fibres in vivo and suggest that reactive astrocytes are not inhibitory to cholinergic
axonal outgrowth, and might serve as a substrate for growing axons in the presence
of NGF.
article_processing_charge: No
article_type: original
author:
- first_name: Carl-Philipp J
full_name: Heisenberg, Carl-Philipp J
id: 39427864-F248-11E8-B48F-1D18A9856A87
last_name: Heisenberg
orcid: 0000-0002-0912-4566
- first_name: John
full_name: Cooper, John
last_name: Cooper
- first_name: J
full_name: Berke, J
last_name: Berke
- first_name: Michael
full_name: Sofroniew, Michael
last_name: Sofroniew
citation:
ama: Heisenberg C-PJ, Cooper J, Berke J, Sofroniew M. NMDA potentiates NGF-induced
sprouting of septal cholinergic fibres. Neuroreport. 1994;5(4):413-416.
doi:10.1097/00001756-199401120-00010
apa: Heisenberg, C.-P. J., Cooper, J., Berke, J., & Sofroniew, M. (1994). NMDA
potentiates NGF-induced sprouting of septal cholinergic fibres. Neuroreport.
Lippincott, Williams & Wilkins. https://doi.org/10.1097/00001756-199401120-00010
chicago: Heisenberg, Carl-Philipp J, John Cooper, J Berke, and Michael Sofroniew.
“NMDA Potentiates NGF-Induced Sprouting of Septal Cholinergic Fibres.” Neuroreport.
Lippincott, Williams & Wilkins, 1994. https://doi.org/10.1097/00001756-199401120-00010 .
ieee: C.-P. J. Heisenberg, J. Cooper, J. Berke, and M. Sofroniew, “NMDA potentiates
NGF-induced sprouting of septal cholinergic fibres,” Neuroreport, vol.
5, no. 4. Lippincott, Williams & Wilkins, pp. 413–416, 1994.
ista: Heisenberg C-PJ, Cooper J, Berke J, Sofroniew M. 1994. NMDA potentiates NGF-induced
sprouting of septal cholinergic fibres. Neuroreport. 5(4), 413–416.
mla: Heisenberg, Carl-Philipp J., et al. “NMDA Potentiates NGF-Induced Sprouting
of Septal Cholinergic Fibres.” Neuroreport, vol. 5, no. 4, Lippincott,
Williams & Wilkins, 1994, pp. 413–16, doi:10.1097/00001756-199401120-00010 .
short: C.-P.J. Heisenberg, J. Cooper, J. Berke, M. Sofroniew, Neuroreport 5 (1994)
413–416.
date_created: 2018-12-11T12:07:33Z
date_published: 1994-01-12T00:00:00Z
date_updated: 2022-06-02T10:07:25Z
day: '12'
doi: '10.1097/00001756-199401120-00010 '
extern: '1'
intvolume: ' 5'
issue: '4'
language:
- iso: eng
main_file_link:
- url: https://journals.lww.com/neuroreport/Abstract/1994/01120/NMDA_potentiates_NGF_induced_sprouting_of_septal.10.aspx
month: '01'
oa_version: None
page: 413 - 416
publication: Neuroreport
publication_identifier:
issn:
- 0959-4965
publication_status: published
publisher: Lippincott, Williams & Wilkins
publist_id: '1915'
quality_controlled: '1'
scopus_import: '1'
status: public
title: NMDA potentiates NGF-induced sprouting of septal cholinergic fibres
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 5
year: '1994'
...
---
_id: '4420'
abstract:
- lang: eng
text: We propose a methodology for the specification, verification, and design of
hybrid systems. The methodology consists of the computational model of Concrete
Phase Transition Systems (cptss), the specification language of Hybrid Temporal
Logic (htl), the graphical system description language of Hybrid Automata, and
a proof system for verifying that hybrid automata satisfy their HTL specifications.
The novelty of the approach lies in the continuous-time logic, which allows specification
of both point-based and interval-based properties (i.e., properties which describe
changes over an interval) and provides direct references to derivatives of variables,
and in the proof system that supports verification of point-based and interval-based
properties. The proof rules demonstrate that sound and convenient induction rules
can be established for continuous-time logics. The proof rules are illustrated
on several examples.
acknowledgement: Supported in part by the National Science Foundation under grants
CCR-92-23226 and CCR-9200794, by the Defense Advanced Research Projects Agency under
grants NAG2-703 and NAG2-892, by the United States Air Force Office of Scientific
Research under contracts F49620-93-1-0139 and F49620-93-1-0056, and by the European
Community ESPRIT Basic Research Action Project 6021 (REACT). Supported in part by
a National Science Foundation Graduate Research Fellowship.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Arjun
full_name: Kapur, Arjun
last_name: Kapur
- 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: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: 'Kapur A, Henzinger TA, Manna Z, Pnueli A. Proving safety properties of hybrid
systems. In: 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. Vol 863. Springer; 1994:431-454. doi:10.1007/3-540-58468-4_177'
apa: 'Kapur, A., Henzinger, T. A., Manna, Z., & Pnueli, A. (1994). Proving safety
properties of hybrid systems. In 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems (Vol. 863, pp. 431–454). Lübeck, Germany:
Springer. https://doi.org/10.1007/3-540-58468-4_177'
chicago: Kapur, Arjun, Thomas A Henzinger, Zohar Manna, and Amir Pnueli. “Proving
Safety Properties of Hybrid Systems.” In 3rd International Symposium on Formal
Techniques in Real-Time and Fault-Tolerant Systems, 863:431–54. Springer,
1994. https://doi.org/10.1007/3-540-58468-4_177.
ieee: A. Kapur, T. A. Henzinger, Z. Manna, and A. Pnueli, “Proving safety properties
of hybrid systems,” in 3rd International Symposium on Formal Techniques in
Real-Time and Fault-Tolerant Systems, Lübeck, Germany, 1994, vol. 863, pp.
431–454.
ista: 'Kapur A, Henzinger TA, Manna Z, Pnueli A. 1994. Proving safety properties
of hybrid systems. 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant
Systems, LNCS, vol. 863, 431–454.'
mla: Kapur, Arjun, et al. “Proving Safety Properties of Hybrid Systems.” 3rd
International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems,
vol. 863, Springer, 1994, pp. 431–54, doi:10.1007/3-540-58468-4_177.
short: A. Kapur, T.A. Henzinger, Z. Manna, A. Pnueli, in:, 3rd International Symposium
on Formal Techniques in Real-Time and Fault-Tolerant Systems, Springer, 1994,
pp. 431–454.
conference:
end_date: 1994-09-23
location: Lübeck, Germany
name: 'FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems'
start_date: 1994-09-19
date_created: 2018-12-11T12:08:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T09:46:37Z
day: '01'
doi: 10.1007/3-540-58468-4_177
extern: '1'
intvolume: ' 863'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-58468-4_177
month: '01'
oa_version: None
page: 431 - 454
publication: 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems
publication_status: published
publisher: Springer
publist_id: '309'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Proving safety properties of hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 863
year: '1994'
...
---
_id: '4440'
abstract:
- lang: eng
text: We present a methodology for proving temporal properties of the divergent
runs of reactive systems with real-valued clocks. A run diverges if time advances
beyond any bound. Since the divergent runs of a system may satisfy liveness properties
that are not satisfied by some convergent runs, the standard proof rules are incomplete
if only divergent runs are considered. First, we develop a sound and complete
proof calculus for divergence, which is based on translating clock systems into
discrete systems. Then, we show that simpler proofs can be obtained for stronger
divergence assumptions, such as unknown -divergence, which requires that all delays
have a minimum duration of some unknown constant . We classify all real-time systems
into an infinite hierarchy, according to how well they admit the translation of
eventuality properties into equivalent safety properties.
acknowledgement: 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, 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: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: 'Henzinger TA, Kopke P. Verification methods for the divergent runs of clock
systems. In: 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. Vol 863. Springer; 1994:351-372. doi:10.1007/3-540-58468-4_173'
apa: 'Henzinger, T. A., & Kopke, P. (1994). Verification methods for the divergent
runs of clock systems. In 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems (Vol. 863, pp. 351–372). Lübeck, Gernany:
Springer. https://doi.org/10.1007/3-540-58468-4_173'
chicago: Henzinger, Thomas A, and Peter Kopke. “Verification Methods for the Divergent
Runs of Clock Systems.” In 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems, 863:351–72. Springer, 1994. https://doi.org/10.1007/3-540-58468-4_173.
ieee: T. A. Henzinger and P. Kopke, “Verification methods for the divergent runs
of clock systems,” in 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems, Lübeck, Gernany, 1994, vol. 863, pp. 351–372.
ista: 'Henzinger TA, Kopke P. 1994. Verification methods for the divergent runs
of clock systems. 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant
Systems, LNCS, vol. 863, 351–372.'
mla: Henzinger, Thomas A., and Peter Kopke. “Verification Methods for the Divergent
Runs of Clock Systems.” 3rd International Symposium on Formal Techniques in
Real-Time and Fault-Tolerant Systems, vol. 863, Springer, 1994, pp. 351–72,
doi:10.1007/3-540-58468-4_173.
short: T.A. Henzinger, P. Kopke, in:, 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems, Springer, 1994, pp. 351–372.
conference:
end_date: 1994-09-23
location: Lübeck, Gernany
name: 'FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems'
start_date: 1994-09-19
date_created: 2018-12-11T12:08:52Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T09:35:58Z
day: '01'
doi: 10.1007/3-540-58468-4_173
extern: '1'
intvolume: ' 863'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-58468-4_173
month: '01'
oa_version: None
page: 351 - 372
publication: 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems
publication_status: published
publisher: Springer
publist_id: '287'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Verification methods for the divergent runs of clock systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 863
year: '1994'
...
---
_id: '4501'
abstract:
- lang: eng
text: 'We extend the specification language of temporal logic, the corresponding
verification framework, and the underlying computational model to deal with real-;time
properties of reactive systems. The abstract notion of timed transition systems
generalizes traditional transition systems conservatively: qualitative fairness
requirements are replaced (and superseded) by quantitative lower-bound and upper-bound
timing constraints on transitions. This framework can model real-time systems
that communicate either through shared variables or by message passing and real-time
issues such as timeouts, process priorities (interrupts), and process scheduling.
We exhibit two styles for the specification of real-time systems. While the first
approach uses time-bounded versions of the temporal operators, the second approach
allows explicit references to time through a special clock variable. Corresponding
to the two styles of specification, we present and compare two different proof
methodologies for the verification of timing requirements that are expressed in
these styles. For the bounded-operator style, we provide a set of proof rules
for establishing bounded-invariance and bounded-responce properties of timed transition
systems. This approach generalizes the standard temporal proof rules for verifying
invariance and response properties conservatively. For the explicit-clock style,
we exploit the observation that every time-bounded property is a safety property
and use the standard temporal proof rules for establishing safety properties.'
acknowledgement: 'This research was supported in part by an IBM graduate fellowship,
by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by
the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by
the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139
and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action
Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in
the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I
a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium
on Principles of Programming Languages RIMP911. '
article_processing_charge: No
article_type: original
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: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition
systems. Information and Computation. 1994;112(2):273-337. doi:10.1006/inco.1994.1060
apa: Henzinger, T. A., Manna, Z., & Pnueli, A. (1994). Temporal proof methodologies
for timed transition systems. Information and Computation. Elsevier. https://doi.org/10.1006/inco.1994.1060
chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies
for Timed Transition Systems.” Information and Computation. Elsevier, 1994.
https://doi.org/10.1006/inco.1994.1060.
ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for
timed transition systems,” Information and Computation, vol. 112, no. 2.
Elsevier, pp. 273–337, 1994.
ista: Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed
transition systems. Information and Computation. 112(2), 273–337.
mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition
Systems.” Information and Computation, vol. 112, no. 2, Elsevier, 1994,
pp. 273–337, doi:10.1006/inco.1994.1060.
short: T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994)
273–337.
date_created: 2018-12-11T12:09:10Z
date_published: 1994-08-01T00:00:00Z
date_updated: 2022-06-02T09:24:58Z
day: '01'
doi: 10.1006/inco.1994.1060
extern: '1'
intvolume: ' 112'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub
month: '08'
oa: 1
oa_version: None
page: 273 - 337
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '227'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal proof methodologies for timed transition systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 112
year: '1994'
...
---
_id: '4503'
abstract:
- lang: eng
text: 'We describe finite-state programs over real-numbered time in a guarded-command
language with real-valued clocks or, equivalently, as finite automata with real-valued
clocks. Model checking answers the question which states of a real-time program
satisfy a branching-time specification (given in an extension of CTL with clock
variables). We develop an algorithm that computes this set of states symbolically
as a fixpoint of a functional on state predicates, without constructing the state
space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered
time. Unfortunately, many standard program properties, such as response for all
nonzeno execution sequences (during which time diverges), cannot be characterized
by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable
to the expressiveness of timed CTL. Fortunately, this result does not impair the
symbolic verification of "implementable" real-time programs-those whose
safety constraints are machine-closed with respect to diverging time and whose
fairness constraints are restricted to finite upper bounds on clock values. All
timed CTL properties of such programs are shown to be computable as finitely approximable
fixpoints in a simple decidable theory.'
acknowledgement: We thank Peter Kopke for a careful reading.
article_processing_charge: No
article_type: original
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: Xavier
full_name: Nicollin, Xavier
last_name: Nicollin
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
- first_name: Sergio
full_name: Yovine, Sergio
last_name: Yovine
citation:
ama: Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for
real-time systems. Information and Computation. 1994;111(2):193-244. doi:10.1006/inco.1994.1045
apa: Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic
model checking for real-time systems. Information and Computation. Elsevier.
https://doi.org/10.1006/inco.1994.1045
chicago: Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
“Symbolic Model Checking for Real-Time Systems.” Information and Computation.
Elsevier, 1994. https://doi.org/10.1006/inco.1994.1045.
ieee: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking
for real-time systems,” Information and Computation, vol. 111, no. 2. Elsevier,
pp. 193–244, 1994.
ista: Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking
for real-time systems. Information and Computation. 111(2), 193–244.
mla: Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.”
Information and Computation, vol. 111, no. 2, Elsevier, 1994, pp. 193–244,
doi:10.1006/inco.1994.1045.
short: T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation
111 (1994) 193–244.
date_created: 2018-12-11T12:09:11Z
date_published: 1994-06-01T00:00:00Z
date_updated: 2022-06-02T09:02:02Z
day: '01'
doi: 10.1006/inco.1994.1045
extern: '1'
intvolume: ' 111'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub
month: '06'
oa_version: None
page: 193 - 244
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '226'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 111
year: '1994'
...
---
_id: '4586'
abstract:
- lang: eng
text: 'Fairness is a mathematical abstraction: in a multiprogramming environment,
fairness abstracts the details of admissible (“fair”) schedulers; in a distributed
environment, fairness abstracts the speeds of independent processors. We argue
that the standard definition of fairness often is unnecessarily weak and can be
replaced by the stronger, yet still abstract, notion of finitary fairness. While
standard weak fairness requires that no enabled transition is postponed forever,
finitary weak fairness requires that for every run of a system there is an unknown
bound k such that no enabled transition is postponed more than k consecutive times.
In general, the finitary restriction fin(F) of any given fairness assumption F
is the union of all w-regular safety properties that are contained in F. The adequacy
of the proposed abstraction is demonstrated in two ways. Suppose that we prove
a program property under the assumption of finitary fairness. In a multiprogramming
environment, the program then satisfies the property for all fair finite-state
schedulers. In a distributed environment, the program then satisfies the property
for all choices of lower and upper bounds on the speeds (or timings) of processors'
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. Finitary fairness. In: Proceedings 9th Annual IEEE
Symposium on Logic in Computer Science. IEEE; 1994:52-61. doi:10.1109/LICS.1994.316087 '
apa: 'Alur, R., & Henzinger, T. A. (1994). Finitary fairness. In Proceedings
9th Annual IEEE Symposium on Logic in Computer Science (pp. 52–61). Paris,
France: IEEE. https://doi.org/10.1109/LICS.1994.316087
'
chicago: Alur, Rajeev, and Thomas A Henzinger. “Finitary Fairness.” In Proceedings
9th Annual IEEE Symposium on Logic in Computer Science, 52–61. IEEE, 1994.
https://doi.org/10.1109/LICS.1994.316087
.
ieee: R. Alur and T. A. Henzinger, “Finitary fairness,” in Proceedings 9th Annual
IEEE Symposium on Logic in Computer Science, Paris, France, 1994, pp. 52–61.
ista: 'Alur R, Henzinger TA. 1994. Finitary fairness. Proceedings 9th Annual IEEE
Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 52–61.'
mla: Alur, Rajeev, and Thomas A. Henzinger. “Finitary Fairness.” Proceedings
9th Annual IEEE Symposium on Logic in Computer Science, IEEE, 1994, pp. 52–61,
doi:10.1109/LICS.1994.316087
.
short: R. Alur, T.A. Henzinger, in:, Proceedings 9th Annual IEEE Symposium on Logic
in Computer Science, IEEE, 1994, pp. 52–61.
conference:
end_date: "\t1994-07-07"
location: Paris, France
name: 'LICS: Logic in Computer Science'
start_date: 1994-07-04
date_created: 2018-12-11T12:09:37Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T08:45:57Z
day: '01'
doi: '10.1109/LICS.1994.316087 '
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ieeexplore.ieee.org/document/316087
month: '01'
oa_version: None
page: 52 - 61
publication: Proceedings 9th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
issn:
- 0018-9162
publication_status: published
publisher: IEEE
publist_id: '119'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Finitary fairness
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1994'
...
---
_id: '4590'
abstract:
- lang: eng
text: 'We introduce a temporal logic for the specification of real-time systems.
Our logic, TPTL, employs a novel quantifier construct for referencing time: the
"freeze" quantifier binds a variable to the time of the local temporal
context. TPTL is both a natural language for specification and a suitable formalism
for verification. We present a tableau-based decision procedure and a model-checking
algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.'
acknowledgement: The authors thank Rance Cleaveland, Limor Fix, David Karr, Peter
Kopke, Fred Schneider, and Bernhard Steffen for helpful comments.
alternative_title:
- AMAST Series in Computing
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. Real-time system = discrete system + clock variables.
In: Rus T, Rattray C, eds. Theories and Experiences for Real-Time System Development.
Vol 2. AMAST Series in Computing. World Scientific Publishing; 1994:1-29. doi:10.1142/9789812831583_0001'
apa: Alur, R., & Henzinger, T. A. (1994). Real-time system = discrete system
+ clock variables. In T. Rus & C. Rattray (Eds.), Theories and Experiences
for Real-Time System Development (Vol. 2, pp. 1–29). World Scientific Publishing.
https://doi.org/10.1142/9789812831583_0001
chicago: Alur, Rajeev, and Thomas A Henzinger. “Real-Time System = Discrete System
+ Clock Variables.” In Theories and Experiences for Real-Time System Development,
edited by Teodor Rus and Charles Rattray, 2:1–29. AMAST Series in Computing. World
Scientific Publishing, 1994. https://doi.org/10.1142/9789812831583_0001.
ieee: R. Alur and T. A. Henzinger, “Real-time system = discrete system + clock variables,”
in Theories and Experiences for Real-Time System Development, vol. 2, T.
Rus and C. Rattray, Eds. World Scientific Publishing, 1994, pp. 1–29.
ista: 'Alur R, Henzinger TA. 1994.Real-time system = discrete system + clock variables.
In: Theories and Experiences for Real-Time System Development. AMAST Series in
Computing, vol. 2, 1–29.'
mla: Alur, Rajeev, and Thomas A. Henzinger. “Real-Time System = Discrete System
+ Clock Variables.” Theories and Experiences for Real-Time System Development,
edited by Teodor Rus and Charles Rattray, vol. 2, World Scientific Publishing,
1994, pp. 1–29, doi:10.1142/9789812831583_0001.
short: R. Alur, T.A. Henzinger, in:, T. Rus, C. Rattray (Eds.), Theories and Experiences
for Real-Time System Development, World Scientific Publishing, 1994, pp. 1–29.
date_created: 2018-12-11T12:09:38Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T08:07:57Z
day: '01'
doi: 10.1142/9789812831583_0001
editor:
- first_name: Teodor
full_name: Rus, Teodor
last_name: Rus
- first_name: Charles
full_name: Rattray, Charles
last_name: Rattray
extern: '1'
intvolume: ' 2'
keyword:
- real-time systems
- clock variables
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/article/10.1007/s100090050007
month: '01'
oa_version: None
page: 1 - 29
publication: Theories and Experiences for Real-Time System Development
publication_identifier:
isbn:
- ' 9789810219239'
publication_status: published
publisher: World Scientific Publishing
publist_id: '117'
quality_controlled: '1'
series_title: AMAST Series in Computing
status: public
title: Real-time system = discrete system + clock variables
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2
year: '1994'
...
---
_id: '4591'
abstract:
- lang: eng
text: 'We introduce a temporal logic for the specification of real-time systems.
Our logic, TPTL, employs a novel quantifier construct for referencing time: the
freeze quantifier binds a variable to the time of the local temporal context.
TPTL is both a natural language for specification and a suitable formalism for
verification. We present a tableau-based decision procedure and a model-checking
algorithm for TPTL. Several generalizations of TPTL are shown to be highly undecidable.'
acknowledgement: "We thank Zohar Manna, Amir Pnueli, and David Dill for their guidance.
Moshe Vardi and Joe Halpern gave us very helpful advice for refining our undecidability
results; in particular, they pointed out to us the completeness of a problem on
Turing machines.\r\n"
article_processing_charge: No
article_type: original
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. A really temporal logic. Journal of the ACM. 1994;41(1):181-204.
doi:10.1145/174644.174651
apa: Alur, R., & Henzinger, T. A. (1994). A really temporal logic. Journal
of the ACM. ACM. https://doi.org/10.1145/174644.174651
chicago: Alur, Rajeev, and Thomas A Henzinger. “A Really Temporal Logic.” Journal
of the ACM. ACM, 1994. https://doi.org/10.1145/174644.174651.
ieee: R. Alur and T. A. Henzinger, “A really temporal logic,” Journal of the
ACM, vol. 41, no. 1. ACM, pp. 181–204, 1994.
ista: Alur R, Henzinger TA. 1994. A really temporal logic. Journal of the ACM. 41(1),
181–204.
mla: Alur, Rajeev, and Thomas A. Henzinger. “A Really Temporal Logic.” Journal
of the ACM, vol. 41, no. 1, ACM, 1994, pp. 181–204, doi:10.1145/174644.174651.
short: R. Alur, T.A. Henzinger, Journal of the ACM 41 (1994) 181–204.
date_created: 2018-12-11T12:09:38Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T08:23:46Z
day: '01'
doi: 10.1145/174644.174651
extern: '1'
intvolume: ' 41'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://dl.acm.org/doi/10.1145/174644.174651
month: '01'
oa_version: None
page: 181 - 204
publication: Journal of the ACM
publication_identifier:
issn:
- 0004-5411
publication_status: published
publisher: ACM
publist_id: '118'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A really temporal logic
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 41
year: '1994'
...
---
_id: '4614'
abstract:
- lang: eng
text: "We develop a theory of equivalences for timed systems. Two systems are equivalent
iff external observers cannot observe differences in their behavior. The notion
of equivalence depends, therefore, on the distinguishing power of the observers.
The power of an observer to measure time results in untimed, clock, and timed
equivalences: an untimed observer cannot measure the time difference between events;
a clock observer uses a clock to measure time differences with finite precision;
a timed observer is able to measure time differences with arbitrary precision.\r\nWe
show that the distinguishing power of clock observers grows with the number of
observers, and approaches, in the limit, the distinguishing power of a timed observer.
More precisely, given any equivalence for untimed systems, two timed systems are
k-clock congruent, for a nonnegative integer k, iff their compositions with every
environment that uses k clocks are untimed equivalent. Both k-clock bisimulation
congruence and k-clock trace congruence form strict decidable hierarchies that
converge towards the corresponding timed equivalences. Moreover, k-clock bisimulation
congruence and k-clock trace congruence provide an adequate and abstract semantics
for branching-time and linear-time logics with k clocks.\r\nOur results impact
on the verification of timed systems in two ways. First, our decision procedure
for k-clock bisimulation congruence leads to a new, symbolic, decision procedure
for timed bisimilarity. Second, timed trace equivalence is known to be undecidable.
If the number of environment clocks is bounded, however, then our decision procedure
for k-clock trace congruence allows the verification of timed systems in a trace
model."
acknowledgement: ESPRIT BRA project REACT, National Science Foundation under grant
CCR-9200794, United States Air Force Office of Scientific Research contract F49620-93-1-0056
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Costas
full_name: Courcoubetis, Costas
last_name: Courcoubetis
- 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, Courcoubetis C, Henzinger TA. The observational power of clocks. In:
5th International Conference on Concurrency Theory. Vol 836. Schloss Dagstuhl
- Leibniz-Zentrum für Informatik; 1994:162-177. doi:10.1007/BFb0015008'
apa: 'Alur, R., Courcoubetis, C., & Henzinger, T. A. (1994). The observational
power of clocks. In 5th International Conference on Concurrency Theory
(Vol. 836, pp. 162–177). Uppsala, Sweden: Schloss Dagstuhl - Leibniz-Zentrum für
Informatik. https://doi.org/10.1007/BFb0015008'
chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “The Observational
Power of Clocks.” In 5th International Conference on Concurrency Theory,
836:162–77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994. https://doi.org/10.1007/BFb0015008.
ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “The observational power of
clocks,” in 5th International Conference on Concurrency Theory, Uppsala,
Sweden, 1994, vol. 836, pp. 162–177.
ista: 'Alur R, Courcoubetis C, Henzinger TA. 1994. The observational power of clocks.
5th International Conference on Concurrency Theory. CONCUR: Concurrency Theory,
LNCS, vol. 836, 162–177.'
mla: Alur, Rajeev, et al. “The Observational Power of Clocks.” 5th International
Conference on Concurrency Theory, vol. 836, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 1994, pp. 162–77, doi:10.1007/BFb0015008.
short: R. Alur, C. Courcoubetis, T.A. Henzinger, in:, 5th International Conference
on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1994,
pp. 162–177.
conference:
end_date: 1994-08-25
location: Uppsala, Sweden
name: 'CONCUR: Concurrency Theory'
start_date: 1994-08-22
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T07:41:46Z
day: '01'
doi: 10.1007/BFb0015008
extern: '1'
intvolume: ' 836'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0015008
month: '01'
oa_version: None
page: 162 - 177
publication: 5th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '3540583297'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '93'
quality_controlled: '1'
status: public
title: The observational power of clocks
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 836
year: '1994'
...
---
_id: '4615'
abstract:
- lang: eng
text: We introduce the class of event- recording timed automata (ERA). An event-recording
automaton contains, for every event a, a clock that records the time of the last
occurrence of a. The class ERA is, on one hand, expressive enough to model (finite)
timed transition systems and, on the other hand, determinizable and closed under
all boolean operations. As a result, the language inclusion problem is decidable
for event-recording automata. We present a translation from timed transition systems
to event-recording automata, which leads to an algorithm for checking if two timed
transition systems have the same set of timed behaviors. We also consider event-predicting
timed automata (EPA), which contain clocks that predict the time of the next occurrence
of an event. The class of event-clock automata (ECA), which contain both event-recording
and event-predicting clocks, is a suitable specification language for real-time
properties. We provide an algorithm for checking if a timed automaton meets a
specification that is given as an event-clock automaton.
acknowledgement: "Supported in part by the Office of Naval Research under contract
N00014-91-J-1219, the National Science Foundation under grant CCR-8701103, and by
DARPA/NSF under grant CCR-9014363.\r\nSupported in part by the National Science
Foundation under grant CCR-9200794 and by the United States Air Force Office of
Scientific Research under contract F49620-93-1-0056."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Limor
full_name: Fix, Limor
last_name: Fix
- 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, Fix L, Henzinger TA. A determinizable class of timed automata. In:
International Conference on Computer Aided Verification. Vol 818. Springer;
1994:1-13. doi:10.1007/3-540-58179-0_39'
apa: 'Alur, R., Fix, L., & Henzinger, T. A. (1994). A determinizable class of
timed automata. In International Conference on Computer Aided Verification
(Vol. 818, pp. 1–13). Stanford, CA, United States of America: Springer. https://doi.org/10.1007/3-540-58179-0_39'
chicago: Alur, Rajeev, Limor Fix, and Thomas A Henzinger. “A Determinizable Class
of Timed Automata.” In International Conference on Computer Aided Verification,
818:1–13. Springer, 1994. https://doi.org/10.1007/3-540-58179-0_39.
ieee: R. Alur, L. Fix, and T. A. Henzinger, “A determinizable class of timed automata,”
in International Conference on Computer Aided Verification, Stanford, CA,
United States of America, 1994, vol. 818, pp. 1–13.
ista: 'Alur R, Fix L, Henzinger TA. 1994. A determinizable class of timed automata.
International Conference on Computer Aided Verification. CAV: Computer Aided Verification,
LNCS, vol. 818, 1–13.'
mla: Alur, Rajeev, et al. “A Determinizable Class of Timed Automata.” International
Conference on Computer Aided Verification, vol. 818, Springer, 1994, pp. 1–13,
doi:10.1007/3-540-58179-0_39.
short: R. Alur, L. Fix, T.A. Henzinger, in:, International Conference on Computer
Aided Verification, Springer, 1994, pp. 1–13.
conference:
end_date: 1994-06-23
location: Stanford, CA, United States of America
name: 'CAV: Computer Aided Verification'
start_date: 1994-06-21
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-01T14:37:25Z
day: '01'
doi: 10.1007/3-540-58179-0_39
extern: '1'
intvolume: ' 818'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-58179-0_39
month: '01'
oa_version: None
page: 1 - 13
publication: International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540484691'
publication_status: published
publisher: Springer
publist_id: '92'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A determinizable class of timed automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 818
year: '1994'
...
---
_id: '4617'
abstract:
- lang: eng
text: 'We extend the timed-automaton model for real-time systems [AD90] to a formal
model for hybrid systems: while the continuous variables of a timed automaton
are clocks that measure time, the continuous variables of a hybrid system are
governed by arbitrary differential equations. We then adopt the verification methodology
for timed automata [ACD90, ACD+92, HNSY92] to analyze hybrid systems: while the
verification problem is decidable for timed automata, we obtain semidecision procedures
for the class of hybrid systems whose continuous variables change in a piecewise
linear fashion. '
alternative_title:
- LNCIS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Costas
full_name: Courcoubetis, Costas
last_name: Courcoubetis
- 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, Henzinger TA, et al. The algorithmic analysis of hybrid
systems. In: 11th International Conference on Analysis and Optimization of
Systems Discrete Event Systems. Vol 199. Springer; 1994:331-351. doi:10.1007/BFb0033565'
apa: 'Alur, R., Courcoubetis, C., Henzinger, T. A., Ho, P., Nicollin, X., Olivero,
A., … Yovine, S. (1994). The algorithmic analysis of hybrid systems. In 11th
International Conference on Analysis and Optimization of Systems Discrete Event
Systems (Vol. 199, pp. 331–351). Sophia-Antipolis, France: Springer. https://doi.org/10.1007/BFb0033565'
chicago: Alur, Rajeev, Costas Courcoubetis, Thomas A Henzinger, Pei Ho, Xavier Nicollin,
Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. “The Algorithmic Analysis
of Hybrid Systems.” In 11th International Conference on Analysis and Optimization
of Systems Discrete Event Systems, 199:331–51. Springer, 1994. https://doi.org/10.1007/BFb0033565.
ieee: R. Alur et al., “The algorithmic analysis of hybrid systems,” in 11th
International Conference on Analysis and Optimization of Systems Discrete Event
Systems, Sophia-Antipolis, France, 1994, vol. 199, pp. 331–351.
ista: 'Alur R, Courcoubetis C, Henzinger TA, Ho P, Nicollin X, Olivero A, Sifakis
J, Yovine S. 1994. The algorithmic analysis of hybrid systems. 11th International
Conference on Analysis and Optimization of Systems Discrete Event Systems. ICAOS:
Analysis and Optimization of Systems - Discrete-Event Systems, LNCIS, vol. 199,
331–351.'
mla: Alur, Rajeev, et al. “The Algorithmic Analysis of Hybrid Systems.” 11th
International Conference on Analysis and Optimization of Systems Discrete Event
Systems, vol. 199, Springer, 1994, pp. 331–51, doi:10.1007/BFb0033565.
short: R. Alur, C. Courcoubetis, T.A. Henzinger, P. Ho, X. Nicollin, A. Olivero,
J. Sifakis, S. Yovine, in:, 11th International Conference on Analysis and Optimization
of Systems Discrete Event Systems, Springer, 1994, pp. 331–351.
conference:
end_date: 1994-06-17
location: Sophia-Antipolis, France
name: 'ICAOS: Analysis and Optimization of Systems - Discrete-Event Systems'
start_date: 1994-06-15
date_created: 2018-12-11T12:09:46Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-01T14:14:31Z
day: '01'
doi: 10.1007/BFb0033565
extern: '1'
intvolume: ' 199'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/BFb0033565
month: '01'
oa_version: None
page: 331 - 351
publication: 11th International Conference on Analysis and Optimization of Systems
Discrete Event Systems
publication_identifier:
isbn:
- 978-3-540-19896-3
publication_status: published
publisher: Springer
publist_id: '91'
quality_controlled: '1'
status: public
title: The algorithmic analysis of hybrid systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 199
year: '1994'
...
---
_id: '2488'
abstract:
- lang: eng
text: Substance P receptor-expressing neurons in the rat cerebral neocortex were
examined by single- and double-immunolabeling methods with an affinity-purified
specific antibody to substance P receptor. Substance P receptor immunoreactivity
was observed exclusively in non-pyramidal neurons. About a quarter of these substance
P receptor-positive neocortical neurons showed intense immunoreactivity, and the
other three quarters displayed weak substance P receptor immunoreactivity. The
neurons showing intense substance P receptor immunoreactivity were large multipolar
cells with a few long aspiny or sparsely-spiny dendrites, and were scattered throughout
the neocortical layers except for layer I, and also in the underlying white matter.
The weakly immunoreactive neurons were medium-sized multipolar cells with oval
to round somata and aspiny varicose dendrites, and were distributed in all cortical
layers with a bias to layers II-III and the superficial part of layer V. The double-immunofluorescence
study revealed that almost all substance P receptor-positive neurons were immunoreactive
for GABA, but negative for glutaminase. Substance P receptor immunoreactivity
in GABAergic neocortical neurons were further examined by the double-immunofluorescence
method with antibodies to markers for subgroups of GABAergic neurons. Somatostatin
immunoreactivity was found in 89% of neurons with intense substance P receptor
immunoreactivity, and in 1.5% of neurons with weak substance P receptor immunoreactivity.
Neuropeptide Y immunoreactivity was also observed in 92% of neurons with intense
immunoreactivity for substance P receptor, and in 1.6% of neurons with weak immunoreactivity
for substance P receptor. In contrast, parvalbumin immunoreactivity was seen in
1.3% of neurons with intense substance P receptor immunoreactivity, and in 59%
of weak substance P receptor immunoreactivity. Calbindin D28k immunoreactivity
was found in 12 and 19% of neurons, respectively, with weak and intense immunoreactivities
for substance P receptor. Virtually no cells showing substance P receptor immunoreactivity
displayed immunoreactivity for vasoactive intestinal polypeptide or choline acetyltransferase.
These results indicate that the neocortical neurons expressing substance P receptor
constitute a subpopulation of GABAergic non-pyramidal cells, and are segregated
into neurons with intense immunoreactivity and those with weak immunoreactivity
for substance P receptor; the vast majority of neurons with intense substance
P receptor immunoreactivity contain somatostatin and neuropeptide Y, and the majority
of neurons with weak substance P receptor immunoreactivity have parvalbumin.
acknowledgement: We are grateful for photographic help of Mr A. Uesugi, and the support
of Drs S. Fukuchi, T. Fukuda, R. Hayashi, M. Katsurada, Y. Kitani, K. Kumagai, H.
Kuroda, H. Matsubara, H. Matsushima, C. Minakuchi, M. Nishio, G. Niwa, H. Ckla,
M. Ohbayashi, S. Ohbayashi, H. Ohtsuka, S. Tamaki, E. Watanabe, K. Yoshino and Y.
Yoshino. This work was supported in part by Grants-in-Aid for Scientific Research
on Priority Areas 05248207 and 05267104, and Scientific Research (B) 05454658 and
(C) 05680658 from the Ministry of Education, Science and Culture of Japan.
article_processing_charge: No
article_type: original
author:
- first_name: Takeshi
full_name: Kaneko, Takeshi
last_name: Kaneko
- 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: Kaneko T, Shigemoto R, Nakanishi S, Mizuno N. Morphological and chemical characteristics
of substance P receptor immunoreactive neurons in the rat neocortex. Neuroscience.
1994;60(1):199-211. doi:10.1016/0306-4522(94)90215-1
apa: Kaneko, T., Shigemoto, R., Nakanishi, S., & Mizuno, N. (1994). Morphological
and chemical characteristics of substance P receptor immunoreactive neurons in
the rat neocortex. Neuroscience. Elsevier. https://doi.org/10.1016/0306-4522(94)90215-1
chicago: Kaneko, Takeshi, Ryuichi Shigemoto, Shigetada Nakanishi, and Noboru Mizuno.
“Morphological and Chemical Characteristics of Substance P Receptor Immunoreactive
Neurons in the Rat Neocortex.” Neuroscience. Elsevier, 1994. https://doi.org/10.1016/0306-4522(94)90215-1.
ieee: T. Kaneko, R. Shigemoto, S. Nakanishi, and N. Mizuno, “Morphological and chemical
characteristics of substance P receptor immunoreactive neurons in the rat neocortex,”
Neuroscience, vol. 60, no. 1. Elsevier, pp. 199–211, 1994.
ista: Kaneko T, Shigemoto R, Nakanishi S, Mizuno N. 1994. Morphological and chemical
characteristics of substance P receptor immunoreactive neurons in the rat neocortex.
Neuroscience. 60(1), 199–211.
mla: Kaneko, Takeshi, et al. “Morphological and Chemical Characteristics of Substance
P Receptor Immunoreactive Neurons in the Rat Neocortex.” Neuroscience,
vol. 60, no. 1, Elsevier, 1994, pp. 199–211, doi:10.1016/0306-4522(94)90215-1.
short: T. Kaneko, R. Shigemoto, S. Nakanishi, N. Mizuno, Neuroscience 60 (1994)
199–211.
date_created: 2018-12-11T11:57:58Z
date_published: 1994-05-01T00:00:00Z
date_updated: 2022-06-09T12:22:16Z
day: '01'
doi: 10.1016/0306-4522(94)90215-1
extern: '1'
external_id:
pmid:
- '8052413'
intvolume: ' 60'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/0306452294902151?via%3Dihub
month: '05'
oa_version: None
page: 199 - 211
pmid: 1
publication: Neuroscience
publication_identifier:
issn:
- 0306-4522
publication_status: published
publisher: Elsevier
publist_id: '4413'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Morphological and chemical characteristics of substance P receptor immunoreactive
neurons in the rat neocortex
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 60
year: '1994'
...
---
_id: '2489'
abstract:
- lang: eng
text: 'Five N-methyl-D-aspartate (NMDA) receptor subunits have been identified thus
far: NR1, NR2A, NR2B, NR2C, and NR2D. Here, we have analyzed the expression patterns
of mRNAs for the NMDA receptor subunits in the developing and adult rats by in
situ hybridization. The developmental changes of the expression patterns were
most salient in the cerebellum. In the external granular layer, hybridization
signals of mRNAs for NR1, NR2A, NR2B, and NR2C appeared by postnatal day 3, but
no NR2D mRNA was expressed at any developmental stage examined. The NR1 mRNA was
expressed in all cerebellar neurons at all developmental stages examined. The
signals for the NR2A mRNA appeared in Purkinje cells and granule cells during
the second postnatal week. The signals for the NR2B mRNA in granule cells were
seen transiently during the first 2 weeks after birth. The signals for NR2C mRNA
appeared in granule cells and glial cells during the second postnatal week. The
signals for NR2D mRNA appeared transiently in Purkinje cells during the first
8 postnatal days; in adult rats, these were seen in stellate and Golgi cells.
In the cerebellar nuclei, mRNAs for NR1, NR2A, NR2B, and NR2D were more or less
expressed on postnatal day 0, while expression signals for the NR2C mRNA were
first detected in postnatal day 14. Thus, the most conspicuous changes of expression
patterns were observed in the cerebellar cortex during the first 2 weeks after
birth, when development and maturation of the cerebellum proceed most rapidly.'
acknowledgement: We are grateful to Mr. Akira Uesugi for photographic help and
for the support of Drs. Satoru Fukuchi, Toshio Fukuda, Ritsu Hayashi, Mizuho Katsurada,
Yutaka Kitani, Keiko Kumagai, Toshihiko Kuroda, Hiroshi Matsubara, Hiroshi Matsushima,
Chisato Minakuchi, Masatoshi Nishio, Gonpei Niwa Hajime Oda, Masahiko Ohbayashi,
Sei-ichi Ohbayashi, Hiroyasu Ohtsuka, Shigeo Tamaki, Eizo Watan- abe, Kazuo Yoshino,
and Toshiaki Yoshino. This work was 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: 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: Yasumasa
full_name: Bessho, Yasumasa
last_name: Bessho
- first_name: Shigetada
full_name: Nakanishi, Shigetada
last_name: Nakanishi
- first_name: Noboru
full_name: Mizuno, Noboru
last_name: Mizuno
citation:
ama: Akazawa C, Shigemoto R, Bessho Y, Nakanishi S, Mizuno N. Differential expression
of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum of developing
and adult rats. Journal of Comparative Neurology. 1994;347(1):150-160.
doi:10.1002/cne.903470112
apa: Akazawa, C., Shigemoto, R., Bessho, Y., Nakanishi, S., & Mizuno, N. (1994).
Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs in
the cerebellum of developing and adult rats. Journal of Comparative Neurology.
Wiley-Blackwell. https://doi.org/10.1002/cne.903470112
chicago: Akazawa, Chihiro, Ryuichi Shigemoto, Yasumasa Bessho, Shigetada Nakanishi,
and Noboru Mizuno. “Differential Expression of Five N-Methyl-D-Aspartate Receptor
Subunit MRNAs in the Cerebellum of Developing and Adult Rats.” Journal of Comparative
Neurology. Wiley-Blackwell, 1994. https://doi.org/10.1002/cne.903470112.
ieee: C. Akazawa, R. Shigemoto, Y. Bessho, S. Nakanishi, and N. Mizuno, “Differential
expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum
of developing and adult rats,” Journal of Comparative Neurology, vol. 347,
no. 1. Wiley-Blackwell, pp. 150–160, 1994.
ista: Akazawa C, Shigemoto R, Bessho Y, Nakanishi S, Mizuno N. 1994. Differential
expression of five N-methyl-D-aspartate receptor subunit mRNAs in the cerebellum
of developing and adult rats. Journal of Comparative Neurology. 347(1), 150–160.
mla: Akazawa, Chihiro, et al. “Differential Expression of Five N-Methyl-D-Aspartate
Receptor Subunit MRNAs in the Cerebellum of Developing and Adult Rats.” Journal
of Comparative Neurology, vol. 347, no. 1, Wiley-Blackwell, 1994, pp. 150–60,
doi:10.1002/cne.903470112.
short: C. Akazawa, R. Shigemoto, Y. Bessho, S. Nakanishi, N. Mizuno, Journal of
Comparative Neurology 347 (1994) 150–160.
date_created: 2018-12-11T11:57:58Z
date_published: 1994-09-01T00:00:00Z
date_updated: 2022-06-09T12:11:20Z
day: '01'
doi: 10.1002/cne.903470112
extern: '1'
external_id:
pmid:
- '7798379'
intvolume: ' 347'
issue: '1'
language:
- iso: eng
main_file_link:
- url: https://onlinelibrary.wiley.com/doi/10.1002/cne.903470112
month: '09'
oa_version: None
page: 150 - 160
pmid: 1
publication: Journal of Comparative Neurology
publication_identifier:
issn:
- 0021-9967
publication_status: published
publisher: Wiley-Blackwell
publist_id: '4412'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Differential expression of five N-methyl-D-aspartate receptor subunit mRNAs
in the cerebellum of developing and adult rats
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 347
year: '1994'
...
---
_id: '2490'
abstract:
- lang: eng
text: Distribution of the messenger RNA for the prostaglandin E receptor subtype
EP3 was investigated by in situ hybridization in the nervous system of the mouse.
The hybridization signals for EP3 were widely distributed in the brain and sensory
ganglia and specifically localized to neurons. In the dorsal root and trigeminal
ganglia, about half of the neurons were labeled intensely. In the brain, intensely
labeled neurons were found in Ammon's horn, the preoptic nuclei, lateral hypothalamic
area, dorsomedial hypothalamic nucleus, lateral mammillary nucleus, entopeduncular
nucleus, substantia nigra pars compacta, locus coeruleus and raphe nuclei. Moderately
labeled neurons were seen in the mitral cell layer of the main olfactory bulb,
layer V of the entorhinal and parasubicular cortices, layers V and VI of the cerebral
neocortex, nuclei of the diagonal band, magnocellular preoptic nucleus, globus
pallidus and lateral parabrachial nucleus. In the thalamus, moderately labeled
neurons were distributed in the anterior, ventromedial, laterodorsal, paraventricular
and central medial nuclei. Based on these distributions, we suggest that EP3 not
only mediates prostaglandin E2 signals evoked by blood-borne cytokines in the
areas poor in the blood-brain barrier, but also responds to those formed intrinsically
within the brain to modulate various neuronal activities. Possible EP3 actions
are discussed in relation to the reported neuronal activities of prostaglandin
E2 in the brain.
acknowledgement: 'This work was supported in part by Grants-in-aid for Scientific
Research 05404020, 04255103. 05771975, 05671816 and 05454568 from the Ministry of
Education, Science and Culture of Japan and by grants from the Mitsubishi Foundation
and the Takeda Science Foundation. We are grateful to Mr Akira Uesugi for photographic
help. We also thank Drs Chihiro Akazawa, Hitoshi Ohishi and Masabumi Minami for
helpful discussions. '
article_processing_charge: No
article_type: original
author:
- first_name: Yukihiko
full_name: Sugimoto, Yukihiko
last_name: Sugimoto
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
- first_name: Tsunehisa
full_name: Namba, Tsunehisa
last_name: Namba
- first_name: Manabu
full_name: Negishi, Manabu
last_name: Negishi
- first_name: Noboru
full_name: Mizuno, Noboru
last_name: Mizuno
- first_name: Shuh
full_name: Narumiya, Shuh
last_name: Narumiya
- first_name: Atsushi
full_name: Ichikawa, Atsushi
last_name: Ichikawa
citation:
ama: Sugimoto Y, Shigemoto R, Namba T, et al. Distribution of the messenger rna
for the prostaglandin e receptor subtype ep3 in the mouse nervous system. Neuroscience.
1994;62(3):919-928. doi:10.1016/0306-4522(94)90483-9
apa: Sugimoto, Y., Shigemoto, R., Namba, T., Negishi, M., Mizuno, N., Narumiya,
S., & Ichikawa, A. (1994). Distribution of the messenger rna for the prostaglandin
e receptor subtype ep3 in the mouse nervous system. Neuroscience. Elsevier.
https://doi.org/10.1016/0306-4522(94)90483-9
chicago: Sugimoto, Yukihiko, Ryuichi Shigemoto, Tsunehisa Namba, Manabu Negishi,
Noboru Mizuno, Shuh Narumiya, and Atsushi Ichikawa. “Distribution of the Messenger
Rna for the Prostaglandin e Receptor Subtype Ep3 in the Mouse Nervous System.”
Neuroscience. Elsevier, 1994. https://doi.org/10.1016/0306-4522(94)90483-9.
ieee: Y. Sugimoto et al., “Distribution of the messenger rna for the prostaglandin
e receptor subtype ep3 in the mouse nervous system,” Neuroscience, vol.
62, no. 3. Elsevier, pp. 919–928, 1994.
ista: Sugimoto Y, Shigemoto R, Namba T, Negishi M, Mizuno N, Narumiya S, Ichikawa
A. 1994. Distribution of the messenger rna for the prostaglandin e receptor subtype
ep3 in the mouse nervous system. Neuroscience. 62(3), 919–928.
mla: Sugimoto, Yukihiko, et al. “Distribution of the Messenger Rna for the Prostaglandin
e Receptor Subtype Ep3 in the Mouse Nervous System.” Neuroscience, vol.
62, no. 3, Elsevier, 1994, pp. 919–28, doi:10.1016/0306-4522(94)90483-9.
short: Y. Sugimoto, R. Shigemoto, T. Namba, M. Negishi, N. Mizuno, S. Narumiya,
A. Ichikawa, Neuroscience 62 (1994) 919–928.
date_created: 2018-12-11T11:57:58Z
date_published: 1994-10-01T00:00:00Z
date_updated: 2022-06-09T11:56:23Z
day: '01'
doi: 10.1016/0306-4522(94)90483-9
extern: '1'
external_id:
pmid:
- '7870313'
intvolume: ' 62'
issue: '3'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/0306452294904839?via%3Dihub
month: '10'
oa_version: None
page: 919 - 928
pmid: 1
publication: Neuroscience
publication_identifier:
issn:
- 0306-4522
publication_status: published
publisher: Elsevier
publist_id: '4411'
quality_controlled: '1'
status: public
title: Distribution of the messenger rna for the prostaglandin e receptor subtype
ep3 in the mouse nervous system
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 62
year: '1994'
...
---
_id: '2545'
abstract:
- lang: eng
text: 'Glutamate receptors play an important role in many integrative brain functions
and in neuronal development. We report the molecular diversity of NMDA receptors
and metabotropic glutamate receptors on the basis of our studies of molecular
cloning and characterization of the diverse members of these receptors. The NMDA
receptors consist of two distinct types of subunits. NMDAR1 possesses all properties
characteristic of the NMDA receptor-channel complex, whereas the four NMDAR2 subunits,
termed NMDAR2A-2D, show no channel activity but potentiate the NMDAR1 activity
and confer functional variability by different heteromeric formations. The NMDA
receptor subunits are considerably divergent from the other ligand-gated ion channels,
and the structural architecture of these subunits remains elusive. The mGluRs
form a family of at least seven different subtypes termed mGluR1-mGluR7. These
receptor subtypes have, seven transmembrane segments and possess a large extracellular
domain at their N-terminal regions. The seven mGluR subtypes are classified into
three subgroups according to their sequence similarities, signal transduction
mechanisms and agonist selectivities: mGluR1/mGluR5, mGluR2/mGluR3 and mGluR4/mGluR6/mGluR7.
On the basis of our knowledge of the molecular diversity of the NMDA receptors
and mGluRs, we have studied the physiological roles of individual receptor subunits
or subtypes. We have shown that K(+)-induced depolarization or NMDA treatment
in primary cultures of neonatal cerebellar granule cells induces the functional
NMDA receptor and specifically up-regulates NMDAR2A mRNA among the multiple NMDA
receptor subunits through the increase in resting intracellular Ca2+ concentrations.
Our study demonstrates that the regulation of the specific NMDA receptor subunit
mRNA governs the NMDA receptor induction that is thought to play an important
role in granule cell survival and death. Analysis of an agonist selectivity and
an expression pattern of mGluR6 has indicated that mGluR6 is responsible for synaptic
neurotransmission from photoreceptor cells to ON-bipolar cells in the visual system.
We have also investigated the function of mGluR2 in granule cells of the accessory
olfactory bulb by combining immunoelectron-microscopic analysis with slice-patch
recordings on the basis of the identification of a new agonist selective for this
receptor subtype. Our results demonstrate that mGluR2 is present at the presynaptic
site of granule cells and modulates inhibitory GABA transmission from granule
cells to mitral cells. This finding indicates that the mGluR2 activation relieves
excited mitral cells from GABA inhibition but maintains the lateral inhibition
of unexcited mitral cells, thus resulting in enhancement of the signal-to-noise
ratio between the excited mitral cells and their neighboring unexcited mitral
cells.'
article_processing_charge: No
author:
- first_name: Shigetada
full_name: Nakanishi, Shigetada
last_name: Nakanishi
- first_name: Masayuki
full_name: Masu, Masayuki
last_name: Masu
- first_name: Yasumasa
full_name: Bessho, Yasumasa
last_name: Bessho
- first_name: Yoshiaki
full_name: Nakajima, Yoshiaki
last_name: Nakajima
- first_name: Yasunori
full_name: Hayashi, Yasunori
last_name: Hayashi
- first_name: Ryuichi
full_name: Shigemoto, Ryuichi
id: 499F3ABC-F248-11E8-B48F-1D18A9856A87
last_name: Shigemoto
orcid: 0000-0001-8761-9444
citation:
ama: 'Nakanishi S, Masu M, Bessho Y, Nakajima Y, Hayashi Y, Shigemoto R. Molecular
diversity of glutamate receptors and their physiological functions. In: Experientia
Supplementum. Vol 71. Birkhäuser; 1994:71-80. doi:10.1007/978-3-0348-7330-7_8'
apa: Nakanishi, S., Masu, M., Bessho, Y., Nakajima, Y., Hayashi, Y., & Shigemoto,
R. (1994). Molecular diversity of glutamate receptors and their physiological
functions. In Experientia Supplementum (Vol. 71, pp. 71–80). Birkhäuser.
https://doi.org/10.1007/978-3-0348-7330-7_8
chicago: Nakanishi, Shigetada, Masayuki Masu, Yasumasa Bessho, Yoshiaki Nakajima,
Yasunori Hayashi, and Ryuichi Shigemoto. “Molecular Diversity of Glutamate Receptors
and Their Physiological Functions.” In Experientia Supplementum, 71:71–80.
Birkhäuser, 1994. https://doi.org/10.1007/978-3-0348-7330-7_8.
ieee: S. Nakanishi, M. Masu, Y. Bessho, Y. Nakajima, Y. Hayashi, and R. Shigemoto,
“Molecular diversity of glutamate receptors and their physiological functions,”
in Experientia Supplementum, vol. 71, Birkhäuser, 1994, pp. 71–80.
ista: 'Nakanishi S, Masu M, Bessho Y, Nakajima Y, Hayashi Y, Shigemoto R. 1994.Molecular
diversity of glutamate receptors and their physiological functions. In: Experientia
Supplementum. vol. 71, 71–80.'
mla: Nakanishi, Shigetada, et al. “Molecular Diversity of Glutamate Receptors and
Their Physiological Functions.” Experientia Supplementum, vol. 71, Birkhäuser,
1994, pp. 71–80, doi:10.1007/978-3-0348-7330-7_8.
short: S. Nakanishi, M. Masu, Y. Bessho, Y. Nakajima, Y. Hayashi, R. Shigemoto,
in:, Experientia Supplementum, Birkhäuser, 1994, pp. 71–80.
date_created: 2018-12-11T11:58:18Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-09T10:08:24Z
day: '01'
doi: 10.1007/978-3-0348-7330-7_8
extern: '1'
external_id:
pmid:
- '8032174'
intvolume: ' 71'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/978-3-0348-7330-7_8
month: '01'
oa_version: None
page: 71 - 80
pmid: 1
publication: Experientia Supplementum
publication_identifier:
isbn:
- '9783034873321'
publication_status: published
publisher: Birkhäuser
publist_id: '4352'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Molecular diversity of glutamate receptors and their physiological functions
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 71
year: '1994'
...