---
_id: '867'
abstract:
- lang: eng
text: Genes with new functions often evolve by gene duplication. Alternative splicing
is another means of evolutionary innovation in eukaryotes, which allows a single
gene to encode functionally diverse proteins. We investigate a connection between
these two evolutionary phenomena. For ∼10% of the described cases of substitution
alternative splicing, such that either one or another amino acid sequence is included
into the protein, evidence of origin by tandem exon duplication was found. This
is a conservative estimate because alternative exons are typically short and,
on many occasions, duplicates may have diverged beyond recognition. Dating exon
duplications through a combination of the available experimental data on alternative
splicing in orthologous genes from different species and computational analysis
indicates that most of the duplications antedate at least the radiation of mammalian
orders or even the radiation of vertebrate classes. At present, tandem exon duplication
is the only mechanism of evolution of substitution alternative splicing that can
be specifically demonstrated. Along with gene duplication, this could be a major
route for generating functional diversity during evolution of multicellular eukaryotes.
article_processing_charge: No
article_type: original
author:
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
citation:
ama: Kondrashov F, Koonin E. Origin of alternative splicing by tandem exon duplication.
Human Molecular Genetics. 2001;10(23):2661-2669. doi:10.1093/hmg/10.23.2661
apa: Kondrashov, F., & Koonin, E. (2001). Origin of alternative splicing by
tandem exon duplication. Human Molecular Genetics. Oxford University Press.
https://doi.org/10.1093/hmg/10.23.2661
chicago: Kondrashov, Fyodor, and Eugene Koonin. “Origin of Alternative Splicing
by Tandem Exon Duplication.” Human Molecular Genetics. Oxford University
Press, 2001. https://doi.org/10.1093/hmg/10.23.2661.
ieee: F. Kondrashov and E. Koonin, “Origin of alternative splicing by tandem exon
duplication,” Human Molecular Genetics, vol. 10, no. 23. Oxford University
Press, pp. 2661–2669, 2001.
ista: Kondrashov F, Koonin E. 2001. Origin of alternative splicing by tandem exon
duplication. Human Molecular Genetics. 10(23), 2661–2669.
mla: Kondrashov, Fyodor, and Eugene Koonin. “Origin of Alternative Splicing by Tandem
Exon Duplication.” Human Molecular Genetics, vol. 10, no. 23, Oxford University
Press, 2001, pp. 2661–69, doi:10.1093/hmg/10.23.2661.
short: F. Kondrashov, E. Koonin, Human Molecular Genetics 10 (2001) 2661–2669.
date_created: 2018-12-11T11:48:55Z
date_published: 2001-11-01T00:00:00Z
date_updated: 2023-06-02T08:39:47Z
day: '01'
doi: 10.1093/hmg/10.23.2661
extern: '1'
external_id:
pmid:
- '11726553'
intvolume: ' 10'
issue: '23'
language:
- iso: eng
month: '11'
oa_version: Published Version
page: 2661 - 2669
pmid: 1
publication: Human Molecular Genetics
publication_identifier:
issn:
- 0964-6906
publication_status: published
publisher: Oxford University Press
publist_id: '6777'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Origin of alternative splicing by tandem exon duplication
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 10
year: '2001'
...
---
_id: '874'
abstract:
- lang: eng
text: Sex is thought to facilitate accumulation of initially rare beneficial mutations
by allowing simultaneous allele replacements at many loci. However, this advantage
of sex depends on a restrictive assumption that the fitness of a genotype is determined
by fitness potential, a single intermediate variable to which all loci contribute
additively, so that new alleles can accumulate in any order. Individual-based
simulations of sexual and asexual populations reveal that under generic selection,
sex often retards adaptive evolution. When new alleles are beneficial only if
they accumulate in a prescribed order, a sexual population may evolve two or more
times slower than an asexual population because only asexual reproduction allows
some overlap of successive allele replacements. Many other fitness surfaces lead
to an even greater disadvantage of sex. Thus, either sex exists in spite of its
impact on the rate of adaptive allele replacements, or natural fitness surfaces
have rather specific properties, at least at the scale of intrapopulation genetic
variability.
article_processing_charge: No
article_type: original
author:
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Alexey
full_name: Kondrashov, Alexey
last_name: Kondrashov
citation:
ama: Kondrashov F, Kondrashov A. Multidimensional epistasis and the disadvantage
of sex. PNAS. 2001;98(21):12089-12092. doi:10.1073/pnas.211214298
apa: Kondrashov, F., & Kondrashov, A. (2001). Multidimensional epistasis and
the disadvantage of sex. PNAS. National Academy of Sciences. https://doi.org/10.1073/pnas.211214298
chicago: Kondrashov, Fyodor, and Alexey Kondrashov. “Multidimensional Epistasis
and the Disadvantage of Sex.” PNAS. National Academy of Sciences, 2001.
https://doi.org/10.1073/pnas.211214298.
ieee: F. Kondrashov and A. Kondrashov, “Multidimensional epistasis and the disadvantage
of sex,” PNAS, vol. 98, no. 21. National Academy of Sciences, pp. 12089–12092,
2001.
ista: Kondrashov F, Kondrashov A. 2001. Multidimensional epistasis and the disadvantage
of sex. PNAS. 98(21), 12089–12092.
mla: Kondrashov, Fyodor, and Alexey Kondrashov. “Multidimensional Epistasis and
the Disadvantage of Sex.” PNAS, vol. 98, no. 21, National Academy of Sciences,
2001, pp. 12089–92, doi:10.1073/pnas.211214298.
short: F. Kondrashov, A. Kondrashov, PNAS 98 (2001) 12089–12092.
date_created: 2018-12-11T11:48:58Z
date_published: 2001-10-09T00:00:00Z
date_updated: 2023-06-02T08:18:22Z
day: '09'
doi: 10.1073/pnas.211214298
extern: '1'
external_id:
pmid:
- '11593020'
intvolume: ' 98'
issue: '21'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC59772/
month: '10'
oa: 1
oa_version: Published Version
page: 12089 - 12092
pmid: 1
publication: PNAS
publication_identifier:
issn:
- 0027-8424
publication_status: published
publisher: National Academy of Sciences
publist_id: '6774'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Multidimensional epistasis and the disadvantage of sex
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 98
year: '2001'
...
---
_id: '888'
abstract:
- lang: eng
text: 'BACKGROUND: Detection of changes in a protein''s evolutionary rate may reveal
cases of change in that protein''s function. We developed and implemented a simple
relative rates test in an attempt to assess the rate constancy of protein evolution
and to detect cases of functional diversification between orthologous proteins.
The test was performed on clusters of orthologous protein sequences from complete
bacterial genomes (Chlamydia trachomatis, C. muridarum and Chlamydophila pneumoniae),
complete archaeal genomes (Pyrococcus horikoshii, P. abyssi and P. furiosus) and
partially sequenced mammalian genomes (human, mouse and rat). RESULTS: Amino-acid
sequence evolution rates are significantly correlated on different branches of
phylogenetic trees representing the great majority of analyzed orthologous protein
sets from all three domains of life. However, approximately 1% of the proteins
from each group of species deviates from this pattern and instead shows variation
that is consistent with an acceleration of the rate of amino-acid substitution,
which may be due to functional diversification. Most of the putative functionally
diversified proteins from all three species groups are predicted to function at
the periphery of the cells and mediate their interaction with the environment.
CONCLUSIONS: Relative rates of protein evolution are remarkably constant for the
three species groups analyzed here. Deviations from this rate constancy are probably
due to changes in selective constraints associated with diversification between
orthologs. Functional diversification between orthologs is thought to be a relatively
rare event. However, the resolution afforded by the test designed specifically
for genomic-scale datasets allowed us to identify numerous cases of possible functional
diversification between orthologous proteins.'
acknowledgement: We thank Alexey Kondrashov for many helpful discussions and constructive
criticisms, Charles DeLisi, David Landsman, Detlef Leipe, Wojciech Makalowski and
Itai Yanai for critical reading of the manuscript and constructive comments and
L. Aravind for advice on protein function prediction. The release of the unpublished
P. furiosus genome sequence by the Utah Genome Center at the University of Utah
is acknowledged and appreciated.
article_number: research0053.1
article_processing_charge: No
article_type: original
author:
- first_name: Ingo
full_name: Jordan, Ingo
last_name: Jordan
- first_name: Fyodor
full_name: Kondrashov, Fyodor
id: 44FDEF62-F248-11E8-B48F-1D18A9856A87
last_name: Kondrashov
orcid: 0000-0001-8243-4694
- first_name: Igor
full_name: Rogozin, Igor
last_name: Rogozin
- first_name: Roman
full_name: Tatusov, Roman
last_name: Tatusov
- first_name: Yuri
full_name: Wolf, Yuri
last_name: Wolf
- first_name: Eugene
full_name: Koonin, Eugene
last_name: Koonin
citation:
ama: Jordan I, Kondrashov F, Rogozin I, Tatusov R, Wolf Y, Koonin E. Constant relative
rate of protein evolution and detection of functional diversification among bacterial,
archaeal and eukaryotic proteins . Genome Biology. 2001;2(12). doi:10.1186/gb-2001-2-12-research0053
apa: Jordan, I., Kondrashov, F., Rogozin, I., Tatusov, R., Wolf, Y., & Koonin,
E. (2001). Constant relative rate of protein evolution and detection of functional
diversification among bacterial, archaeal and eukaryotic proteins . Genome
Biology. BioMed Central. https://doi.org/10.1186/gb-2001-2-12-research0053
chicago: Jordan, Ingo, Fyodor Kondrashov, Igor Rogozin, Roman Tatusov, Yuri Wolf,
and Eugene Koonin. “Constant Relative Rate of Protein Evolution and Detection
of Functional Diversification among Bacterial, Archaeal and Eukaryotic Proteins
.” Genome Biology. BioMed Central, 2001. https://doi.org/10.1186/gb-2001-2-12-research0053.
ieee: I. Jordan, F. Kondrashov, I. Rogozin, R. Tatusov, Y. Wolf, and E. Koonin,
“Constant relative rate of protein evolution and detection of functional diversification
among bacterial, archaeal and eukaryotic proteins ,” Genome Biology, vol.
2, no. 12. BioMed Central, 2001.
ista: Jordan I, Kondrashov F, Rogozin I, Tatusov R, Wolf Y, Koonin E. 2001. Constant
relative rate of protein evolution and detection of functional diversification
among bacterial, archaeal and eukaryotic proteins . Genome Biology. 2(12), research0053.1.
mla: Jordan, Ingo, et al. “Constant Relative Rate of Protein Evolution and Detection
of Functional Diversification among Bacterial, Archaeal and Eukaryotic Proteins
.” Genome Biology, vol. 2, no. 12, research0053.1, BioMed Central, 2001,
doi:10.1186/gb-2001-2-12-research0053.
short: I. Jordan, F. Kondrashov, I. Rogozin, R. Tatusov, Y. Wolf, E. Koonin, Genome
Biology 2 (2001).
date_created: 2018-12-11T11:49:02Z
date_published: 2001-01-01T00:00:00Z
date_updated: 2023-05-31T12:15:37Z
day: '01'
doi: 10.1186/gb-2001-2-12-research0053
extern: '1'
external_id:
pmid:
- '11790256'
intvolume: ' 2'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC64838/
month: '01'
oa: 1
oa_version: Published Version
pmid: 1
publication: Genome Biology
publication_identifier:
issn:
- 1465-6906
publication_status: published
publisher: BioMed Central
publist_id: '6758'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Constant relative rate of protein evolution and detection of functional diversification
among bacterial, archaeal and eukaryotic proteins '
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2
year: '2001'
...
---
_id: '9444'
abstract:
- lang: eng
text: Epigenetic silenced alleles of the Arabidopsis SUPERMANlocus (the clark kent
alleles) are associated with dense hypermethylation at noncanonical cytosines
(CpXpG and asymmetric sites, where X = A, T, C, or G). A genetic screen for suppressors
of a hypermethylated clark kent mutant identified nine loss-of-function alleles
of CHROMOMETHYLASE3(CMT3), a novel cytosine methyltransferase homolog. These cmt3
mutants display a wild-type morphology but exhibit decreased CpXpG methylation
of the SUP gene and of other sequences throughout the genome. They also show reactivated
expression of endogenous retrotransposon sequences. These results show that a
non-CpG DNA methyltransferase is responsible for maintaining epigenetic gene silencing.
article_processing_charge: No
article_type: original
author:
- first_name: A. M.
full_name: Lindroth, A. M.
last_name: Lindroth
- first_name: Xiaofeng
full_name: Cao, Xiaofeng
last_name: Cao
- first_name: James P.
full_name: Jackson, James P.
last_name: Jackson
- first_name: Daniel
full_name: Zilberman, Daniel
id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
last_name: Zilberman
orcid: 0000-0002-0123-8649
- first_name: Claire M.
full_name: McCallum, Claire M.
last_name: McCallum
- first_name: Steven
full_name: Henikoff, Steven
last_name: Henikoff
- first_name: Steven E.
full_name: Jacobsen, Steven E.
last_name: Jacobsen
citation:
ama: Lindroth AM, Cao X, Jackson JP, et al. Requirement of CHROMOMETHYLASE3 for
maintenance of CpXpG methylation. Science. 2001;292(5524):2077-2080. doi:10.1126/science.1059745
apa: Lindroth, A. M., Cao, X., Jackson, J. P., Zilberman, D., McCallum, C. M., Henikoff,
S., & Jacobsen, S. E. (2001). Requirement of CHROMOMETHYLASE3 for maintenance
of CpXpG methylation. Science. American Association for the Advancement
of Science. https://doi.org/10.1126/science.1059745
chicago: Lindroth, A. M., Xiaofeng Cao, James P. Jackson, Daniel Zilberman, Claire
M. McCallum, Steven Henikoff, and Steven E. Jacobsen. “Requirement of CHROMOMETHYLASE3
for Maintenance of CpXpG Methylation.” Science. American Association for
the Advancement of Science, 2001. https://doi.org/10.1126/science.1059745.
ieee: A. M. Lindroth et al., “Requirement of CHROMOMETHYLASE3 for maintenance
of CpXpG methylation,” Science, vol. 292, no. 5524. American Association
for the Advancement of Science, pp. 2077–2080, 2001.
ista: Lindroth AM, Cao X, Jackson JP, Zilberman D, McCallum CM, Henikoff S, Jacobsen
SE. 2001. Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation.
Science. 292(5524), 2077–2080.
mla: Lindroth, A. M., et al. “Requirement of CHROMOMETHYLASE3 for Maintenance of
CpXpG Methylation.” Science, vol. 292, no. 5524, American Association for
the Advancement of Science, 2001, pp. 2077–80, doi:10.1126/science.1059745.
short: A.M. Lindroth, X. Cao, J.P. Jackson, D. Zilberman, C.M. McCallum, S. Henikoff,
S.E. Jacobsen, Science 292 (2001) 2077–2080.
date_created: 2021-06-02T13:35:16Z
date_published: 2001-06-15T00:00:00Z
date_updated: 2021-12-14T08:40:32Z
day: '15'
department:
- _id: DaZi
doi: 10.1126/science.1059745
extern: '1'
external_id:
pmid:
- '11349138'
intvolume: ' 292'
issue: '5524'
keyword:
- Multidisciplinary
language:
- iso: eng
month: '06'
oa_version: None
page: 2077-2080
pmid: 1
publication: Science
publication_identifier:
eissn:
- 1095-9203
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Requirement of CHROMOMETHYLASE3 for maintenance of CpXpG methylation
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 292
year: '2001'
...
---
_id: '4599'
abstract:
- lang: eng
text: 'State-space explosion is a fundamental obstacle in the formal verification
of designs and protocols. Several techniques for combating this problem have emerged
in the past few years, among which two are significant: partial-order reduction
and symbolic state-space search. In asynchronous systems, interleavings of independent
concurrent events are equivalent, and only a representative interleaving needs
to be explored to verify local properties. Partial-order methods exploit this
redundancy and visit only a subset of the reachable states. Symbolic techniques,
on the other hand, capture the transition relation of a system and the set of
reachable states as boolean functions. In many cases, these functions can be represented
compactly using binary decision diagrams (BDDs). Traditionally, the two techniques
have been practiced by two different schools—partial-order methods with enumerative
depth-first search for the analysis of asynchronous network protocols, and symbolic
breadth-first search for the analysis of synchronous hardware designs. We combine
both approaches and develop a method for using partial-order reduction techniques
in symbolic BDD-based invariant checking. We present theoretical results to prove
the correctness of the method, and experimental results to demonstrate its efficacy.'
acknowledgement: Gerard Holzmann provided us with information on SPIN. Ken McMillan
and Doron Peled contributed through discussions. The VIS group at UC Berkeley and
Rajeev Ranjan in particular helped with the experiments.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Robert
full_name: Brayton, Robert
last_name: Brayton
- 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: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction
in symbolic state-space exploration. Formal Methods in System Design. 2001;18(2):97-116.
doi:10.1023/A:1008767206905
apa: Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (2001).
Partial-order reduction in symbolic state-space exploration. Formal Methods
in System Design. Springer. https://doi.org/10.1023/A:1008767206905
chicago: Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram
Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal
Methods in System Design. Springer, 2001. https://doi.org/10.1023/A:1008767206905.
ieee: R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order
reduction in symbolic state-space exploration,” Formal Methods in System Design,
vol. 18, no. 2. Springer, pp. 97–116, 2001.
ista: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order
reduction in symbolic state-space exploration. Formal Methods in System Design.
18(2), 97–116.
mla: Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.”
Formal Methods in System Design, vol. 18, no. 2, Springer, 2001, pp. 97–116,
doi:10.1023/A:1008767206905.
short: R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods
in System Design 18 (2001) 97–116.
date_created: 2018-12-11T12:09:41Z
date_published: 2001-03-01T00:00:00Z
date_updated: 2023-05-08T12:22:38Z
day: '01'
doi: 10.1023/A:1008767206905
extern: '1'
intvolume: ' 18'
issue: '2'
language:
- iso: eng
month: '03'
oa_version: None
page: 97 - 116
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '108'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Partial-order reduction in symbolic state-space exploration
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 18
year: '2001'
...
---
_id: '4600'
abstract:
- lang: eng
text: 'Model checking is a practical tool for automated debugging of embedded software.
In model checking, a high-level description of a system is compared against a
logical correctness requirement to discover inconsistencies. Since model checking
is based on exhaustive state-space exploration and the size of the state space
of a design grows exponentially with the size of the description, scalability
remains a challenge. We have thus developed techniques for exploiting modular
design structure during model checking, and the model checker jMocha (Java MOdel-CHecking
Algorithm) is based on this theme. Instead of manipulating unstructured state-transition
graphs, it supports the hierarchical modeling framework of reactive modules. jMocha
is a growing interactive software environment for specification, simulation and
verification, and is intended as a vehicle for the development of new verification
algorithms and approaches. It is written in Java and uses native C-code BDD libraries
from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users;
(2) a simulator that displays traces in a message sequence chart fashion; (3)
requirements verification both by symbolic and enumerative model checking; (4)
implementation verification by checking trace containment; (5) a proof manager
that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting
LANGuage) for the rapid and structured development of new verification algorithms.
jMocha is available publicly at ; it is a successor and extension of the original
Mocha tool that was entirely written in C.'
acknowledgement: 'We thank Himyanshu Anand, Ben Horowitz, Franjo Ivancic, Michael
McDougall, Marius Minea, Oliver Moeller. Shaz Qadeer, Sriram Rajamani, and Jean-Francois
Raskin for their assistance in the development of JMOCHA. The MOCHA project is funded
in part by the DARPA grant NAG2-1214, the NSF CAREER awards CCR95-01708 and CCR97-34115,
the NSF grant CCR99-70925, the NSF ITR grant CCR0085949, the MARC0 grant 98-DT-660,
and the SRC contracts 99-TJ-683.003 and 99-TJ-688. '
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: Radu
full_name: Grosu, Radu
last_name: Grosu
- 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: Myong
full_name: Kang, Myong
last_name: Kang
- first_name: Christoph
full_name: Kirsch, Christoph
last_name: Kirsch
- first_name: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
- first_name: Bow
full_name: Wang, Bow
last_name: Wang
citation:
ama: 'Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits
design structure. In: Proceedings of the 23rd International Conference on Software
Engineering. IEEE; 2001:835-836. doi:10.1109/ICSE.2001.919196'
apa: 'Alur, R., De Alfaro, L., Grosu, R., Henzinger, T. A., Kang, M., Kirsch, C.,
… Wang, B. (2001). jMocha: A model-checking tool that exploits design structure.
In Proceedings of the 23rd International Conference on Software Engineering
(pp. 835–836). IEEE. https://doi.org/10.1109/ICSE.2001.919196'
chicago: 'Alur, Rajeev, Luca De Alfaro, Radu Grosu, Thomas A Henzinger, Myong Kang,
Christoph Kirsch, Ritankar Majumdar, Freddy Mang, and Bow Wang. “JMocha: A Model-Checking
Tool That Exploits Design Structure.” In Proceedings of the 23rd International
Conference on Software Engineering, 835–36. IEEE, 2001. https://doi.org/10.1109/ICSE.2001.919196.'
ieee: 'R. Alur et al., “jMocha: A model-checking tool that exploits design
structure,” in Proceedings of the 23rd International Conference on Software
Engineering, 2001, pp. 835–836.'
ista: 'Alur R, De Alfaro L, Grosu R, Henzinger TA, Kang M, Kirsch C, Majumdar R,
Mang F, Wang B. 2001. jMocha: A model-checking tool that exploits design structure.
Proceedings of the 23rd International Conference on Software Engineering. ICSE:
Software Engineering, 835–836.'
mla: 'Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.”
Proceedings of the 23rd International Conference on Software Engineering,
IEEE, 2001, pp. 835–36, doi:10.1109/ICSE.2001.919196.'
short: R. Alur, L. De Alfaro, R. Grosu, T.A. Henzinger, M. Kang, C. Kirsch, R. Majumdar,
F. Mang, B. Wang, in:, Proceedings of the 23rd International Conference on Software
Engineering, IEEE, 2001, pp. 835–836.
conference:
name: 'ICSE: Software Engineering'
date_created: 2018-12-11T12:09:41Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T14:06:55Z
day: '07'
doi: 10.1109/ICSE.2001.919196
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 835 - 836
publication: Proceedings of the 23rd International Conference on Software Engineering
publication_identifier:
isbn:
- '0769510507'
publication_status: published
publisher: IEEE
publist_id: '109'
quality_controlled: '1'
status: public
title: 'jMocha: A model-checking tool that exploits design structure'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4622'
abstract:
- lang: eng
text: Conventional type systems specify interfaces in terms of values and domains.
We present a light-weight formalism that captures the temporal aspects of software
component interfaces. Specifically, we use an automata-based language to capture
both input assumptions about the order in which the methods of a component are
called, and output guarantees about the order in which the component calls external
methods. The formalism supports automatic compatability checks between interface
models, and thus constitutes a type system for component interaction. Unlike traditional
uses of automata, our formalism is based on an optimistic approach to composition,
and on an alternating approach to design refinement. According to the optimistic
approach, two components are compatible if there is some environment that can
make them work together. According to the alternating approach, one interface
refines another if it has weaker input assumptions, and stronger output guarantees.
We show that these notions have game-theoretic foundations that lead to efficient
algorithms for checking compatibility and refinement.
acknowledgement: We thank Edward A. Lee, Xiaojun Liu, Freddy Mang, and Yuhong Xiong
for fruitful discussions. This research was supported in part by the AFOSR MURI
grant F49620-00-1-0327, the DARPA MoBIES grant F33615-00-C-1703, the MARCO GSRC
grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.
article_processing_charge: No
author:
- 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
citation:
ama: 'De Alfaro L, Henzinger TA. Interface automata. In: Proceedings of the 8th
European Software Engineering Conference. ACM; 2001:109-120. doi:10.1145/503209.503226'
apa: 'De Alfaro, L., & Henzinger, T. A. (2001). Interface automata. In Proceedings
of the 8th European software engineering conference (pp. 109–120). Vienna,
Austria: ACM. https://doi.org/10.1145/503209.503226'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface Automata.” In Proceedings
of the 8th European Software Engineering Conference, 109–20. ACM, 2001. https://doi.org/10.1145/503209.503226.
ieee: L. De Alfaro and T. A. Henzinger, “Interface automata,” in Proceedings
of the 8th European software engineering conference, Vienna, Austria, 2001,
pp. 109–120.
ista: 'De Alfaro L, Henzinger TA. 2001. Interface automata. Proceedings of the 8th
European software engineering conference. FSE: Foundations of Software Engineering,
109–120.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Interface Automata.” Proceedings
of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–20,
doi:10.1145/503209.503226.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 8th European Software
Engineering Conference, ACM, 2001, pp. 109–120.
conference:
end_date: 2001-09-14
location: Vienna, Austria
name: 'FSE: Foundations of Software Engineering'
start_date: 2001-09-10
date_created: 2018-12-11T12:09:48Z
date_published: 2001-06-01T00:00:00Z
date_updated: 2023-05-08T12:01:02Z
day: '01'
doi: 10.1145/503209.503226
extern: '1'
language:
- iso: eng
month: '06'
oa_version: None
page: 109 - 120
publication: Proceedings of the 8th European software engineering conference
publication_identifier:
isbn:
- '9781581133905'
publication_status: published
publisher: ACM
publist_id: '83'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface automata
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4623'
abstract:
- lang: eng
text: We classify component-based models of computation into component models and
interface models. A component model specifies for each component howthe component
behaves in an arbitrary environment; an interface model specifies for each component
what the component expects from the environment. Component models support compositional
abstraction, and therefore component-based verification. Interface models support
compositional refinement, and therefore componentbased design. Many aspects of
interface models, such as compatibility and refinement checking between interfaces,
are properly viewed in a gametheoretic setting, where the input and output values
of an interface are chosen by different players.
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
the DARPA ITO grant F33615-00-C-1693, the MARCO grant 98-DT-660, and the NSF ITR
grant CCR-0085949.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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
citation:
ama: 'De Alfaro L, Henzinger TA. Interface theories for component-based design.
In: Proceedings of the 1st International Workshop on Embedded Software.
Vol 2211. ACM; 2001:148-165. doi:10.1007/3-540-45449-7_11'
apa: 'De Alfaro, L., & Henzinger, T. A. (2001). Interface theories for component-based
design. In Proceedings of the 1st International Workshop on Embedded Software
(Vol. 2211, pp. 148–165). Tahoe City, CA, USA: ACM. https://doi.org/10.1007/3-540-45449-7_11'
chicago: De Alfaro, Luca, and Thomas A Henzinger. “Interface Theories for Component-Based
Design.” In Proceedings of the 1st International Workshop on Embedded Software,
2211:148–65. ACM, 2001. https://doi.org/10.1007/3-540-45449-7_11.
ieee: L. De Alfaro and T. A. Henzinger, “Interface theories for component-based
design,” in Proceedings of the 1st International Workshop on Embedded Software,
Tahoe City, CA, USA, 2001, vol. 2211, pp. 148–165.
ista: 'De Alfaro L, Henzinger TA. 2001. Interface theories for component-based design.
Proceedings of the 1st International Workshop on Embedded Software. EMSOFT: Embedded
Software , LNCS, vol. 2211, 148–165.'
mla: De Alfaro, Luca, and Thomas A. Henzinger. “Interface Theories for Component-Based
Design.” Proceedings of the 1st International Workshop on Embedded Software,
vol. 2211, ACM, 2001, pp. 148–65, doi:10.1007/3-540-45449-7_11.
short: L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 1st International Workshop
on Embedded Software, ACM, 2001, pp. 148–165.
conference:
end_date: 2001-10-10
location: Tahoe City, CA, USA
name: 'EMSOFT: Embedded Software '
start_date: 2001-10-08
date_created: 2018-12-11T12:09:48Z
date_published: 2001-09-26T00:00:00Z
date_updated: 2023-05-08T12:11:20Z
day: '26'
doi: 10.1007/3-540-45449-7_11
extern: '1'
intvolume: ' 2211'
language:
- iso: eng
month: '09'
oa_version: None
page: 148 - 165
publication: Proceedings of the 1st International Workshop on Embedded Software
publication_identifier:
isbn:
- '9783540426738'
publication_status: published
publisher: ACM
publist_id: '84'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Interface theories for component-based design
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2211
year: '2001'
...
---
_id: '4632'
abstract:
- lang: eng
text: We present a compositional trace-based model for probabilistic systems. The
behavior of a system with probabilistic choice is a stochastic process, namely,
a probability distribution on traces, or “bundle.” Consequently, the semantics
of a system with both nondeterministic and probabilistic choice is a set of bundles.
The bundles of a composite system can be obtained by combining the bundles of
the components in a simple mathematical way. Refinement between systems is bundle
containment. We achieve assume-guarantee compositionality for bundle semantics
by introducing two scoping mechanisms. The first mechanism, which is standard
in compositional modeling, distinguishes inputs from outputs and hidden state.
The second mechanism, which arises in probabilistic systems, partitions the state
into probabilistically independent regions.
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
the AFOSR MURI grant F49620-00-1-0327, the MARCO GSRC grant 98-DT-660, the NSF Theory
grant CCR-9988172, and the DARPA SEC grant F33615-C-98-3614.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
citation:
ama: 'De Alfaro L, Henzinger TA, Jhala R. Compositional methods for probabilistic
systems. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:351-365.
doi:10.1007/3-540-44685-0_24'
apa: 'De Alfaro, L., Henzinger, T. A., & Jhala, R. (2001). Compositional methods
for probabilistic systems. In Proceedings of the 12th International Conference
on on Concurrency Theory (Vol. 2154, pp. 351–365). Aalborg, Denmark: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_24'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Ranjit Jhala. “Compositional Methods
for Probabilistic Systems.” In Proceedings of the 12th International Conference
on on Concurrency Theory, 2154:351–65. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_24.
ieee: L. De Alfaro, T. A. Henzinger, and R. Jhala, “Compositional methods for probabilistic
systems,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 351–365.
ista: 'De Alfaro L, Henzinger TA, Jhala R. 2001. Compositional methods for probabilistic
systems. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 351–365.'
mla: De Alfaro, Luca, et al. “Compositional Methods for Probabilistic Systems.”
Proceedings of the 12th International Conference on on Concurrency Theory,
vol. 2154, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 351–65,
doi:10.1007/3-540-44685-0_24.
short: L. De Alfaro, T.A. Henzinger, R. Jhala, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 351–365.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:51Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:24:59Z
day: '13'
doi: 10.1007/3-540-44685-0_24
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 351 - 365
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '75'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Compositional methods for probabilistic systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4633'
abstract:
- lang: eng
text: "A procedure for the analysis of state spaces is called symbolic if it manipulates
not individual states, but sets of states that are represented by constraints.
Such a procedure can be used for the analysis of infinite state spaces, provided
termination is guaranteed. We present symbolic procedures, and corresponding termination
criteria, for the solution of infinite-state games, which occur in the control
and modular verification of infinite-state systems. To characterize the termination
of symbolic procedures for solving infinite-state games, we classify these game
structures into four increasingly restrictive categories:\r\n1 \tClass 1 consists
of infinite-state structures for which all safety and reachability games can be
solved.\r\n2 \tClass 2 consists of infinite-state structures for which all ω-regular
games can be solved.\r\n3 \tClass 3 consists of infinite-state structures for
which all nested positive boolean combinations of ω-regular games can be solved.\r\n4
\ \tClass 4 consists of infinite-state structures for which all nested boolean
combinations of ω-regular games can be solved.\r\nWe give a structural characterization
for each class, using equivalence relations on the state spaces of games which
range from game versions of trace equivalence to a game version of bisimilarity.
We provide infinite-state examples for all four classes of games from control
problems for hybrid systems. We conclude by presenting symbolic algorithms for
the synthesis of winning strategies (“controller synthesis”) for infinitestate
games with arbitrary ω-regular objectives, and prove termination over all class-2
structures. This settles, in particular, the symbolic controller synthesis problem
for rectangular hybrid systems."
acknowledgement: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory
grant CCR-9988172, and the NSF ITR grant CCR-0085949.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'De Alfaro L, Henzinger TA, Majumdar R. Symbolic algorithms for infinite-state
games. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:536-550.
doi:10.1007/3-540-44685-0_36'
apa: 'De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). Symbolic algorithms
for infinite-state games. In Proceedings of the 12th International Conference
on on Concurrency Theory (Vol. 2154, pp. 536–550). Aalborg, Denmark: Schloss
Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_36'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “Symbolic Algorithms
for Infinite-State Games.” In Proceedings of the 12th International Conference
on on Concurrency Theory, 2154:536–50. Schloss Dagstuhl - Leibniz-Zentrum
für Informatik, 2001. https://doi.org/10.1007/3-540-44685-0_36.
ieee: L. De Alfaro, T. A. Henzinger, and R. Majumdar, “Symbolic algorithms for infinite-state
games,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 536–550.
ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. Symbolic algorithms for infinite-state
games. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 536–550.'
mla: De Alfaro, Luca, et al. “Symbolic Algorithms for Infinite-State Games.” Proceedings
of the 12th International Conference on on Concurrency Theory, vol. 2154,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 536–50, doi:10.1007/3-540-44685-0_36.
short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 536–550.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T09:57:31Z
day: '13'
doi: 10.1007/3-540-44685-0_36
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 536 - 550
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '73'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic algorithms for infinite-state games
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4634'
abstract:
- lang: eng
text: "A controller is an environment for a system that achieves a particular control
objective by providing inputs to the system without constraining the choices of
the system. For synchronous systems, where system and controller make simultaneous
and interdependent choices, the notion that a controller must not constrain the
choices of the system can be formalized by type systems for composability. In
a previous paper, we solved the control problem for static and dynamic types:
a static type is a dependency relation between inputs and outputs, and composition
is well-typed if it does not introduce cyclic dependencies; a dynamic type is
a set of static types, one for each state. Static and dynamic types, however,
cannot capture many important digital circuits, such as gated clocks, bidirectional
buses, and random-access memory. We therefore introduce more general type systems,
so-called dependent and bidirectional types, for modeling these situations, and
we solve the corresponding control problems.\r\nIn a system with a dependent type,
the dependencies between inputs and outputs are determined gradually through a
game of the system against the controller. In a system with a bidirectional type,
also the distinction between inputs and outputs is resolved dynamically by such
a game. The game proceeds in several rounds. In each round the system and the
controller choose to update some variables dependent on variables that have already
been updated. The solution of the control problem for dependent and bidirectional
types is based on algorithms for solving these games."
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003,
the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the AFOSR
MURI grant F49620-00-1-0327, and the NSF Theory grant CCR-9988172.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: 'De Alfaro L, Henzinger TA, Mang F. The control of synchronous systems, Part
II. In: Proceedings of the 12th International Conference on on Concurrency
Theory. Vol 2154. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2001:566-581.
doi:10.1007/3-540-44685-0_38'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). The control of synchronous
systems, Part II. In Proceedings of the 12th International Conference on on
Concurrency Theory (Vol. 2154, pp. 566–581). Aalborg, Denmark: Schloss Dagstuhl
- Leibniz-Zentrum für Informatik. https://doi.org/10.1007/3-540-44685-0_38'
chicago: De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “The Control of Synchronous
Systems, Part II.” In Proceedings of the 12th International Conference on on
Concurrency Theory, 2154:566–81. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001. https://doi.org/10.1007/3-540-44685-0_38.
ieee: L. De Alfaro, T. A. Henzinger, and F. Mang, “The control of synchronous systems,
Part II,” in Proceedings of the 12th International Conference on on Concurrency
Theory, Aalborg, Denmark, 2001, vol. 2154, pp. 566–581.
ista: 'De Alfaro L, Henzinger TA, Mang F. 2001. The control of synchronous systems,
Part II. Proceedings of the 12th International Conference on on Concurrency Theory.
CONCUR: Concurrency Theory, LNCS, vol. 2154, 566–581.'
mla: De Alfaro, Luca, et al. “The Control of Synchronous Systems, Part II.” Proceedings
of the 12th International Conference on on Concurrency Theory, vol. 2154,
Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2001, pp. 566–81, doi:10.1007/3-540-44685-0_38.
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 12th International
Conference on on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
2001, pp. 566–581.
conference:
end_date: 2001-08-25
location: Aalborg, Denmark
name: 'CONCUR: Concurrency Theory'
start_date: 2001-08-20
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-13T00:00:00Z
date_updated: 2023-05-08T10:20:19Z
day: '13'
doi: 10.1007/3-540-44685-0_38
extern: '1'
intvolume: ' 2154'
language:
- iso: eng
month: '08'
oa_version: None
page: 566 - 581
publication: Proceedings of the 12th International Conference on on Concurrency Theory
publication_identifier:
isbn:
- '9783540424970'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '74'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The control of synchronous systems, Part II
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 2154
year: '2001'
...
---
_id: '4635'
abstract:
- lang: eng
text: We show how model checking techniques can be applied to the analysis of connectivity
and cost-of-traversal properties of Web sites.
article_processing_charge: No
author:
- 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: 'De Alfaro L, Henzinger TA, Mang F. MCWEB: A model-checking tool for web-site
debugging. In: Proceedings of the 10th International Conference on World Wide
Web. ACM; 2001:86-87.'
apa: 'De Alfaro, L., Henzinger, T. A., & Mang, F. (2001). MCWEB: A model-checking
tool for web-site debugging. In Proceedings of the 10th international conference
on World Wide Web (pp. 86–87). Hong Kong, Hong Kong: ACM.'
chicago: 'De Alfaro, Luca, Thomas A Henzinger, and Freddy Mang. “MCWEB: A Model-Checking
Tool for Web-Site Debugging.” In Proceedings of the 10th International Conference
on World Wide Web, 86–87. ACM, 2001.'
ieee: 'L. De Alfaro, T. A. Henzinger, and F. Mang, “MCWEB: A model-checking tool
for web-site debugging,” in Proceedings of the 10th international conference
on World Wide Web, Hong Kong, Hong Kong, 2001, pp. 86–87.'
ista: 'De Alfaro L, Henzinger TA, Mang F. 2001. MCWEB: A model-checking tool for
web-site debugging. Proceedings of the 10th international conference on World
Wide Web. WWW: World Wide Web Conference, 86–87.'
mla: 'De Alfaro, Luca, et al. “MCWEB: A Model-Checking Tool for Web-Site Debugging.”
Proceedings of the 10th International Conference on World Wide Web, ACM,
2001, pp. 86–87.'
short: L. De Alfaro, T.A. Henzinger, F. Mang, in:, Proceedings of the 10th International
Conference on World Wide Web, ACM, 2001, pp. 86–87.
conference:
end_date: 2000-05-05
location: Hong Kong, Hong Kong
name: 'WWW: World Wide Web Conference'
start_date: 2001-05-01
date_created: 2018-12-11T12:09:52Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-08T09:39:02Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: https://ir.webis.de/anthology/2001.wwwconf_conference-2001p.57/
month: '05'
oa_version: None
page: 86 - 87
publication: Proceedings of the 10th international conference on World Wide Web
publication_identifier:
isbn:
- '9781581133486'
publication_status: published
publisher: ACM
publist_id: '71'
quality_controlled: '1'
status: public
title: 'MCWEB: A model-checking tool for web-site debugging'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '4636'
abstract:
- lang: eng
text: 'Abstract. Dynamic programs, or fixpoint iteration schemes, are useful for
solving many problems on state spaces, including model checking on Kripke structures
(“verification”), computing shortest paths on weighted graphs (“optimization”),
computing the value of games played on game graphs (“control”). For Kripke structures,
a rich fixpoint theory is available in the form of the µ-calculus. Yet few connections
have been made between different interpretations of fixpoint algorithms. We study
the question of when a particular fixpoint iteration scheme ϕ for verifying an
ω-regular property Ψ on a Kripke structure can be used also for solving a two-player
game on a game graph with winning objective Ψ. We provide a sufficient and necessary
criterion for the answer to be affirmative in the form of an extremal-model theorem
for games: under a game interpretation, the dynamic program ϕ solves the game
with objective Ψ if and only if both (1) under an existential interpretation on
Kripke structures, ϕ is equivalent to ∃Ψ, and (2) under a universal interpretation
on Kripke structures, ϕ is equivalent to ∀Ψ. In other words, ϕ is correct on all
two-player game graphs iff it is correct on all extremal game graphs, where one
or the other player has no choice of moves. The theorem generalizes to quantitative
interpretations, where it connects two-player games with costs to weighted graphs.
While the standard translations from ω-regular properties to the µ-calculus violate
(1) or (2), we give a translation that satisfies both conditions. Our construction,
therefore, yields fixpoint iteration schemes that can be uniformly applied on
Kripke structures, weighted graphs, game graphs, and game graphs with costs, in
order to meet or optimize a given ω-regular objective.'
article_processing_charge: No
author:
- 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: Ritankar
full_name: Majumdar, Ritankar
last_name: Majumdar
citation:
ama: 'De Alfaro L, Henzinger TA, Majumdar R. From verification to control: dynamic
programs for omega-regular objectives. In: Proceedings of the 16th Annual IEEE
Symposium on Logic in Computer Science. IEEE; 2001:279-290. doi:10.1109/LICS.2001.932504'
apa: 'De Alfaro, L., Henzinger, T. A., & Majumdar, R. (2001). From verification
to control: dynamic programs for omega-regular objectives. In Proceedings of
the 16th Annual IEEE Symposium on Logic in Computer Science (pp. 279–290).
Boston, MA, USA: IEEE. https://doi.org/10.1109/LICS.2001.932504'
chicago: 'De Alfaro, Luca, Thomas A Henzinger, and Ritankar Majumdar. “From Verification
to Control: Dynamic Programs for Omega-Regular Objectives.” In Proceedings
of the 16th Annual IEEE Symposium on Logic in Computer Science, 279–90. IEEE,
2001. https://doi.org/10.1109/LICS.2001.932504.'
ieee: 'L. De Alfaro, T. A. Henzinger, and R. Majumdar, “From verification to control:
dynamic programs for omega-regular objectives,” in Proceedings of the 16th
Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, 2001,
pp. 279–290.'
ista: 'De Alfaro L, Henzinger TA, Majumdar R. 2001. From verification to control:
dynamic programs for omega-regular objectives. Proceedings of the 16th Annual
IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science,
279–290.'
mla: 'De Alfaro, Luca, et al. “From Verification to Control: Dynamic Programs for
Omega-Regular Objectives.” Proceedings of the 16th Annual IEEE Symposium on
Logic in Computer Science, IEEE, 2001, pp. 279–90, doi:10.1109/LICS.2001.932504.'
short: L. De Alfaro, T.A. Henzinger, R. Majumdar, in:, Proceedings of the 16th Annual
IEEE Symposium on Logic in Computer Science, IEEE, 2001, pp. 279–290.
conference:
end_date: 2001-06-19
location: Boston, MA, USA
name: 'LICS: Logic in Computer Science'
start_date: 2001-06-16
date_created: 2018-12-11T12:09:52Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T09:48:06Z
day: '07'
doi: 10.1109/LICS.2001.932504
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 279 - 290
publication: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science
publication_identifier:
isbn:
- 076951281X
publication_status: published
publisher: IEEE
publist_id: '72'
quality_controlled: '1'
status: public
title: 'From verification to control: dynamic programs for omega-regular objectives'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '3434'
abstract:
- lang: eng
text: "This chapter contains sections titled:\r\n\r\nIntroduction\r\n\r\n- History\r\n\r\n-
Developing an Intuition of Likelihood\r\n\r\n- Method of Maximum Likelihood\r\n\r\n-
Bayesian Inference\r\n\r\n- Markov Chain Monte Carlo\r\n\r\n- Assessing Uncertainty
of Phylogenies\r\n\r\n- Hypothesis Testing and Model Choice\r\n\r\n- Comparative
Analysis\r\n\r\n- Conclusions\r\n\r\n- References"
article_processing_charge: No
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: 'Huelsenbeck J, Bollback JP. Application of the likelihood function in phylogenetic
analysis. In: Balding D, Bishop M, Cannings C, eds. Handbook of Statistical
Genetics. Wiley-Blackwell; 2001:415-439. doi:10.1002/9780470061619.ch15'
apa: Huelsenbeck, J., & Bollback, J. P. (2001). Application of the likelihood
function in phylogenetic analysis. In D. Balding, M. Bishop, & C. Cannings
(Eds.), Handbook of Statistical Genetics (pp. 415–439). Wiley-Blackwell.
https://doi.org/10.1002/9780470061619.ch15
chicago: Huelsenbeck, John, and Jonathan P Bollback. “Application of the Likelihood
Function in Phylogenetic Analysis.” In Handbook of Statistical Genetics,
edited by David Balding, Martin Bishop, and Chriss Cannings, 415–39. Wiley-Blackwell,
2001. https://doi.org/10.1002/9780470061619.ch15.
ieee: J. Huelsenbeck and J. P. Bollback, “Application of the likelihood function
in phylogenetic analysis,” in Handbook of Statistical Genetics, D. Balding,
M. Bishop, and C. Cannings, Eds. Wiley-Blackwell, 2001, pp. 415–439.
ista: 'Huelsenbeck J, Bollback JP. 2001.Application of the likelihood function in
phylogenetic analysis. In: Handbook of Statistical Genetics. , 415–439.'
mla: Huelsenbeck, John, and Jonathan P. Bollback. “Application of the Likelihood
Function in Phylogenetic Analysis.” Handbook of Statistical Genetics, edited
by David Balding et al., Wiley-Blackwell, 2001, pp. 415–39, doi:10.1002/9780470061619.ch15.
short: J. Huelsenbeck, J.P. Bollback, in:, D. Balding, M. Bishop, C. Cannings (Eds.),
Handbook of Statistical Genetics, Wiley-Blackwell, 2001, pp. 415–439.
date_created: 2018-12-11T12:03:19Z
date_published: 2001-01-01T00:00:00Z
date_updated: 2023-05-15T14:43:39Z
day: '01'
doi: 10.1002/9780470061619.ch15
editor:
- first_name: David
full_name: Balding, David
last_name: Balding
- first_name: Martin
full_name: Bishop, Martin
last_name: Bishop
- first_name: Chriss
full_name: Cannings, Chriss
last_name: Cannings
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 415 - 439
publication: Handbook of Statistical Genetics
publication_identifier:
isbn:
- '9781119429142 '
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2966'
quality_controlled: '1'
status: public
title: Application of the likelihood function in phylogenetic analysis
type: book_chapter
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...
---
_id: '3438'
abstract:
- lang: eng
text: As a discipline, phylogenetics is becoming transformed by a flood of molecular
data. These data allow broad questions to be asked about the history of life,
but also present difficult statistical and computational problems. Bayesian inference
of phylogeny brings a new perspective to a number of outstanding issues in evolutionary
biology, including the analysis of large phylogenetic trees and complex evolutionary
models and the detection of the footprint of natural selection in DNA sequences.
article_processing_charge: No
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Fredrik
full_name: Ronquist, Fredrik
last_name: Ronquist
- first_name: Rasmus
full_name: Nielsen, Rasmus
last_name: Nielsen
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. Bayesian inference of phylogeny
and its impact on evolutionary biology. Science. 2001;294(5550):2310-2314.
doi:10.1126/science.1065889
apa: Huelsenbeck, J., Ronquist, F., Nielsen, R., & Bollback, J. P. (2001). Bayesian
inference of phylogeny and its impact on evolutionary biology. Science.
American Association for the Advancement of Science. https://doi.org/10.1126/science.1065889
chicago: Huelsenbeck, John, Fredrik Ronquist, Rasmus Nielsen, and Jonathan P Bollback.
“Bayesian Inference of Phylogeny and Its Impact on Evolutionary Biology.” Science.
American Association for the Advancement of Science, 2001. https://doi.org/10.1126/science.1065889.
ieee: J. Huelsenbeck, F. Ronquist, R. Nielsen, and J. P. Bollback, “Bayesian inference
of phylogeny and its impact on evolutionary biology,” Science, vol. 294,
no. 5550. American Association for the Advancement of Science, pp. 2310–2314,
2001.
ista: Huelsenbeck J, Ronquist F, Nielsen R, Bollback JP. 2001. Bayesian inference
of phylogeny and its impact on evolutionary biology. Science. 294(5550), 2310–2314.
mla: Huelsenbeck, John, et al. “Bayesian Inference of Phylogeny and Its Impact on
Evolutionary Biology.” Science, vol. 294, no. 5550, American Association
for the Advancement of Science, 2001, pp. 2310–14, doi:10.1126/science.1065889.
short: J. Huelsenbeck, F. Ronquist, R. Nielsen, J.P. Bollback, Science 294 (2001)
2310–2314.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-12-14T00:00:00Z
date_updated: 2023-05-15T14:10:13Z
day: '14'
doi: 10.1126/science.1065889
extern: '1'
external_id:
pmid:
- '11743192 '
intvolume: ' 294'
issue: '5550'
language:
- iso: eng
month: '12'
oa_version: None
page: 2310 - 2314
pmid: 1
publication: Science
publication_identifier:
issn:
- 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '2962'
quality_controlled: '1'
status: public
title: Bayesian inference of phylogeny and its impact on evolutionary biology
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 294
year: '2001'
...
---
_id: '3439'
abstract:
- lang: eng
text: High molecular weight DNA was extracted from the primary Neotropical malaria
vector, Anopheles darlingi from Capanema, Pará, Brazil, to create a small insert
genomic library, and then a phagemid library. Enriched sublibraries were constructed
from the phagemid library using a microsatellite oligo primed second strand synthesis
protocol. The resulting 242 760 individual clones were screened. The mean clone
size of the positive clones was 302 bp. Flanking primers were designed for each
suitable microsatellite sequence. Eight polymorphic loci were optimized and characterized.
The allele size ranges are based on 253 samples of A. darlingi from eastern Amazonian
and central Brazil.
acknowledgement: For support in Brazil we thank D. Galiza, R.N.L. Lacerda,E.P.
Santa Rosa, M.N.O. Segura, and R.T.L. de Souza. We also thankM.J. Braun for allowing work on the library construction at theLaboratory
of Molecular Systematics, Washington. Supported byNIH AI 40116 to JEC and Instituto
Evandro Chagas, Belém, Brazil.
article_processing_charge: No
article_type: original
author:
- first_name: Jan
full_name: Conn, Jan
last_name: Conn
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: David
full_name: Onyabe, David
last_name: Onyabe
- first_name: Tessa
full_name: Robinson, Tessa
last_name: Robinson
- first_name: Richard
full_name: Wilkerson, Richard
last_name: Wilkerson
- first_name: Marinete
full_name: Povoa, Marinete
last_name: Povoa
citation:
ama: Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. Isolation
of polymorphic microsatellite markers from the malaria vector Anopheles darlingi.
Molecular Ecology Notes. 2001;1(4):223-225. doi: 10.1046/j.1471-8278.2001.00078.x
apa: Conn, J., Bollback, J. P., Onyabe, D., Robinson, T., Wilkerson, R., & Povoa,
M. (2001). Isolation of polymorphic microsatellite markers from the malaria vector
Anopheles darlingi. Molecular Ecology Notes. Wiley-Blackwell. https://doi.org/ 10.1046/j.1471-8278.2001.00078.x
chicago: Conn, Jan, Jonathan P Bollback, David Onyabe, Tessa Robinson, Richard Wilkerson,
and Marinete Povoa. “Isolation of Polymorphic Microsatellite Markers from the
Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes. Wiley-Blackwell,
2001. https://doi.org/
10.1046/j.1471-8278.2001.00078.x.
ieee: J. Conn, J. P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, and M. Povoa,
“Isolation of polymorphic microsatellite markers from the malaria vector Anopheles
darlingi,” Molecular Ecology Notes, vol. 1, no. 4. Wiley-Blackwell, pp.
223–225, 2001.
ista: Conn J, Bollback JP, Onyabe D, Robinson T, Wilkerson R, Povoa M. 2001. Isolation
of polymorphic microsatellite markers from the malaria vector Anopheles darlingi.
Molecular Ecology Notes. 1(4), 223–225.
mla: Conn, Jan, et al. “Isolation of Polymorphic Microsatellite Markers from the
Malaria Vector Anopheles Darlingi.” Molecular Ecology Notes, vol. 1, no.
4, Wiley-Blackwell, 2001, pp. 223–25, doi:
10.1046/j.1471-8278.2001.00078.x.
short: J. Conn, J.P. Bollback, D. Onyabe, T. Robinson, R. Wilkerson, M. Povoa, Molecular
Ecology Notes 1 (2001) 223–225.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-12-01T00:00:00Z
date_updated: 2023-05-15T13:58:49Z
day: '01'
doi: ' 10.1046/j.1471-8278.2001.00078.x'
extern: '1'
intvolume: ' 1'
issue: '4'
language:
- iso: eng
month: '12'
oa_version: None
page: 223 - 225
publication: Molecular Ecology Notes
publication_identifier:
issn:
- 1471-8278
publication_status: published
publisher: Wiley-Blackwell
publist_id: '2961'
quality_controlled: '1'
status: public
title: Isolation of polymorphic microsatellite markers from the malaria vector Anopheles
darlingi
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1
year: '2001'
...
---
_id: '3440'
abstract:
- lang: eng
text: "Several methods have been proposed to infer the states at the ancestral nodes
on a phylogeny. These methods assume a specific tree and set of branch lengths
when estimating the ancestral character state. Inferences of the ancestral states,
then, are conditioned on the tree and branch lengths being true. We develop a
hierarchical Bayes method for inferring the ancestral states on a tree. The method
integrates over uncertainty in the tree, branch lengths, and substitution model
parameters by using Markov chain Monte Carlo. We compare the hierarchical Bayes
inferences of ancestral states with inferences of ancestral states made under
the assumption that a specific tree is correct. We find that the methods are correlated,
but that accommodating uncertainty in parameters of the phylogenetic model can
make inferences of ancestral states even more uncertain than they would be in
an empirical Bayes analysis.\r\n"
article_processing_charge: No
article_type: original
author:
- first_name: John
full_name: Huelsenbeck, John
last_name: Huelsenbeck
- first_name: Jonathan P
full_name: Bollback, Jonathan P
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
citation:
ama: Huelsenbeck J, Bollback JP. Empirical and hierarchical Bayesian estimation
of ancestral states. Systematic Biology. 2001;50(3):351-366. doi:10.1080/10635150119871
apa: Huelsenbeck, J., & Bollback, J. P. (2001). Empirical and hierarchical Bayesian
estimation of ancestral states. Systematic Biology. Oxford University Press.
https://doi.org/10.1080/10635150119871
chicago: Huelsenbeck, John, and Jonathan P Bollback. “Empirical and Hierarchical
Bayesian Estimation of Ancestral States.” Systematic Biology. Oxford University
Press, 2001. https://doi.org/10.1080/10635150119871.
ieee: J. Huelsenbeck and J. P. Bollback, “Empirical and hierarchical Bayesian estimation
of ancestral states,” Systematic Biology, vol. 50, no. 3. Oxford University
Press, pp. 351–366, 2001.
ista: Huelsenbeck J, Bollback JP. 2001. Empirical and hierarchical Bayesian estimation
of ancestral states. Systematic Biology. 50(3), 351–366.
mla: Huelsenbeck, John, and Jonathan P. Bollback. “Empirical and Hierarchical Bayesian
Estimation of Ancestral States.” Systematic Biology, vol. 50, no. 3, Oxford
University Press, 2001, pp. 351–66, doi:10.1080/10635150119871.
short: J. Huelsenbeck, J.P. Bollback, Systematic Biology 50 (2001) 351–366.
date_created: 2018-12-11T12:03:20Z
date_published: 2001-05-01T00:00:00Z
date_updated: 2023-05-15T13:54:01Z
day: '01'
doi: 10.1080/10635150119871
extern: '1'
external_id:
pmid:
- '12116580'
intvolume: ' 50'
issue: '3'
language:
- iso: eng
month: '05'
oa_version: None
page: 351 - 366
pmid: 1
publication: Systematic Biology
publication_identifier:
issn:
- 0039-7989
publication_status: published
publisher: Oxford University Press
publist_id: '2960'
quality_controlled: '1'
status: public
title: Empirical and hierarchical Bayesian estimation of ancestral states
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 50
year: '2001'
...
---
_id: '3447'
author:
- first_name: Krishnendu
full_name: Krishnendu Chatterjee
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Pallab
full_name: Dasgupta, Pallab
last_name: Dasgupta
- first_name: Partha
full_name: Chakrabarti, Partha P
last_name: Chakrabarti
citation:
ama: 'Chatterjee K, Dasgupta P, Chakrabarti P. Weighted quantified computation tree
logic. In: Elsevier; 2001.'
apa: 'Chatterjee, K., Dasgupta, P., & Chakrabarti, P. (2001). Weighted quantified
computation tree logic. Presented at the CIT: Conference on Information Technology,
Elsevier.'
chicago: Chatterjee, Krishnendu, Pallab Dasgupta, and Partha Chakrabarti. “Weighted
Quantified Computation Tree Logic.” Elsevier, 2001.
ieee: 'K. Chatterjee, P. Dasgupta, and P. Chakrabarti, “Weighted quantified computation
tree logic,” presented at the CIT: Conference on Information Technology, 2001.'
ista: 'Chatterjee K, Dasgupta P, Chakrabarti P. 2001. Weighted quantified computation
tree logic. CIT: Conference on Information Technology.'
mla: Chatterjee, Krishnendu, et al. Weighted Quantified Computation Tree Logic.
Elsevier, 2001.
short: K. Chatterjee, P. Dasgupta, P. Chakrabarti, in:, Elsevier, 2001.
conference:
name: 'CIT: Conference on Information Technology'
date_created: 2018-12-11T12:03:23Z
date_published: 2001-11-14T00:00:00Z
date_updated: 2021-01-12T07:43:31Z
day: '14'
extern: 1
month: '11'
publication_status: published
publisher: Elsevier
publist_id: '2940'
quality_controlled: 0
status: public
title: Weighted quantified computation tree logic
type: conference
year: '2001'
...
---
_id: '3493'
abstract:
- lang: eng
text: Although agonists and competitive antagonists presumably occupy overlapping
binding sites on ligand-gated channels, these interactions cannot be identical
because agonists cause channel opening whereas antagonists do not. One explanation
is that only agonist binding performs enough work on the receptor to cause the
conformational changes that lead to gating. This idea is supported by agonist
binding rates at GABAA and nicotinic acetylcholine receptors that are slower than
expected for a diffusion-limited process, suggesting that agonist binding involves
an energy-requiring event. This hypothesis predicts that competitive antagonist
binding should require less activation energy than agonist binding. To test this
idea, we developed a novel deconvolution-based method to compare binding and unbinding
kinetics of GABAA receptor agonists and antagonists in outside-out patches from
rat hippocampal neurons. Agonist and antagonist unbinding rates were steeply correlated
with affinity. Unlike the agonists, three of the four antagonists tested had binding
rates that were fast, independent of affinity, and could be accounted for by diffusion-
and dehydration-limited processes. In contrast, agonist binding involved additional
energy-requiring steps, consistent with the idea that channel gating is initiated
by agonist-triggered movements within the ligand binding site. Antagonist binding
does not appear to produce such movements, and may in fact prevent them.
article_processing_charge: No
article_type: original
author:
- first_name: M.V
full_name: Jones, M.V
last_name: Jones
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
- first_name: Y.
full_name: Sahara, Y.
last_name: Sahara
- first_name: G.
full_name: Westbrook, G.
last_name: Westbrook
citation:
ama: Jones M., Jonas PM, Sahara Y, Westbrook G. Microscopic kinetics and energetics
distinguish GABAA receptor agonists from antagonists. Biophysical Journal.
2001;81(5):2660-2670. doi:10.1016/S0006-3495(01)75909-7
apa: Jones, M. ., Jonas, P. M., Sahara, Y., & Westbrook, G. (2001). Microscopic
kinetics and energetics distinguish GABAA receptor agonists from antagonists.
Biophysical Journal. Biophysical Society. https://doi.org/10.1016/S0006-3495(01)75909-7
chicago: Jones, M.V, Peter M Jonas, Y. Sahara, and G. Westbrook. “Microscopic Kinetics
and Energetics Distinguish GABAA Receptor Agonists from Antagonists.” Biophysical
Journal. Biophysical Society, 2001. https://doi.org/10.1016/S0006-3495(01)75909-7 .
ieee: M. . Jones, P. M. Jonas, Y. Sahara, and G. Westbrook, “Microscopic kinetics
and energetics distinguish GABAA receptor agonists from antagonists,” Biophysical
Journal, vol. 81, no. 5. Biophysical Society, pp. 2660–2670, 2001.
ista: Jones M., Jonas PM, Sahara Y, Westbrook G. 2001. Microscopic kinetics and
energetics distinguish GABAA receptor agonists from antagonists. Biophysical Journal.
81(5), 2660–2670.
mla: Jones, M. .., et al. “Microscopic Kinetics and Energetics Distinguish GABAA
Receptor Agonists from Antagonists.” Biophysical Journal, vol. 81, no.
5, Biophysical Society, 2001, pp. 2660–70, doi:10.1016/S0006-3495(01)75909-7 .
short: M.. Jones, P.M. Jonas, Y. Sahara, G. Westbrook, Biophysical Journal 81 (2001)
2660–2670.
date_created: 2018-12-11T12:03:37Z
date_published: 2001-11-01T00:00:00Z
date_updated: 2023-05-15T13:50:21Z
day: '01'
doi: '10.1016/S0006-3495(01)75909-7 '
extern: '1'
external_id:
pmid:
- '11606279'
intvolume: ' 81'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC1301733/
month: '11'
oa: 1
oa_version: Published Version
page: 2660 - 2670
pmid: 1
publication: Biophysical Journal
publication_identifier:
issn:
- 0006-3495
publication_status: published
publisher: Biophysical Society
publist_id: '2894'
quality_controlled: '1'
status: public
title: Microscopic kinetics and energetics distinguish GABAA receptor agonists from
antagonists
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 81
year: '2001'
...
---
_id: '3494'
abstract:
- lang: eng
text: 'Mutual synaptic interactions between GABAergic interneurons are thought to
be of critical importance for the generation of network oscillations and for temporal
encoding of information in the hippocampus. However, the functional properties
of synaptic transmission between hippocampal interneurons are largely unknown.
We have made paired recordings from basket cells (BCs) in the dentate gyrus of
rat hippocampal slices, followed by correlated light and electron microscopical
analysis. Unitary GABAAreceptor-mediated IPSCs at BC–BC synapses recorded at the
soma showed a fast rise and decay, with a mean decay time constant of 2.5 ± 0.2
msec (32°C). Synaptic transmission at BC–BC synapses showed paired-pulse depression
(PPD) (32 ± 5% for 10 msec interpulse intervals) and multiple-pulse depression
during repetitive stimulation. Detailed passive cable model simulations based
on somatodendritic morphology and localization of synaptic contacts further indicated
that the conductance change at the postsynaptic site was even faster, decaying
with a mean time constant of 1.8 ± 0.6 msec. Sequential triple recordings revealed
that the decay time course of IPSCs at BC–BC synapses was approximately twofold
faster than that at BC–granule cell synapses, whereas the extent of PPD was comparable.
To examine the consequences of the fast postsynaptic conductance change for the
generation of oscillatory activity, we developed a computational model of an interneuron
network. The model showed robust oscillations at frequencies >60 Hz if the
excitatory drive was sufficiently large. Thus the fast conductance change at interneuron–interneuron
synapses may promote the generation of high-frequency oscillations observed in
the dentate gyrusin vivo. '
acknowledgement: This work was supported by grants of the Deutsche Forschungsgemeinschaft
(SFB 505/C6) and the Human Frontiers Science Program Organization (RG0017/1998-B).
We thank Drs. M. V. Jones, J. Bischofberger, and U. Kraushaar for critically reading
this manuscript. We also thank B. Taskin and A. Roth for advice in the use of reconstruction
and modeling software, and S. Nestel, M. Winter, and A. Blomenkamp for technical
assistance.
article_processing_charge: No
article_type: original
author:
- first_name: Marlene
full_name: Bartos, Marlene
last_name: Bartos
- first_name: Imre
full_name: Vida, Imre
last_name: Vida
- first_name: Michael
full_name: Frotscher, Michael
last_name: Frotscher
- first_name: Jörg
full_name: Geiger, Jörg
last_name: Geiger
- first_name: Peter M
full_name: Jonas, Peter M
id: 353C1B58-F248-11E8-B48F-1D18A9856A87
last_name: Jonas
orcid: 0000-0001-5001-4804
citation:
ama: Bartos M, Vida I, Frotscher M, Geiger J, Jonas PM. Rapid signaling at inhibitory
synapses in a dentate gyrus interneuron network. Journal of Neuroscience.
2001;21(8):2687-2698. doi:10.1523/JNEUROSCI.21-08-02687.2001
apa: Bartos, M., Vida, I., Frotscher, M., Geiger, J., & Jonas, P. M. (2001).
Rapid signaling at inhibitory synapses in a dentate gyrus interneuron network.
Journal of Neuroscience. Society for Neuroscience. https://doi.org/10.1523/JNEUROSCI.21-08-02687.2001
chicago: Bartos, Marlene, Imre Vida, Michael Frotscher, Jörg Geiger, and Peter M
Jonas. “Rapid Signaling at Inhibitory Synapses in a Dentate Gyrus Interneuron
Network.” Journal of Neuroscience. Society for Neuroscience, 2001. https://doi.org/10.1523/JNEUROSCI.21-08-02687.2001.
ieee: M. Bartos, I. Vida, M. Frotscher, J. Geiger, and P. M. Jonas, “Rapid signaling
at inhibitory synapses in a dentate gyrus interneuron network.,” Journal of
Neuroscience, vol. 21, no. 8. Society for Neuroscience, pp. 2687–2698, 2001.
ista: Bartos M, Vida I, Frotscher M, Geiger J, Jonas PM. 2001. Rapid signaling at
inhibitory synapses in a dentate gyrus interneuron network. Journal of Neuroscience.
21(8), 2687–2698.
mla: Bartos, Marlene, et al. “Rapid Signaling at Inhibitory Synapses in a Dentate
Gyrus Interneuron Network.” Journal of Neuroscience, vol. 21, no. 8, Society
for Neuroscience, 2001, pp. 2687–98, doi:10.1523/JNEUROSCI.21-08-02687.2001.
short: M. Bartos, I. Vida, M. Frotscher, J. Geiger, P.M. Jonas, Journal of Neuroscience
21 (2001) 2687–2698.
date_created: 2018-12-11T12:03:37Z
date_published: 2001-04-15T00:00:00Z
date_updated: 2023-05-15T13:47:04Z
day: '15'
doi: 10.1523/JNEUROSCI.21-08-02687.2001
extern: '1'
external_id:
pmid:
- '11306622'
intvolume: ' 21'
issue: '8'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: ncbi.nlm.nih.gov/pmc/articles/PMC6762544/
month: '04'
oa: 1
oa_version: Published Version
page: 2687 - 2698
pmid: 1
publication: Journal of Neuroscience
publication_identifier:
issn:
- 0270-6474
publication_status: published
publisher: Society for Neuroscience
publist_id: '2893'
quality_controlled: '1'
status: public
title: Rapid signaling at inhibitory synapses in a dentate gyrus interneuron network.
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 21
year: '2001'
...