---
_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'
...
---
_id: '4582'
abstract:
- lang: eng
text: "We present a formal model for concurrent systems. The model represents synchronous
and asynchronous components in a uniform framework that supports compositional
(assume-guarantee) and hierarchical (stepwise-refinement) design and verification.
While synchronous models are based on a notion of atomic computation step, and
asynchronous models remove that notion by introducing stuttering, our model is
based on a flexible notion of what constitutes a computation step: by applying
an abstraction operator to a system, arbitrarily many consecutive steps can be
collapsed into a single step. The abstraction operator, which may turn an asynchronous
system into a synchronous one, allows us to describe systems at various levels
of temporal detail. For describing systems at various levels of spatial detail,
we use a hiding operator that may turn a synchronous system into an asynchronous
one. We illustrate the model with diverse examples from synchronous circuits,
asynchronous shared-memory programs, and synchronous message-passing protocols.\r\n"
acknowledgement: "We thank Albert Benveniste, Bob Kurshan, Ken McMillan, Amir Pnueli,
and the VIS group at UC Berkeley for fruitful discussions. We also thank the anonymous
referees for suggesting improvements. Alur was supported in part by the DARPA/NASA
grant NAG2-1214 and Henzinger was supported in part by the ONR YIP award N00014-95-1-0520,
the\r\nNSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the DARPA/NASA grant
NAG2-1214, and by the SRC contract 97-DC-324.041."
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. Reactive modules. Formal Methods in System Design.
1999;15(1):7-48. doi:10.1023/A:1008739929481
apa: Alur, R., & Henzinger, T. A. (1999). Reactive modules. Formal Methods
in System Design. Springer. https://doi.org/10.1023/A:1008739929481
chicago: Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” Formal Methods
in System Design. Springer, 1999. https://doi.org/10.1023/A:1008739929481.
ieee: R. Alur and T. A. Henzinger, “Reactive modules,” Formal Methods in System
Design, vol. 15, no. 1. Springer, pp. 7–48, 1999.
ista: Alur R, Henzinger TA. 1999. Reactive modules. Formal Methods in System Design.
15(1), 7–48.
mla: Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” Formal Methods
in System Design, vol. 15, no. 1, Springer, 1999, pp. 7–48, doi:10.1023/A:1008739929481.
short: R. Alur, T.A. Henzinger, Formal Methods in System Design 15 (1999) 7–48.
date_created: 2018-12-11T12:09:35Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T08:45:58Z
day: '01'
doi: 10.1023/A:1008739929481
extern: '1'
intvolume: ' 15'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 7 - 48
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '125'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reactive modules
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 15
year: '1999'
...
---
_id: '4601'
abstract:
- lang: eng
text: "Temporal logic comes in two varieties: linear-time temporal logic assumes
implicit universal quantification over all paths that are generated by system
moves; branching-time temporal logic allows explicit existential and universal
quantification over all paths. We introduce a third, more general variety of temporal
logic: alternating-time temporal logic offers selective quantification over those
paths that are possible outcomes of games, such as the game in which the system
and the environment alternate moves. While linear-time and branching-time logics
are natural specification languages for closed systems, alternating-time logics
are natural specification languages for open systems. For example, by preceding
the temporal operator “eventually” with a selective path quantifier, we can specify
that in the game between the system and the environment, the system has a strategy
to reach a certain state. Also the problems of receptiveness, realizability, and
controllability can be formulated as model-checking problems for alternating-time
formulas.\r\nDepending on whether we admit arbitrary nesting of selective path
quantifiers and temporal operators, we obtain the two alternating-time temporal
logics ATL and ATL. We interpret the formulas of ATL and ATL over alternating
transition systems. While in ordinary transition systems, each transition corresponds
to a possible step of the system, in alternating transition systems, each transition
corresponds to a possible move in the game between the system and the environment.
Fair alternating transition systems can capture both synchronous and asynchronous
compositions of open systems. For synchronous systems, the expressive power of
ATL beyond CTL comes at no cost: the model-checking complexity of synchronous
ATL is linear in the size of the system and the length of the formula. The symbolic
model-checking algorithm for CTL extends with few modifications to synchronous
ATL, and with some work, also to asynchronous ATL, whose model-checking complexity
is quadratic. This makes ATL an obvious candidate for the automatic verification
of open systems. In the case of ATL, the model-checking problem is closely related
to the synthesis problem for linear-time formulas, and requires doubly exponential
time for both synchronous and asynchronous systems.\r\nA preliminary version of
this paper appeared in the Proceedings of the 38th IEEE Symposium on Foundations
of Computer Science (FOCS 1997), pp. 100–109."
acknowledgement: This work was supported in part by the ONR YIP award N00014-95-1-0520,
by the NSF CAREER award CCR-9501708, by the NSF grant CCR-9504469, by the AFOSR
contract F49620-93-1-0056, by the ARO MURI grant DAAH-04-96-1-0341, by the ARPA
grant NAG2-892, and by the SRC contract 97-DC-324.041.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Orna
full_name: Kupferman, Orna
last_name: Kupferman
citation:
ama: 'Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. In: Proceedings
of the International Symposium on Compositionality. Vol 1536. Springer; 1999:23-60.
doi:10.1007/3-540-49213-5_2'
apa: 'Alur, R., Henzinger, T. A., & Kupferman, O. (1999). Alternating-time temporal
logic. In Proceedings of the International Symposium on Compositionality
(Vol. 1536, pp. 23–60). Bad Malente, Germany: Springer. https://doi.org/10.1007/3-540-49213-5_2'
chicago: Alur, Rajeev, Thomas A Henzinger, and Orna Kupferman. “Alternating-Time
Temporal Logic.” In Proceedings of the International Symposium on Compositionality,
1536:23–60. Springer, 1999. https://doi.org/10.1007/3-540-49213-5_2.
ieee: R. Alur, T. A. Henzinger, and O. Kupferman, “Alternating-time temporal logic,”
in Proceedings of the International Symposium on Compositionality, Bad
Malente, Germany, 1999, vol. 1536, pp. 23–60.
ista: 'Alur R, Henzinger TA, Kupferman O. 1999. Alternating-time temporal logic.
Proceedings of the International Symposium on Compositionality. COMPOS: Compositionality,
LNCS, vol. 1536, 23–60.'
mla: Alur, Rajeev, et al. “Alternating-Time Temporal Logic.” Proceedings of the
International Symposium on Compositionality, vol. 1536, Springer, 1999, pp.
23–60, doi:10.1007/3-540-49213-5_2.
short: R. Alur, T.A. Henzinger, O. Kupferman, in:, Proceedings of the International
Symposium on Compositionality, Springer, 1999, pp. 23–60.
conference:
end_date: 1997-09-12
location: Bad Malente, Germany
name: 'COMPOS: Compositionality'
start_date: 1997-09-08
date_created: 2018-12-11T12:09:41Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-01T14:23:41Z
day: '01'
doi: 10.1007/3-540-49213-5_2
extern: '1'
intvolume: ' 1536'
language:
- iso: eng
month: '01'
oa_version: None
page: 23 - 60
publication: Proceedings of the International Symposium on Compositionality
publication_identifier:
isbn:
- '9783540654933'
publication_status: published
publisher: Springer
publist_id: '106'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Alternating-time temporal logic
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1536
year: '1999'
...
---
_id: '4602'
abstract:
- lang: eng
text: 'Modular techniques for automatic verification attempt to overcome the state-explosion
problem by exploiting the modular structure naturally present in many system designs.
Unlike other tasks in the verification of finite-state systems, current modular
techniques rely heavily on user guidance. In particular, the user is typically
required to construct module abstractions that are neither too detailed as to
render insufficient benefits in state exploration, nor too coarse as to invalidate
the desired systemproperties. In this paper, we construct abstractmodules automatically,
using reachability and controllability information about the concrete modules.
This allows us to leverage automatic verification techniques by applying them
in layers: first we compute on the state spaces of system components, then we
use the results for constructing abstractions, and finally we compute on the abstract
state space of the system. Our experimental results indicate that if reachability
and controllability information is used in the construction of abstractions, the
resulting abstract modules are often significantly smaller than the concrete modules
and can drastically reduce the space and time requirements for verification.'
acknowledgement: This research was supported in part by the NSF CAREER award CCR-9734115,
by the NSF CAREER award CCR-9501708, by the DARPA (NASA Ames) grant NAG2-1214, by
the DARPA (Wright-Patterson AFB) grant F33615-98-C-3614, by the ARO MURI grant DAAH-
04-96-1-0341, and by the Gigascale Silicon Research Center.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Luca
full_name: De Alfaro, Luca
last_name: De Alfaro
- 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: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: 'Alur R, De Alfaro L, Henzinger TA, Mang F. Automating modular verification.
In: Proceedings of the 10th International Conference on Concurrency Theory.
Vol 1664. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 1999:82-97. doi:10.1007/3-540-48320-9_8'
apa: 'Alur, R., De Alfaro, L., Henzinger, T. A., & Mang, F. (1999). Automating
modular verification. In Proceedings of the 10th International Conference on
Concurrency Theory (Vol. 1664, pp. 82–97). Eindhoven, The Netherlands: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-48320-9_8'
chicago: Alur, Rajeev, Luca De Alfaro, Thomas A Henzinger, and Freddy Mang. “Automating
Modular Verification.” In Proceedings of the 10th International Conference
on Concurrency Theory, 1664:82–97. Schloss Dagstuhl - Leibniz-Zentrum für
Informatik, 1999. https://doi.org/10.1007/3-540-48320-9_8.
ieee: R. Alur, L. De Alfaro, T. A. Henzinger, and F. Mang, “Automating modular verification,”
in Proceedings of the 10th International Conference on Concurrency Theory,
Eindhoven, The Netherlands, 1999, vol. 1664, pp. 82–97.
ista: 'Alur R, De Alfaro L, Henzinger TA, Mang F. 1999. Automating modular verification.
Proceedings of the 10th International Conference on Concurrency Theory. CONCUR:
Concurrency Theory, LNCS, vol. 1664, 82–97.'
mla: Alur, Rajeev, et al. “Automating Modular Verification.” Proceedings of the
10th International Conference on Concurrency Theory, vol. 1664, Schloss Dagstuhl
- Leibniz-Zentrum für Informatik, 1999, pp. 82–97, doi:10.1007/3-540-48320-9_8.
short: R. Alur, L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th
International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 1999, pp. 82–97.
conference:
end_date: 1999-08-27
location: Eindhoven, The Netherlands
name: 'CONCUR: Concurrency Theory'
start_date: 1999-08-24
date_created: 2018-12-11T12:09:42Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-01T14:15:35Z
day: '01'
doi: 10.1007/3-540-48320-9_8
extern: '1'
intvolume: ' 1664'
language:
- iso: eng
month: '01'
oa_version: None
page: 82 - 97
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: '105'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Automating modular verification
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1664
year: '1999'
...
---
_id: '1954'
abstract:
- lang: eng
text: "\r\nWe have examined the effects of heat stress on electron transfer in the
thylakoid membrane of an engineered plastid ndh deletion mutant, Δ1, incapable
of performing the Ndh-mediated reduction of the plastoquinone pool in the chloroplast.
Upon heat stress in the dark, the rate of PSII- independent reduction of PSI after
subsequent illumination by far-red light is dramatically enhanced in both Δ1 and
a wild-type control plant (WT). In contrast, in the dark, only the WT shows an
increase in the reduction state of the plastoquinone pool. We conclude that the
heat stress-induced reduction of the intersystem electron transport chain can
be mediated by Ndh- independent pathways in the light but that in the dark the
dominant pathway for reduction of the plastoquinone pool is catalysed by the Ndh
complex. Our results therefore demonstrate a functional role for the Ndh complex
in the dark.\r\n"
acknowledgement: This work was funded by the BBSRC. We would like to thank Professor
Peter Horton (University of Sheffield) for the loan of the ED 800 T unit.
article_processing_charge: No
article_type: original
author:
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
- first_name: Paul
full_name: Burrows, Paul
last_name: Burrows
- first_name: Peter
full_name: Nixon, Peter
last_name: Nixon
citation:
ama: Sazanov LA, Burrows P, Nixon P. The chloroplast Ndh complex mediates the dark
reduction of the plastoquinone pool in response to heat stress in tobacco leaves.
FEBS Letters. 1998;429(1):115-118. doi:10.1016/S0014-5793(98)00573-0
apa: Sazanov, L. A., Burrows, P., & Nixon, P. (1998). The chloroplast Ndh complex
mediates the dark reduction of the plastoquinone pool in response to heat stress
in tobacco leaves. FEBS Letters. Elsevier. https://doi.org/10.1016/S0014-5793(98)00573-0
chicago: Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “The Chloroplast Ndh
Complex Mediates the Dark Reduction of the Plastoquinone Pool in Response to Heat
Stress in Tobacco Leaves.” FEBS Letters. Elsevier, 1998. https://doi.org/10.1016/S0014-5793(98)00573-0.
ieee: L. A. Sazanov, P. Burrows, and P. Nixon, “The chloroplast Ndh complex mediates
the dark reduction of the plastoquinone pool in response to heat stress in tobacco
leaves,” FEBS Letters, vol. 429, no. 1. Elsevier, pp. 115–118, 1998.
ista: Sazanov LA, Burrows P, Nixon P. 1998. The chloroplast Ndh complex mediates
the dark reduction of the plastoquinone pool in response to heat stress in tobacco
leaves. FEBS Letters. 429(1), 115–118.
mla: Sazanov, Leonid A., et al. “The Chloroplast Ndh Complex Mediates the Dark Reduction
of the Plastoquinone Pool in Response to Heat Stress in Tobacco Leaves.” FEBS
Letters, vol. 429, no. 1, Elsevier, 1998, pp. 115–18, doi:10.1016/S0014-5793(98)00573-0.
short: L.A. Sazanov, P. Burrows, P. Nixon, FEBS Letters 429 (1998) 115–118.
date_created: 2018-12-11T11:54:54Z
date_published: 1998-06-05T00:00:00Z
date_updated: 2022-09-01T13:12:15Z
day: '05'
doi: 10.1016/S0014-5793(98)00573-0
extern: '1'
external_id:
pmid:
- '9657394 '
intvolume: ' 429'
issue: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 115 - 118
pmid: 1
publication: FEBS Letters
publication_identifier:
issn:
- 0014-5793
publication_status: published
publisher: Elsevier
publist_id: '5128'
quality_controlled: '1'
status: public
title: The chloroplast Ndh complex mediates the dark reduction of the plastoquinone
pool in response to heat stress in tobacco leaves
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 429
year: '1998'
...
---
_id: '1955'
abstract:
- lang: eng
text: 'The plastid genomes of several plants contain homologues, termed ndh genes,
of genes encoding subunits of the NADH:ubiquinone oxidoreductase or complex I
of mitochondria and eubacteria. The functional significance of the Ndh proteins
in higher plants is uncertain. We show here that tobacco chloroplasts contain
a protein complex of 550 kDa consisting of at least three of the ndh gene products:
NdhI, NdhJ and NdhK. We have constructed mutant tobacco plants with disrupted
ndhC, ndhK and ndhJ plastid genes, indicating that the Ndh complex is dispensible
for plant growth under optimal growth conditions. Chlorophyll fluorescence analysis
shows that in vivo the Ndh complex catalyses the post-illumination reduction of
the plastoquinone pool and in the light optimizes the induction of photosynthesis
under conditions of water stress. We conclude that the Ndh complex catalyses the
reduction of the plastoquinone pool using stromal reductant and so acts as a respiratory
complex. Overall, our data are compatible with the participation of the Ndh complex
in cyclic electron flow around the photosystem I complex in the light and possibly
in a chloroplast respiratory chain in the dark.'
acknowledgement: We thank Professor Süss (Institute of Plant Genetics and Crop Plant
Research, Gatersleben, Germany) for the gift of the anti-FNR antiserum, Professor
Masahiro Sugiura (Nagoya University, Japan) for the gift of plasmid pTB19 and Professor
Peter Horton (University of Sheffield) for the loan of his ED-800T unit. P.B. is
a recipient of a BBSRC studentship and the work was supported by grants from the
BBSRC, The Royal Society (to P.J.N.) and The National Science Foundation (to P.M.).
article_processing_charge: No
article_type: original
author:
- first_name: Paul
full_name: Burrows, Paul
last_name: Burrows
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
- first_name: Zóra
full_name: Sváb, Zóra
last_name: Sváb
- first_name: Pàl
full_name: Maliga, Pàl
last_name: Maliga
- first_name: Peter
full_name: Nixon, Peter
last_name: Nixon
citation:
ama: Burrows P, Sazanov LA, Sváb Z, Maliga P, Nixon P. Identification of a functional
respiratory complex in chloroplasts through analysis of tobacco mutants containing
disrupted plastid ndh genes. EMBO Journal. 1998;17(4):868-876. doi:10.1093/emboj/17.4.868
apa: Burrows, P., Sazanov, L. A., Sváb, Z., Maliga, P., & Nixon, P. (1998).
Identification of a functional respiratory complex in chloroplasts through analysis
of tobacco mutants containing disrupted plastid ndh genes. EMBO Journal.
Wiley-Blackwell. https://doi.org/10.1093/emboj/17.4.868
chicago: Burrows, Paul, Leonid A Sazanov, Zóra Sváb, Pàl Maliga, and Peter Nixon.
“Identification of a Functional Respiratory Complex in Chloroplasts through Analysis
of Tobacco Mutants Containing Disrupted Plastid Ndh Genes.” EMBO Journal.
Wiley-Blackwell, 1998. https://doi.org/10.1093/emboj/17.4.868.
ieee: P. Burrows, L. A. Sazanov, Z. Sváb, P. Maliga, and P. Nixon, “Identification
of a functional respiratory complex in chloroplasts through analysis of tobacco
mutants containing disrupted plastid ndh genes,” EMBO Journal, vol. 17,
no. 4. Wiley-Blackwell, pp. 868–876, 1998.
ista: Burrows P, Sazanov LA, Sváb Z, Maliga P, Nixon P. 1998. Identification of
a functional respiratory complex in chloroplasts through analysis of tobacco mutants
containing disrupted plastid ndh genes. EMBO Journal. 17(4), 868–876.
mla: Burrows, Paul, et al. “Identification of a Functional Respiratory Complex in
Chloroplasts through Analysis of Tobacco Mutants Containing Disrupted Plastid
Ndh Genes.” EMBO Journal, vol. 17, no. 4, Wiley-Blackwell, 1998, pp. 868–76,
doi:10.1093/emboj/17.4.868.
short: P. Burrows, L.A. Sazanov, Z. Sváb, P. Maliga, P. Nixon, EMBO Journal 17 (1998)
868–876.
date_created: 2018-12-11T11:54:54Z
date_published: 1998-02-04T00:00:00Z
date_updated: 2022-09-01T13:17:49Z
day: '04'
doi: 10.1093/emboj/17.4.868
extern: '1'
external_id:
pmid:
- '9463365'
intvolume: ' 17'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1170436/
month: '02'
oa: 1
oa_version: None
page: 868 - 876
pmid: 1
publication: EMBO Journal
publication_identifier:
issn:
- 0261-4189
publication_status: published
publisher: Wiley-Blackwell
publist_id: '5129'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Identification of a functional respiratory complex in chloroplasts through
analysis of tobacco mutants containing disrupted plastid ndh genes
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 17
year: '1998'
...
---
_id: '1956'
abstract:
- lang: eng
text: "\r\nThe plastid genomes of several plants contain ndh genes-homologues of
genes encoding subunits of the proton-pumping NADH:ubiquinone oxidoreductase,
or complex I, involved in respiration in mitochondria and eubacteria. From sequence
similarities with these genes, the ndh gene products have been suggested to form
a large protein complex (Ndh complex); however, the structure and function of
this complex remains to be established. Herein we report the isolation of the
Ndh complex from the chloroplasts of the higher plant Pisum sativum. The purification
procedure involved selective solubilization of the thylakoid membrane with dodecyl
maltoside, followed by two anion-exchange chromatography steps and one size-exclusion
chromatography step. The isolated Ndh complex has an apparent total molecular
mass of approximately 550 kDa and according to SDS/PAGE consists of at least 16
subunits including NdhA, NdhI, NdhJ, NdhK, and NdhH, which were identified by
N-terminal sequencing and immunoblotting. The Ndh complex showed an NADH- and
deamino-NADH-specific dehydrogenase activity, characteristic of complex I, when
either ferricyanide or the quinones menadione and duroquinone were used as electron
acceptors. This study describes the isolation of the chloroplast analogue of the
respiratory complex I and provides direct evidence for the function of the plastid
Ndh complex as an NADH:plastoquinone oxidoreductase. Our results are compatible
with a dual role for the Ndh complex in the chloro-respiratory and cyclic photophosphorylation
pathways."
acknowledgement: We gratefully acknowledge Dr. A.Carne (Institute of Cancer Research,
London, U.K.) for help with N-terminal sequencing. We thank Prof. C. J. Leaver (University
of Oxford, U.K.), Prof. K.-H. Süss (Institute of Plant Genetics and Crop Plant Research,
Gatersleben, Germany), and Prof. L. J. Rogers (University of Aberystwyth, U.K.)
for gifts of antiserum against maize mitochondrial cytochrome oxidase subunit 1
and cytochrome bc1 complex, spinach FNR, and spinach ferredoxin, respectively. This
work was supported by grants from The Royal Society and the Biotechnology and Biological
Sciences Research Council.
article_processing_charge: No
article_type: original
author:
- first_name: Leonid A
full_name: Sazanov, Leonid A
id: 338D39FE-F248-11E8-B48F-1D18A9856A87
last_name: Sazanov
orcid: 0000-0002-0977-7989
- first_name: Paul
full_name: Burrows, Paul
last_name: Burrows
- first_name: Peter
full_name: Nixon, Peter
last_name: Nixon
citation:
ama: 'Sazanov LA, Burrows P, Nixon P. The plastid ndh genes code for an NADH-specific
dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes.
PNAS. 1998;95(3):1319-1324. doi:10.1073/pnas.95.3.1319'
apa: 'Sazanov, L. A., Burrows, P., & Nixon, P. (1998). The plastid ndh genes
code for an NADH-specific dehydrogenase: Isolation of a complex I analogue from
pea thylakoid membranes. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.95.3.1319'
chicago: 'Sazanov, Leonid A, Paul Burrows, and Peter Nixon. “The Plastid Ndh Genes
Code for an NADH-Specific Dehydrogenase: Isolation of a Complex I Analogue from
Pea Thylakoid Membranes.” PNAS. National Academy of Sciences, 1998. https://doi.org/10.1073/pnas.95.3.1319.'
ieee: 'L. A. Sazanov, P. Burrows, and P. Nixon, “The plastid ndh genes code for
an NADH-specific dehydrogenase: Isolation of a complex I analogue from pea thylakoid
membranes,” PNAS, vol. 95, no. 3. National Academy of Sciences, pp. 1319–1324,
1998.'
ista: 'Sazanov LA, Burrows P, Nixon P. 1998. The plastid ndh genes code for an NADH-specific
dehydrogenase: Isolation of a complex I analogue from pea thylakoid membranes.
PNAS. 95(3), 1319–1324.'
mla: 'Sazanov, Leonid A., et al. “The Plastid Ndh Genes Code for an NADH-Specific
Dehydrogenase: Isolation of a Complex I Analogue from Pea Thylakoid Membranes.”
PNAS, vol. 95, no. 3, National Academy of Sciences, 1998, pp. 1319–24,
doi:10.1073/pnas.95.3.1319.'
short: L.A. Sazanov, P. Burrows, P. Nixon, PNAS 95 (1998) 1319–1324.
date_created: 2018-12-11T11:54:54Z
date_published: 1998-02-03T00:00:00Z
date_updated: 2022-09-01T13:47:05Z
day: '03'
doi: 10.1073/pnas.95.3.1319
extern: '1'
external_id:
pmid:
- '9448329 '
intvolume: ' 95'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://europepmc.org/article/pmc/18756
month: '02'
oa: 1
oa_version: None
page: 1319 - 1324
pmid: 1
publication: PNAS
publication_identifier:
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
publist_id: '5130'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The plastid ndh genes code for an NADH-specific dehydrogenase: Isolation of
a complex I analogue from pea thylakoid membranes'
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 95
year: '1998'
...
---
_id: '1449'
abstract:
- lang: eng
text: In this paper we consider a canonical compactification of M, the moduli space
of stable Higgs bundles with fixed determinant of odd degree over a Riemann surface
Σ, producing a projective variety M̄ = M ∪ Z. We give a detailed study of the
spaces M̄, Z and M. In doing so we reprove some assertions of Laumon and Thaddeus
on the nilpotent cone.
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Tamas
full_name: Hausel, Tamas
id: 4A0666D8-F248-11E8-B48F-1D18A9856A87
last_name: Hausel
citation:
ama: Hausel T. Compactification of moduli of Higgs bundles. Journal fur die Reine
und Angewandte Mathematik. 1998;1998(503):169-192. doi:10.1515/crll.1998.096
apa: Hausel, T. (1998). Compactification of moduli of Higgs bundles. Journal
Fur Die Reine Und Angewandte Mathematik. Walter de Gruyter. https://doi.org/10.1515/crll.1998.096
chicago: Hausel, Tamás. “Compactification of Moduli of Higgs Bundles.” Journal
Fur Die Reine Und Angewandte Mathematik. Walter de Gruyter, 1998. https://doi.org/10.1515/crll.1998.096.
ieee: T. Hausel, “Compactification of moduli of Higgs bundles,” Journal fur die
Reine und Angewandte Mathematik, vol. 1998, no. 503. Walter de Gruyter, pp.
169–192, 1998.
ista: Hausel T. 1998. Compactification of moduli of Higgs bundles. Journal fur die
Reine und Angewandte Mathematik. 1998(503), 169–192.
mla: Hausel, Tamás. “Compactification of Moduli of Higgs Bundles.” Journal Fur
Die Reine Und Angewandte Mathematik, vol. 1998, no. 503, Walter de Gruyter,
1998, pp. 169–92, doi:10.1515/crll.1998.096.
short: T. Hausel, Journal Fur Die Reine Und Angewandte Mathematik 1998 (1998) 169–192.
date_created: 2018-12-11T11:52:05Z
date_published: 1998-10-01T00:00:00Z
date_updated: 2022-09-01T13:51:07Z
day: '01'
doi: 10.1515/crll.1998.096
extern: '1'
external_id:
arxiv:
- math/9804083
intvolume: ' 1998'
issue: '503'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/math/9804083
month: '10'
oa: 1
oa_version: Preprint
page: 169 - 192
publication: Journal fur die Reine und Angewandte Mathematik
publication_identifier:
issn:
- 1435-5345
publication_status: published
publisher: Walter de Gruyter
publist_id: '5746'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Compactification of moduli of Higgs bundles
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1998
year: '1998'
...
---
_id: '1450'
abstract:
- lang: eng
text: In this paper we consider the topological side of a problem which is the analogue
of Sen's S-duality testing conjecture for Hitchin's moduli space M of rank 2 stable
Higgs bundles of fixed determinant of odd degree over a Riemann surface ∑. We
prove that all intersection numbers in the compactly supported cohomology of M
vanish, i.e. "there are no topological L2 harmonic forms on M". This
result generalizes the well known vanishing of the Euler characteristic of the
moduli space of rank 2 stable bundles N of fixed determinant of odd degree over
∑. Our proof shows that the vanishing of all intersection numbers of H* cpt(M)
is given by relations analogous to the Mumford relations in the cohomology ring
of N.
acknowledgement: "First of all I would like to thank my supervisor Nigel Hitchin for
suggesting Problem 1, and for his help and \r\n encouragement. I am grateful to
Michael Thaddeus for his inspiring paper [Thai], enlightening communications and
his constant interest in my work. I am also indebted to Manfred Lehn for the idea
of the proof of Theorem 6.2. I have found\r\nconversations with Michael Atiyah,
Frances Kirwan and Graeme Segal very stimulating. I thank the Mathematical Institute
and St. Catherine's College, Oxford for their hospitality during the preparation
of this work. Finally I thank Trinity College, Cambridge for financial support."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Tamas
full_name: Hausel, Tamas
id: 4A0666D8-F248-11E8-B48F-1D18A9856A87
last_name: Hausel
citation:
ama: Hausel T. Vanishing of intersection numbers on the moduli space of Higgs bundles.
Advances in Theoretical and Mathematical Physics. 1998;2(5):1011-1040.
doi:10.4310/ATMP.1998.v2.n5.a3
apa: Hausel, T. (1998). Vanishing of intersection numbers on the moduli space of
Higgs bundles. Advances in Theoretical and Mathematical Physics. International
Press. https://doi.org/10.4310/ATMP.1998.v2.n5.a3
chicago: Hausel, Tamás. “Vanishing of Intersection Numbers on the Moduli Space of
Higgs Bundles.” Advances in Theoretical and Mathematical Physics. International
Press, 1998. https://doi.org/10.4310/ATMP.1998.v2.n5.a3.
ieee: T. Hausel, “Vanishing of intersection numbers on the moduli space of Higgs
bundles,” Advances in Theoretical and Mathematical Physics, vol. 2, no.
5. International Press, pp. 1011–1040, 1998.
ista: Hausel T. 1998. Vanishing of intersection numbers on the moduli space of Higgs
bundles. Advances in Theoretical and Mathematical Physics. 2(5), 1011–1040.
mla: Hausel, Tamás. “Vanishing of Intersection Numbers on the Moduli Space of Higgs
Bundles.” Advances in Theoretical and Mathematical Physics, vol. 2, no.
5, International Press, 1998, pp. 1011–40, doi:10.4310/ATMP.1998.v2.n5.a3.
short: T. Hausel, Advances in Theoretical and Mathematical Physics 2 (1998) 1011–1040.
date_created: 2018-12-11T11:52:06Z
date_published: 1998-09-01T00:00:00Z
date_updated: 2022-09-01T14:09:49Z
day: '01'
doi: 10.4310/ATMP.1998.v2.n5.a3
extern: '1'
external_id:
arxiv:
- math/9805071
intvolume: ' 2'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://arxiv.org/abs/math/9805071
month: '09'
oa: 1
oa_version: Preprint
page: 1011 - 1040
publication: Advances in Theoretical and Mathematical Physics
publication_identifier:
issn:
- 1095-0761
publication_status: published
publisher: International Press
publist_id: '5747'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Vanishing of intersection numbers on the moduli space of Higgs bundles
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2
year: '1998'
...
---
_id: '6160'
abstract:
- lang: eng
text: Natural isolates of C. elegans exhibit either solitary or social feeding behavior.
Solitary foragers move slowly on a bacterial lawn and disperse across it, while
social foragers move rapidly on bacteria and aggregate together. A loss-of-function
mutation in the npr-1 gene, which encodes a predicted G protein–coupled receptor
similar to neuropeptide Y receptors, causes a solitary strain to take on social
behavior. Two isoforms of NPR-1 that differ at a single residue occur in the wild.
One isoform, NPR-1 215F, is found exclusively in social strains, while the other
isoform, NPR-1 215V, is found exclusively in solitary strains. An NPR-1 215V transgene
can induce solitary feeding behavior in a wild social strain. Thus, isoforms of
a putative neuropeptide receptor generate natural variation in C. elegans feeding
behavior.
author:
- first_name: Mario
full_name: de Bono, Mario
id: 4E3FF80E-F248-11E8-B48F-1D18A9856A87
last_name: de Bono
orcid: 0000-0001-8347-0443
- first_name: Cornelia I
full_name: Bargmann, Cornelia I
last_name: Bargmann
citation:
ama: de Bono M, Bargmann CI. Natural variation in a neuropeptide Y receptor homolog
modifies social behavior and food response in C. elegans. Cell. 1998;94(5):679-689.
doi:10.1016/s0092-8674(00)81609-8
apa: de Bono, M., & Bargmann, C. I. (1998). Natural variation in a neuropeptide
Y receptor homolog modifies social behavior and food response in C. elegans. Cell.
Elsevier. https://doi.org/10.1016/s0092-8674(00)81609-8
chicago: Bono, Mario de, and Cornelia I Bargmann. “Natural Variation in a Neuropeptide
Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.”
Cell. Elsevier, 1998. https://doi.org/10.1016/s0092-8674(00)81609-8.
ieee: M. de Bono and C. I. Bargmann, “Natural variation in a neuropeptide Y receptor
homolog modifies social behavior and food response in C. elegans,” Cell,
vol. 94, no. 5. Elsevier, pp. 679–689, 1998.
ista: de Bono M, Bargmann CI. 1998. Natural variation in a neuropeptide Y receptor
homolog modifies social behavior and food response in C. elegans. Cell. 94(5),
679–689.
mla: de Bono, Mario, and Cornelia I. Bargmann. “Natural Variation in a Neuropeptide
Y Receptor Homolog Modifies Social Behavior and Food Response in C. Elegans.”
Cell, vol. 94, no. 5, Elsevier, 1998, pp. 679–89, doi:10.1016/s0092-8674(00)81609-8.
short: M. de Bono, C.I. Bargmann, Cell 94 (1998) 679–689.
date_created: 2019-03-21T10:32:06Z
date_published: 1998-09-04T00:00:00Z
date_updated: 2021-01-12T08:06:28Z
day: '04'
doi: 10.1016/s0092-8674(00)81609-8
extern: '1'
external_id:
pmid:
- '9741632'
intvolume: ' 94'
issue: '5'
language:
- iso: eng
month: '09'
oa_version: None
page: 679-689
pmid: 1
publication: Cell
publication_identifier:
issn:
- 0092-8674
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Natural variation in a neuropeptide Y receptor homolog modifies social behavior
and food response in C. elegans
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 94
year: '1998'
...
---
_id: '11680'
abstract:
- lang: eng
text: 'We present a model for edge updates with restricted randomness in dynamic
graph algorithms and a general technique for analyzing the expected running time
of an update operation. This model is able to capture the average case in many
applications, since (1) it allows restrictions on the set of edges which can be
used for insertions and (2) the type (insertion or deletion) of each update operation
is arbitrary, i.e., not random. We use our technique to analyze existing and new
dynamic algorithms for the following problems: maximum cardinality matching, minimum
spanning forest, connectivity, 2-edge connectivity, k -edge connectivity, k -vertex
connectivity, and bipartiteness. Given a random graph G with m 0 edges and n vertices
and a sequence of l update operations such that the graph contains m i edges after
operation i , the expected time for performing the updates for any l is O(llogn+∑li=1n/m−−√i)
in the case of minimum spanning forests, connectivity, 2-edge connectivity, and
bipartiteness. The expected time per update operation is O(n) in the case of maximum
matching. We also give improved bounds for k -edge and k -vertex connectivity.
Additionally we give an insertions-only algorithm for maximum cardinality matching
with worst-case O(n) amortized time per insertion.'
acknowledgement: The authors would like to thank Emo Welzl for helpful discussions.
article_processing_charge: No
article_type: original
author:
- first_name: D.
full_name: Alberts, D.
last_name: Alberts
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: Alberts D, Henzinger MH. Average-case analysis of dynamic graph algorithms.
Algorithmica. 1998;20:31-60. doi:10.1007/pl00009186
apa: Alberts, D., & Henzinger, M. H. (1998). Average-case analysis of dynamic
graph algorithms. Algorithmica. Springer Nature. https://doi.org/10.1007/pl00009186
chicago: Alberts, D., and Monika H Henzinger. “Average-Case Analysis of Dynamic
Graph Algorithms.” Algorithmica. Springer Nature, 1998. https://doi.org/10.1007/pl00009186.
ieee: D. Alberts and M. H. Henzinger, “Average-case analysis of dynamic graph algorithms,”
Algorithmica, vol. 20. Springer Nature, pp. 31–60, 1998.
ista: Alberts D, Henzinger MH. 1998. Average-case analysis of dynamic graph algorithms.
Algorithmica. 20, 31–60.
mla: Alberts, D., and Monika H. Henzinger. “Average-Case Analysis of Dynamic Graph
Algorithms.” Algorithmica, vol. 20, Springer Nature, 1998, pp. 31–60, doi:10.1007/pl00009186.
short: D. Alberts, M.H. Henzinger, Algorithmica 20 (1998) 31–60.
date_created: 2022-07-28T06:50:51Z
date_published: 1998-01-01T00:00:00Z
date_updated: 2023-02-21T16:33:27Z
day: '01'
doi: 10.1007/pl00009186
extern: '1'
intvolume: ' 20'
keyword:
- Dynamic graph algorithm
- Average-case analysis
- Minimum spanning forest
- Connectivity
- Bipartiteness
- Maximum matching.
language:
- iso: eng
month: '01'
oa_version: None
page: 31-60
publication: Algorithmica
publication_identifier:
eissn:
- 1432-0541
issn:
- 0178-4617
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
record:
- id: '11928'
relation: earlier_version
status: public
scopus_import: '1'
status: public
title: Average-case analysis of dynamic graph algorithms
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20
year: '1998'
...
---
_id: '11681'
abstract:
- lang: eng
text: We prove lower bounds on the complexity of maintaining fully dynamic k -edge
or k -vertex connectivity in plane graphs and in (k-1) -vertex connected graphs.
We show an amortized lower bound of Ω (log n / {k (log log n} + log b)) per edge
insertion, deletion, or query operation in the cell probe model, where b is the
word size of the machine and n is the number of vertices in G . We also show an
amortized lower bound of Ω (log n /(log log n + log b)) per operation for fully
dynamic planarity testing in embedded graphs. These are the first lower bounds
for fully dynamic connectivity problems.
acknowledgement: .
article_processing_charge: No
article_type: original
author:
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
- first_name: M. L.
full_name: Fredman, M. L.
last_name: Fredman
citation:
ama: Henzinger MH, Fredman ML. Lower bounds for fully dynamic connectivity problems
in graphs. Algorithmica. 1998;22(3):351-362. doi:10.1007/pl00009228
apa: Henzinger, M. H., & Fredman, M. L. (1998). Lower bounds for fully dynamic
connectivity problems in graphs. Algorithmica. Springer Nature. https://doi.org/10.1007/pl00009228
chicago: Henzinger, Monika H, and M. L. Fredman. “Lower Bounds for Fully Dynamic
Connectivity Problems in Graphs.” Algorithmica. Springer Nature, 1998.
https://doi.org/10.1007/pl00009228.
ieee: M. H. Henzinger and M. L. Fredman, “Lower bounds for fully dynamic connectivity
problems in graphs,” Algorithmica, vol. 22, no. 3. Springer Nature, pp.
351–362, 1998.
ista: Henzinger MH, Fredman ML. 1998. Lower bounds for fully dynamic connectivity
problems in graphs. Algorithmica. 22(3), 351–362.
mla: Henzinger, Monika H., and M. L. Fredman. “Lower Bounds for Fully Dynamic Connectivity
Problems in Graphs.” Algorithmica, vol. 22, no. 3, Springer Nature, 1998,
pp. 351–62, doi:10.1007/pl00009228.
short: M.H. Henzinger, M.L. Fredman, Algorithmica 22 (1998) 351–362.
date_created: 2022-07-28T06:58:36Z
date_published: 1998-11-01T00:00:00Z
date_updated: 2022-09-12T09:03:36Z
day: '01'
doi: 10.1007/pl00009228
extern: '1'
intvolume: ' 22'
issue: '3'
keyword:
- Dynamic planarity testing
- Dynamic connectivity testing
- Lower bounds
- Cell probe model
language:
- iso: eng
month: '11'
oa_version: None
page: 351-362
publication: Algorithmica
publication_identifier:
eissn:
- 1432-0541
issn:
- 0178-4617
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Lower bounds for fully dynamic connectivity problems in graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 22
year: '1998'
...
---
_id: '11682'
abstract:
- lang: eng
text: We consider the parametric minimum spanning tree problem, in which we are
given a graph with edge weights that are linear functions of a parameter /spl
lambda/ and wish to compute the sequence of minimum spanning trees generated as
/spl lambda/ varies. We also consider the kinetic minimum spanning tree problem,
in which /spl lambda/ represents time and the graph is subject in addition to
changes such as edge insertions, deletions, and modifications of the weight functions
as time progresses. We solve both problems in time O(n/sup 2/3/log/sup 4/3/) per
combinatorial change in the tree (or randomized O(n/sup 2/3/log/sup 4/3/ n) per
change). Our time bounds reduce to O(n/sup 1/2/log/sup 3/2/ n) per change (O(n/sup
1/2/log n) randomized) for planar graphs or other minor-closed families of graphs,
and O(n/sup 1/4/log/sup 3/2/ n) per change (O(n/sup 1/4/ log n) randomized) for
planar graphs with weight changes but no insertions or deletions.
article_processing_charge: No
author:
- first_name: P. K.
full_name: Agarwal, P. K.
last_name: Agarwal
- first_name: D.
full_name: EppsteinL. J. Guibas, D.
last_name: EppsteinL. J. Guibas
- first_name: Monika H
full_name: Henzinger, Monika H
id: 540c9bbd-f2de-11ec-812d-d04a5be85630
last_name: Henzinger
orcid: 0000-0002-5008-6530
citation:
ama: 'Agarwal PK, EppsteinL. J. Guibas D, Henzinger MH. Parametric and kinetic minimum
spanning trees. In: Proceedings of the 39th Annual Symposium on Foundations
of Computer Science. ; 1998:596-605. doi:10.1109/SFCS.1998.743510'
apa: Agarwal, P. K., EppsteinL. J. Guibas, D., & Henzinger, M. H. (1998). Parametric
and kinetic minimum spanning trees. In Proceedings of the 39th Annual Symposium
on Foundations of Computer Science (pp. 596–605). Palo Alto, CA, United States.
https://doi.org/10.1109/SFCS.1998.743510
chicago: Agarwal, P. K., D. EppsteinL. J. Guibas, and Monika H Henzinger. “Parametric
and Kinetic Minimum Spanning Trees.” In Proceedings of the 39th Annual Symposium
on Foundations of Computer Science, 596–605, 1998. https://doi.org/10.1109/SFCS.1998.743510.
ieee: P. K. Agarwal, D. EppsteinL. J. Guibas, and M. H. Henzinger, “Parametric and
kinetic minimum spanning trees,” in Proceedings of the 39th Annual Symposium
on Foundations of Computer Science, Palo Alto, CA, United States, 1998, pp.
596–605.
ista: Agarwal PK, EppsteinL. J. Guibas D, Henzinger MH. 1998. Parametric and kinetic
minimum spanning trees. Proceedings of the 39th Annual Symposium on Foundations
of Computer Science. Annual IEEE Symposium on Foundations of Computer Science,
596–605.
mla: Agarwal, P. K., et al. “Parametric and Kinetic Minimum Spanning Trees.” Proceedings
of the 39th Annual Symposium on Foundations of Computer Science, 1998, pp.
596–605, doi:10.1109/SFCS.1998.743510.
short: P.K. Agarwal, D. EppsteinL. J. Guibas, M.H. Henzinger, in:, Proceedings of
the 39th Annual Symposium on Foundations of Computer Science, 1998, pp. 596–605.
conference:
end_date: 1998-11-11
location: Palo Alto, CA, United States
name: Annual IEEE Symposium on Foundations of Computer Science
start_date: 1998-11-08
date_created: 2022-07-28T07:21:34Z
date_published: 1998-09-01T00:00:00Z
date_updated: 2023-02-09T11:28:52Z
day: '01'
doi: 10.1109/SFCS.1998.743510
extern: '1'
language:
- iso: eng
month: '09'
oa_version: None
page: 596-605
publication: Proceedings of the 39th Annual Symposium on Foundations of Computer Science
publication_identifier:
isbn:
- 0-8186-9172-7
issn:
- 0272-5428
publication_status: published
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parametric and kinetic minimum spanning trees
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1998'
...