---
_id: '3515'
abstract:
- lang: eng
text: Oscillations in neuronal networks are assumed to serve various physiological
functions, from coordination of motor patterns to perceptual binding of sensory
information. Here, we describe an ultra-slow oscillation (0.025 Hz) in the hippocampus.
Extracellular and intracellular activity was recorded from the CA1 and subicular
regions in rats of the Wistar and Sprague-Dawley strains. anesthetized with urethane.
in a subgroup of Wistar rats (23%), spontaneous afterdischarges (4.7 +/- 1.6 s)
occurred regularly at 40.8 +/- 15.7 s. The afterdischarge was initiated by a fast
increase of population synchrony (100-250 Hz oscillation; “tonic” phase), followed
by large-amplitude rhythmic waves and associated action potentials at gamma and
beta frequency (15-50 Hz; “clonic” phase). The afterdischarges were bilaterally
synchronous and terminated relatively abruptly without post-ictal depression.
Single-pulse stimulation of the commissural input could trigger afterdischarges,
but only at times when they were about to occur. Commissural stimulation evoked
inhibitory postsynaptic potentials in pyramidal cells. However, when the stimulus
triggered an afterdischarge, the inhibitory postsynaptic potential was absent
and the cells remained depolarized during most of the afterdischarge. Afterdischarges
were not observed in the Sprague-Dawley rats. Long-term analysis of interneuronal
activity in intact, drug-free rats also revealed periodic excitability changes
in the hippocampal network at 0.025 Hz. These findings indicate the presence of
an ultra-slow oscillation in the hippocampal formation. The ultra-slow clock induced
afterdischarges in susceptible animals. We hypothesize that a transient failure
of GABAergic inhibition in a subset of Wistar rats is responsible for the emergence
of epileptiform patterns. (C) 1999 IBRO. Published by Elsevier Science Ltd.
acknowledgement: This work was supported by the Academy of Finland (32391) and the
NIH (NS34994, MH54671).
article_processing_charge: No
article_type: original
author:
- first_name: Markku
full_name: Penttonen, Markku
last_name: Penttonen
- first_name: Nina
full_name: Nurminen, Nina
last_name: Nurminen
- first_name: Riitta
full_name: Miettinen, Riitta
last_name: Miettinen
- first_name: Jouni
full_name: Sirviö, Jouni
last_name: Sirviö
- first_name: Darrell
full_name: Henze, Darrell
last_name: Henze
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Penttonen M, Nurminen N, Miettinen R, et al. Ultra-slow oscillation (0.025
Hz) triggers hippocampal afterdischarges in Wistar rats. Neuroscience.
1999;94(3):735-743. doi:10.1016/S0306-4522(99)00367-X
apa: Penttonen, M., Nurminen, N., Miettinen, R., Sirviö, J., Henze, D., Csicsvari,
J. L., & Buzsáki, G. (1999). Ultra-slow oscillation (0.025 Hz) triggers hippocampal
afterdischarges in Wistar rats. Neuroscience. Elsevier. https://doi.org/10.1016/S0306-4522(99)00367-X
chicago: Penttonen, Markku, Nina Nurminen, Riitta Miettinen, Jouni Sirviö, Darrell
Henze, Jozsef L Csicsvari, and György Buzsáki. “Ultra-Slow Oscillation (0.025
Hz) Triggers Hippocampal Afterdischarges in Wistar Rats.” Neuroscience.
Elsevier, 1999. https://doi.org/10.1016/S0306-4522(99)00367-X.
ieee: M. Penttonen et al., “Ultra-slow oscillation (0.025 Hz) triggers hippocampal
afterdischarges in Wistar rats,” Neuroscience, vol. 94, no. 3. Elsevier,
pp. 735–743, 1999.
ista: Penttonen M, Nurminen N, Miettinen R, Sirviö J, Henze D, Csicsvari JL, Buzsáki
G. 1999. Ultra-slow oscillation (0.025 Hz) triggers hippocampal afterdischarges
in Wistar rats. Neuroscience. 94(3), 735–743.
mla: Penttonen, Markku, et al. “Ultra-Slow Oscillation (0.025 Hz) Triggers Hippocampal
Afterdischarges in Wistar Rats.” Neuroscience, vol. 94, no. 3, Elsevier,
1999, pp. 735–43, doi:10.1016/S0306-4522(99)00367-X.
short: M. Penttonen, N. Nurminen, R. Miettinen, J. Sirviö, D. Henze, J.L. Csicsvari,
G. Buzsáki, Neuroscience 94 (1999) 735–743.
date_created: 2018-12-11T12:03:44Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-07T13:16:01Z
day: '01'
doi: 10.1016/S0306-4522(99)00367-X
extern: '1'
external_id:
pmid:
- '10579564'
intvolume: ' 94'
issue: '3'
language:
- iso: eng
month: '10'
oa_version: None
page: 735 - 743
pmid: 1
publication: Neuroscience
publication_identifier:
issn:
- 0306-4522
publication_status: published
publisher: Elsevier
publist_id: '2870'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Ultra-slow oscillation (0.025 Hz) triggers hippocampal afterdischarges in Wistar
rats
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 94
year: '1999'
...
---
_id: '3518'
abstract:
- lang: eng
text: Information in neuronal networks may be represented by the spatiotemporal
patterns of spikes. Here we examined the temporal coordination of pyramidal cell
spikes in the rat hippocampus during slow-wave sleep. In addition, rats were trained
to run in a defined position in space (running wheel) to activate a selected group
of pyramidal cells. A template-matching method and a joint probability map method
were used for sequence search. Repeating spike sequences in excess of chance occurrence
were examined by comparing the number of repeating sequences in the original spike
trains and in surrogate trains after Monte Carlo shuffling of the spikes. Four
different shuffling procedures were used to control for the population dynamics
of hippocampal neurons. Repeating spike sequences in the recorded cell assemblies
were present in both the awake and sleeping animal in excess of what might be
predicted by random variations. Spike sequences observed during wheel running
were “replayed” at a faster timescale during single sharp-wave bursts of slow-wave
sleep. We hypothesize that the endogenously expressed spike sequences during sleep
reflect reactivation of the circuitry modified by previous experience. Reactivation
of acquired sequences may serve to consolidate information.
acknowledgement: This work was supported by National Institutes of Health Grants NS34994
and MH54671 and by the Human Science Frontier Program. We thank Moshe Abeles, Michale
Fee, Stuart Geman, Stephen Hanson, Darrell Henze, Günther Palm, Michael Recce, and
Matthew Wilson for their suggestions with data analysis and comments on this manuscript.
article_processing_charge: No
article_type: original
author:
- first_name: Zoltán
full_name: Nádasdy, Zoltán
last_name: Nádasdy
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: András
full_name: Czurkó, András
last_name: Czurkó
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Nádasdy Z, Hirase H, Czurkó A, Csicsvari JL, Buzsáki G. Replay and time compression
of recurring spike sequences in the hippocampus. Journal of Neuroscience.
1999;19(21):9497-9507. doi:10.1523/JNEUROSCI.19-21-09497.1999
apa: Nádasdy, Z., Hirase, H., Czurkó, A., Csicsvari, J. L., & Buzsáki, G. (1999).
Replay and time compression of recurring spike sequences in the hippocampus. Journal
of Neuroscience. Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.19-21-09497.1999
chicago: Nádasdy, Zoltán, Hajima Hirase, András Czurkó, Jozsef L Csicsvari, and
György Buzsáki. “Replay and Time Compression of Recurring Spike Sequences in the
Hippocampus.” Journal of Neuroscience. Society for Neuroscience, 1999.
https://doi.org/10.1523/JNEUROSCI.19-21-09497.1999.
ieee: Z. Nádasdy, H. Hirase, A. Czurkó, J. L. Csicsvari, and G. Buzsáki, “Replay
and time compression of recurring spike sequences in the hippocampus,” Journal
of Neuroscience, vol. 19, no. 21. Society for Neuroscience, pp. 9497–9507,
1999.
ista: Nádasdy Z, Hirase H, Czurkó A, Csicsvari JL, Buzsáki G. 1999. Replay and time
compression of recurring spike sequences in the hippocampus. Journal of Neuroscience.
19(21), 9497–9507.
mla: Nádasdy, Zoltán, et al. “Replay and Time Compression of Recurring Spike Sequences
in the Hippocampus.” Journal of Neuroscience, vol. 19, no. 21, Society
for Neuroscience, 1999, pp. 9497–507, doi:10.1523/JNEUROSCI.19-21-09497.1999.
short: Z. Nádasdy, H. Hirase, A. Czurkó, J.L. Csicsvari, G. Buzsáki, Journal of
Neuroscience 19 (1999) 9497–9507.
date_created: 2018-12-11T12:03:45Z
date_published: 1999-11-01T00:00:00Z
date_updated: 2022-09-07T12:48:08Z
day: '01'
doi: 10.1523/JNEUROSCI.19-21-09497.1999
extern: '1'
external_id:
pmid:
- '10531452'
intvolume: ' 19'
issue: '21'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6782894/
month: '11'
oa: 1
oa_version: Published Version
page: 9497 - 9507
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2866'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Replay and time compression of recurring spike sequences in the hippocampus
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 19
year: '1999'
...
---
_id: '3519'
abstract:
- lang: eng
text: 'In contrast to sensory cortical areas of the brain, the relevant physiological
inputs to the hippocampus, leading to selective activation of pyramidal cells,
are largely unknown. Pyramidal cells are thought to be phasically activated by
spatial cues and a variety of sensory and motor stimuli. Here, we used a behavioural
`space clamp'' method, which involved the confinement of the actively running
animal in a defined position in space (running wheel) and kept sensory inputs
constant. Twelve percent of the recorded CA1 pyramidal cells were selectively
active while the rat was running in the wheel. Cell firing was specific to the
direction of running and disappeared after rotating the recording apparatus. The
discharge frequency of pyramidal cells and interneurons was sustained as long
as the rat ran continuously in the wheel. Furthermore, the discharge frequency
of pyramidal cells and interneurons increased with increasing running velocity,
even though the frequency of hippocampal theta waves remained constant. The discharge
frequency of some `wheel-related'' pyramidal cells could increase more than 10-fold
between 10 and 100 cm/s, whereas the firing rate of `non-wheel'' cells remained
constantly low. We hypothesize that: (i) a necessary condition for place-specific
discharge of hippocampal pyramidal cells is the presence of theta oscillation;
and (ii) relevant stimuli can tonically and selectively activate hippocampal pyramidal
cells as long as theta activity is present.'
acknowledgement: We thank M. Recce for continuous support, A. Berthoz for advice,
K. Moorefor his participation in the early stages of the experiments, J. Lee for helpand
C. King for his comments on the manuscript. This work was supportedby NIH (NS34994,
MH54671), the Human Frontier Science Program (H.H.),the Hungarian Eo ̈tvo ̈s State
Fellowship (A.C.) and the Soros Foundation (A.C.)
article_processing_charge: No
article_type: original
author:
- first_name: András
full_name: Czurkó, András
last_name: Czurkó
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Czurkó A, Hirase H, Csicsvari JL, Buzsáki G. Sustained activation of hippocampal
pyramidal cells by ‘space clamping’’ in a running wheel.’ European Journal
of Neuroscience. 1999;11(1):344-352. doi:10.1046/j.1460-9568.1999.00446.x
apa: Czurkó, A., Hirase, H., Csicsvari, J. L., & Buzsáki, G. (1999). Sustained
activation of hippocampal pyramidal cells by ‘space clamping’’ in a running wheel.’
European Journal of Neuroscience. Wiley-Blackwell. https://doi.org/10.1046/j.1460-9568.1999.00446.x
chicago: Czurkó, András, Hajima Hirase, Jozsef L Csicsvari, and György Buzsáki.
“Sustained Activation of Hippocampal Pyramidal Cells by ‘space Clamping’’ in a
Running Wheel.’” European Journal of Neuroscience. Wiley-Blackwell, 1999.
https://doi.org/10.1046/j.1460-9568.1999.00446.x.
ieee: A. Czurkó, H. Hirase, J. L. Csicsvari, and G. Buzsáki, “Sustained activation
of hippocampal pyramidal cells by ‘space clamping’’ in a running wheel,’” European
Journal of Neuroscience, vol. 11, no. 1. Wiley-Blackwell, pp. 344–352, 1999.
ista: Czurkó A, Hirase H, Csicsvari JL, Buzsáki G. 1999. Sustained activation of
hippocampal pyramidal cells by ‘space clamping’’ in a running wheel’. European
Journal of Neuroscience. 11(1), 344–352.
mla: Czurkó, András, et al. “Sustained Activation of Hippocampal Pyramidal Cells
by ‘space Clamping’’ in a Running Wheel.’” European Journal of Neuroscience,
vol. 11, no. 1, Wiley-Blackwell, 1999, pp. 344–52, doi:10.1046/j.1460-9568.1999.00446.x.
short: A. Czurkó, H. Hirase, J.L. Csicsvari, G. Buzsáki, European Journal of Neuroscience
11 (1999) 344–352.
date_created: 2018-12-11T12:03:45Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-07T13:09:08Z
day: '01'
doi: 10.1046/j.1460-9568.1999.00446.x
extern: '1'
external_id:
pmid:
- '9987037'
intvolume: ' 11'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 344 - 352
pmid: 1
publication: European Journal of Neuroscience
publication_identifier:
issn:
- 0953-816X
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2867'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Sustained activation of hippocampal pyramidal cells by ‘space clamping' in
a running wheel
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 11
year: '1999'
...
---
_id: '3524'
abstract:
- lang: eng
text: We examined whether excitation and inhibition are balanced in hippocampal
cortical networks. Extracellular field and single-unit activity were recorded
by multiple tetrodes and multisite silicon probes to reveal the timing of the
activity of hippocampal CAI pyramidal cells and classes of interneurons during
theta waves and sharp wave burst (SPW)-associated field ripples. The somatic and
dendritic inhibition of pyramidal cells was deduced from the activity of interneurons
in the pyramidal layer [int(p)] and in the alveus and st. oriens [int(a/o)], respectively.
int(p) and int(a/o) discharged an average of 60 and 20 degrees before the population
discharge of pyramidal cells during the theta cycle, respectively. SPW ripples
were associated with a 2.5-fold net increase of excitation. The discharge frequency
of int(a/o) increased, decreased (”anti-SPW” cells), or did not change (”SPW-independent”
cells) during SPW suggesting that not all interneurons are innervated by pyramidal
cells. Int(p) either fired together with (unimodal cells) or both before and after
(bimodal cells) the pyramidal cell burst. During fast-ripple oscillation, the
activity of interneurons in both the int(p) and int(a/o) groups lagged the maximum
discharge probability of pyramidal neurons by 1-2 msec. Network state changes,
as reflected by field activity, covaried with changes in the spike train dynamics
of single cells and their interactions. Summed activity of parallel-recorded interneurons,
but not of pyramidal cells, reliably predicted theta cycles, whereas the reverse
was true for the ripple cycles of SPWs. We suggest that network-driven excitability
changes provide temporal windows of opportunity for single pyramidal cells to
suppress, enable, or facilitate selective synaptic inputs.
acknowledgement: This work was supported by National Institutes of Health Grants NS34994,
MH54671, and 1P41RR09754 and by the Human Frontier Science Program. We thank Darrell
A. Henze and M. Recce for their comments on this manuscript and Jamie Hetke and
Ken Wise for supplying us with silicon probes.
article_processing_charge: No
article_type: original
author:
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: András
full_name: Czurkó, András
last_name: Czurkó
- first_name: Akira
full_name: Mamiya, Akira
last_name: Mamiya
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Csicsvari JL, Hirase H, Czurkó A, Mamiya A, Buzsáki G. Oscillatory coupling
of hippocampal pyramidal cells and interneurons in the behaving rat. Journal
of Neuroscience. 1999;19(1):274-287. doi:10.1523/JNEUROSCI.19-01-00274.1999
apa: Csicsvari, J. L., Hirase, H., Czurkó, A., Mamiya, A., & Buzsáki, G. (1999).
Oscillatory coupling of hippocampal pyramidal cells and interneurons in the behaving
rat. Journal of Neuroscience. Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.19-01-00274.1999
chicago: Csicsvari, Jozsef L, Hajima Hirase, András Czurkó, Akira Mamiya, and György
Buzsáki. “Oscillatory Coupling of Hippocampal Pyramidal Cells and Interneurons
in the Behaving Rat.” Journal of Neuroscience. Society for Neuroscience,
1999. https://doi.org/10.1523/JNEUROSCI.19-01-00274.1999.
ieee: J. L. Csicsvari, H. Hirase, A. Czurkó, A. Mamiya, and G. Buzsáki, “Oscillatory
coupling of hippocampal pyramidal cells and interneurons in the behaving rat,”
Journal of Neuroscience, vol. 19, no. 1. Society for Neuroscience, pp.
274–287, 1999.
ista: Csicsvari JL, Hirase H, Czurkó A, Mamiya A, Buzsáki G. 1999. Oscillatory coupling
of hippocampal pyramidal cells and interneurons in the behaving rat. Journal of
Neuroscience. 19(1), 274–287.
mla: Csicsvari, Jozsef L., et al. “Oscillatory Coupling of Hippocampal Pyramidal
Cells and Interneurons in the Behaving Rat.” Journal of Neuroscience, vol.
19, no. 1, Society for Neuroscience, 1999, pp. 274–87, doi:10.1523/JNEUROSCI.19-01-00274.1999.
short: J.L. Csicsvari, H. Hirase, A. Czurkó, A. Mamiya, G. Buzsáki, Journal of Neuroscience
19 (1999) 274–287.
date_created: 2018-12-11T12:03:47Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-07T10:00:45Z
day: '01'
doi: 10.1523/JNEUROSCI.19-01-00274.1999
extern: '1'
external_id:
pmid:
- '9870957'
intvolume: ' 19'
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6782375/
month: '01'
oa: 1
oa_version: Published Version
page: 274 - 287
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2860'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Oscillatory coupling of hippocampal pyramidal cells and interneurons in the
behaving rat
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 19
year: '1999'
...
---
_id: '3539'
abstract:
- lang: eng
text: In the hippocampus, spatial representation of the environment has been suggested
to be coded by either the firing rate of pyramidal cell assemblies or the relative
timing of the action potentials during the theta EEG cycle. Here, we used a behavioural
`space clamp' method, which involved the confinement of the actively running animal
in a defined position in space (running wheel) to examine how `spatial' and other
inputs affect firing rate and timing of hippocampal CA1 pyramidal cells and interneurons.
Nineteen per cent of the recorded CA1 pyramidal cells were selectively active
while the rat was running in the wheel in a given direction ('wheel' cells). Spatial
rotation of the apparatus showed that selective discharge of pyramidal cells in
the wheel was under the combined influence of distal and apparatus cues. During
steady running, both discharge rate and theta phase were constant. Rotation of
the wheel apparatus resulted in a shift of both firing rate and preferred theta
phase. The discharge frequency of `wheel' cells increased threefold (on average)
with increasing running velocity. In contrast, change in running speed had relatively
little effect on the theta phase-related discharge of `wheel' cells. Our findings
indicate that mechanisms that regulate rate and phase of spikes are overlapping
but not necessarily identical.
acknowledgement: 'We thank M. Recce for his comments on the manuscript. This work
wassupported by NIH (NS34994, MH54671), the Human Frontier ScienceProgram (H.H.),
the EoÈtvoÈs State Fellowship (A.C.) and the Soros Foundation (A.C.) '
article_processing_charge: No
article_type: original
author:
- first_name: Hajima
full_name: Hirase, Hajima
last_name: Hirase
- first_name: András
full_name: Czurkó, András
last_name: Czurkó
- first_name: Jozsef L
full_name: Csicsvari, Jozsef L
id: 3FA14672-F248-11E8-B48F-1D18A9856A87
last_name: Csicsvari
orcid: 0000-0002-5193-4036
- first_name: György
full_name: Buzsáki, György
last_name: Buzsáki
citation:
ama: Hirase H, Czurkó A, Csicsvari JL, Buzsáki G. Firing rate and theta-phase coding
by hippocampal pyramidal neurons during ‘space clamping.’ European Journal
of Neuroscience. 1999;11(12):4373-4380. doi:10.1046/j.1460-9568.1999.00853.x
apa: Hirase, H., Czurkó, A., Csicsvari, J. L., & Buzsáki, G. (1999). Firing
rate and theta-phase coding by hippocampal pyramidal neurons during ‘space clamping.’
European Journal of Neuroscience. Wiley-Blackwell. https://doi.org/10.1046/j.1460-9568.1999.00853.x
chicago: Hirase, Hajima, András Czurkó, Jozsef L Csicsvari, and György Buzsáki.
“Firing Rate and Theta-Phase Coding by Hippocampal Pyramidal Neurons during ‘Space
Clamping.’” European Journal of Neuroscience. Wiley-Blackwell, 1999. https://doi.org/10.1046/j.1460-9568.1999.00853.x.
ieee: H. Hirase, A. Czurkó, J. L. Csicsvari, and G. Buzsáki, “Firing rate and theta-phase
coding by hippocampal pyramidal neurons during ‘space clamping,’” European
Journal of Neuroscience, vol. 11, no. 12. Wiley-Blackwell, pp. 4373–4380,
1999.
ista: Hirase H, Czurkó A, Csicsvari JL, Buzsáki G. 1999. Firing rate and theta-phase
coding by hippocampal pyramidal neurons during ‘space clamping’. European Journal
of Neuroscience. 11(12), 4373–4380.
mla: Hirase, Hajima, et al. “Firing Rate and Theta-Phase Coding by Hippocampal Pyramidal
Neurons during ‘Space Clamping.’” European Journal of Neuroscience, vol.
11, no. 12, Wiley-Blackwell, 1999, pp. 4373–80, doi:10.1046/j.1460-9568.1999.00853.x.
short: H. Hirase, A. Czurkó, J.L. Csicsvari, G. Buzsáki, European Journal of Neuroscience
11 (1999) 4373–4380.
date_created: 2018-12-11T12:03:51Z
date_published: 1999-12-01T00:00:00Z
date_updated: 2022-09-06T09:45:36Z
day: '01'
doi: 10.1046/j.1460-9568.1999.00853.x
extern: '1'
external_id:
pmid:
- '10594664 '
intvolume: ' 11'
issue: '12'
language:
- iso: eng
month: '12'
oa_version: None
page: 4373 - 4380
pmid: 1
publication: European Journal of Neuroscience
publication_identifier:
issn:
- 0953-816X
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2845'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Firing rate and theta-phase coding by hippocampal pyramidal neurons during
‘space clamping’
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 11
year: '1999'
...
---
_id: '3554'
abstract:
- lang: eng
text: In computational simulation of coupled, multicomponent systems, it is frequently
necessary to transfer data between meshes that may differ in resolution, structure,
and discretization methodology. Typically, nodes from one mesh must be associated
with elements of another mesh. In this paper, we formulate mesh association as
a geometric problem and introduce two efficient mesh association algorithms. One
of these algorithms requires linear time in the worst case if the meshes are well
shaped and geometrically well aligned. Our formulation of the problem and our
algorithms are more general than previous work and can be applied to surface meshes
with curved elements.
article_processing_charge: No
author:
- first_name: Xiangmin
full_name: Jiao, Xiangmin
last_name: Jiao
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Michael
full_name: Heath, Michael
last_name: Heath
citation:
ama: 'Jiao X, Edelsbrunner H, Heath M. Mesh association: formulation and algorithms.
In: Proceedings of the 8th International Meshing Roundtable. Elsevier;
1999:75-82.'
apa: 'Jiao, X., Edelsbrunner, H., & Heath, M. (1999). Mesh association: formulation
and algorithms. In Proceedings of the 8th International Meshing Roundtable
(pp. 75–82). South Lake Tahoe, CA, United States of America: Elsevier.'
chicago: 'Jiao, Xiangmin, Herbert Edelsbrunner, and Michael Heath. “Mesh Association:
Formulation and Algorithms.” In Proceedings of the 8th International Meshing
Roundtable, 75–82. Elsevier, 1999.'
ieee: 'X. Jiao, H. Edelsbrunner, and M. Heath, “Mesh association: formulation and
algorithms,” in Proceedings of the 8th International Meshing Roundtable,
South Lake Tahoe, CA, United States of America, 1999, pp. 75–82.'
ista: 'Jiao X, Edelsbrunner H, Heath M. 1999. Mesh association: formulation and
algorithms. Proceedings of the 8th International Meshing Roundtable. IMR: International
Meshing Roundtable, 75–82.'
mla: 'Jiao, Xiangmin, et al. “Mesh Association: Formulation and Algorithms.” Proceedings
of the 8th International Meshing Roundtable, Elsevier, 1999, pp. 75–82.'
short: X. Jiao, H. Edelsbrunner, M. Heath, in:, Proceedings of the 8th International
Meshing Roundtable, Elsevier, 1999, pp. 75–82.
conference:
end_date: 1999-10-13
location: South Lake Tahoe, CA, United States of America
name: 'IMR: International Meshing Roundtable'
start_date: 1999-10-10
date_created: 2018-12-11T12:03:56Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-06T09:35:53Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.2959
month: '10'
oa_version: None
page: 75 - 82
publication: Proceedings of the 8th International Meshing Roundtable
publication_status: published
publisher: Elsevier
publist_id: '2831'
quality_controlled: '1'
status: public
title: 'Mesh association: formulation and algorithms'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...
---
_id: '3571'
alternative_title:
- Contemporary Mathematics
article_processing_charge: No
author:
- first_name: Tamal
full_name: Dey, Tamal
last_name: Dey
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Sumanta
full_name: Guha, Sumanta
last_name: Guha
citation:
ama: 'Dey T, Edelsbrunner H, Guha S. Computational topology. In: Advances in
Discrete and Computational Geometry. Vol 223. American Mathematical Society;
1999:109-143.'
apa: Dey, T., Edelsbrunner, H., & Guha, S. (1999). Computational topology. In
Advances in Discrete and Computational Geometry (Vol. 223, pp. 109–143).
American Mathematical Society.
chicago: Dey, Tamal, Herbert Edelsbrunner, and Sumanta Guha. “Computational Topology.”
In Advances in Discrete and Computational Geometry, 223:109–43. American
Mathematical Society, 1999.
ieee: T. Dey, H. Edelsbrunner, and S. Guha, “Computational topology,” in Advances
in Discrete and Computational Geometry, vol. 223, American Mathematical Society,
1999, pp. 109–143.
ista: 'Dey T, Edelsbrunner H, Guha S. 1999.Computational topology. In: Advances
in Discrete and Computational Geometry. Contemporary Mathematics, vol. 223, 109–143.'
mla: Dey, Tamal, et al. “Computational Topology.” Advances in Discrete and Computational
Geometry, vol. 223, American Mathematical Society, 1999, pp. 109–43.
short: T. Dey, H. Edelsbrunner, S. Guha, in:, Advances in Discrete and Computational
Geometry, American Mathematical Society, 1999, pp. 109–143.
date_created: 2018-12-11T12:04:01Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-06T09:28:57Z
day: '01'
extern: '1'
intvolume: ' 223'
language:
- iso: eng
month: '01'
oa_version: None
page: 109 - 143
publication: Advances in Discrete and Computational Geometry
publication_identifier:
isbn:
- '9780821878149'
publication_status: published
publisher: American Mathematical Society
publist_id: '2814'
quality_controlled: '1'
status: public
title: Computational topology
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 223
year: '1999'
...
---
_id: '3582'
abstract:
- lang: eng
text: We study edge contractions in simplicial complexes and local conditions under
which they preserve the topological type. The conditions are based on a generalized
notion of boundary, which lends itself to defining a nested hierarchy of triangulable
spaces measuring the distance to being a manifold.
acknowledgement: The second author thanks Wolfgang Haken and Min Yan for interesting
discussions and Günter Ziegler for suggesting the knot construction in the triangulation
of the 3-sphere mentioned in Section 7.
article_processing_charge: No
article_type: original
author:
- first_name: Tamal
full_name: Dey, Tamal
last_name: Dey
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
- first_name: Sumanta
full_name: Guha, Sumanta
last_name: Guha
- first_name: Dmitry
full_name: Nekhayev, Dmitry
last_name: Nekhayev
citation:
ama: Dey T, Edelsbrunner H, Guha S, Nekhayev D. Topology preserving edge contraction.
Publications de l’Institut Mathématique. 1999;66:23-45.
apa: Dey, T., Edelsbrunner, H., Guha, S., & Nekhayev, D. (1999). Topology preserving
edge contraction. Publications de l’Institut Mathématique. Mathematical
Institute, Serbian Academy of Sciences and Arts.
chicago: Dey, Tamal, Herbert Edelsbrunner, Sumanta Guha, and Dmitry Nekhayev. “Topology
Preserving Edge Contraction.” Publications de l’Institut Mathématique.
Mathematical Institute, Serbian Academy of Sciences and Arts, 1999.
ieee: T. Dey, H. Edelsbrunner, S. Guha, and D. Nekhayev, “Topology preserving edge
contraction,” Publications de l’Institut Mathématique, vol. 66. Mathematical
Institute, Serbian Academy of Sciences and Arts, pp. 23–45, 1999.
ista: Dey T, Edelsbrunner H, Guha S, Nekhayev D. 1999. Topology preserving edge
contraction. Publications de l’Institut Mathématique. 66, 23–45.
mla: Dey, Tamal, et al. “Topology Preserving Edge Contraction.” Publications
de l’Institut Mathématique, vol. 66, Mathematical Institute, Serbian Academy
of Sciences and Arts, 1999, pp. 23–45.
short: T. Dey, H. Edelsbrunner, S. Guha, D. Nekhayev, Publications de l’Institut
Mathématique 66 (1999) 23–45.
date_created: 2018-12-11T12:04:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2023-03-22T13:20:32Z
day: '01'
extern: '1'
intvolume: ' 66'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.emis.de/journals/PIMB/080/3.html
month: '01'
oa: 1
oa_version: None
page: 23 - 45
publication: Publications de l'Institut Mathématique
publication_identifier:
issn:
- 0350-1302
publication_status: published
publisher: Mathematical Institute, Serbian Academy of Sciences and Arts
publist_id: '2803'
quality_controlled: '1'
status: public
title: Topology preserving edge contraction
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 66
year: '1999'
...
---
_id: '3625'
abstract:
- lang: eng
text: 'This article outlines theoretical models of clines in additive polygenic
traits, which are maintained by stabilizing selection towards a spatially varying
optimum. Clines in the trait mean can be accurately predicted, given knowledge
of the genetic variance. However, predicting the variance is difficult, because
it depends on genetic details. Changes in genetic variance arise from changes
in allele frequency, and in linkage disequilibria. Allele frequency changes dominate
when selection is weak relative to recombination, and when there are a moderate
number of loci. With a continuum of alleles, gene flow inflates the genetic variance
in the same way as a source of mutations of small effect. The variance can be
approximated by assuming a Gaussian distribution of allelic effects; with a sufficiently
steep cline, this is accurate even when mutation and selection alone are better
described by the ''House of Cards'' approximation. With just two alleles at each
locus, the phenotype changes in a similar way: the mean remains close to the optimum,
while the variance changes more slowly, and over a wider region. However, there
may be substantial cryptic divergence at the underlying loci. With strong selection
and many loci, linkage disequilibria are the main cause of changes in genetic
variance. Even for strong selection, the infinitesimal model can be closely approximated
by assuming a Gaussian distribution of breeding values. Linkage disequilibria
can generate a substantial increase in genetic variance, which is concentrated
at sharp gradients in trait means.'
acknowledgement: This work was supported by the Darwin Trust of Edinburgh, and by
grants MMI09726 from the BBSRC}EPSRC and GR3}11635 from the NERC. I would like to
thank R. Lande and M. Slatkin for their comments on an earlier incarnation of this
article, and Mark Kirkpatrick, Loeske Kruuk and Michael Turelli for their comments
on this manuscript.
article_processing_charge: No
article_type: original
author:
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Barton NH. Clines in polygenic traits. Genetical Research. 1999;74(3):223-236.
doi:10.1017/S001667239900422X
apa: Barton, N. H. (1999). Clines in polygenic traits. Genetical Research.
Cambridge University Press. https://doi.org/10.1017/S001667239900422X
chicago: Barton, Nicholas H. “Clines in Polygenic Traits.” Genetical Research.
Cambridge University Press, 1999. https://doi.org/10.1017/S001667239900422X.
ieee: N. H. Barton, “Clines in polygenic traits,” Genetical Research, vol.
74, no. 3. Cambridge University Press, pp. 223–236, 1999.
ista: Barton NH. 1999. Clines in polygenic traits. Genetical Research. 74(3), 223–236.
mla: Barton, Nicholas H. “Clines in Polygenic Traits.” Genetical Research,
vol. 74, no. 3, Cambridge University Press, 1999, pp. 223–36, doi:10.1017/S001667239900422X.
short: N.H. Barton, Genetical Research 74 (1999) 223–236.
date_created: 2018-12-11T12:04:18Z
date_published: 1999-12-01T00:00:00Z
date_updated: 2022-09-06T09:10:35Z
day: '01'
doi: 10.1017/S001667239900422X
extern: '1'
external_id:
pmid:
- '10689800 '
intvolume: ' 74'
issue: '3'
language:
- iso: eng
month: '12'
oa_version: None
page: 223 - 236
pmid: 1
publication: Genetical Research
publication_identifier:
issn:
- 0016-6723
publication_status: published
publisher: Cambridge University Press
publist_id: '2758'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Clines in polygenic traits
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 74
year: '1999'
...
---
_id: '3626'
abstract:
- lang: eng
text: There has recently been considerable debate over the relative importance of
selection against hybrids ("endogenous" selection) vs. adaptation to
different environments ("exogenous") in maintaining stable hybrid zones
and hence in speciation. Single-locus models of endogenous and exogenous viability
selection generate clines of similar shape, but the comparison has not been extended
to multilocus systems, which are both quantitatively and qualitatively very different
from the single-locus case. Here we develop an analytical multilocus model of
differential adaptation across an environmental transition and compare it to previous
heterozygote disadvantage models. We show that the shape of clines generated by
exogenous selection is indistinguishable from that generated by endogenous selection.
A stochastic simulation model is used to test the robustness of the analytical
description to the effects of drift and strong selection, and confirms the prediction
that pairwise linkage disequilibria are predominantly generated by migration.
However, although analytical predictions for the width of clines maintained by
heterozygote disadvantage fit well with the simulation results, those for environmental
adaptation are consistently too narrow; reasons for the discrepancy are discussed.
There is a smooth transition between a system in which a set of loci effectively
act independently of each other and one in which they act as a single nonrecombining
unit.
article_processing_charge: No
article_type: original
author:
- first_name: Loeske
full_name: Kruuk, Loeske
last_name: Kruuk
- first_name: Stuart
full_name: Baird, Stuart
last_name: Baird
- first_name: Katherine
full_name: Gale, Katherine
last_name: Gale
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Kruuk L, Baird S, Gale K, Barton NH. A comparison of multilocus clines maintained
by environmental adaptation or by selection against hybrids. Genetics.
1999;153(4):1959-1971. doi:10.1093/genetics/153.4.1959
apa: Kruuk, L., Baird, S., Gale, K., & Barton, N. H. (1999). A comparison of
multilocus clines maintained by environmental adaptation or by selection against
hybrids. Genetics. Genetics Society of America. https://doi.org/10.1093/genetics/153.4.1959
chicago: Kruuk, Loeske, Stuart Baird, Katherine Gale, and Nicholas H Barton. “A
Comparison of Multilocus Clines Maintained by Environmental Adaptation or by Selection
against Hybrids.” Genetics. Genetics Society of America, 1999. https://doi.org/10.1093/genetics/153.4.1959.
ieee: L. Kruuk, S. Baird, K. Gale, and N. H. Barton, “A comparison of multilocus
clines maintained by environmental adaptation or by selection against hybrids,”
Genetics, vol. 153, no. 4. Genetics Society of America, pp. 1959–1971,
1999.
ista: Kruuk L, Baird S, Gale K, Barton NH. 1999. A comparison of multilocus clines
maintained by environmental adaptation or by selection against hybrids. Genetics.
153(4), 1959–1971.
mla: Kruuk, Loeske, et al. “A Comparison of Multilocus Clines Maintained by Environmental
Adaptation or by Selection against Hybrids.” Genetics, vol. 153, no. 4,
Genetics Society of America, 1999, pp. 1959–71, doi:10.1093/genetics/153.4.1959.
short: L. Kruuk, S. Baird, K. Gale, N.H. Barton, Genetics 153 (1999) 1959–1971.
date_created: 2018-12-11T12:04:19Z
date_published: 1999-12-01T00:00:00Z
date_updated: 2022-09-06T09:06:02Z
day: '01'
doi: 10.1093/genetics/153.4.1959
extern: '1'
external_id:
pmid:
- '10581299'
intvolume: ' 153'
issue: '4'
language:
- iso: eng
month: '12'
oa_version: None
page: 1959 - 1971
pmid: 1
publication: Genetics
publication_identifier:
issn:
- 0016-6731
publication_status: published
publisher: Genetics Society of America
publist_id: '2757'
quality_controlled: '1'
scopus_import: '1'
status: public
title: A comparison of multilocus clines maintained by environmental adaptation or
by selection against hybrids
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 153
year: '1999'
...
---
_id: '4014'
abstract:
- lang: eng
text: A new paradigm for designing smooth surfaces is described. A finite set of
points with weights specifies a closed surface in space referred to as skin. It
consists of one or more components, each tangent continuous and free of self-intersections
and intersections with other components. The skin varies continuously with the
weights and locations of the points, and the variation includes the possibility
of a topology change facilitated by the violation of tangent continuity at a single
point in space and time. Applications of the skin to molecular modeling and to
geometric deformation are discussed.
article_processing_charge: No
article_type: original
author:
- first_name: Herbert
full_name: Edelsbrunner, Herbert
id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
last_name: Edelsbrunner
orcid: 0000-0002-9823-6833
citation:
ama: Edelsbrunner H. Deformable smooth surface design. Discrete & Computational
Geometry. 1999;21(1):87-115. doi:10.1007/PL00009412
apa: Edelsbrunner, H. (1999). Deformable smooth surface design. Discrete &
Computational Geometry. Springer. https://doi.org/10.1007/PL00009412
chicago: Edelsbrunner, Herbert. “Deformable Smooth Surface Design.” Discrete
& Computational Geometry. Springer, 1999. https://doi.org/10.1007/PL00009412.
ieee: H. Edelsbrunner, “Deformable smooth surface design,” Discrete & Computational
Geometry, vol. 21, no. 1. Springer, pp. 87–115, 1999.
ista: Edelsbrunner H. 1999. Deformable smooth surface design. Discrete & Computational
Geometry. 21(1), 87–115.
mla: Edelsbrunner, Herbert. “Deformable Smooth Surface Design.” Discrete &
Computational Geometry, vol. 21, no. 1, Springer, 1999, pp. 87–115, doi:10.1007/PL00009412.
short: H. Edelsbrunner, Discrete & Computational Geometry 21 (1999) 87–115.
date_created: 2018-12-11T12:06:26Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-06T09:02:23Z
day: '01'
doi: 10.1007/PL00009412
extern: '1'
intvolume: ' 21'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 87 - 115
publication: Discrete & Computational Geometry
publication_identifier:
issn:
- 0179-5376
publication_status: published
publisher: Springer
publist_id: '2115'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Deformable smooth surface design
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 21
year: '1999'
...
---
_id: '4204'
abstract:
- lang: eng
text: During the development of the zebrafish nervous system both noi, a zebrafish
pax2 homolog, and ace, a zebrafish fgf8 homolog, are required for development
of the midbrain and cerebellum. Here we describe a dominant mutation, aussicht
(aus), in which the expression of noi and ace is upregulated, In aus mutant embryos,
ace is upregulated at many sites in the embryo, while Itoi expression is only
upregulated in regions of the forebrain and midbrain which also express ace. Subsequent
to the alterations in noi and ace expression, aus mutants exhibit defects in the
differentiation of the forebrain, midbrain and eyes. Within the forebrain, the
formation of the anterior and postoptic commissures is delayed and the expression
of markers within the pretectal area is reduced. Within the midbrain, En and wnt1
expression is expanded. In heterozygous aus embryos, there is ectopic outgrowth
of neural retina in the temporal half of the eyes, whereas in putative homozygous
aus embryos, the ventral retina is reduced and the pigmented retinal epithelium
is expanded towards the midline, The observation that ans mutant embryos exhibit
widespread upregulation of ace raised the possibility that aus might represent
an allele of the ace gene itself. However, by crossing carriers for both aus and
ace, we were able to generate homozygous ace mutant embryos that also exhibited
the aus phenotype, This indicated that aus is not tightly linked to ace and is
unlikely to be a mutation directly affecting the ace locus. However, increased
Ace activity may underly many aspects of the aus phenotype and we show that the
upregulation of noi in the forebrain of aus mutants is partially dependent upon
functional Ace activity. Conversely, increased ace expression in the forebrain
of arcs mutants is not dependent upon functional Noi activity. We conclude that
aus represents a mutation involving a locus normally required for the regulation
of ace expression during embryogenesis.
acknowledgement: "We thank Corinne Houart, Michael Brand and the late Nigel Holder
for comments and advice on this study, many colleagues for providing probes used
in this analysis, other members of our laboratories for suggestions throughout the
course of the work and Michael Brand, Jörg Rauch and Pascal Haffter for providing
data prior to publication. We also would like to thank Christiane Nüsslein-Volhard
in whose laboratory the mutant described in this study was initially isolated.\r\nThis
study was supported by grants from The Wellcome Trust and\r\nBBSRC. C. P. H. was
supported by Fellowships from EMBO and the\r\nEC, and S. W. W. is a Wellcome Trust
Senior Research Fellow.\r\n"
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: Caroline
full_name: Brennan, Caroline
last_name: Brennan
- first_name: Stephen
full_name: Wilson, Stephen
last_name: Wilson
citation:
ama: Heisenberg C-PJ, Brennan C, Wilson S. Zebrafish aussicht mutant embryos exhibit
widespread overexpression of ace (fgf8) and coincident defects in CNS development.
Development. 1999;126(10):2129-2140. doi:10.1242/dev.126.10.2129
apa: Heisenberg, C.-P. J., Brennan, C., & Wilson, S. (1999). Zebrafish aussicht
mutant embryos exhibit widespread overexpression of ace (fgf8) and coincident
defects in CNS development. Development. Company of Biologists. https://doi.org/10.1242/dev.126.10.2129
chicago: Heisenberg, Carl-Philipp J, Caroline Brennan, and Stephen Wilson. “Zebrafish
Aussicht Mutant Embryos Exhibit Widespread Overexpression of Ace (Fgf8) and Coincident
Defects in CNS Development.” Development. Company of Biologists, 1999.
https://doi.org/10.1242/dev.126.10.2129.
ieee: C.-P. J. Heisenberg, C. Brennan, and S. Wilson, “Zebrafish aussicht mutant
embryos exhibit widespread overexpression of ace (fgf8) and coincident defects
in CNS development,” Development, vol. 126, no. 10. Company of Biologists,
pp. 2129–2140, 1999.
ista: Heisenberg C-PJ, Brennan C, Wilson S. 1999. Zebrafish aussicht mutant embryos
exhibit widespread overexpression of ace (fgf8) and coincident defects in CNS
development. Development. 126(10), 2129–2140.
mla: Heisenberg, Carl-Philipp J., et al. “Zebrafish Aussicht Mutant Embryos Exhibit
Widespread Overexpression of Ace (Fgf8) and Coincident Defects in CNS Development.”
Development, vol. 126, no. 10, Company of Biologists, 1999, pp. 2129–40,
doi:10.1242/dev.126.10.2129.
short: C.-P.J. Heisenberg, C. Brennan, S. Wilson, Development 126 (1999) 2129–2140.
date_created: 2018-12-11T12:07:34Z
date_published: 1999-05-15T00:00:00Z
date_updated: 2022-09-06T08:38:01Z
day: '15'
doi: 10.1242/dev.126.10.2129
extern: '1'
external_id:
pmid:
- '10207138'
intvolume: ' 126'
issue: '10'
language:
- iso: eng
month: '05'
oa_version: None
page: 2129 - 2140
pmid: 1
publication: Development
publication_identifier:
issn:
- 0950-1991
publication_status: published
publisher: Company of Biologists
publist_id: '1914'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Zebrafish aussicht mutant embryos exhibit widespread overexpression of ace
(fgf8) and coincident defects in CNS development
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 126
year: '1999'
...
---
_id: '4277'
abstract:
- lang: eng
text: 'Reproductive isolation between two taxa may be due to endogenous selection,
which is generated by incompatibilities between the respective genomes, to exogenous
selection, which is generated by differential adaptations to alternative environments,
or to both. The continuing debate over the relative importance of either mode
of selection has highlighted the need for unambiguous data on the fitness of hybrid
genotypes. The hybrid zone between the fire-bellied toad (Bombina bombina) and
the yellow-bellied toad (B. variegata) in central Europe involves adaptation to
different environments, but evidence of hybrid dysfunction is equivocal. In this
study, we followed the development under laboratory conditions of naturally laid
eggs collected from a transect across the Bombina hybrid zone in Croatia. Fitness
was significantly reduced in hybrid populations: Egg batches from the center of
the hybrid zone showed significantly higher embryonic and larval mortality and
higher frequencies of morphological abnormalities relative to either parental
type. Overall mortality from day of egg collection to three weeks after hatching
reached 20% in central hybrid populations, compared to 2% in pure populations.
There was no significant difference in fitness between two parental types. Within
hybrid populations, there was considerable variation in fitness, with some genotypes
showing no evidence of reduced viability. We discuss the implications of these
findings for our understanding of barriers to gene flow between species.'
acknowledgement: We thank the Perovic family for their generous hospitality in Croatia
and B.Nurnberger, C.MacCallum, D.Howard, and ananonymous reviewer for comments on
the manuscript. The work was supported by a Natural Environment Research Council
studentship to LEBK.
article_processing_charge: No
article_type: original
author:
- first_name: Loeske
full_name: Kruuk, Loeske
last_name: Kruuk
- first_name: Jason
full_name: Gilchrist, Jason
last_name: Gilchrist
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Kruuk L, Gilchrist J, Barton NH. Hybrid dysfunction in fire-bellied toads (Bombina).
Evolution; International Journal of Organic Evolution. 1999;53(5):1611-1616.
doi:10.2307/2640907
apa: Kruuk, L., Gilchrist, J., & Barton, N. H. (1999). Hybrid dysfunction in
fire-bellied toads (Bombina). Evolution; International Journal of Organic Evolution.
Wiley-Blackwell. https://doi.org/10.2307/2640907
chicago: Kruuk, Loeske, Jason Gilchrist, and Nicholas H Barton. “Hybrid Dysfunction
in Fire-Bellied Toads (Bombina).” Evolution; International Journal of Organic
Evolution. Wiley-Blackwell, 1999. https://doi.org/10.2307/2640907.
ieee: L. Kruuk, J. Gilchrist, and N. H. Barton, “Hybrid dysfunction in fire-bellied
toads (Bombina),” Evolution; International Journal of Organic Evolution,
vol. 53, no. 5. Wiley-Blackwell, pp. 1611–1616, 1999.
ista: Kruuk L, Gilchrist J, Barton NH. 1999. Hybrid dysfunction in fire-bellied
toads (Bombina). Evolution; International Journal of Organic Evolution. 53(5),
1611–1616.
mla: Kruuk, Loeske, et al. “Hybrid Dysfunction in Fire-Bellied Toads (Bombina).”
Evolution; International Journal of Organic Evolution, vol. 53, no. 5,
Wiley-Blackwell, 1999, pp. 1611–16, doi:10.2307/2640907.
short: L. Kruuk, J. Gilchrist, N.H. Barton, Evolution; International Journal of
Organic Evolution 53 (1999) 1611–1616.
date_created: 2018-12-11T12:08:00Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-06T08:20:03Z
day: '01'
doi: 10.2307/2640907
extern: '1'
external_id:
pmid:
- '28565554'
intvolume: ' 53'
issue: '5'
language:
- iso: eng
month: '10'
oa_version: None
page: 1611 - 1616
pmid: 1
publication: Evolution; International Journal of Organic Evolution
publication_identifier:
issn:
- 0014-3820
publication_status: published
publisher: Wiley-Blackwell
publist_id: '1811'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Hybrid dysfunction in fire-bellied toads (Bombina)
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 53
year: '1999'
...
---
_id: '4279'
abstract:
- lang: eng
text: In this article we describe the structure of a hybrid zone in Argyll, Scotland,
between native red deer (Cervus elaphus) and introduced Japanese sika deer (Cervus
nippon), on the basis of a genetic analysis using 11 microsatellite markers and
mitochondrial DNA. In contrast to the findings of a previous study of the same
population, we conclude that the deer fall into two distinct genetic classes,
corresponding to either a sika-like or red- like phenotype. Introgression is rare
at any one locus, but where the taxa overlap up to 40% of deer carry apparently
introgressed alleles. While most putative hybrids are heterozygous at only one
locus, there are rare multiple heterozygotes, reflecting significant linkage disequilibrium
within both sika- and red-like populations. The rate of backcrossing into the
sika population is estimated as H = 0.002 per generation and into red, H = 0.001
per generation. On the basis of historical evidence that red deer entered Kintyre
only recently, a diffusion model evaluated by maximum likelihood shows that sika
have increased at ~9.2% yr-1 from low frequency and disperse at a rate of ~3.7
km yr-1. Introgression into the red-like population is greater in the south, while
introgression into sika varies little along the transect. For both sika- and red-like
populations, the degree of introgression is 30-40% of that predicted from the
rates of current hybridization inferred from linkage disequilibria; however, in
neither case is this statistically significant evidence for selection against
introgression.
acknowledgement: We are grateful to Forest Enterprise in Argyll for providing the
samples used in this study. We also thank Loeske Kruuk plus the communicating editor
and two anonymous referees for their helpful comments on the manuscript. This work
was supported by a Natural Environment Research Council grant to N.B. and J.P. and
by a University of Edinburgh postgraduate bursary to G.S.
article_processing_charge: No
article_type: original
author:
- first_name: Simon
full_name: Goodman, Simon
last_name: Goodman
- first_name: Nicholas H
full_name: Barton, Nicholas H
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
- first_name: Graeme
full_name: Swanson, Graeme
last_name: Swanson
- first_name: Kate
full_name: Abernethy, Kate
last_name: Abernethy
- first_name: Josephine
full_name: Pemberton, Josephine
last_name: Pemberton
citation:
ama: 'Goodman S, Barton NH, Swanson G, Abernethy K, Pemberton J. Introgression through
rare hybridisation: A genetic study of a hybrid zone between red and sika deer
(genus Cervus), in Argyll, Scotland. Genetics. 1999;152(1):355-371. doi:10.1093/genetics/152.1.355'
apa: 'Goodman, S., Barton, N. H., Swanson, G., Abernethy, K., & Pemberton, J.
(1999). Introgression through rare hybridisation: A genetic study of a hybrid
zone between red and sika deer (genus Cervus), in Argyll, Scotland. Genetics.
Genetics Society of America. https://doi.org/10.1093/genetics/152.1.355'
chicago: 'Goodman, Simon, Nicholas H Barton, Graeme Swanson, Kate Abernethy, and
Josephine Pemberton. “Introgression through Rare Hybridisation: A Genetic Study
of a Hybrid Zone between Red and Sika Deer (Genus Cervus), in Argyll, Scotland.”
Genetics. Genetics Society of America, 1999. https://doi.org/10.1093/genetics/152.1.355.'
ieee: 'S. Goodman, N. H. Barton, G. Swanson, K. Abernethy, and J. Pemberton, “Introgression
through rare hybridisation: A genetic study of a hybrid zone between red and sika
deer (genus Cervus), in Argyll, Scotland,” Genetics, vol. 152, no. 1. Genetics
Society of America, pp. 355–371, 1999.'
ista: 'Goodman S, Barton NH, Swanson G, Abernethy K, Pemberton J. 1999. Introgression
through rare hybridisation: A genetic study of a hybrid zone between red and sika
deer (genus Cervus), in Argyll, Scotland. Genetics. 152(1), 355–371.'
mla: 'Goodman, Simon, et al. “Introgression through Rare Hybridisation: A Genetic
Study of a Hybrid Zone between Red and Sika Deer (Genus Cervus), in Argyll, Scotland.”
Genetics, vol. 152, no. 1, Genetics Society of America, 1999, pp. 355–71,
doi:10.1093/genetics/152.1.355.'
short: S. Goodman, N.H. Barton, G. Swanson, K. Abernethy, J. Pemberton, Genetics
152 (1999) 355–371.
date_created: 2018-12-11T12:08:01Z
date_published: 1999-05-01T00:00:00Z
date_updated: 2022-09-06T08:12:14Z
day: '01'
doi: 10.1093/genetics/152.1.355
extern: '1'
external_id:
pmid:
- '10224266'
intvolume: ' 152'
issue: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 355 - 371
pmid: 1
publication: Genetics
publication_identifier:
issn:
- 0016-6731
publication_status: published
publisher: Genetics Society of America
publist_id: '1809'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Introgression through rare hybridisation: A genetic study of a hybrid zone
between red and sika deer (genus Cervus), in Argyll, Scotland'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 152
year: '1999'
...
---
_id: '4411'
abstract:
- lang: eng
text: "Model checking algorithms for the verification of reactive systems proceed
by a systematic and exhaustive exploration of the system state space. They do
not scale to large designs because of the state explosion problem --the number
of states grows exponentially with the number of components in the design. Consequently,
the model checking problem is PSPACE-hard in the size of the design description.
This dissertation proposes three novel techniques to combat the state explosion
problem.\r\n\r\nOne of the most important advances in model checking in recent
years has been the discovery of symbolic methods, which use a calculus of expressions,
such as binary decision diagrams, to represent the state sets encountered during
state space exploration. Symbolic model checking has proved to be effective for
verifying hardware designs. Traditionally, symbolic checking of temporal logic
specifications is performed by backward fixpoint reasoning with the operator Pre.
Backward reasoning can be wasteful since unreachable states are explored. We suggest
the use of forward fixpoint reasoning based on the operator Post. We show how
all linear temporal logic specifications can be model checked symbolically by
forward reasoning. In contrast to backward reasoning, forward reasoning performs
computations only on the reachable states.\r\n\r\nHeuristics that improve algorithms
for application domains, such as symbolic methods for hardware designs, are useful
but not enough to make model checking feasible on industrial designs. Currently,
exhaustive state exploration is possible only on designs with about 50-100 boolean
state variables. Assume-guarantee verification attempts to combat the state explosion
problem by using the principle of "divide and conquer," where the components
of the implementation are analyzed one at a time. Typically, an implementation
component refines its specification only when its inputs are suitably constrained
by other components in the implementation. The assume-guarantee principle states
that instead of constraining the inputs by implementation components, it is sound
to constrain them by the corresponding specification components, which can be
significantly smaller. We extend the assume-guarantee proof rule to deal with
the case where the specification operates at a coarser time scale than the implementation.
Using our model checker Mocha, which implements this methodology, we verify VGI,
a parallel DSP processor chip with 64 compute processors each containing approximately
800 state variables and 30K gates.\r\n\r\nOur third contribution is a systematic
model checking methodology for verifying the abstract shared-memory interface
of sequential consistency on multiprocessor systems with three parameters --number
of processors, number of memory locations, and number of data values. Sequential
consistency requires that some interleaving of the local temporal orders of read/write
events at different processors be a trace of serial memory. Therefore, it suffices
to construct a non-interfering serializer that watches and reorders read/write
events so that a trace of serial memory is obtained. While in general such a serializer
must be unbounded even for fixed values of the parameters --checking sequential
consistency is undecidable!-- we show that the paradigmatic class of snoopy cache
coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter
problem to the fixed-parameter problem, we develop a novel framework for induction
over the number of processors and use the notion of a serializer to reduce the
problem of verifying sequential consistency to that of checking language inclusion
between finite state machines."
article_processing_charge: No
author:
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: Qadeer S. Algorithms and Methodology for Scalable Model Checking. 1999:1-150.
apa: Qadeer, S. (1999). Algorithms and Methodology for Scalable Model Checking.
University of California, Berkeley.
chicago: Qadeer, Shaz. “Algorithms and Methodology for Scalable Model Checking.”
University of California, Berkeley, 1999.
ieee: S. Qadeer, “Algorithms and Methodology for Scalable Model Checking,” University
of California, Berkeley, 1999.
ista: Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking. University
of California, Berkeley.
mla: Qadeer, Shaz. Algorithms and Methodology for Scalable Model Checking.
University of California, Berkeley, 1999, pp. 1–150.
short: S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University
of California, Berkeley, 1999.
date_created: 2018-12-11T12:08:43Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2022-09-06T08:07:40Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://www.microsoft.com/en-us/research/publication/algorithms-methodology-scalable-model-checking/
month: '10'
oa_version: None
page: 1 - 150
publication_status: published
publisher: University of California, Berkeley
publist_id: '321'
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
- first_name: Robert
full_name: Bryton, Robert
last_name: Bryton
- first_name: John
full_name: Steel, John
last_name: Steel
title: Algorithms and Methodology for Scalable Model Checking
type: dissertation
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...
---
_id: '4442'
abstract:
- lang: eng
text: Rectangular hybrid automata model digital control programs of analog plant
environments. We study rectangular hybrid automata where the plant state evolves
continuously in real-numbered time, and the controller samples the plant state
and changes the control state discretely, only at the integer points in time.
We prove that rectangular hybrid automata have finite bisimilarity quotients when
all control transitions happen at integer times, even if the constraints on the
derivatives of the variables vary between control states. This is in contrast
with the conventional model where control transitions may happen at any real time,
and already the reachability problem is undecidable. Based on the finite bisimilarity
quotients, we give an exponential algorithm for the symbolic sampling-controller
synthesis of rectangular automata. We show our algorithm to be optimal by proving
the problem to be EXPTIME-hard. We also show that rectangular automata form a
maximal class of systems for which the sampling-controller synthesis problem can
be solved algorithmically.
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: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: Henzinger TA, Kopke P. Discrete-time control for rectangular hybrid automata.
Theoretical Computer Science. 1999;221(1-2):369-392. doi:10.1016/S0304-3975(99)00038-9
apa: Henzinger, T. A., & Kopke, P. (1999). Discrete-time control for rectangular
hybrid automata. Theoretical Computer Science. Elsevier. https://doi.org/10.1016/S0304-3975(99)00038-9
chicago: Henzinger, Thomas A, and Peter Kopke. “Discrete-Time Control for Rectangular
Hybrid Automata.” Theoretical Computer Science. Elsevier, 1999. https://doi.org/10.1016/S0304-3975(99)00038-9.
ieee: T. A. Henzinger and P. Kopke, “Discrete-time control for rectangular hybrid
automata,” Theoretical Computer Science, vol. 221, no. 1–2. Elsevier, pp.
369–392, 1999.
ista: Henzinger TA, Kopke P. 1999. Discrete-time control for rectangular hybrid
automata. Theoretical Computer Science. 221(1–2), 369–392.
mla: Henzinger, Thomas A., and Peter Kopke. “Discrete-Time Control for Rectangular
Hybrid Automata.” Theoretical Computer Science, vol. 221, no. 1–2, Elsevier,
1999, pp. 369–92, doi:10.1016/S0304-3975(99)00038-9.
short: T.A. Henzinger, P. Kopke, Theoretical Computer Science 221 (1999) 369–392.
date_created: 2018-12-11T12:08:52Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-06T08:03:48Z
day: '01'
doi: 10.1016/S0304-3975(99)00038-9
extern: '1'
intvolume: ' 221'
issue: 1-2
language:
- iso: eng
month: '01'
oa_version: None
page: 369 - 392
publication: Theoretical Computer Science
publication_identifier:
issn:
- 0304-3975
publication_status: published
publisher: Elsevier
publist_id: '290'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Discrete-time control for rectangular hybrid automata
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 221
year: '1999'
...
---
_id: '4480'
abstract:
- lang: eng
text: 'We describe the formal specification and verification of the VGI parallel
DSP chip [1], which contains 64 compute processors with ~30K gates in each processor.
Our effort coincided in time with the “informal” verification stage of the chip.
By interacting with the designers, we produced an abstract but executable specification
of the design which embodies the programmer''s view of the system. Given the size
of the design, an automatic check that even one of the 64 processors satisfies
its specification is well beyond the scope of current verification tools. However,
the check can be decomposed using assume-guarantee reasoning. For VGI, the implementation
and specification operate at different time scales: several steps of the implementation
correspond to a single step in the specification. We generalized both the assume-guarantee
method and our model checker MOCHA to allow compositional verification for such
applications. We used our proof rule to decompose the verification problem of
the VGI chip into smaller proof obligations that were discharged automatically
by MOCHA. Using our formal approach, we uncovered and fixed subtle bugs that were
unknown to the designers.'
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: Xiaojun
full_name: Liu, Xiaojun
last_name: Liu
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Liu X, Qadeer S, Rajamani S. Formal specification and verification
of a dataflow processor array. In: IEEE; 1999:494-499. doi:10.1109/ICCAD.1999.810700'
apa: 'Henzinger, T. A., Liu, X., Qadeer, S., & Rajamani, S. (1999). Formal specification
and verification of a dataflow processor array (pp. 494–499). Presented at the
ICCAD: Computer-Aided Design, San Jose, CA, United States of America: IEEE. https://doi.org/10.1109/ICCAD.1999.810700'
chicago: Henzinger, Thomas A, Xiaojun Liu, Shaz Qadeer, and Sriram Rajamani. “Formal
Specification and Verification of a Dataflow Processor Array,” 494–99. IEEE, 1999.
https://doi.org/10.1109/ICCAD.1999.810700.
ieee: 'T. A. Henzinger, X. Liu, S. Qadeer, and S. Rajamani, “Formal specification
and verification of a dataflow processor array,” presented at the ICCAD: Computer-Aided
Design, San Jose, CA, United States of America, 1999, pp. 494–499.'
ista: 'Henzinger TA, Liu X, Qadeer S, Rajamani S. 1999. Formal specification and
verification of a dataflow processor array. ICCAD: Computer-Aided Design, 494–499.'
mla: Henzinger, Thomas A., et al. Formal Specification and Verification of a
Dataflow Processor Array. IEEE, 1999, pp. 494–99, doi:10.1109/ICCAD.1999.810700.
short: T.A. Henzinger, X. Liu, S. Qadeer, S. Rajamani, in:, IEEE, 1999, pp. 494–499.
conference:
end_date: 1999-11-11
location: San Jose, CA, United States of America
name: 'ICCAD: Computer-Aided Design'
start_date: 1999-11-07
date_created: 2018-12-11T12:09:04Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-05T14:48:48Z
day: '01'
doi: 10.1109/ICCAD.1999.810700
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 494 - 499
publication_identifier:
issn:
- 1092-3152
publication_status: published
publisher: IEEE
publist_id: '246'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal specification and verification of a dataflow processor array
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...
---
_id: '4484'
abstract:
- lang: eng
text: "In shared-memory multiprocessors sequential consistency offers a natural
tradeoff between the flexibility afforded to the implementor and the complexity
of the programmer’s view of the memory. Sequential consistency requires that some
interleaving of the local temporal orders of read/write events at different processors
be a trace of serial memory. We develop a systematic methodology for proving sequential
consistency for memory systems with three parameters —number of processors, number
of memory locations, and number of data values. From the definition of sequential
consistency it suffices to construct a non-interfering observer that watches and
reorders read/write events so that a trace of serial memory is obtained. While
in general such an observer must be unbounded even for fixed values of the parameters
—checking sequential consistency is undecidable!— we show that for two paradigmatic
protocol classes—lazy caching and snoopy cache coherence—there exist finite-state
observers. In these cases, sequential consistency for fixed parameter values can
thus be checked by language inclusion between finite automata.\r\nIn order to
reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop
a novel framework for induction over the number of processors. Classical induction
schemas, which are based on process invariants that are inductive with respect
to an implementation preorder that preserves the temporal sequence of events,
are inadequate for our purposes, because proving sequential consistency requires
the reordering of events. Hence we introduce merge invariants, which permit certain
reorderings of read/write events. We show that under certain reasonable assumptions
about the memory system, it is possible to conclude sequential consistency for
any number of processors, memory locations, and data values by model checking
two finite-state lemmas about process and merge invariants: they involve two processors
each accessing a maximum of three locations, where each location stores at most
two data values. For both lazy caching and snoopy cache coherence we are able
to discharge the two lemmas using the model checker MOCHA."
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: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S. Verifying sequential consistency on shared-memory
multiprocessor systems. In: Proceedings of the 11th International Conference
on Computer Aided Verification. Vol 1633. Springer; 1999:301-315. doi:10.1007/3-540-48683-6_27'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (1999). Verifying sequential
consistency on shared-memory multiprocessor systems. In Proceedings of the
11th International Conference on Computer Aided Verification (Vol. 1633, pp.
301–315). Trento, Italy: Springer. https://doi.org/10.1007/3-540-48683-6_27'
chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Verifying Sequential
Consistency on Shared-Memory Multiprocessor Systems.” In Proceedings of the
11th International Conference on Computer Aided Verification, 1633:301–15.
Springer, 1999. https://doi.org/10.1007/3-540-48683-6_27.
ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Verifying sequential consistency
on shared-memory multiprocessor systems,” in Proceedings of the 11th International
Conference on Computer Aided Verification, Trento, Italy, 1999, vol. 1633,
pp. 301–315.
ista: 'Henzinger TA, Qadeer S, Rajamani S. 1999. Verifying sequential consistency
on shared-memory multiprocessor systems. Proceedings of the 11th International
Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
vol. 1633, 301–315.'
mla: Henzinger, Thomas A., et al. “Verifying Sequential Consistency on Shared-Memory
Multiprocessor Systems.” Proceedings of the 11th International Conference on
Computer Aided Verification, vol. 1633, Springer, 1999, pp. 301–15, doi:10.1007/3-540-48683-6_27.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International
Conference on Computer Aided Verification, Springer, 1999, pp. 301–315.
conference:
end_date: 1999-07-10
location: Trento, Italy
name: 'CAV: Computer Aided Verification'
start_date: 1999-07-06
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:21:11Z
day: '01'
doi: 10.1007/3-540-48683-6_27
extern: '1'
intvolume: ' 1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 301 - 315
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540662020'
publication_status: published
publisher: Springer
publist_id: '244'
quality_controlled: '1'
status: public
title: Verifying sequential consistency on shared-memory multiprocessor systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...
---
_id: '4485'
abstract:
- lang: eng
text: 'In order to study control problems for hybrid systems, we generalize hybrid
automata to hybrid games —say, controller vs. plant. If we specify the continuous
dynamics by constant lower and upper bounds, we obtain rectangular games. We show
that for rectangular games with objectives expressed in Ltl (linear temporal logic),
the winning states for each player can be computed, and winning strategies can
be synthesized. Our result is sharp, as already reachability is undecidable for
generalizations of rectangular systems, and optimal —singly exponential in the
size of the game structure and doubly exponential in the size of the Ltl objective.
Our proof systematically generalizes the theory of hybrid systems from automata
(single-player structures) [9] to games (multi-player structures): we show that
the successively more general infinite-state classes of timed, 2D rectangular,
and rectangular games induce successively weaker, but still finite, quotient structures
called game bisimilarity, game similarity, and game trace equivalence. These quotients
can be used, in particular, to solve the Ltl control problem.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-9501708,
by the NSF grant CCR-9504469, by the DARPA (NASA Ames) grant NAG2-1214, by the DARPA
(Wright-Patterson AFB) grant F33615-98-C-3614, and by the ARO MURI grant DAAH-04-96-1-0341.
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: Benjamin
full_name: Horowitz, Benjamin
last_name: Horowitz
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'Henzinger TA, Horowitz B, Majumdar R. Rectangular hybrid games. In: Proceedings
of the 10th International Conference on Concurrency Theory. Vol 1664. Schloss
Dagstuhl - Leibniz-Zentrum für Informatik; 1999:320-335. doi:10.1007/3-540-48320-9_23'
apa: 'Henzinger, T. A., Horowitz, B., & Majumdar, R. (1999). Rectangular hybrid
games. In Proceedings of the 10th International Conference on Concurrency Theory
(Vol. 1664, pp. 320–335). Eindhoven, The Netherlands: Schloss Dagstuhl - Leibniz-Zentrum
für Informatik. https://doi.org/10.1007/3-540-48320-9_23'
chicago: Henzinger, Thomas A, Benjamin Horowitz, and Ritankar Majumdar. “Rectangular
Hybrid Games.” In Proceedings of the 10th International Conference on Concurrency
Theory, 1664:320–35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 1999.
https://doi.org/10.1007/3-540-48320-9_23.
ieee: T. A. Henzinger, B. Horowitz, and R. Majumdar, “Rectangular hybrid games,”
in Proceedings of the 10th International Conference on Concurrency Theory,
Eindhoven, The Netherlands, 1999, vol. 1664, pp. 320–335.
ista: 'Henzinger TA, Horowitz B, Majumdar R. 1999. Rectangular hybrid games. Proceedings
of the 10th International Conference on Concurrency Theory. CONCUR: Concurrency
Theory, LNCS, vol. 1664, 320–335.'
mla: Henzinger, Thomas A., et al. “Rectangular Hybrid Games.” Proceedings of
the 10th International Conference on Concurrency Theory, vol. 1664, Schloss
Dagstuhl - Leibniz-Zentrum für Informatik, 1999, pp. 320–35, doi:10.1007/3-540-48320-9_23.
short: T.A. Henzinger, B. Horowitz, R. Majumdar, in:, Proceedings of the 10th International
Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
1999, pp. 320–335.
conference:
location: Eindhoven, The Netherlands
name: 'CONCUR: Concurrency Theory'
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T10:54:12Z
day: '01'
doi: 10.1007/3-540-48320-9_23
extern: '1'
intvolume: ' 1664'
language:
- iso: eng
month: '01'
oa_version: None
page: 320 - 335
publication: Proceedings of the 10th International Conference on Concurrency Theory
publication_identifier:
isbn:
- '9783540664253'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '245'
quality_controlled: '1'
status: public
title: Rectangular hybrid games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1664
year: '1999'
...
---
_id: '4487'
abstract:
- lang: eng
text: Refinement checking is used to verify implementations against more abstract
specifications. Assume-guarantee reasoning is used to decompose refinement proofs
in order to avoid state-space explosion. In previous approaches, specifications
are forced to operate on the same time scale as the implementation. This may lead
to unnatural specifications and inefficiencies in verification. We introduce a
novel methodology for decomposing refinement proofs of temporally abstract specifications,
which specify implementation requirements only at certain sampling instances in
time. Our new assume-guarantee rule allows separate refinement maps for specifying
functionality and timing.We present the theory for the correctness of our methodology,
and illustrate it using a simple example. Support for sampling and the generalized
assume-guarantee rule have been implemented in the model checker Mocha and successfully
applied to verify the VGI multiprocessor dataflow chip with 6 million transistors.
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: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: 'Henzinger TA, Qadeer S, Rajamani S. Assume-guarantee refinement between different
time scales. In: Proceedings of the 11th International Conference on Computer
Aided Verification. Vol 1633. Springer; 1999:208-221. doi:10.1007/3-540-48683-6_20'
apa: 'Henzinger, T. A., Qadeer, S., & Rajamani, S. (1999). Assume-guarantee
refinement between different time scales. In Proceedings of the 11th International
Conference on Computer Aided Verification (Vol. 1633, pp. 208–221). Trento,
Italy: Springer. https://doi.org/10.1007/3-540-48683-6_20'
chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Assume-Guarantee
Refinement between Different Time Scales.” In Proceedings of the 11th International
Conference on Computer Aided Verification, 1633:208–21. Springer, 1999. https://doi.org/10.1007/3-540-48683-6_20.
ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Assume-guarantee refinement
between different time scales,” in Proceedings of the 11th International Conference
on Computer Aided Verification, Trento, Italy, 1999, vol. 1633, pp. 208–221.
ista: 'Henzinger TA, Qadeer S, Rajamani S. 1999. Assume-guarantee refinement between
different time scales. Proceedings of the 11th International Conference on Computer
Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1633, 208–221.'
mla: Henzinger, Thomas A., et al. “Assume-Guarantee Refinement between Different
Time Scales.” Proceedings of the 11th International Conference on Computer
Aided Verification, vol. 1633, Springer, 1999, pp. 208–21, doi:10.1007/3-540-48683-6_20.
short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International
Conference on Computer Aided Verification, Springer, 1999, pp. 208–221.
conference:
end_date: 1999-07-10
location: Trento, Italy
name: 'CAV: Computer Aided Verification'
start_date: 1999-07-06
date_created: 2018-12-11T12:09:06Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:04:26Z
day: '01'
doi: 10.1007/3-540-48683-6_20
extern: '1'
intvolume: ' 1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 208 - 221
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
isbn:
- '9783540662020'
publication_status: published
publisher: Springer
publist_id: '243'
quality_controlled: '1'
status: public
title: Assume-guarantee refinement between different time scales
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...