---
_id: '4228'
abstract:
- lang: eng
text: Suppressive drug interactions, in which one antibiotic can actually help bacterial
cells to grow faster in the presence of another, occur between protein and DNA
synthesis inhibitors. Here, we show that this suppression results from nonoptimal
regulation of ribosomal genes in the presence of DNA stress. Using GFP-tagged
transcription reporters in Escherichia coli, we find that ribosomal genes are
not directly regulated by DNA stress, leading to an imbalance between cellular
DNA and protein content. To test whether ribosomal gene expression under DNA stress
is nonoptimal for growth rate, we sequentially deleted up to six of the seven
ribosomal RNA operons. These synthetic manipulations of ribosomal gene expression
correct the protein-DNA imbalance, lead to improved survival and growth, and completely
remove the suppressive drug interaction. A simple mathematical model explains
the nonoptimal regulation in different nutrient environments. These results reveal
the genetic mechanism underlying an important class of suppressive drug interactions.
author:
- first_name: Tobias
full_name: Bollenbach, Tobias
last_name: Bollenbach
- first_name: Selwyn
full_name: Quan, Selwyn
last_name: Quan
- first_name: Remy P
full_name: Remy Chait
id: 3464AE84-F248-11E8-B48F-1D18A9856A87
last_name: Chait
orcid: 0000-0003-0876-3187
- first_name: Roy
full_name: Kishony, Roy
last_name: Kishony
citation:
ama: Bollenbach T, Quan S, Chait RP, Kishony R. Nonoptimal Microbial Response to
Antibiotics Underlies Suppressive Drug Interactions. Cell. 2009;139(4):707-718.
doi:10.1016/j.cell.2009.10.025
apa: Bollenbach, T., Quan, S., Chait, R. P., & Kishony, R. (2009). Nonoptimal
Microbial Response to Antibiotics Underlies Suppressive Drug Interactions. Cell.
Cell Press. https://doi.org/10.1016/j.cell.2009.10.025
chicago: Bollenbach, Tobias, Selwyn Quan, Remy P Chait, and Roy Kishony. “Nonoptimal
Microbial Response to Antibiotics Underlies Suppressive Drug Interactions.” Cell.
Cell Press, 2009. https://doi.org/10.1016/j.cell.2009.10.025.
ieee: T. Bollenbach, S. Quan, R. P. Chait, and R. Kishony, “Nonoptimal Microbial
Response to Antibiotics Underlies Suppressive Drug Interactions,” Cell,
vol. 139, no. 4. Cell Press, pp. 707–718, 2009.
ista: Bollenbach T, Quan S, Chait RP, Kishony R. 2009. Nonoptimal Microbial Response
to Antibiotics Underlies Suppressive Drug Interactions. Cell. 139(4), 707–718.
mla: Bollenbach, Tobias, et al. “Nonoptimal Microbial Response to Antibiotics Underlies
Suppressive Drug Interactions.” Cell, vol. 139, no. 4, Cell Press, 2009,
pp. 707–18, doi:10.1016/j.cell.2009.10.025.
short: T. Bollenbach, S. Quan, R.P. Chait, R. Kishony, Cell 139 (2009) 707–718.
date_created: 2018-12-11T12:07:43Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:27Z
day: '01'
doi: 10.1016/j.cell.2009.10.025
extern: 1
intvolume: ' 139'
issue: '4'
month: '01'
page: 707 - 718
publication: Cell
publication_status: published
publisher: Cell Press
publist_id: '1890'
quality_controlled: 0
status: public
title: Nonoptimal Microbial Response to Antibiotics Underlies Suppressive Drug Interactions
type: journal_article
volume: 139
year: '2009'
...
---
_id: '4231'
abstract:
- lang: eng
text: The evolution of quantitative characters depends on the frequencies of the
alleles involved, yet these frequencies cannot usually be measured. Previous groups
have proposed an approximation to the dynamics of quantitative traits, based on
an analogy with statistical mechanics. We present a modified version of that approach,
which makes the analogy more precise and applies quite generally to describe the
evolution of allele frequencies. We calculate explicitly how the macroscopic quantities
(i.e., quantities that depend on the quantitative trait) depend on evolutionary
forces, in a way that is independent of the microscopic details. We first show
that the stationary distribution of allele frequencies under drift, selection,
and mutation maximizes a certain measure of entropy, subject to constraints on
the expectation of observable quantities. We then approximate the dynamical changes
in these expectations, assuming that the distribution of allele frequencies always
maximizes entropy, conditional on the expected values. When applied to directional
selection on an additive trait, this gives a very good approximation to the evolution
of the trait mean and the genetic variance, when the number of mutations per generation
is sufficiently high (4Nμ > 1). We show how the method can be modified for
small mutation rates (4Nμ → 0). We outline how this method describes epistatic
interactions as, for example, with stabilizing selection.
acknowledgement: "N.B. was supported by the Engineering and Physical Sciences Research
Council (GR/T11753 and GR/T19537) and by the Royal Society.\r\nWe are grateful to
Ellen Baake for helping to initiate this project and for her comments on this manuscript.
We also thank Michael Turelli for his comments on the manuscript and I. Pen for
discussions and support in this project. This project was a result of a collaboration
supported by the European Science Foundation grant “Integrating population genetics
and conservation biology.” "
author:
- 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: Harold
full_name: De Vladar, Harold
last_name: De Vladar
citation:
ama: Barton NH, De Vladar H. Statistical mechanics and the evolution of polygenic
quantitative traits. Genetics. 2009;181(3):997-1011. doi:10.1534/genetics.108.099309
apa: Barton, N. H., & De Vladar, H. (2009). Statistical mechanics and the evolution
of polygenic quantitative traits. Genetics. Genetics Society of America.
https://doi.org/10.1534/genetics.108.099309
chicago: Barton, Nicholas H, and Harold De Vladar. “Statistical Mechanics and the
Evolution of Polygenic Quantitative Traits.” Genetics. Genetics Society
of America, 2009. https://doi.org/10.1534/genetics.108.099309.
ieee: N. H. Barton and H. De Vladar, “Statistical mechanics and the evolution of
polygenic quantitative traits,” Genetics, vol. 181, no. 3. Genetics Society
of America, pp. 997–1011, 2009.
ista: Barton NH, De Vladar H. 2009. Statistical mechanics and the evolution of polygenic
quantitative traits. Genetics. 181(3), 997–1011.
mla: Barton, Nicholas H., and Harold De Vladar. “Statistical Mechanics and the Evolution
of Polygenic Quantitative Traits.” Genetics, vol. 181, no. 3, Genetics
Society of America, 2009, pp. 997–1011, doi:10.1534/genetics.108.099309.
short: N.H. Barton, H. De Vladar, Genetics 181 (2009) 997–1011.
date_created: 2018-12-11T12:07:44Z
date_published: 2009-03-01T00:00:00Z
date_updated: 2021-01-12T07:55:29Z
day: '01'
department:
- _id: NiBa
doi: 10.1534/genetics.108.099309
intvolume: ' 181'
issue: '3'
language:
- iso: eng
month: '03'
oa_version: None
page: 997 - 1011
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '1882'
quality_controlled: '1'
scopus_import: 1
status: public
title: Statistical mechanics and the evolution of polygenic quantitative traits
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 181
year: '2009'
...
---
_id: '4232'
author:
- first_name: Harold
full_name: Harold Vladar
id: 2A181218-F248-11E8-B48F-1D18A9856A87
last_name: Vladar
orcid: 0000-0002-5985-7653
citation:
ama: de Vladar H. Stochasticity and Variability in the dynamics and genetics of
populations. 2009. doi:3811
apa: de Vladar, H. (2009). Stochasticity and Variability in the dynamics and
genetics of populations. Faculty of mathematical and natural sciences, University
of Groningen. https://doi.org/3811
chicago: Vladar, Harold de. “Stochasticity and Variability in the Dynamics and Genetics
of Populations.” Faculty of mathematical and natural sciences, University of Groningen,
2009. https://doi.org/3811.
ieee: H. de Vladar, “Stochasticity and Variability in the dynamics and genetics
of populations,” Faculty of mathematical and natural sciences, University of Groningen,
2009.
ista: de Vladar H. 2009. Stochasticity and Variability in the dynamics and genetics
of populations. Faculty of mathematical and natural sciences, University of Groningen.
mla: de Vladar, Harold. Stochasticity and Variability in the Dynamics and Genetics
of Populations. Faculty of mathematical and natural sciences, University of
Groningen, 2009, doi:3811.
short: H. de Vladar, Stochasticity and Variability in the Dynamics and Genetics
of Populations, Faculty of mathematical and natural sciences, University of Groningen,
2009.
date_created: 2018-12-11T12:07:44Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:55:29Z
day: '01'
doi: '3811'
extern: 1
month: '01'
publication_status: published
publisher: Faculty of mathematical and natural sciences, University of Groningen
publist_id: '1883'
quality_controlled: 0
status: public
title: Stochasticity and Variability in the dynamics and genetics of populations
type: dissertation
year: '2009'
...
---
_id: '4242'
abstract:
- lang: eng
text: 'Felsenstein distinguished two ways by which selection can directly strengthen
isolation. First, a modifier that strengthens prezygotic isolation can be favored
everywhere. This fits with the traditional view of reinforcement as an adaptation
to reduce deleterious hybridization by strengthening assortative mating. Second,
selection can favor association between different incompatibilities, despite recombination.
We generalize this “two allele” model to follow associations among any number
of incompatibilities, which may include both assortment and hybrid inviability.
Our key argument is that this process, of coupling between incompatibilities,
may be quite different from the usual view of reinforcement: strong isolation
can evolve through the coupling of any kind of incompatibility, whether prezygotic
or postzygotic. Single locus incompatibilities become coupled because associations
between them increase the variance in compatibility, which in turn increases mean
fitness if there is positive epistasis. Multiple incompatibilities, each maintained
by epistasis, can become coupled in the same way. In contrast, a single-locus
incompatibility can become coupled with loci that reduce the viability of haploid
hybrids because this reduces harmful recombination. We obtain simple approximations
for the limits of tight linkage, and strong assortment, and show how assortment
alleles can invade through associations with other components of reproductive
isolation.'
acknowledgement: "This work was supported by a Royal Society/Wolfson Research Merit
award, and by a grant from the Natural Environment Research Council.\r\nWe are very
grateful for insightful comments from S. P. Otto, and for helpful suggestions from
the referees and the Associate Editor, Maria Servedio."
author:
- 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: Maria
full_name: De Cara, Maria
last_name: De Cara
citation:
ama: Barton NH, De Cara M. The evolution of strong reproductive isolation. Evolution;
International Journal of Organic Evolution. 2009;63(5):1171-1190. doi:10.1111/j.1558-5646.2009.00622.x
apa: Barton, N. H., & De Cara, M. (2009). The evolution of strong reproductive
isolation. Evolution; International Journal of Organic Evolution. Wiley.
https://doi.org/10.1111/j.1558-5646.2009.00622.x
chicago: Barton, Nicholas H, and Maria De Cara. “The Evolution of Strong Reproductive
Isolation.” Evolution; International Journal of Organic Evolution. Wiley,
2009. https://doi.org/10.1111/j.1558-5646.2009.00622.x.
ieee: N. H. Barton and M. De Cara, “The evolution of strong reproductive isolation,”
Evolution; International Journal of Organic Evolution, vol. 63, no. 5.
Wiley, pp. 1171–1190, 2009.
ista: Barton NH, De Cara M. 2009. The evolution of strong reproductive isolation.
Evolution; International Journal of Organic Evolution. 63(5), 1171–1190.
mla: Barton, Nicholas H., and Maria De Cara. “The Evolution of Strong Reproductive
Isolation.” Evolution; International Journal of Organic Evolution, vol.
63, no. 5, Wiley, 2009, pp. 1171–90, doi:10.1111/j.1558-5646.2009.00622.x.
short: N.H. Barton, M. De Cara, Evolution; International Journal of Organic Evolution
63 (2009) 1171–1190.
date_created: 2018-12-11T12:07:48Z
date_published: 2009-05-01T00:00:00Z
date_updated: 2021-01-12T07:55:33Z
day: '01'
ddc:
- '570'
department:
- _id: NiBa
doi: 10.1111/j.1558-5646.2009.00622.x
file:
- access_level: open_access
checksum: 1920d2e25ef335833764256c1a47bbfb
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:46Z
date_updated: 2020-07-14T12:46:25Z
file_id: '4903'
file_name: IST-2016-551-v1+1_BartonDeCaraRevNew.pdf
file_size: 720913
relation: main_file
- access_level: open_access
checksum: c1c51bbc10d4f328fc96fc5b0e5dc25d
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:11:47Z
date_updated: 2020-07-14T12:46:25Z
file_id: '4904'
file_name: IST-2016-551-v1+2_BartonDeCaraRevNewSI.pdf
file_size: 290160
relation: main_file
file_date_updated: 2020-07-14T12:46:25Z
has_accepted_license: '1'
intvolume: ' 63'
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
page: 1171 - 1190
publication: Evolution; International Journal of Organic Evolution
publication_status: published
publisher: Wiley
publist_id: '1866'
pubrep_id: '551'
quality_controlled: '1'
scopus_import: 1
status: public
title: The evolution of strong reproductive isolation
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 63
year: '2009'
...
---
_id: '4357'
abstract:
- lang: eng
text: Parallel evolution is the acquisition of identical adaptive traits in independently
evolving populations. Understanding whether the genetic changes underlying adaptation
to a common selective environment are parallel within and between species is interesting
because it sheds light on the degree of evolutionary constraints. If parallel
evolution is perfect, then the implication is that forces such as functional constraints,
epistasis, and pleiotropy play an important role in shaping the outcomes of adaptive
evolution. In addition, population genetic theory predicts that the probability
of parallel evolution will decline with an increase in the number of adaptive
solutions-if a single adaptive solution exists, then parallel evolution will be
observed among highly divergent species. For this reason, it is predicted that
close relatives-which likely overlap more in the details of their adaptive solutions-will
show more parallel evolution. By adapting three related bacteriophage species
to a novel environment we find (1) a high rate of parallel genetic evolution at
orthologous nucleotide and amino acid residues within species, (2) parallel beneficial
mutations do not occur in a common order in which they fix or appear in an evolving
population, (3) low rates of parallel evolution and convergent evolution between
species, and (4) the probability of parallel and convergent evolution between
species is strongly effected by divergence.
author:
- first_name: Jonathan P
full_name: Jonathan Bollback
id: 2C6FA9CC-F248-11E8-B48F-1D18A9856A87
last_name: Bollback
orcid: 0000-0002-4624-4612
- first_name: John
full_name: Huelsenbeck, John P
last_name: Huelsenbeck
citation:
ama: Bollback JP, Huelsenbeck J. Parallel genetic evolution within and between bacteriophage
species of varying degrees of divergence. Genetics. 2009;181(1):225-234.
doi:10.1534/genetics.107.085225
apa: Bollback, J. P., & Huelsenbeck, J. (2009). Parallel genetic evolution within
and between bacteriophage species of varying degrees of divergence. Genetics.
Genetics Society of America. https://doi.org/10.1534/genetics.107.085225
chicago: Bollback, Jonathan P, and John Huelsenbeck. “Parallel Genetic Evolution
within and between Bacteriophage Species of Varying Degrees of Divergence.” Genetics.
Genetics Society of America, 2009. https://doi.org/10.1534/genetics.107.085225.
ieee: J. P. Bollback and J. Huelsenbeck, “Parallel genetic evolution within and
between bacteriophage species of varying degrees of divergence,” Genetics,
vol. 181, no. 1. Genetics Society of America, pp. 225–234, 2009.
ista: Bollback JP, Huelsenbeck J. 2009. Parallel genetic evolution within and between
bacteriophage species of varying degrees of divergence. Genetics. 181(1), 225–234.
mla: Bollback, Jonathan P., and John Huelsenbeck. “Parallel Genetic Evolution within
and between Bacteriophage Species of Varying Degrees of Divergence.” Genetics,
vol. 181, no. 1, Genetics Society of America, 2009, pp. 225–34, doi:10.1534/genetics.107.085225.
short: J.P. Bollback, J. Huelsenbeck, Genetics 181 (2009) 225–234.
date_created: 2018-12-11T12:08:26Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:22Z
day: '01'
doi: 10.1534/genetics.107.085225
extern: 1
intvolume: ' 181'
issue: '1'
month: '01'
page: 225 - 234
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '1101'
quality_controlled: 0
status: public
title: Parallel genetic evolution within and between bacteriophage species of varying
degrees of divergence
type: journal_article
volume: 181
year: '2009'
...
---
_id: '4360'
alternative_title:
- LNCS 5749
author:
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
- first_name: Ruzica
full_name: Piskac, Ruzica
last_name: Piskac
- first_name: Viktor
full_name: Kuncak, Viktor
last_name: Kuncak
citation:
ama: 'Wies T, Piskac R, Kuncak V. Combining Theories with Shared Set Operations.
In: Springer; 2009:366-382. doi:1558'
apa: 'Wies, T., Piskac, R., & Kuncak, V. (2009). Combining Theories with Shared
Set Operations (pp. 366–382). Presented at the FroCoS: Frontiers of Combining
Systems, Springer. https://doi.org/1558'
chicago: Wies, Thomas, Ruzica Piskac, and Viktor Kuncak. “Combining Theories with
Shared Set Operations,” 366–82. Springer, 2009. https://doi.org/1558.
ieee: 'T. Wies, R. Piskac, and V. Kuncak, “Combining Theories with Shared Set Operations,”
presented at the FroCoS: Frontiers of Combining Systems, 2009, pp. 366–382.'
ista: 'Wies T, Piskac R, Kuncak V. 2009. Combining Theories with Shared Set Operations.
FroCoS: Frontiers of Combining Systems, LNCS 5749, , 366–382.'
mla: Wies, Thomas, et al. Combining Theories with Shared Set Operations.
Springer, 2009, pp. 366–82, doi:1558.
short: T. Wies, R. Piskac, V. Kuncak, in:, Springer, 2009, pp. 366–382.
conference:
name: 'FroCoS: Frontiers of Combining Systems'
date_created: 2018-12-11T12:08:27Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:24Z
day: '01'
doi: '1558'
extern: 1
month: '01'
page: 366 - 382
publication_status: published
publisher: Springer
publist_id: '1098'
quality_controlled: 0
status: public
title: Combining Theories with Shared Set Operations
type: conference
year: '2009'
...
---
_id: '4363'
author:
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: Singh V. Formalizing and Verifying Transactional Memories. Formalizing and
Verifying Transactional Memories. 2009.
apa: Singh, V. (2009). Formalizing and Verifying Transactional Memories.
Formalizing and Verifying Transactional Memories. EPFL Lausanne.
chicago: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing
and Verifying Transactional Memories. EPFL Lausanne, 2009.
ieee: V. Singh, “Formalizing and Verifying Transactional Memories,” EPFL Lausanne,
2009.
ista: Singh V. 2009. Formalizing and Verifying Transactional Memories. EPFL Lausanne.
mla: Singh, Vasu. “Formalizing and Verifying Transactional Memories.” Formalizing
and Verifying Transactional Memories, EPFL Lausanne, 2009.
short: V. Singh, Formalizing and Verifying Transactional Memories, EPFL Lausanne,
2009.
date_created: 2018-12-11T12:08:28Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:25Z
day: '01'
extern: 1
month: '01'
publication: Formalizing and Verifying Transactional Memories
publication_status: published
publisher: EPFL Lausanne
publist_id: '1095'
quality_controlled: 0
status: public
title: Formalizing and Verifying Transactional Memories
type: dissertation
year: '2009'
...
---
_id: '4365'
alternative_title:
- LNCS 5673
author:
- first_name: Mohamed
full_name: Seghir,Mohamed Nassim
last_name: Seghir
- first_name: Andreas
full_name: Podelski,Andreas
last_name: Podelski
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Seghir M, Podelski A, Wies T. Abstraction Refinement for Quantified Array
Assertions. In: Springer; 2009:3-18. doi:1556'
apa: 'Seghir, M., Podelski, A., & Wies, T. (2009). Abstraction Refinement for
Quantified Array Assertions (pp. 3–18). Presented at the SAS: Static Analysis
Symposium, Springer. https://doi.org/1556'
chicago: Seghir, Mohamed, Andreas Podelski, and Thomas Wies. “Abstraction Refinement
for Quantified Array Assertions,” 3–18. Springer, 2009. https://doi.org/1556.
ieee: 'M. Seghir, A. Podelski, and T. Wies, “Abstraction Refinement for Quantified
Array Assertions,” presented at the SAS: Static Analysis Symposium, 2009, pp.
3–18.'
ista: 'Seghir M, Podelski A, Wies T. 2009. Abstraction Refinement for Quantified
Array Assertions. SAS: Static Analysis Symposium, LNCS 5673, , 3–18.'
mla: Seghir, Mohamed, et al. Abstraction Refinement for Quantified Array Assertions.
Springer, 2009, pp. 3–18, doi:1556.
short: M. Seghir, A. Podelski, T. Wies, in:, Springer, 2009, pp. 3–18.
conference:
name: 'SAS: Static Analysis Symposium'
date_created: 2018-12-11T12:08:29Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:26Z
day: '01'
doi: '1556'
extern: 1
month: '01'
page: 3 - 18
publication_status: published
publisher: Springer
publist_id: '1094'
quality_controlled: 0
status: public
title: Abstraction Refinement for Quantified Array Assertions
type: conference
year: '2009'
...
---
_id: '4375'
alternative_title:
- LNCS 5643
author:
- first_name: Shuvendu
full_name: Lahiri,Shuvendu K.
last_name: Lahiri
- first_name: Shaz
full_name: Qadeer,Shaz
last_name: Qadeer
- first_name: Juan
full_name: Galeotti,Juan P.
last_name: Galeotti
- first_name: Jan
full_name: Voung,Jan W.
last_name: Voung
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. Intra-module Inference. In:
Springer; 2009:493-508. doi:1555'
apa: 'Lahiri, S., Qadeer, S., Galeotti, J., Voung, J., & Wies, T. (2009). Intra-module
Inference (pp. 493–508). Presented at the CAV: Computer Aided Verification, Springer.
https://doi.org/1555'
chicago: Lahiri, Shuvendu, Shaz Qadeer, Juan Galeotti, Jan Voung, and Thomas Wies.
“Intra-Module Inference,” 493–508. Springer, 2009. https://doi.org/1555.
ieee: 'S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, and T. Wies, “Intra-module Inference,”
presented at the CAV: Computer Aided Verification, 2009, pp. 493–508.'
ista: 'Lahiri S, Qadeer S, Galeotti J, Voung J, Wies T. 2009. Intra-module Inference.
CAV: Computer Aided Verification, LNCS 5643, , 493–508.'
mla: Lahiri, Shuvendu, et al. Intra-Module Inference. Springer, 2009, pp.
493–508, doi:1555.
short: S. Lahiri, S. Qadeer, J. Galeotti, J. Voung, T. Wies, in:, Springer, 2009,
pp. 493–508.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:32Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:30Z
day: '01'
doi: '1555'
extern: 1
month: '01'
page: 493 - 508
publication_status: published
publisher: Springer
publist_id: '1082'
quality_controlled: 0
status: public
title: Intra-module Inference
type: conference
year: '2009'
...
---
_id: '4376'
author:
- first_name: Roberto
full_name: Lublinerman,Roberto
last_name: Lublinerman
- first_name: Swarat
full_name: Chaudhuri,Swarat
last_name: Chaudhuri
- first_name: Pavol
full_name: Pavol Cerny
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
citation:
ama: 'Lublinerman R, Chaudhuri S, Cerny P. Parallel programming with object assemblies.
In: ACM; 2009:61-80. doi:1546'
apa: Lublinerman, R., Chaudhuri, S., & Cerny, P. (2009). Parallel programming
with object assemblies (pp. 61–80). Presented at the Oopsla Object Oriented Programming
Systems Languages and Applications, ACM. https://doi.org/1546
chicago: Lublinerman, Roberto, Swarat Chaudhuri, and Pavol Cerny. “Parallel Programming
with Object Assemblies,” 61–80. ACM, 2009. https://doi.org/1546.
ieee: R. Lublinerman, S. Chaudhuri, and P. Cerny, “Parallel programming with object
assemblies,” presented at the Oopsla Object Oriented Programming Systems Languages
and Applications, 2009, pp. 61–80.
ista: Lublinerman R, Chaudhuri S, Cerny P. 2009. Parallel programming with object
assemblies. Oopsla Object Oriented Programming Systems Languages and Applications,
61–80.
mla: Lublinerman, Roberto, et al. Parallel Programming with Object Assemblies.
ACM, 2009, pp. 61–80, doi:1546.
short: R. Lublinerman, S. Chaudhuri, P. Cerny, in:, ACM, 2009, pp. 61–80.
conference:
name: Oopsla Object Oriented Programming Systems Languages and Applications
date_created: 2018-12-11T12:08:32Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:30Z
day: '01'
doi: '1546'
extern: 1
month: '01'
page: 61 - 80
publication_status: published
publisher: ACM
publist_id: '1083'
quality_controlled: 0
status: public
title: Parallel programming with object assemblies
type: conference
year: '2009'
...
---
_id: '4377'
alternative_title:
- LNCS 5850
author:
- first_name: Jochen
full_name: Hoenicke,Jochen
last_name: Hoenicke
- first_name: K Rustan
full_name: Leino, K Rustan
last_name: Leino
- first_name: Andreas
full_name: Podelski,Andreas
last_name: Podelski
- first_name: Martin
full_name: Schäf,Martin
last_name: Schäf
- first_name: Thomas
full_name: Thomas Wies
id: 447BFB88-F248-11E8-B48F-1D18A9856A87
last_name: Wies
citation:
ama: 'Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. It’s Doomed; We Can Prove
It. In: Springer; 2009:338-353. doi:1557'
apa: 'Hoenicke, J., Leino, K. R., Podelski, A., Schäf, M., & Wies, T. (2009).
It’s Doomed; We Can Prove It (pp. 338–353). Presented at the FM: Formal Methods,
Springer. https://doi.org/1557'
chicago: Hoenicke, Jochen, K Rustan Leino, Andreas Podelski, Martin Schäf, and Thomas
Wies. “It’s Doomed; We Can Prove It,” 338–53. Springer, 2009. https://doi.org/1557.
ieee: 'J. Hoenicke, K. R. Leino, A. Podelski, M. Schäf, and T. Wies, “It’s Doomed;
We Can Prove It,” presented at the FM: Formal Methods, 2009, pp. 338–353.'
ista: 'Hoenicke J, Leino KR, Podelski A, Schäf M, Wies T. 2009. It’s Doomed; We
Can Prove It. FM: Formal Methods, LNCS 5850, , 338–353.'
mla: Hoenicke, Jochen, et al. It’s Doomed; We Can Prove It. Springer, 2009,
pp. 338–53, doi:1557.
short: J. Hoenicke, K.R. Leino, A. Podelski, M. Schäf, T. Wies, in:, Springer, 2009,
pp. 338–353.
conference:
name: 'FM: Formal Methods'
date_created: 2018-12-11T12:08:32Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:31Z
day: '01'
doi: '1557'
extern: 1
month: '01'
page: 338 - 353
publication_status: published
publisher: Springer
publist_id: '1079'
quality_controlled: 0
status: public
title: It's Doomed; We Can Prove It
type: conference
year: '2009'
...
---
_id: '4383'
abstract:
- lang: eng
text: Pseudo-code descriptions of STMs assume sequentially consistent program execution
and atomicity of high-level STM operations like read, write, and commit. These
assumptions are often violated in realistic settings, as STM implementations run
on relaxed memory models, with the atomicity of operations as provided by the
hardware. This paper presents the first approach to verify STMs under relaxed
memory models with atomicity of 32 bit loads and stores, and read-modify-write
operations. We present RML, a new high-level language for expressing concurrent
algorithms with a hardware-level atomicity of instructions, and whose semantics
is parametrized by various relaxed memory models. We then present our tool, FOIL,
which takes as input the RML description of an STM algorithm and the description
of a memory model, and automatically determines the locations of fences, which
if inserted, ensure the correctness of the STM algorithm under the given memory
model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of
sequential consistency, total store order, partial store order, and relaxed memory
order.
acknowledgement: This research was supported by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Guerraoui R, Henzinger TA, Singh V. Software transactional memory on relaxed
memory models. In: Vol 5643. Springer; 2009:321-336. doi:10.1007/978-3-642-02658-4_26'
apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2009). Software transactional
memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV:
Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_26'
chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional
Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_26.
ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Software transactional memory
on relaxed memory models,” presented at the CAV: Computer Aided Verification,
2009, vol. 5643, pp. 321–336.'
ista: 'Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on
relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336.'
mla: Guerraoui, Rachid, et al. Software Transactional Memory on Relaxed Memory
Models. Vol. 5643, Springer, 2009, pp. 321–36, doi:10.1007/978-3-642-02658-4_26.
short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:34Z
date_published: 2009-06-19T00:00:00Z
date_updated: 2021-01-12T07:56:34Z
day: '19'
doi: 10.1007/978-3-642-02658-4_26
extern: 1
file:
- access_level: open_access
checksum: df3c3e6306afd3f630a9146f91642f0a
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:14:50Z
date_updated: 2020-07-14T12:46:28Z
file_id: '5105'
file_name: IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf
file_size: 265763
relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
intvolume: ' 5643'
month: '06'
oa: 1
page: 321 - 336
publication_status: published
publisher: Springer
publist_id: '1074'
pubrep_id: '45'
quality_controlled: 0
status: public
title: Software transactional memory on relaxed memory models
type: conference
volume: 5643
year: '2009'
...
---
_id: '4385'
author:
- first_name: Aleksandar
full_name: Dragojevic,Aleksandar
last_name: Dragojevic
- first_name: Rachid
full_name: Guerraoui, Rachid
last_name: Guerraoui
- first_name: Anmol
full_name: Singh, Anmol V
last_name: Singh
- first_name: Vasu
full_name: Vasu Singh
id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
last_name: Singh
citation:
ama: 'Dragojevic A, Guerraoui R, Singh A, Singh V. Preventing versus curing: avoiding
conflicts in transactional memories. In: ACM; 2009:7-16. doi:1533'
apa: 'Dragojevic, A., Guerraoui, R., Singh, A., & Singh, V. (2009). Preventing
versus curing: avoiding conflicts in transactional memories (pp. 7–16). Presented
at the POPL: Principles of Programming Languages, ACM. https://doi.org/1533'
chicago: 'Dragojevic, Aleksandar, Rachid Guerraoui, Anmol Singh, and Vasu Singh.
“Preventing versus Curing: Avoiding Conflicts in Transactional Memories,” 7–16.
ACM, 2009. https://doi.org/1533.'
ieee: 'A. Dragojevic, R. Guerraoui, A. Singh, and V. Singh, “Preventing versus curing:
avoiding conflicts in transactional memories,” presented at the POPL: Principles
of Programming Languages, 2009, pp. 7–16.'
ista: 'Dragojevic A, Guerraoui R, Singh A, Singh V. 2009. Preventing versus curing:
avoiding conflicts in transactional memories. POPL: Principles of Programming
Languages, 7–16.'
mla: 'Dragojevic, Aleksandar, et al. Preventing versus Curing: Avoiding Conflicts
in Transactional Memories. ACM, 2009, pp. 7–16, doi:1533.'
short: A. Dragojevic, R. Guerraoui, A. Singh, V. Singh, in:, ACM, 2009, pp. 7–16.
conference:
name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:08:35Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:34Z
day: '01'
doi: '1533'
extern: 1
month: '01'
page: 7 - 16
publication_status: published
publisher: ACM
publist_id: '1070'
quality_controlled: 0
status: public
title: 'Preventing versus curing: avoiding conflicts in transactional memories'
type: conference
year: '2009'
...
---
_id: '4391'
alternative_title:
- LNCS
author:
- first_name: Pavol
full_name: Pavol Cerny
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
citation:
ama: 'Cerny P, Alur R. Automated Analysis of Java Methods for Confidentiality. In:
Springer; 2009:173-187. doi:1548'
apa: 'Cerny, P., & Alur, R. (2009). Automated Analysis of Java Methods for Confidentiality
(pp. 173–187). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/1548'
chicago: Cerny, Pavol, and Rajeev Alur. “Automated Analysis of Java Methods for
Confidentiality,” 173–87. Springer, 2009. https://doi.org/1548.
ieee: 'P. Cerny and R. Alur, “Automated Analysis of Java Methods for Confidentiality,”
presented at the CAV: Computer Aided Verification, 2009, pp. 173–187.'
ista: 'Cerny P, Alur R. 2009. Automated Analysis of Java Methods for Confidentiality.
CAV: Computer Aided Verification, LNCS, , 173–187.'
mla: Cerny, Pavol, and Rajeev Alur. Automated Analysis of Java Methods for Confidentiality.
Springer, 2009, pp. 173–87, doi:1548.
short: P. Cerny, R. Alur, in:, Springer, 2009, pp. 173–187.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:36Z
date_published: 2009-07-01T00:00:00Z
date_updated: 2021-01-12T07:56:37Z
day: '01'
doi: '1548'
extern: 1
month: '07'
page: 173 - 187
publication_status: published
publisher: Springer
publist_id: '1067'
quality_controlled: 0
status: public
title: Automated Analysis of Java Methods for Confidentiality
type: conference
year: '2009'
...
---
_id: '4403'
abstract:
- lang: eng
text: For programs whose data variables range over boolean or finite domains, program
verification is decidable, and this forms the basis of recent tools for software
model checking. In this paper, we consider algorithmic verification of programs
that use boolean variables, and in addition, access a single read-only array whose
length is potentially unbounded, and whose elements range over a potentially unbounded
data domain. We show that the reachability problem, while undecidable in general,
is (1) Pspace-complete for programs in which the array-accessing for-loops are
not nested, (2) decidable for a restricted class of programs with doubly-nested
loops. The second result establishes connections to automata and logics defining
languages over data words.
alternative_title:
- LNCS
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Pavol
full_name: Cerny, Pavol
id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
last_name: Cerny
- first_name: Scott
full_name: Weinstein, Scott
last_name: Weinstein
citation:
ama: 'Alur R, Cerny P, Weinstein S. Algorithmic analysis of array-accessing programs.
In: Vol 5771. Springer; 2009:86-101. doi:10.1007/978-3-642-04027-6_9'
apa: 'Alur, R., Cerny, P., & Weinstein, S. (2009). Algorithmic analysis of array-accessing
programs (Vol. 5771, pp. 86–101). Presented at the CSL: Computer Science Logic,
Coimbra, Portugal: Springer. https://doi.org/10.1007/978-3-642-04027-6_9'
chicago: Alur, Rajeev, Pavol Cerny, and Scott Weinstein. “Algorithmic Analysis of
Array-Accessing Programs,” 5771:86–101. Springer, 2009. https://doi.org/10.1007/978-3-642-04027-6_9.
ieee: 'R. Alur, P. Cerny, and S. Weinstein, “Algorithmic analysis of array-accessing
programs,” presented at the CSL: Computer Science Logic, Coimbra, Portugal, 2009,
vol. 5771, pp. 86–101.'
ista: 'Alur R, Cerny P, Weinstein S. 2009. Algorithmic analysis of array-accessing
programs. CSL: Computer Science Logic, LNCS, vol. 5771, 86–101.'
mla: Alur, Rajeev, et al. Algorithmic Analysis of Array-Accessing Programs.
Vol. 5771, Springer, 2009, pp. 86–101, doi:10.1007/978-3-642-04027-6_9.
short: R. Alur, P. Cerny, S. Weinstein, in:, Springer, 2009, pp. 86–101.
conference:
end_date: 2009-09-11
location: Coimbra, Portugal
name: 'CSL: Computer Science Logic'
start_date: 2009-09-07
date_created: 2018-12-11T12:08:40Z
date_published: 2009-09-01T00:00:00Z
date_updated: 2023-02-23T11:06:20Z
day: '01'
doi: 10.1007/978-3-642-04027-6_9
extern: '1'
intvolume: ' 5771'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: http://repository.upenn.edu/cis_reports/894/
month: '09'
oa: 1
oa_version: Submitted Version
page: 86 - 101
publication_status: published
publisher: Springer
publist_id: '1056'
quality_controlled: '1'
related_material:
record:
- id: '2967'
relation: later_version
status: public
status: public
title: Algorithmic analysis of array-accessing programs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 5771
year: '2009'
...
---
_id: '4453'
abstract:
- lang: eng
text: We present an on-the-fly abstraction technique for infinite-state continuous
-time Markov chains. We consider Markov chains that are specified by a finite
set of transition classes. Such models naturally represent biochemical reactions
and therefore play an important role in the stochastic modeling of biological
systems. We approximate the transient probability distributions at various time
instances by solving a sequence of dynamically constructed abstract models, each
depending on the previous one. Each abstract model is a finite Markov chain that
represents the behavior of the original, infinite chain during a specific time
interval. Our approach provides complete information about probability distributions,
not just about individual parameters like the mean. The error of each abstraction
can be computed, and the precision of the abstraction refined when desired. We
implemented the algorithm and demonstrate its usefulness and efficiency on several
case studies from systems biology.
acknowledgement: The research has been partially funded by the Swiss National Science
Foundation under grant 205321-111840.
alternative_title:
- LNCS
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: 'Henzinger TA, Mateescu M, Wolf V. Sliding-window abstraction for infinite
Markov chains. In: Vol 5643. Springer; 2009:337-352. doi:10.1007/978-3-642-02658-4_27'
apa: 'Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Sliding-window abstraction
for infinite Markov chains (Vol. 5643, pp. 337–352). Presented at the CAV: Computer
Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_27'
chicago: Henzinger, Thomas A, Maria Mateescu, and Verena Wolf. “Sliding-Window Abstraction
for Infinite Markov Chains,” 5643:337–52. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_27.
ieee: 'T. A. Henzinger, M. Mateescu, and V. Wolf, “Sliding-window abstraction for
infinite Markov chains,” presented at the CAV: Computer Aided Verification, 2009,
vol. 5643, pp. 337–352.'
ista: 'Henzinger TA, Mateescu M, Wolf V. 2009. Sliding-window abstraction for infinite
Markov chains. CAV: Computer Aided Verification, LNCS, vol. 5643, 337–352.'
mla: Henzinger, Thomas A., et al. Sliding-Window Abstraction for Infinite Markov
Chains. Vol. 5643, Springer, 2009, pp. 337–52, doi:10.1007/978-3-642-02658-4_27.
short: T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp. 337–352.
conference:
name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:55Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '01'
doi: 10.1007/978-3-642-02658-4_27
extern: 1
file:
- access_level: open_access
checksum: 36b974111521ea534aae294166e93a63
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:12:20Z
date_updated: 2020-07-14T12:46:30Z
file_id: '4938'
file_name: IST-2012-40-v1+1_Sliding-window_abstraction_for_infinite_markov_chains.pdf
file_size: 804295
relation: main_file
file_date_updated: 2020-07-14T12:46:30Z
intvolume: ' 5643'
main_file_link:
- open_access: '0'
url: http://pub.ist.ac.at/%7Etah/Publications/sliding-window_abstraction_for_infinite_markov_chains.pdf
month: '01'
oa: 1
page: 337 - 352
publication_status: published
publisher: Springer
publist_id: '278'
pubrep_id: '40'
quality_controlled: 0
status: public
title: Sliding-window abstraction for infinite Markov chains
type: conference
volume: 5643
year: '2009'
...
---
_id: '4535'
abstract:
- lang: eng
text: |-
Molecular noise, which arises from the randomness of the discrete events in the cell, significantly influences fundamental biological processes. Discrete -state continuous-time stochastic models (CTMC) can be used to describe such effects, but the calculation of the probabilities of certain events is computationally expensive.
We present a comparison of two analysis approaches for CTMC. On one hand, we estimate the probabilities of interest using repeated Gillespie simulation and determine the statistical accuracy that we obtain. On the other hand, we apply a numerical reachability analysis that approximates the probability distributions of the system at several time instances. We use examples of cellular processes to demonstrate the superiority of the reachability analysis if accurate results are required.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under grant 205321-111840 and by the Excellence Cluster on Multimodal
Computing and Interaction.
alternative_title:
- LNCS
author:
- first_name: Frédéric
full_name: Didier, Frédéric
last_name: Didier
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Maria
full_name: Maria Mateescu
id: 3B43276C-F248-11E8-B48F-1D18A9856A87
last_name: Mateescu
- first_name: Verena
full_name: Wolf, Verena
last_name: Wolf
citation:
ama: 'Didier F, Henzinger TA, Mateescu M, Wolf V. Approximation of event probabilities
in noisy cellular processes. In: Vol 5688. Springer; 2009:173-188. doi:10.1007/978-3-642-03845-7_12'
apa: 'Didier, F., Henzinger, T. A., Mateescu, M., & Wolf, V. (2009). Approximation
of event probabilities in noisy cellular processes (Vol. 5688, pp. 173–188). Presented
at the CMSB: Computational Methods in Systems Biology, Springer. https://doi.org/10.1007/978-3-642-03845-7_12'
chicago: Didier, Frédéric, Thomas A Henzinger, Maria Mateescu, and Verena Wolf.
“Approximation of Event Probabilities in Noisy Cellular Processes,” 5688:173–88.
Springer, 2009. https://doi.org/10.1007/978-3-642-03845-7_12.
ieee: 'F. Didier, T. A. Henzinger, M. Mateescu, and V. Wolf, “Approximation of event
probabilities in noisy cellular processes,” presented at the CMSB: Computational
Methods in Systems Biology, 2009, vol. 5688, pp. 173–188.'
ista: 'Didier F, Henzinger TA, Mateescu M, Wolf V. 2009. Approximation of event
probabilities in noisy cellular processes. CMSB: Computational Methods in Systems
Biology, LNCS, vol. 5688, 173–188.'
mla: Didier, Frédéric, et al. Approximation of Event Probabilities in Noisy Cellular
Processes. Vol. 5688, Springer, 2009, pp. 173–88, doi:10.1007/978-3-642-03845-7_12.
short: F. Didier, T.A. Henzinger, M. Mateescu, V. Wolf, in:, Springer, 2009, pp.
173–188.
conference:
name: 'CMSB: Computational Methods in Systems Biology'
date_created: 2018-12-11T12:09:21Z
date_published: 2009-08-17T00:00:00Z
date_updated: 2023-02-23T11:24:03Z
day: '17'
doi: 10.1007/978-3-642-03845-7_12
extern: 1
intvolume: ' 5688'
month: '08'
page: 173 - 188
publication_status: published
publisher: Springer
publist_id: '189'
quality_controlled: 0
related_material:
record:
- id: '3364'
relation: later_version
status: public
status: public
title: Approximation of event probabilities in noisy cellular processes
type: conference
volume: 5688
year: '2009'
...
---
_id: '4540'
abstract:
- lang: eng
text: Weighted automata are nondeterministic automata with numerical weights on
transitions. They can define quantitative languages L that assign to each word
w a real number L(w). In the case of infinite words, the value of a run is naturally
computed as the maximum, limsup, liminf, limit average, or discounted sum of the
transition weights. We study expressiveness and closure questions about these
quantitative languages. We first show that the set of words with value greater
than a threshold can be non-w-regular for deterministic limit-average and discounted-sum
automata, while this set is always w-regular when the threshold is isolated (i.e.,
some neighborhood around the threshold contains no word). In the latter case,
we prove that the w-regular language is robust against small perturbations of
the transition weights. We next consider automata with transition weights 0 or
1 and show that they are as expressive as general weighted automata in the limit-average
case, but not in the discounted-sum case. Third, for quantitative languages L-1
and L-2, we consider the operations max(L-1, L-2), min(L-1, L-2), and 1-L-1, which
generalize the boolean operations on languages, as well as the sum L-1 + L-2.
We establish the closure properties of all classes of quantitative languages with
respect to these four operations.
article_processing_charge: No
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- 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: 'Chatterjee K, Doyen L, Henzinger TA. Expressiveness and closure properties
for quantitative languages. In: IEEE; 2009:199-208. doi:10.1109/LICS.2009.16'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2009). Expressiveness and
closure properties for quantitative languages (pp. 199–208). Presented at the
LICS: Logic in Computer Science, IEEE. https://doi.org/10.1109/LICS.2009.16'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Expressiveness
and Closure Properties for Quantitative Languages,” 199–208. IEEE, 2009. https://doi.org/10.1109/LICS.2009.16.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Expressiveness and closure
properties for quantitative languages,” presented at the LICS: Logic in Computer
Science, 2009, pp. 199–208.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2009. Expressiveness and closure properties
for quantitative languages. LICS: Logic in Computer Science, 199–208.'
mla: Chatterjee, Krishnendu, et al. Expressiveness and Closure Properties for
Quantitative Languages. IEEE, 2009, pp. 199–208, doi:10.1109/LICS.2009.16.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, IEEE, 2009, pp. 199–208.
conference:
name: 'LICS: Logic in Computer Science'
date_created: 2018-12-11T12:09:23Z
date_published: 2009-01-01T00:00:00Z
date_updated: 2023-02-23T11:46:11Z
day: '01'
doi: 10.1109/LICS.2009.16
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 199 - 208
publication_status: published
publisher: IEEE
publist_id: '181'
pubrep_id: '55'
quality_controlled: '1'
related_material:
record:
- id: '3867'
relation: later_version
status: public
scopus_import: '1'
status: public
title: Expressiveness and closure properties for quantitative languages
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2009'
...
---
_id: '4542'
abstract:
- lang: eng
text: "Weighted automata are finite automata with numerical weights on transitions.
Nondeterministic weighted automata define quantitative languages L that assign
to each word w a real number L(w) computed as the maximal value of all runs over
w, and the value of a run r is a function of the sequence of weights that appear
along r. There are several natural functions to consider such as Sup, LimSup,
LimInf, limit average, and discounted sum of transition weights.\r\nWe introduce
alternating weighted automata in which the transitions of the runs are chosen
by two players in a turn-based fashion. Each word is assigned the maximal value
of a run that the first player can enforce regardless of the choices made by the
second player. We survey the results about closure properties, expressiveness,
and decision problems for nondeterministic weighted automata, and we extend these
results to alternating weighted automata.\r\nFor quantitative languages L 1 and
L 2, we consider the pointwise operations max(L 1,L 2), min(L 1,L 2), 1 − L 1,
and the sum L 1 + L 2. We establish the closure properties of all classes of alternating
weighted automata with respect to these four operations.\r\nWe next compare the
expressive power of the various classes of alternating and nondeterministic weighted
automata over infinite words. In particular, for limit average and discounted
sum, we show that alternation brings more expressive power than nondeterminism.\r\nFinally,
we present decidability results and open questions for the quantitative extension
of the classical decision problems in automata theory: emptiness, universality,
language inclusion, and language equivalence."
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under the Indo-Swiss Joint Research Programme, by the European Network
of Excellence on Embedded Systems Design (ArtistDesign), by the European Combest,
Quasimodo, and Gasics projects, by the PAI program Moves funded by the Belgian Federal
Government, and by the CFV (Federated Center in Verification) funded by the F.R.S.-FNRS.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Laurent
full_name: Doyen, Laurent
last_name: Doyen
- 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: 'Chatterjee K, Doyen L, Henzinger TA. Alternating weighted automata. In: Vol
5699. Springer; 2009:3-13. doi:10.1007/978-3-642-03409-1_2'
apa: 'Chatterjee, K., Doyen, L., & Henzinger, T. A. (2009). Alternating weighted
automata (Vol. 5699, pp. 3–13). Presented at the FCT: Fundamentals of Computation
Theory, Wroclaw, Poland: Springer. https://doi.org/10.1007/978-3-642-03409-1_2'
chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “Alternating
Weighted Automata,” 5699:3–13. Springer, 2009. https://doi.org/10.1007/978-3-642-03409-1_2.
ieee: 'K. Chatterjee, L. Doyen, and T. A. Henzinger, “Alternating weighted automata,”
presented at the FCT: Fundamentals of Computation Theory, Wroclaw, Poland, 2009,
vol. 5699, pp. 3–13.'
ista: 'Chatterjee K, Doyen L, Henzinger TA. 2009. Alternating weighted automata.
FCT: Fundamentals of Computation Theory, LNCS, vol. 5699, 3–13.'
mla: Chatterjee, Krishnendu, et al. Alternating Weighted Automata. Vol. 5699,
Springer, 2009, pp. 3–13, doi:10.1007/978-3-642-03409-1_2.
short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, Springer, 2009, pp. 3–13.
conference:
end_date: 2009-09-04
location: Wroclaw, Poland
name: 'FCT: Fundamentals of Computation Theory'
start_date: 2009-09-02
date_created: 2018-12-11T12:09:23Z
date_published: 2009-09-10T00:00:00Z
date_updated: 2021-01-12T07:59:34Z
day: '10'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1007/978-3-642-03409-1_2
ec_funded: 1
file:
- access_level: open_access
checksum: e8f53abb63579de3f2bff58b2a1188e2
content_type: application/pdf
creator: system
date_created: 2018-12-12T10:15:09Z
date_updated: 2020-07-14T12:46:31Z
file_id: '5126'
file_name: IST-2012-39-v1+1_Alternating_Weighted_Automata.pdf
file_size: 164428
relation: main_file
file_date_updated: 2020-07-14T12:46:31Z
has_accepted_license: '1'
intvolume: ' 5699'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 3 - 13
project:
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
publication_status: published
publisher: Springer
publist_id: '180'
pubrep_id: '39'
quality_controlled: '1'
scopus_import: 1
status: public
title: Alternating weighted automata
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5699
year: '2009'
...
---
_id: '4543'
abstract:
- lang: eng
text: The synthesis of a reactive system with respect to all omega-regular specification
requires the solution of a graph game. Such games have been extended in two natural
ways. First, a game graph can be equipped with probabilistic choices between alternative
transitions, thus allowing the, modeling of uncertain behaviour. These are called
stochastic games. Second, a liveness specification can he strengthened to require
satisfaction within all unknown but bounded amount of time. These are called finitary
objectives. We study. for the first time, the, combination of Stochastic games
and finitary objectives. We characterize the requirements on optimal strategies
and provide algorithms for Computing the maximal achievable probability of winning
stochastic games with finitary parity or Street, objectives. Most notably the
set of state's from which a player can win with probability . for a finitary parity
objective can he computed in polynomial time even though no polynomial-time algorithm
is known in the nonfinitary case.
acknowledgement: This research was supported in part by the Swiss National Science
Foundation under the Indo-Swiss Joint Research Programme, by the European Network
of Excellence on Embedded Systems Design (ArtistDesign), and by the European project
Combest.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- 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: Florian
full_name: Horn, Florian
id: 37327ACE-F248-11E8-B48F-1D18A9856A87
last_name: Horn
citation:
ama: 'Chatterjee K, Henzinger TA, Horn F. Stochastic games with finitary objectives.
In: Vol 5734. Springer; 2009:34-54. doi:10.1007/978-3-642-03816-7_4'
apa: 'Chatterjee, K., Henzinger, T. A., & Horn, F. (2009). Stochastic games
with finitary objectives (Vol. 5734, pp. 34–54). Presented at the MFCS: Mathematical
Foundations of Computer Science, High Tatras, Slovakia: Springer. https://doi.org/10.1007/978-3-642-03816-7_4'
chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Florian Horn. “Stochastic
Games with Finitary Objectives,” 5734:34–54. Springer, 2009. https://doi.org/10.1007/978-3-642-03816-7_4.
ieee: 'K. Chatterjee, T. A. Henzinger, and F. Horn, “Stochastic games with finitary
objectives,” presented at the MFCS: Mathematical Foundations of Computer Science,
High Tatras, Slovakia, 2009, vol. 5734, pp. 34–54.'
ista: 'Chatterjee K, Henzinger TA, Horn F. 2009. Stochastic games with finitary
objectives. MFCS: Mathematical Foundations of Computer Science, LNCS, vol. 5734,
34–54.'
mla: Chatterjee, Krishnendu, et al. Stochastic Games with Finitary Objectives.
Vol. 5734, Springer, 2009, pp. 34–54, doi:10.1007/978-3-642-03816-7_4.
short: K. Chatterjee, T.A. Henzinger, F. Horn, in:, Springer, 2009, pp. 34–54.
conference:
end_date: 2009-08-28
location: High Tatras, Slovakia
name: 'MFCS: Mathematical Foundations of Computer Science'
start_date: 2009-08-24
date_created: 2018-12-11T12:09:24Z
date_published: 2009-08-01T00:00:00Z
date_updated: 2021-01-12T07:59:35Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-03816-7_4
ec_funded: 1
intvolume: ' 5734'
language:
- iso: eng
month: '08'
oa_version: None
page: 34 - 54
project:
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '215543'
name: COMponent-Based Embedded Systems design Techniques
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '214373'
name: Design for Embedded Systems
publication_status: published
publisher: Springer
publist_id: '178'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic games with finitary objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 5734
year: '2009'
...