---
_id: '9528'
abstract:
- lang: eng
  text: Accumulating evidence points toward diverse functions for plant chromatin.
    Remarkable progress has been made over the last few years in elucidating the mechanisms
    for a number of these functions. Activity of the histone demethylase IBM1 accurately
    targets DNA methylation to silent repeats and transposable elements, not to genes.
    A genetic screen uncovered the surprising role of H2A.Z-containing nucleosomes
    in sensing precise differences in ambient temperature and consequent gene regulation.
    Precise maintenance of chromosome number is assured by a histone modification
    that suppresses inappropriate DNA replication and by centromeric histone H3 regulation
    of chromosome segregation. Histones and noncoding RNAs regulate FLOWERING LOCUS
    C, the expression of which quantitatively measures the duration of cold exposure,
    functioning as memory of winter. These findings are a testament to the power of
    using plants to research chromatin organization, and demonstrate examples of how
    chromatin functions to achieve biological accuracy, precision, and memory.
article_processing_charge: No
article_type: review
author:
- first_name: Jason T.
  full_name: Huff, Jason T.
  last_name: Huff
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Huff JT, Zilberman D. Regulation of biological accuracy, precision, and memory
    by plant chromatin organization. <i>Current Opinion in Genetics and Development</i>.
    2012;22(2):132-138. doi:<a href="https://doi.org/10.1016/j.gde.2012.01.007">10.1016/j.gde.2012.01.007</a>
  apa: Huff, J. T., &#38; Zilberman, D. (2012). Regulation of biological accuracy,
    precision, and memory by plant chromatin organization. <i>Current Opinion in Genetics
    and Development</i>. Elsevier. <a href="https://doi.org/10.1016/j.gde.2012.01.007">https://doi.org/10.1016/j.gde.2012.01.007</a>
  chicago: Huff, Jason T., and Daniel Zilberman. “Regulation of Biological Accuracy,
    Precision, and Memory by Plant Chromatin Organization.” <i>Current Opinion in
    Genetics and Development</i>. Elsevier, 2012. <a href="https://doi.org/10.1016/j.gde.2012.01.007">https://doi.org/10.1016/j.gde.2012.01.007</a>.
  ieee: J. T. Huff and D. Zilberman, “Regulation of biological accuracy, precision,
    and memory by plant chromatin organization,” <i>Current Opinion in Genetics and
    Development</i>, vol. 22, no. 2. Elsevier, pp. 132–138, 2012.
  ista: Huff JT, Zilberman D. 2012. Regulation of biological accuracy, precision,
    and memory by plant chromatin organization. Current Opinion in Genetics and Development.
    22(2), 132–138.
  mla: Huff, Jason T., and Daniel Zilberman. “Regulation of Biological Accuracy, Precision,
    and Memory by Plant Chromatin Organization.” <i>Current Opinion in Genetics and
    Development</i>, vol. 22, no. 2, Elsevier, 2012, pp. 132–38, doi:<a href="https://doi.org/10.1016/j.gde.2012.01.007">10.1016/j.gde.2012.01.007</a>.
  short: J.T. Huff, D. Zilberman, Current Opinion in Genetics and Development 22 (2012)
    132–138.
date_created: 2021-06-08T08:58:52Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2021-12-14T08:32:38Z
department:
- _id: DaZi
doi: 10.1016/j.gde.2012.01.007
extern: '1'
external_id:
  pmid:
  - '22336527'
intvolume: '        22'
issue: '2'
language:
- iso: eng
month: '04'
oa_version: None
page: 132-138
pmid: 1
publication: Current Opinion in Genetics and Development
publication_identifier:
  issn:
  - 0959-437X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Regulation of biological accuracy, precision, and memory by plant chromatin
  organization
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 22
year: '2012'
...
---
_id: '9535'
abstract:
- lang: eng
  text: The most well-studied function of DNA methylation in eukaryotic cells is the
    transcriptional silencing of genes and transposons. More recent results showed
    that many eukaryotes methylate the bodies of genes as well and that this methylation
    correlates with transcriptional activity rather than repression. The purpose of
    gene body methylation remains mysterious, but is potentially related to the histone
    variant H2A.Z. Studies in plants and animals have shown that the genome-wide distributions
    of H2A.Z and DNA methylation are strikingly anticorrelated. Furthermore, we and
    other investigators have shown that this relationship is likely to be the result
    of an ancient but unknown mechanism by which DNA methylation prevents the incorporation
    of H2A.Z. Recently, we discovered strong correlations between the presence of
    H2A.Z within gene bodies, the degree to which a gene's expression varies across
    tissue types or environmental conditions, and transcriptional misregulation in
    an h2a.z mutant. We propose that one basal function of gene body methylation is
    the establishment of constitutive expression patterns within housekeeping genes
    by excluding H2A.Z from their bodies.
article_processing_charge: No
article_type: review
author:
- first_name: D.
  full_name: Coleman-Derr, D.
  last_name: Coleman-Derr
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Coleman-Derr D, Zilberman D. DNA methylation, H2A.Z, and the regulation of
    constitutive expression. <i>Cold Spring Harbor Symposia on Quantitative Biology</i>.
    2012;77:147-154. doi:<a href="https://doi.org/10.1101/sqb.2012.77.014944">10.1101/sqb.2012.77.014944</a>
  apa: Coleman-Derr, D., &#38; Zilberman, D. (2012). DNA methylation, H2A.Z, and the
    regulation of constitutive expression. <i>Cold Spring Harbor Symposia on Quantitative
    Biology</i>. Cold Spring Harbor Laboratory Press. <a href="https://doi.org/10.1101/sqb.2012.77.014944">https://doi.org/10.1101/sqb.2012.77.014944</a>
  chicago: Coleman-Derr, D., and Daniel Zilberman. “DNA Methylation, H2A.Z, and the
    Regulation of Constitutive Expression.” <i>Cold Spring Harbor Symposia on Quantitative
    Biology</i>. Cold Spring Harbor Laboratory Press, 2012. <a href="https://doi.org/10.1101/sqb.2012.77.014944">https://doi.org/10.1101/sqb.2012.77.014944</a>.
  ieee: D. Coleman-Derr and D. Zilberman, “DNA methylation, H2A.Z, and the regulation
    of constitutive expression,” <i>Cold Spring Harbor Symposia on Quantitative Biology</i>,
    vol. 77. Cold Spring Harbor Laboratory Press, pp. 147–154, 2012.
  ista: Coleman-Derr D, Zilberman D. 2012. DNA methylation, H2A.Z, and the regulation
    of constitutive expression. Cold Spring Harbor Symposia on Quantitative Biology.
    77, 147–154.
  mla: Coleman-Derr, D., and Daniel Zilberman. “DNA Methylation, H2A.Z, and the Regulation
    of Constitutive Expression.” <i>Cold Spring Harbor Symposia on Quantitative Biology</i>,
    vol. 77, Cold Spring Harbor Laboratory Press, 2012, pp. 147–54, doi:<a href="https://doi.org/10.1101/sqb.2012.77.014944">10.1101/sqb.2012.77.014944</a>.
  short: D. Coleman-Derr, D. Zilberman, Cold Spring Harbor Symposia on Quantitative
    Biology 77 (2012) 147–154.
date_created: 2021-06-08T13:01:23Z
date_published: 2012-12-18T00:00:00Z
date_updated: 2021-12-14T08:33:09Z
day: '18'
department:
- _id: DaZi
doi: 10.1101/sqb.2012.77.014944
extern: '1'
external_id:
  pmid:
  - '23250988'
intvolume: '        77'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1101/sqb.2012.77.014944
month: '12'
oa: 1
oa_version: Published Version
page: 147-154
pmid: 1
publication: Cold Spring Harbor Symposia on Quantitative Biology
publication_identifier:
  eissn:
  - 1943-4456
  issn:
  - 0091-7451
publication_status: published
publisher: Cold Spring Harbor Laboratory Press
quality_controlled: '1'
scopus_import: '1'
status: public
title: DNA methylation, H2A.Z, and the regulation of constitutive expression
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 77
year: '2012'
...
---
_id: '9755'
abstract:
- lang: eng
  text: Due to the omnipresent risk of epidemics, insect societies have evolved sophisticated
    disease defences at the individual and colony level. An intriguing yet little
    understood phenomenon is that social contact to pathogen-exposed individuals reduces
    susceptibility of previously naive nestmates to this pathogen. We tested whether
    such social immunisation in Lasius ants against the entomopathogenic fungus Metarhizium
    anisopliae is based on active upregulation of the immune system of nestmates following
    contact to an infectious individual or passive protection via transfer of immune
    effectors among group members—that is, active versus passive immunisation. We
    found no evidence for involvement of passive immunisation via transfer of antimicrobials
    among colony members. Instead, intensive allogrooming behaviour between naive
    and pathogen-exposed ants before fungal conidia firmly attached to their cuticle
    suggested passage of the pathogen from the exposed individuals to their nestmates.
    By tracing fluorescence-labelled conidia we indeed detected frequent pathogen
    transfer to the nestmates, where they caused low-level infections as revealed
    by growth of small numbers of fungal colony forming units from their dissected
    body content. These infections rarely led to death, but instead promoted an enhanced
    ability to inhibit fungal growth and an active upregulation of immune genes involved
    in antifungal defences (defensin and prophenoloxidase, PPO). Contrarily, there
    was no upregulation of the gene cathepsin L, which is associated with antibacterial
    and antiviral defences, and we found no increased antibacterial activity of nestmates
    of fungus-exposed ants. This indicates that social immunisation after fungal exposure
    is specific, similar to recent findings for individual-level immune priming in
    invertebrates. Epidemiological modeling further suggests that active social immunisation
    is adaptive, as it leads to faster elimination of the disease and lower death
    rates than passive immunisation. Interestingly, humans have also utilised the
    protective effect of low-level infections to fight smallpox by intentional transfer
    of low pathogen doses (“variolation” or “inoculation”).
article_processing_charge: No
author:
- first_name: Matthias
  full_name: Konrad, Matthias
  id: 46528076-F248-11E8-B48F-1D18A9856A87
  last_name: Konrad
- first_name: Meghan
  full_name: Vyleta, Meghan
  id: 418901AA-F248-11E8-B48F-1D18A9856A87
  last_name: Vyleta
- first_name: Fabian
  full_name: Theis, Fabian
  last_name: Theis
- first_name: Miriam
  full_name: Stock, Miriam
  id: 42462816-F248-11E8-B48F-1D18A9856A87
  last_name: Stock
- first_name: Martina
  full_name: Klatt, Martina
  id: E60F29C6-E9AE-11E9-AF6E-D190C7302F38
  last_name: Klatt
- first_name: Verena
  full_name: Drescher, Verena
  last_name: Drescher
- first_name: Carsten
  full_name: Marr, Carsten
  last_name: Marr
- first_name: Line V
  full_name: Ugelvig, Line V
  id: 3DC97C8E-F248-11E8-B48F-1D18A9856A87
  last_name: Ugelvig
  orcid: 0000-0003-1832-8883
- first_name: Sylvia
  full_name: Cremer, Sylvia
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
citation:
  ama: 'Konrad M, Vyleta M, Theis F, et al. Data from: Social transfer of pathogenic
    fungus promotes active immunisation in ant colonies. 2012. doi:<a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>'
  apa: 'Konrad, M., Vyleta, M., Theis, F., Stock, M., Klatt, M., Drescher, V., … Cremer,
    S. (2012). Data from: Social transfer of pathogenic fungus promotes active immunisation
    in ant colonies. Dryad. <a href="https://doi.org/10.5061/dryad.sv37s">https://doi.org/10.5061/dryad.sv37s</a>'
  chicago: 'Konrad, Matthias, Meghan Vyleta, Fabian Theis, Miriam Stock, Martina Klatt,
    Verena Drescher, Carsten Marr, Line V Ugelvig, and Sylvia Cremer. “Data from:
    Social Transfer of Pathogenic Fungus Promotes Active Immunisation in Ant Colonies.”
    Dryad, 2012. <a href="https://doi.org/10.5061/dryad.sv37s">https://doi.org/10.5061/dryad.sv37s</a>.'
  ieee: 'M. Konrad <i>et al.</i>, “Data from: Social transfer of pathogenic fungus
    promotes active immunisation in ant colonies.” Dryad, 2012.'
  ista: 'Konrad M, Vyleta M, Theis F, Stock M, Klatt M, Drescher V, Marr C, Ugelvig
    LV, Cremer S. 2012. Data from: Social transfer of pathogenic fungus promotes active
    immunisation in ant colonies, Dryad, <a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>.'
  mla: 'Konrad, Matthias, et al. <i>Data from: Social Transfer of Pathogenic Fungus
    Promotes Active Immunisation in Ant Colonies</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.sv37s">10.5061/dryad.sv37s</a>.'
  short: M. Konrad, M. Vyleta, F. Theis, M. Stock, M. Klatt, V. Drescher, C. Marr,
    L.V. Ugelvig, S. Cremer, (2012).
date_created: 2021-07-30T08:39:13Z
date_published: 2012-09-27T00:00:00Z
date_updated: 2023-02-23T11:18:41Z
day: '27'
department:
- _id: SyCr
doi: 10.5061/dryad.sv37s
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.sv37s
month: '09'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '3242'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Social transfer of pathogenic fungus promotes active immunisation
  in ant colonies'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '9757'
abstract:
- lang: eng
  text: To fight infectious diseases, host immune defences are employed at multiple
    levels. Sanitary behaviour, such as pathogen avoidance and removal, acts as a
    first line of defence to prevent infection [1] before activation of the physiological
    immune system. Insect societies have evolved a wide range of collective hygiene
    measures and intensive health care towards pathogen-exposed group members [2].
    One of the most common behaviours is allogrooming, in which nestmates remove infectious
    particles from the body surfaces of exposed individuals [3]. Here we show that,
    in invasive garden ants, grooming of fungus-exposed brood is effective beyond
    the sheer mechanical removal of fungal conidiospores as it also includes chemical
    disinfection through the application of poison produced by the ants themselves.
    Formic acid is the main active component of the poison. It inhibits fungal growth
    of conidiospores remaining on the brood surface after grooming and also those
    collected in the mouth of the grooming ant. This dual function is achieved by
    uptake of the poison droplet into the mouth through acidopore self-grooming and
    subsequent application onto the infectious brood via brood grooming. This extraordinary
    behaviour extends current understanding of grooming and the establishment of social
    immunity in insect societies.
article_processing_charge: No
author:
- first_name: Simon
  full_name: Tragust, Simon
  id: 35A7A418-F248-11E8-B48F-1D18A9856A87
  last_name: Tragust
- first_name: Barbara
  full_name: Mitteregger, Barbara
  id: 479DDAAC-E9CD-11E9-9B5F-82450873F7A1
  last_name: Mitteregger
- first_name: Vanessa
  full_name: Barone, Vanessa
  id: 419EECCC-F248-11E8-B48F-1D18A9856A87
  last_name: Barone
  orcid: 0000-0003-2676-3367
- first_name: Matthias
  full_name: Konrad, Matthias
  id: 46528076-F248-11E8-B48F-1D18A9856A87
  last_name: Konrad
- first_name: Line V
  full_name: Ugelvig, Line V
  id: 3DC97C8E-F248-11E8-B48F-1D18A9856A87
  last_name: Ugelvig
  orcid: 0000-0003-1832-8883
- first_name: Sylvia
  full_name: Cremer, Sylvia
  id: 2F64EC8C-F248-11E8-B48F-1D18A9856A87
  last_name: Cremer
  orcid: 0000-0002-2193-3868
citation:
  ama: 'Tragust S, Mitteregger B, Barone V, Konrad M, Ugelvig LV, Cremer S. Data from:
    Ants disinfect fungus-exposed brood by oral uptake and spread of their poison.
    2012. doi:<a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>'
  apa: 'Tragust, S., Mitteregger, B., Barone, V., Konrad, M., Ugelvig, L. V., &#38;
    Cremer, S. (2012). Data from: Ants disinfect fungus-exposed brood by oral uptake
    and spread of their poison. Dryad. <a href="https://doi.org/10.5061/dryad.61649">https://doi.org/10.5061/dryad.61649</a>'
  chicago: 'Tragust, Simon, Barbara Mitteregger, Vanessa Barone, Matthias Konrad,
    Line V Ugelvig, and Sylvia Cremer. “Data from: Ants Disinfect Fungus-Exposed Brood
    by Oral Uptake and Spread of Their Poison.” Dryad, 2012. <a href="https://doi.org/10.5061/dryad.61649">https://doi.org/10.5061/dryad.61649</a>.'
  ieee: 'S. Tragust, B. Mitteregger, V. Barone, M. Konrad, L. V. Ugelvig, and S. Cremer,
    “Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of their
    poison.” Dryad, 2012.'
  ista: 'Tragust S, Mitteregger B, Barone V, Konrad M, Ugelvig LV, Cremer S. 2012.
    Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of their
    poison, Dryad, <a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>.'
  mla: 'Tragust, Simon, et al. <i>Data from: Ants Disinfect Fungus-Exposed Brood by
    Oral Uptake and Spread of Their Poison</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.61649">10.5061/dryad.61649</a>.'
  short: S. Tragust, B. Mitteregger, V. Barone, M. Konrad, L.V. Ugelvig, S. Cremer,
    (2012).
date_created: 2021-07-30T12:31:31Z
date_published: 2012-12-14T00:00:00Z
date_updated: 2023-02-23T11:04:28Z
day: '14'
department:
- _id: SyCr
doi: 10.5061/dryad.61649
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.61649
month: '12'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2926'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Ants disinfect fungus-exposed brood by oral uptake and spread of
  their poison'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '9758'
abstract:
- lang: eng
  text: 'We propose a two-step procedure for estimating multiple migration rates in
    an approximate Bayesian computation (ABC) framework, accounting for global nuisance
    parameters. The approach is not limited to migration, but generally of interest
    for inference problems with multiple parameters and a modular structure (e.g.
    independent sets of demes or loci). We condition on a known, but complex demographic
    model of a spatially subdivided population, motivated by the reintroduction of
    Alpine ibex (Capra ibex) into Switzerland. In the first step, the global parameters
    ancestral mutation rate and male mating skew have been estimated for the whole
    population in Aeschbacher et al. (Genetics 2012; 192: 1027). In the second step,
    we estimate in this study the migration rates independently for clusters of demes
    putatively connected by migration. For large clusters (many migration rates),
    ABC faces the problem of too many summary statistics. We therefore assess by simulation
    if estimation per pair of demes is a valid alternative. We find that the trade-off
    between reduced dimensionality for the pairwise estimation on the one hand and
    lower accuracy due to the assumption of pairwise independence on the other depends
    on the number of migration rates to be inferred: the accuracy of the pairwise
    approach increases with the number of parameters, relative to the joint estimation
    approach. To distinguish between low and zero migration, we perform ABC-type model
    comparison between a model with migration and one without. Applying the approach
    to microsatellite data from Alpine ibex, we find no evidence for substantial gene
    flow via migration, except for one pair of demes in one direction.'
article_processing_charge: No
author:
- first_name: Simon
  full_name: Aeschbacher, Simon
  id: 2D35326E-F248-11E8-B48F-1D18A9856A87
  last_name: Aeschbacher
- first_name: Andreas
  full_name: Futschik, Andreas
  last_name: Futschik
- first_name: Mark
  full_name: Beaumont, Mark
  last_name: Beaumont
citation:
  ama: 'Aeschbacher S, Futschik A, Beaumont M. Data from: Approximate Bayesian computation
    for modular inference problems with many parameters: the example of migration
    rates. 2012. doi:<a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>'
  apa: 'Aeschbacher, S., Futschik, A., &#38; Beaumont, M. (2012). Data from: Approximate
    Bayesian computation for modular inference problems with many parameters: the
    example of migration rates. Dryad. <a href="https://doi.org/10.5061/dryad.274b1">https://doi.org/10.5061/dryad.274b1</a>'
  chicago: 'Aeschbacher, Simon, Andreas Futschik, and Mark Beaumont. “Data from: Approximate
    Bayesian Computation for Modular Inference Problems with Many Parameters: The
    Example of Migration Rates.” Dryad, 2012. <a href="https://doi.org/10.5061/dryad.274b1">https://doi.org/10.5061/dryad.274b1</a>.'
  ieee: 'S. Aeschbacher, A. Futschik, and M. Beaumont, “Data from: Approximate Bayesian
    computation for modular inference problems with many parameters: the example of
    migration rates.” Dryad, 2012.'
  ista: 'Aeschbacher S, Futschik A, Beaumont M. 2012. Data from: Approximate Bayesian
    computation for modular inference problems with many parameters: the example of
    migration rates, Dryad, <a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>.'
  mla: 'Aeschbacher, Simon, et al. <i>Data from: Approximate Bayesian Computation
    for Modular Inference Problems with Many Parameters: The Example of Migration
    Rates</i>. Dryad, 2012, doi:<a href="https://doi.org/10.5061/dryad.274b1">10.5061/dryad.274b1</a>.'
  short: S. Aeschbacher, A. Futschik, M. Beaumont, (2012).
date_created: 2021-07-30T12:36:39Z
date_published: 2012-11-14T00:00:00Z
date_updated: 2023-02-23T11:05:19Z
day: '14'
department:
- _id: NiBa
doi: 10.5061/dryad.274b1
main_file_link:
- open_access: '1'
  url: https://doi.org/10.5061/dryad.274b1
month: '11'
oa: 1
oa_version: Published Version
publisher: Dryad
related_material:
  record:
  - id: '2944'
    relation: used_in_publication
    status: public
status: public
title: 'Data from: Approximate Bayesian computation for modular inference problems
  with many parameters: the example of migration rates'
type: research_data_reference
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2012'
...
---
_id: '10896'
abstract:
- lang: eng
  text: Under physiological conditions the brain, via the purine salvage pathway,
    reuses the preformed purine bases hypoxanthine, derived from ATP degradation,
    and adenine (Ade), derived from polyamine synthesis, to restore its ATP pool.
    However, the massive degradation of ATP during ischemia, although providing valuable
    neuroprotective adenosine, results in the accumulation and loss of diffusible
    purine metabolites and thereby leads to a protracted reduction in the post-ischemic
    ATP pool size. In vivo, this may both limit the ability to deploy ATP-dependent
    reparative mechanisms and reduce the subsequent availability of adenosine, whilst
    in brain slices results in tissue with substantially lower levels of ATP than
    in vivo. In the present review, we describe the mechanisms by which brain tissue
    replenishes its ATP, how this can be improved with the clinically tolerated chemicals
    D-ribose and adenine, and the functional, and potential therapeutic, implications
    of doing so.
acknowledgement: We are grateful to Research into Ageing/Ageing UK and The Dunhill
  Trust for funding SzN’s graduate studies, and to Prof Nicholas Dale for his valuable
  input.
article_processing_charge: No
author:
- first_name: Stephanie
  full_name: zur Nedden, Stephanie
  id: 3C77F464-F248-11E8-B48F-1D18A9856A87
  last_name: zur Nedden
- first_name: Alexander S.
  full_name: Doney, Alexander S.
  last_name: Doney
- first_name: Bruno G.
  full_name: Frenguelli, Bruno G.
  last_name: Frenguelli
citation:
  ama: 'zur Nedden S, Doney AS, Frenguelli BG. The double-edged sword: Gaining Adenosine
    at the expense of ATP. How to balance the books. In: Masino S, Boison D, eds.
    <i>Adenosine</i>. 1st ed. New York: Springer; 2012:109-129. doi:<a href="https://doi.org/10.1007/978-1-4614-3903-5_6">10.1007/978-1-4614-3903-5_6</a>'
  apa: 'zur Nedden, S., Doney, A. S., &#38; Frenguelli, B. G. (2012). The double-edged
    sword: Gaining Adenosine at the expense of ATP. How to balance the books. In S.
    Masino &#38; D. Boison (Eds.), <i>Adenosine</i> (1st ed., pp. 109–129). New York:
    Springer. <a href="https://doi.org/10.1007/978-1-4614-3903-5_6">https://doi.org/10.1007/978-1-4614-3903-5_6</a>'
  chicago: 'Nedden, Stephanie zur, Alexander S. Doney, and Bruno G. Frenguelli. “The
    Double-Edged Sword: Gaining Adenosine at the Expense of ATP. How to Balance the
    Books.” In <i>Adenosine</i>, edited by Susan Masino and Detlev Boison, 1st ed.,
    109–29. New York: Springer, 2012. <a href="https://doi.org/10.1007/978-1-4614-3903-5_6">https://doi.org/10.1007/978-1-4614-3903-5_6</a>.'
  ieee: 'S. zur Nedden, A. S. Doney, and B. G. Frenguelli, “The double-edged sword:
    Gaining Adenosine at the expense of ATP. How to balance the books,” in <i>Adenosine</i>,
    1st ed., S. Masino and D. Boison, Eds. New York: Springer, 2012, pp. 109–129.'
  ista: 'zur Nedden S, Doney AS, Frenguelli BG. 2012.The double-edged sword: Gaining
    Adenosine at the expense of ATP. How to balance the books. In: Adenosine. , 109–129.'
  mla: 'zur Nedden, Stephanie, et al. “The Double-Edged Sword: Gaining Adenosine at
    the Expense of ATP. How to Balance the Books.” <i>Adenosine</i>, edited by Susan
    Masino and Detlev Boison, 1st ed., Springer, 2012, pp. 109–29, doi:<a href="https://doi.org/10.1007/978-1-4614-3903-5_6">10.1007/978-1-4614-3903-5_6</a>.'
  short: S. zur Nedden, A.S. Doney, B.G. Frenguelli, in:, S. Masino, D. Boison (Eds.),
    Adenosine, 1st ed., Springer, New York, 2012, pp. 109–129.
date_created: 2022-03-21T07:16:12Z
date_published: 2012-07-23T00:00:00Z
date_updated: 2022-06-21T11:51:58Z
day: '23'
department:
- _id: HaJa
doi: 10.1007/978-1-4614-3903-5_6
edition: '1'
editor:
- first_name: Susan
  full_name: Masino, Susan
  last_name: Masino
- first_name: Detlev
  full_name: Boison, Detlev
  last_name: Boison
language:
- iso: eng
month: '07'
oa_version: None
page: 109-129
place: New York
publication: Adenosine
publication_identifier:
  eisbn:
  - '9781461439035'
  isbn:
  - '9781461439028'
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The double-edged sword: Gaining Adenosine at the expense of ATP. How to balance
  the books'
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
---
_id: '10903'
abstract:
- lang: eng
  text: We propose a logic-based framework for automated reasoning about sequential
    programs manipulating singly-linked lists and arrays with unbounded data. We introduce
    the logic SLAD, which allows combining shape constraints, written in a fragment
    of Separation Logic, with data and size constraints. We address the problem of
    checking the entailment between SLAD formulas, which is crucial in performing
    pre-post condition reasoning. Although this problem is undecidable in general
    for SLAD, we propose a sound and powerful procedure that is able to solve this
    problem for a large class of formulas, beyond the capabilities of existing techniques
    and tools. We prove that this procedure is complete, i.e., it is actually a decision
    procedure for this problem, for an important fragment of SLAD including known
    decidable logics. We implemented this procedure and shown its preciseness and
    its efficiency on a significant benchmark of formulas.
acknowledgement: This work has been partially supported by the French ANR project
  Veridyc
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Ahmed
  full_name: Bouajjani, Ahmed
  last_name: Bouajjani
- first_name: Cezara
  full_name: Dragoi, Cezara
  id: 2B2B5ED0-F248-11E8-B48F-1D18A9856A87
  last_name: Dragoi
- first_name: Constantin
  full_name: Enea, Constantin
  last_name: Enea
- first_name: Mihaela
  full_name: Sighireanu, Mihaela
  last_name: Sighireanu
citation:
  ama: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. Accurate invariant checking for
    programs manipulating lists and arrays with infinite data. In: <i>Automated Technology
    for Verification and Analysis</i>. Vol 7561. LNCS. Berlin, Heidelberg: Springer;
    2012:167-182. doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>'
  apa: 'Bouajjani, A., Dragoi, C., Enea, C., &#38; Sighireanu, M. (2012). Accurate
    invariant checking for programs manipulating lists and arrays with infinite data.
    In <i>Automated Technology for Verification and Analysis</i> (Vol. 7561, pp. 167–182).
    Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>'
  chicago: 'Bouajjani, Ahmed, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu.
    “Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite
    Data.” In <i>Automated Technology for Verification and Analysis</i>, 7561:167–82.
    LNCS. Berlin, Heidelberg: Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33386-6_14">https://doi.org/10.1007/978-3-642-33386-6_14</a>.'
  ieee: A. Bouajjani, C. Dragoi, C. Enea, and M. Sighireanu, “Accurate invariant checking
    for programs manipulating lists and arrays with infinite data,” in <i>Automated
    Technology for Verification and Analysis</i>, Thiruvananthapuram, India, 2012,
    vol. 7561, pp. 167–182.
  ista: 'Bouajjani A, Dragoi C, Enea C, Sighireanu M. 2012. Accurate invariant checking
    for programs manipulating lists and arrays with infinite data. Automated Technology
    for Verification and Analysis. ATVA: Automated Technology for Verification and
    AnalysisLNCS, LNCS, vol. 7561, 167–182.'
  mla: Bouajjani, Ahmed, et al. “Accurate Invariant Checking for Programs Manipulating
    Lists and Arrays with Infinite Data.” <i>Automated Technology for Verification
    and Analysis</i>, vol. 7561, Springer, 2012, pp. 167–82, doi:<a href="https://doi.org/10.1007/978-3-642-33386-6_14">10.1007/978-3-642-33386-6_14</a>.
  short: A. Bouajjani, C. Dragoi, C. Enea, M. Sighireanu, in:, Automated Technology
    for Verification and Analysis, Springer, Berlin, Heidelberg, 2012, pp. 167–182.
conference:
  end_date: 2012-10-06
  location: Thiruvananthapuram, India
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2012-10-03
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2023-09-05T14:07:24Z
day: '15'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33386-6_14
intvolume: '      7561'
language:
- iso: eng
month: '10'
oa_version: None
page: 167-182
place: Berlin, Heidelberg
publication: Automated Technology for Verification and Analysis
publication_identifier:
  eisbn:
  - '9783642333866'
  eissn:
  - 1611-3349
  isbn:
  - '9783642333859'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Accurate invariant checking for programs manipulating lists and arrays with
  infinite data
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7561
year: '2012'
...
---
_id: '10904'
abstract:
- lang: eng
  text: Multi-dimensional mean-payoff and energy games provide the mathematical foundation
    for the quantitative study of reactive systems, and play a central role in the
    emerging quantitative theory of verification and synthesis. In this work, we study
    the strategy synthesis problem for games with such multi-dimensional objectives
    along with a parity condition, a canonical way to express ω-regular conditions.
    While in general, the winning strategies in such games may require infinite memory,
    for synthesis the most relevant problem is the construction of a finite-memory
    winning strategy (if one exists). Our main contributions are as follows. First,
    we show a tight exponential bound (matching upper and lower bounds) on the memory
    required for finite-memory winning strategies in both multi-dimensional mean-payoff
    and energy games along with parity objectives. This significantly improves the
    triple exponential upper bound for multi energy games (without parity) that could
    be derived from results in literature for games on VASS (vector addition systems
    with states). Second, we present an optimal symbolic and incremental algorithm
    to compute a finite-memory winning strategy (if one exists) in such games. Finally,
    we give a complete characterization of when finite memory of strategies can be
    traded off for randomness. In particular, we show that for one-dimension mean-payoff
    parity games, randomized memoryless strategies are as powerful as their pure finite-memory
    counterparts.
acknowledgement: 'Author supported by Austrian Science Fund (FWF) Grant No P 23499-N23,
  FWF NFN Grant No S11407 (RiSE), ERC Start Grant (279307: Graph Games), Microsoft
  faculty fellowship.'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Mickael
  full_name: Randour, Mickael
  last_name: Randour
- first_name: Jean-François
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: 'Chatterjee K, Randour M, Raskin J-F. Strategy synthesis for multi-dimensional
    quantitative objectives. In: Koutny M, Ulidowski I, eds. <i>CONCUR 2012 - Concurrency
    Theory</i>. Vol 7454. Berlin, Heidelberg: Springer; 2012:115-131. doi:<a href="https://doi.org/10.1007/978-3-642-32940-1_10">10.1007/978-3-642-32940-1_10</a>'
  apa: 'Chatterjee, K., Randour, M., &#38; Raskin, J.-F. (2012). Strategy synthesis
    for multi-dimensional quantitative objectives. In M. Koutny &#38; I. Ulidowski
    (Eds.), <i>CONCUR 2012 - Concurrency Theory</i> (Vol. 7454, pp. 115–131). Berlin,
    Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-32940-1_10">https://doi.org/10.1007/978-3-642-32940-1_10</a>'
  chicago: 'Chatterjee, Krishnendu, Mickael Randour, and Jean-François Raskin. “Strategy
    Synthesis for Multi-Dimensional Quantitative Objectives.” In <i>CONCUR 2012 -
    Concurrency Theory</i>, edited by Maciej Koutny and Irek Ulidowski, 7454:115–31.
    Berlin, Heidelberg: Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-32940-1_10">https://doi.org/10.1007/978-3-642-32940-1_10</a>.'
  ieee: K. Chatterjee, M. Randour, and J.-F. Raskin, “Strategy synthesis for multi-dimensional
    quantitative objectives,” in <i>CONCUR 2012 - Concurrency Theory</i>, Newcastle
    upon Tyne, United Kingdom, 2012, vol. 7454, pp. 115–131.
  ista: 'Chatterjee K, Randour M, Raskin J-F. 2012. Strategy synthesis for multi-dimensional
    quantitative objectives. CONCUR 2012 - Concurrency Theory. CONCUR: Conference
    on Concurrency Theory, LNCS, vol. 7454, 115–131.'
  mla: Chatterjee, Krishnendu, et al. “Strategy Synthesis for Multi-Dimensional Quantitative
    Objectives.” <i>CONCUR 2012 - Concurrency Theory</i>, edited by Maciej Koutny
    and Irek Ulidowski, vol. 7454, Springer, 2012, pp. 115–31, doi:<a href="https://doi.org/10.1007/978-3-642-32940-1_10">10.1007/978-3-642-32940-1_10</a>.
  short: K. Chatterjee, M. Randour, J.-F. Raskin, in:, M. Koutny, I. Ulidowski (Eds.),
    CONCUR 2012 - Concurrency Theory, Springer, Berlin, Heidelberg, 2012, pp. 115–131.
conference:
  end_date: 2012-09-07
  location: Newcastle upon Tyne, United Kingdom
  name: 'CONCUR: Conference on Concurrency Theory'
  start_date: 2012-09-04
date_created: 2022-03-21T08:00:21Z
date_published: 2012-09-15T00:00:00Z
date_updated: 2023-02-23T10:55:06Z
day: '15'
department:
- _id: KrCh
doi: 10.1007/978-3-642-32940-1_10
ec_funded: 1
editor:
- first_name: Maciej
  full_name: Koutny, Maciej
  last_name: Koutny
- first_name: Irek
  full_name: Ulidowski, Irek
  last_name: Ulidowski
external_id:
  arxiv:
  - '1201.5073'
intvolume: '      7454'
language:
- iso: eng
month: '09'
oa_version: Preprint
page: 115-131
place: Berlin, Heidelberg
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: CONCUR 2012 - Concurrency Theory
publication_identifier:
  eisbn:
  - '9783642329401'
  isbn:
  - '9783642329395'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
  record:
  - id: '2716'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Strategy synthesis for multi-dimensional quantitative objectives
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7454
year: '2012'
...
---
_id: '10905'
abstract:
- lang: eng
  text: "Energy games belong to a class of turn-based two-player infinite-duration
    games played on a weighted directed graph. It is one of the rare and intriguing
    combinatorial problems that lie in NP ∩ co−NP, but are not known to be in P. While
    the existence of polynomial-time algorithms has been a major open problem for
    decades, there is no algorithm that solves any non-trivial subclass in polynomial
    time.\r\nIn this paper, we give several results based on the weight structures
    of the graph. First, we identify a notion of penalty and present a polynomial-time
    algorithm when the penalty is large. Our algorithm is the first polynomial-time
    algorithm on a large class of weighted graphs. It includes several counter examples
    that show that many previous algorithms, such as value iteration and random facet
    algorithms, require at least sub-exponential time. Our main technique is developing
    the first non-trivial approximation algorithm and showing how to convert it to
    an exact algorithm. Moreover, we show that in a practical case in verification
    where weights are clustered around a constant number of values, the energy game
    problem can be solved in polynomial time. We also show that the problem is still
    as hard as in general when the clique-width is bounded or the graph is strongly
    ergodic, suggesting that restricting graph structures need not help."
acknowledgement: 'Supported by the Austrian Science Fund (FWF): P23499-N23, the Austrian
  Science Fund (FWF): S11407-N23 (RiSE), an ERC Start Grant (279307: Graph Games),
  and a Microsoft Faculty Fellows Award'
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Sebastian
  full_name: Krinninger, Sebastian
  last_name: Krinninger
- first_name: Danupon
  full_name: Nanongkai, Danupon
  last_name: Nanongkai
citation:
  ama: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. Polynomial-time algorithms
    for energy games with special weight structures. In: <i>Algorithms – ESA 2012</i>.
    Vol 7501. Springer; 2012:301-312. doi:<a href="https://doi.org/10.1007/978-3-642-33090-2_27">10.1007/978-3-642-33090-2_27</a>'
  apa: 'Chatterjee, K., Henzinger, M. H., Krinninger, S., &#38; Nanongkai, D. (2012).
    Polynomial-time algorithms for energy games with special weight structures. In
    <i>Algorithms – ESA 2012</i> (Vol. 7501, pp. 301–312). Ljubljana, Slovenia: Springer.
    <a href="https://doi.org/10.1007/978-3-642-33090-2_27">https://doi.org/10.1007/978-3-642-33090-2_27</a>'
  chicago: Chatterjee, Krishnendu, Monika H Henzinger, Sebastian Krinninger, and Danupon
    Nanongkai. “Polynomial-Time Algorithms for Energy Games with Special Weight Structures.”
    In <i>Algorithms – ESA 2012</i>, 7501:301–12. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33090-2_27">https://doi.org/10.1007/978-3-642-33090-2_27</a>.
  ieee: K. Chatterjee, M. H. Henzinger, S. Krinninger, and D. Nanongkai, “Polynomial-time
    algorithms for energy games with special weight structures,” in <i>Algorithms
    – ESA 2012</i>, Ljubljana, Slovenia, 2012, vol. 7501, pp. 301–312.
  ista: 'Chatterjee K, Henzinger MH, Krinninger S, Nanongkai D. 2012. Polynomial-time
    algorithms for energy games with special weight structures. Algorithms – ESA 2012.
    ESA: European Symposium on Algorithms, LNCS, vol. 7501, 301–312.'
  mla: Chatterjee, Krishnendu, et al. “Polynomial-Time Algorithms for Energy Games
    with Special Weight Structures.” <i>Algorithms – ESA 2012</i>, vol. 7501, Springer,
    2012, pp. 301–12, doi:<a href="https://doi.org/10.1007/978-3-642-33090-2_27">10.1007/978-3-642-33090-2_27</a>.
  short: K. Chatterjee, M.H. Henzinger, S. Krinninger, D. Nanongkai, in:, Algorithms
    – ESA 2012, Springer, 2012, pp. 301–312.
conference:
  end_date: 2012-09-12
  location: Ljubljana, Slovenia
  name: 'ESA: European Symposium on Algorithms'
  start_date: 2012-09-10
date_created: 2022-03-21T08:01:45Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2023-09-05T14:09:30Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-33090-2_27
ec_funded: 1
external_id:
  arxiv:
  - '1604.08234'
intvolume: '      7501'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1604.08234
month: '10'
oa: 1
oa_version: Preprint
page: 301-312
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Algorithms – ESA 2012
publication_identifier:
  eisbn:
  - '9783642330902'
  eissn:
  - 1611-3349
  isbn:
  - '9783642330896'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
related_material:
  record:
  - id: '535'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Polynomial-time algorithms for energy games with special weight structures
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7501
year: '2012'
...
---
_id: '10906'
abstract:
- lang: eng
  text: HSF(C) is a tool that automates verification of safety and liveness properties
    for C programs. This paper describes the verification approach taken by HSF(C)
    and provides instructions on how to install and use the tool.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergey
  full_name: Grebenshchikov, Sergey
  last_name: Grebenshchikov
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Nuno P.
  full_name: Lopes, Nuno P.
  last_name: Lopes
- first_name: Corneliu
  full_name: Popeea, Corneliu
  last_name: Popeea
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
citation:
  ama: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. HSF(C): A software
    verifier based on Horn clauses. In: Flanagan C, König B, eds. <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>. Vol 7214. LNCS. Berlin, Heidelberg:
    Springer; 2012:549-551. doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>'
  apa: 'Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C., &#38; Rybalchenko,
    A. (2012). HSF(C): A software verifier based on Horn clauses. In C. Flanagan &#38;
    B. König (Eds.), <i>Tools and Algorithms for the Construction and Analysis of
    Systems</i> (Vol. 7214, pp. 549–551). Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>'
  chicago: 'Grebenshchikov, Sergey, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea,
    and Andrey Rybalchenko. “HSF(C): A Software Verifier Based on Horn Clauses.” In
    <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, edited
    by Cormac Flanagan and Barbara König, 7214:549–51. LNCS. Berlin, Heidelberg: Springer,
    2012. <a href="https://doi.org/10.1007/978-3-642-28756-5_46">https://doi.org/10.1007/978-3-642-28756-5_46</a>.'
  ieee: 'S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko,
    “HSF(C): A software verifier based on Horn clauses,” in <i>Tools and Algorithms
    for the Construction and Analysis of Systems</i>, Tallinn, Estonia, 2012, vol.
    7214, pp. 549–551.'
  ista: 'Grebenshchikov S, Gupta A, Lopes NP, Popeea C, Rybalchenko A. 2012. HSF(C):
    A software verifier based on Horn clauses. Tools and Algorithms for the Construction
    and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and
    Analysis of SystemsLNCS, LNCS, vol. 7214, 549–551.'
  mla: 'Grebenshchikov, Sergey, et al. “HSF(C): A Software Verifier Based on Horn
    Clauses.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>,
    edited by Cormac Flanagan and Barbara König, vol. 7214, Springer, 2012, pp. 549–51,
    doi:<a href="https://doi.org/10.1007/978-3-642-28756-5_46">10.1007/978-3-642-28756-5_46</a>.'
  short: S. Grebenshchikov, A. Gupta, N.P. Lopes, C. Popeea, A. Rybalchenko, in:,
    C. Flanagan, B. König (Eds.), Tools and Algorithms for the Construction and Analysis
    of Systems, Springer, Berlin, Heidelberg, 2012, pp. 549–551.
conference:
  end_date: 2012-04-01
  location: Tallinn, Estonia
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2012-03-24
date_created: 2022-03-21T08:03:30Z
date_published: 2012-04-01T00:00:00Z
date_updated: 2023-09-05T14:09:54Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-28756-5_46
editor:
- first_name: Cormac
  full_name: Flanagan, Cormac
  last_name: Flanagan
- first_name: Barbara
  full_name: König, Barbara
  last_name: König
intvolume: '      7214'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/978-3-642-28756-5_46
month: '04'
oa: 1
oa_version: Published Version
page: 549-551
place: Berlin, Heidelberg
publication: Tools and Algorithms for the Construction and Analysis of Systems
publication_identifier:
  eisbn:
  - '9783642287565'
  eissn:
  - 1611-3349
  isbn:
  - '9783642287558'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'HSF(C): A software verifier based on Horn clauses'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 7214
year: '2012'
...
---
_id: '2263'
abstract:
- lang: eng
  text: Nestin-cre transgenic mice have been widely used to direct recombination to
    neural stem cells (NSCs) and intermediate neural progenitor cells (NPCs). Here
    we report that a readily utilized, and the only commercially available, Nestin-cre
    line is insufficient for directing recombination in early embryonic NSCs and NPCs.
    Analysis of recombination efficiency in multiple cre-dependent reporters and a
    genetic mosaic line revealed consistent temporal and spatial patterns of recombination
    in NSCs and NPCs. For comparison we utilized a knock-in Emx1cre line and found
    robust recombination in NSCs and NPCs in ventricular and subventricular zones
    of the cerebral cortices as early as embryonic day 12.5. In addition we found
    that the rate of Nestin-cre driven recombination only reaches sufficiently high
    levels in NSCs and NPCs during late embryonic and early postnatal periods. These
    findings are important when commercially available cre lines are considered for
    directing recombination to embryonic NSCs and NPCs.
author:
- first_name: Huixuan
  full_name: Liang, Huixuan
  last_name: Liang
- first_name: Simon
  full_name: Hippenmeyer, Simon
  id: 37B36620-F248-11E8-B48F-1D18A9856A87
  last_name: Hippenmeyer
  orcid: 0000-0003-2279-1061
- first_name: H.
  full_name: Ghashghaei, H.
  last_name: Ghashghaei
citation:
  ama: Liang H, Hippenmeyer S, Ghashghaei H. A Nestin-cre transgenic mouse is insufficient
    for recombination in early embryonic neural progenitors. <i>Biology open</i>.
    2012;1(12):1200-1203. doi:<a href="https://doi.org/10.1242/bio.20122287">10.1242/bio.20122287</a>
  apa: Liang, H., Hippenmeyer, S., &#38; Ghashghaei, H. (2012). A Nestin-cre transgenic
    mouse is insufficient for recombination in early embryonic neural progenitors.
    <i>Biology Open</i>. The Company of Biologists. <a href="https://doi.org/10.1242/bio.20122287">https://doi.org/10.1242/bio.20122287</a>
  chicago: Liang, Huixuan, Simon Hippenmeyer, and H. Ghashghaei. “A Nestin-Cre Transgenic
    Mouse Is Insufficient for Recombination in Early Embryonic Neural Progenitors.”
    <i>Biology Open</i>. The Company of Biologists, 2012. <a href="https://doi.org/10.1242/bio.20122287">https://doi.org/10.1242/bio.20122287</a>.
  ieee: H. Liang, S. Hippenmeyer, and H. Ghashghaei, “A Nestin-cre transgenic mouse
    is insufficient for recombination in early embryonic neural progenitors,” <i>Biology
    open</i>, vol. 1, no. 12. The Company of Biologists, pp. 1200–1203, 2012.
  ista: Liang H, Hippenmeyer S, Ghashghaei H. 2012. A Nestin-cre transgenic mouse
    is insufficient for recombination in early embryonic neural progenitors. Biology
    open. 1(12), 1200–1203.
  mla: Liang, Huixuan, et al. “A Nestin-Cre Transgenic Mouse Is Insufficient for Recombination
    in Early Embryonic Neural Progenitors.” <i>Biology Open</i>, vol. 1, no. 12, The
    Company of Biologists, 2012, pp. 1200–03, doi:<a href="https://doi.org/10.1242/bio.20122287">10.1242/bio.20122287</a>.
  short: H. Liang, S. Hippenmeyer, H. Ghashghaei, Biology Open 1 (2012) 1200–1203.
date_created: 2018-12-11T11:56:38Z
date_published: 2012-12-15T00:00:00Z
date_updated: 2021-01-12T06:56:23Z
day: '15'
ddc:
- '576'
department:
- _id: SiHi
doi: 10.1242/bio.20122287
file:
- access_level: open_access
  checksum: 605a1800b81227848c361fd6ba7d22ba
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:09Z
  date_updated: 2020-07-14T12:45:35Z
  file_id: '4990'
  file_name: IST-2015-387-v1+1_1200.full.pdf
  file_size: 726695
  relation: main_file
file_date_updated: 2020-07-14T12:45:35Z
has_accepted_license: '1'
intvolume: '         1'
issue: '12'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-sa/4.0/
month: '12'
oa: 1
oa_version: Published Version
page: 1200 - 1203
publication: Biology open
publication_status: published
publisher: The Company of Biologists
publist_id: '4682'
pubrep_id: '387'
quality_controlled: '1'
scopus_import: 1
status: public
title: A Nestin-cre transgenic mouse is insufficient for recombination in early embryonic
  neural progenitors
tmp:
  image: /images/cc_by_nc_sa.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International (CC
    BY-NC-SA 4.0)
  short: CC BY-NC-SA (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 1
year: '2012'
...
---
_id: '2302'
abstract:
- lang: eng
  text: 'We introduce propagation models (PMs), a formalism able to express several
    kinds of equations that describe the behavior of biochemical reaction networks.
    Furthermore, we introduce the propagation abstract data type (PADT), which separates
    concerns regarding different numerical algorithms for the transient analysis of
    biochemical reaction networks from concerns regarding their implementation, thus
    allowing for portable and efficient solutions. The state of a propagation abstract
    data type is given by a vector that assigns mass values to a set of nodes, and
    its (next) operator propagates mass values through this set of nodes. We propose
    an approximate implementation of the (next) operator, based on threshold abstraction,
    which propagates only &quot;significant&quot; mass values and thus achieves a
    compromise between efficiency and accuracy. Finally, we give three use cases for
    propagation models: the chemical master equation (CME), the reaction rate equation
    (RRE), and a hybrid method that combines these two equations. These three applications
    use propagation models in order to propagate probabilities and/or expected values
    and variances of the model''s variables.'
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Maria
  full_name: Mateescu, Maria
  id: 3B43276C-F248-11E8-B48F-1D18A9856A87
  last_name: Mateescu
citation:
  ama: Henzinger TA, Mateescu M. The propagation approach for computing biochemical
    reaction networks. <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>.
    2012;10(2):310-322. doi:<a href="https://doi.org/10.1109/TCBB.2012.91">10.1109/TCBB.2012.91</a>
  apa: Henzinger, T. A., &#38; Mateescu, M. (2012). The propagation approach for computing
    biochemical reaction networks. <i>IEEE ACM Transactions on Computational Biology
    and Bioinformatics</i>. IEEE. <a href="https://doi.org/10.1109/TCBB.2012.91">https://doi.org/10.1109/TCBB.2012.91</a>
  chicago: Henzinger, Thomas A, and Maria Mateescu. “The Propagation Approach for
    Computing Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational
    Biology and Bioinformatics</i>. IEEE, 2012. <a href="https://doi.org/10.1109/TCBB.2012.91">https://doi.org/10.1109/TCBB.2012.91</a>.
  ieee: T. A. Henzinger and M. Mateescu, “The propagation approach for computing biochemical
    reaction networks,” <i>IEEE ACM Transactions on Computational Biology and Bioinformatics</i>,
    vol. 10, no. 2. IEEE, pp. 310–322, 2012.
  ista: Henzinger TA, Mateescu M. 2012. The propagation approach for computing biochemical
    reaction networks. IEEE ACM Transactions on Computational Biology and Bioinformatics.
    10(2), 310–322.
  mla: Henzinger, Thomas A., and Maria Mateescu. “The Propagation Approach for Computing
    Biochemical Reaction Networks.” <i>IEEE ACM Transactions on Computational Biology
    and Bioinformatics</i>, vol. 10, no. 2, IEEE, 2012, pp. 310–22, doi:<a href="https://doi.org/10.1109/TCBB.2012.91">10.1109/TCBB.2012.91</a>.
  short: T.A. Henzinger, M. Mateescu, IEEE ACM Transactions on Computational Biology
    and Bioinformatics 10 (2012) 310–322.
date_created: 2018-12-11T11:56:52Z
date_published: 2012-07-03T00:00:00Z
date_updated: 2021-01-12T06:56:38Z
day: '03'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/TCBB.2012.91
ec_funded: 1
external_id:
  pmid:
  - '22778152'
intvolume: '        10'
issue: '2'
language:
- iso: eng
month: '07'
oa_version: None
page: 310 - 322
pmid: 1
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: IEEE ACM Transactions on Computational Biology and Bioinformatics
publication_status: published
publisher: IEEE
publist_id: '4625'
quality_controlled: '1'
scopus_import: 1
status: public
title: The propagation approach for computing biochemical reaction networks
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2012'
...
---
_id: '2318'
abstract:
- lang: eng
  text: 'We show that bosons interacting via pair potentials with negative scattering
    length form bound states for a suitable number of particles. In other words, the
    absence of many-particle bound states of any kind implies the non-negativity of
    the scattering length of the interaction potential. '
acknowledgement: 'Partial financial support by NSERC '
author:
- first_name: Robert
  full_name: Seiringer, Robert
  id: 4AFD0470-F248-11E8-B48F-1D18A9856A87
  last_name: Seiringer
  orcid: 0000-0002-6781-0521
citation:
  ama: Seiringer R. Absence of bound states implies non-negativity of the scattering
    length. <i>Journal of Spectral Theory</i>. 2012;2(3):321-328. doi:<a href="https://doi.org/10.4171/JST/31">10.4171/JST/31</a>
  apa: Seiringer, R. (2012). Absence of bound states implies non-negativity of the
    scattering length. <i>Journal of Spectral Theory</i>. European Mathematical Society.
    <a href="https://doi.org/10.4171/JST/31">https://doi.org/10.4171/JST/31</a>
  chicago: Seiringer, Robert. “Absence of Bound States Implies Non-Negativity of the
    Scattering Length.” <i>Journal of Spectral Theory</i>. European Mathematical Society,
    2012. <a href="https://doi.org/10.4171/JST/31">https://doi.org/10.4171/JST/31</a>.
  ieee: R. Seiringer, “Absence of bound states implies non-negativity of the scattering
    length,” <i>Journal of Spectral Theory</i>, vol. 2, no. 3. European Mathematical
    Society, pp. 321–328, 2012.
  ista: Seiringer R. 2012. Absence of bound states implies non-negativity of the scattering
    length. Journal of Spectral Theory. 2(3), 321–328.
  mla: Seiringer, Robert. “Absence of Bound States Implies Non-Negativity of the Scattering
    Length.” <i>Journal of Spectral Theory</i>, vol. 2, no. 3, European Mathematical
    Society, 2012, pp. 321–28, doi:<a href="https://doi.org/10.4171/JST/31">10.4171/JST/31</a>.
  short: R. Seiringer, Journal of Spectral Theory 2 (2012) 321–328.
date_created: 2018-12-11T11:56:58Z
date_published: 2012-06-24T00:00:00Z
date_updated: 2021-01-12T06:56:44Z
day: '24'
department:
- _id: RoSe
doi: 10.4171/JST/31
intvolume: '         2'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1204.0435
month: '06'
oa: 1
oa_version: Preprint
page: 321-328
publication: Journal of Spectral Theory
publication_status: published
publisher: European Mathematical Society
publist_id: '4609'
quality_controlled: '1'
status: public
title: Absence of bound states implies non-negativity of the scattering length
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2
year: '2012'
...
---
_id: '2411'
abstract:
- lang: eng
  text: The kingdom of fungi provides model organisms for biotechnology, cell biology,
    genetics, and life sciences in general. Only when their phylogenetic relationships
    are stably resolved, can individual results from fungal research be integrated
    into a holistic picture of biology. However, and despite recent progress, many
    deep relationships within the fungi remain unclear. Here, we present the first
    phylogenomic study of an entire eukaryotic kingdom that uses a consistency criterion
    to strengthen phylogenetic conclusions. We reason that branches (splits) recovered
    with independent data and different tree reconstruction methods are likely to
    reflect true evolutionary relationships. Two complementary phylogenomic data sets
    based on 99 fungal genomes and 109 fungal expressed sequence tag (EST) sets analyzed
    with four different tree reconstruction methods shed light from different angles
    on the fungal tree of life. Eleven additional data sets address specifically the
    phylogenetic position of Blastocladiomycota, Ustilaginomycotina, and Dothideomycetes,
    respectively. The combined evidence from the resulting trees supports the deep-level
    stability of the fungal groups toward a comprehensive natural system of the fungi.
    In addition, our analysis reveals methodologically interesting aspects. Enrichment
    for EST encoded data-a common practice in phylogenomic analyses-introduces a strong
    bias toward slowly evolving and functionally correlated genes. Consequently, the
    generalization of phylogenomic data sets as collections of randomly selected genes
    cannot be taken for granted. A thorough characterization of the data to assess
    possible influences on the tree reconstruction should therefore become a standard
    in phylogenomic analyses.
author:
- first_name: Ingo
  full_name: Ebersberger, Ingo
  last_name: Ebersberger
- first_name: Ricardo
  full_name: De Matos Simoes, Ricardo
  last_name: De Matos Simoes
- first_name: Anne
  full_name: Kupczok, Anne
  id: 2BB22BC2-F248-11E8-B48F-1D18A9856A87
  last_name: Kupczok
- first_name: Matthias
  full_name: Gube, Matthias
  last_name: Gube
- first_name: Erika
  full_name: Kothe, Erika
  last_name: Kothe
- first_name: Kerstin
  full_name: Voigt, Kerstin
  last_name: Voigt
- first_name: Arndt
  full_name: Von Haeseler, Arndt
  last_name: Von Haeseler
citation:
  ama: Ebersberger I, De Matos Simoes R, Kupczok A, et al. A consistent phylogenetic
    backbone for the fungi. <i>Molecular Biology and Evolution</i>. 2012;29(5):1319-1334.
    doi:<a href="https://doi.org/10.1093/molbev/msr285">10.1093/molbev/msr285</a>
  apa: Ebersberger, I., De Matos Simoes, R., Kupczok, A., Gube, M., Kothe, E., Voigt,
    K., &#38; Von Haeseler, A. (2012). A consistent phylogenetic backbone for the
    fungi. <i>Molecular Biology and Evolution</i>. Oxford University Press. <a href="https://doi.org/10.1093/molbev/msr285">https://doi.org/10.1093/molbev/msr285</a>
  chicago: Ebersberger, Ingo, Ricardo De Matos Simoes, Anne Kupczok, Matthias Gube,
    Erika Kothe, Kerstin Voigt, and Arndt Von Haeseler. “A Consistent Phylogenetic
    Backbone for the Fungi.” <i>Molecular Biology and Evolution</i>. Oxford University
    Press, 2012. <a href="https://doi.org/10.1093/molbev/msr285">https://doi.org/10.1093/molbev/msr285</a>.
  ieee: I. Ebersberger <i>et al.</i>, “A consistent phylogenetic backbone for the
    fungi,” <i>Molecular Biology and Evolution</i>, vol. 29, no. 5. Oxford University
    Press, pp. 1319–1334, 2012.
  ista: Ebersberger I, De Matos Simoes R, Kupczok A, Gube M, Kothe E, Voigt K, Von
    Haeseler A. 2012. A consistent phylogenetic backbone for the fungi. Molecular
    Biology and Evolution. 29(5), 1319–1334.
  mla: Ebersberger, Ingo, et al. “A Consistent Phylogenetic Backbone for the Fungi.”
    <i>Molecular Biology and Evolution</i>, vol. 29, no. 5, Oxford University Press,
    2012, pp. 1319–34, doi:<a href="https://doi.org/10.1093/molbev/msr285">10.1093/molbev/msr285</a>.
  short: I. Ebersberger, R. De Matos Simoes, A. Kupczok, M. Gube, E. Kothe, K. Voigt,
    A. Von Haeseler, Molecular Biology and Evolution 29 (2012) 1319–1334.
date_created: 2018-12-11T11:57:30Z
date_published: 2012-05-01T00:00:00Z
date_updated: 2021-01-12T06:57:19Z
day: '01'
ddc:
- '570'
- '576'
department:
- _id: JoBo
doi: 10.1093/molbev/msr285
file:
- access_level: open_access
  checksum: d565dcac27d1736c0c378ea6fcf22d69
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:30Z
  date_updated: 2020-07-14T12:45:40Z
  file_id: '5013'
  file_name: IST-2015-384-v1+1_Mol_Biol_Evol-2012-Ebersberger-1319-34.pdf
  file_size: 754922
  relation: main_file
file_date_updated: 2020-07-14T12:45:40Z
has_accepted_license: '1'
intvolume: '        29'
issue: '5'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: 1319 - 1334
publication: Molecular Biology and Evolution
publication_status: published
publisher: Oxford University Press
publist_id: '4515'
pubrep_id: '384'
quality_controlled: '1'
scopus_import: 1
status: public
title: A consistent phylogenetic backbone for the fungi
tmp:
  image: /images/cc_by_nc.png
  legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
  short: CC BY-NC (4.0)
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 29
year: '2012'
...
---
_id: '2715'
abstract:
- lang: eng
  text: 'We consider Markov decision processes (MDPs) with specifications given as
    Büchi (liveness) objectives. We consider the problem of computing the set of almost-sure
    winning vertices from where the objective can be ensured with probability 1. We
    study for the first time the average case complexity of the classical algorithm
    for computing the set of almost-sure winning vertices for MDPs with Büchi objectives.
    Our contributions are as follows: First, we show that for MDPs with constant out-degree
    the expected number of iterations is at most logarithmic and the average case
    running time is linear (as compared to the worst case linear number of iterations
    and quadratic time complexity). Second, for the average case analysis over all
    MDPs we show that the expected number of iterations is constant and the average
    case running time is linear (again as compared to the worst case linear number
    of iterations and quadratic time complexity). Finally we also show that given
    that all MDPs are equally likely, the probability that the classical algorithm
    requires more than constant number of iterations is exponentially small.'
alternative_title:
- LIPIcs
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Manas
  full_name: Joglekar, Manas
  last_name: Joglekar
- first_name: Nisarg
  full_name: Shah, Nisarg
  last_name: Shah
citation:
  ama: 'Chatterjee K, Joglekar M, Shah N. Average case analysis of the classical algorithm
    for Markov decision processes with Büchi objectives. In: Vol 18. Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik; 2012:461-473. doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">10.4230/LIPIcs.FSTTCS.2012.461</a>'
  apa: 'Chatterjee, K., Joglekar, M., &#38; Shah, N. (2012). Average case analysis
    of the classical algorithm for Markov decision processes with Büchi objectives
    (Vol. 18, pp. 461–473). Presented at the FSTTCS: Foundations of Software Technology
    and Theoretical Computer Science, Hyderabad, India: Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>'
  chicago: Chatterjee, Krishnendu, Manas Joglekar, and Nisarg Shah. “Average Case
    Analysis of the Classical Algorithm for Markov Decision Processes with Büchi Objectives,”
    18:461–73. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. <a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461</a>.
  ieee: 'K. Chatterjee, M. Joglekar, and N. Shah, “Average case analysis of the classical
    algorithm for Markov decision processes with Büchi objectives,” presented at the
    FSTTCS: Foundations of Software Technology and Theoretical Computer Science, Hyderabad,
    India, 2012, vol. 18, pp. 461–473.'
  ista: 'Chatterjee K, Joglekar M, Shah N. 2012. Average case analysis of the classical
    algorithm for Markov decision processes with Büchi objectives. FSTTCS: Foundations
    of Software Technology and Theoretical Computer Science, LIPIcs, vol. 18, 461–473.'
  mla: Chatterjee, Krishnendu, et al. <i>Average Case Analysis of the Classical Algorithm
    for Markov Decision Processes with Büchi Objectives</i>. Vol. 18, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2012, pp. 461–73, doi:<a href="https://doi.org/10.4230/LIPIcs.FSTTCS.2012.461">10.4230/LIPIcs.FSTTCS.2012.461</a>.
  short: K. Chatterjee, M. Joglekar, N. Shah, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2012, pp. 461–473.
conference:
  end_date: 2012-12-17
  location: Hyderabad, India
  name: 'FSTTCS: Foundations of Software Technology and Theoretical Computer Science'
  start_date: 2012-12-15
date_created: 2018-12-11T11:59:13Z
date_published: 2012-12-10T00:00:00Z
date_updated: 2023-02-23T10:06:04Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.FSTTCS.2012.461
ec_funded: 1
file:
- access_level: open_access
  checksum: d4d644ed1a885dbfc4fa1ef4c5724dab
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:53Z
  date_updated: 2020-07-14T12:45:45Z
  file_id: '5040'
  file_name: IST-2016-525-v1+1_42_1_.pdf
  file_size: 519040
  relation: main_file
file_date_updated: 2020-07-14T12:45:45Z
has_accepted_license: '1'
intvolume: '        18'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '12'
oa: 1
oa_version: Published Version
page: 461 - 473
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '4180'
pubrep_id: '525'
quality_controlled: '1'
related_material:
  record:
  - id: '1598'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Average case analysis of the classical algorithm for Markov decision processes
  with Büchi objectives
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2012'
...
---
_id: '2825'
abstract:
- lang: eng
  text: 'We study the problem of maximum marginal prediction (MMP) in probabilistic
    graphical models, a task that occurs, for example, as the Bayes optimal decision
    rule under a Hamming loss. MMP is typically performed as a two-stage procedure:
    one estimates each variable''s marginal probability and then forms a prediction
    from the states of maximal probability. In this work we propose a simple yet effective
    technique for accelerating MMP when inference is sampling-based: instead of the
    above two-stage procedure we directly estimate the posterior probability of each
    decision variable. This allows us to identify the point of time when we are sufficiently
    certain about any individual decision. Whenever this is the case, we dynamically
    prune the variables we are confident about from the underlying factor graph. Consequently,
    at any time only samples of variables whose decision is still uncertain need to
    be created. Experiments in two prototypical scenarios, multi-label classification
    and image inpainting, show that adaptive sampling can drastically accelerate MMP
    without sacrificing prediction accuracy.'
author:
- first_name: Christoph
  full_name: Lampert, Christoph
  id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
  last_name: Lampert
  orcid: 0000-0001-8622-7887
citation:
  ama: 'Lampert C. Dynamic pruning of factor graphs for maximum marginal prediction.
    In: Vol 1. Neural Information Processing Systems; 2012:82-90.'
  apa: 'Lampert, C. (2012). Dynamic pruning of factor graphs for maximum marginal
    prediction (Vol. 1, pp. 82–90). Presented at the NIPS: Neural Information Processing
    Systems, Lake Tahoe, NV, United States: Neural Information Processing Systems.'
  chicago: Lampert, Christoph. “Dynamic Pruning of Factor Graphs for Maximum Marginal
    Prediction,” 1:82–90. Neural Information Processing Systems, 2012.
  ieee: 'C. Lampert, “Dynamic pruning of factor graphs for maximum marginal prediction,”
    presented at the NIPS: Neural Information Processing Systems, Lake Tahoe, NV,
    United States, 2012, vol. 1, pp. 82–90.'
  ista: 'Lampert C. 2012. Dynamic pruning of factor graphs for maximum marginal prediction.
    NIPS: Neural Information Processing Systems vol. 1, 82–90.'
  mla: Lampert, Christoph. <i>Dynamic Pruning of Factor Graphs for Maximum Marginal
    Prediction</i>. Vol. 1, Neural Information Processing Systems, 2012, pp. 82–90.
  short: C. Lampert, in:, Neural Information Processing Systems, 2012, pp. 82–90.
conference:
  end_date: 2012-12-06
  location: Lake Tahoe, NV, United States
  name: 'NIPS: Neural Information Processing Systems'
  start_date: 2012-12-03
date_created: 2018-12-11T11:59:48Z
date_published: 2012-12-01T00:00:00Z
date_updated: 2021-01-12T06:59:59Z
day: '01'
department:
- _id: ChLa
intvolume: '         1'
language:
- iso: eng
month: '12'
oa_version: None
page: 82 - 90
publication_status: published
publisher: Neural Information Processing Systems
publist_id: '3975'
quality_controlled: '1'
scopus_import: 1
status: public
title: Dynamic pruning of factor graphs for maximum marginal prediction
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 1
year: '2012'
...
---
_id: '2848'
abstract:
- lang: eng
  text: We study evolutionary game theory in a setting where individuals learn from
    each other. We extend the traditional approach by assuming that a population contains
    individuals with different learning abilities. In particular, we explore the situation
    where individuals have different search spaces, when attempting to learn the strategies
    of others. The search space of an individual specifies the set of strategies learnable
    by that individual. The search space is genetically given and does not change
    under social evolutionary dynamics. We introduce a general framework and study
    a specific example in the context of direct reciprocity. For this example, we
    obtain the counter intuitive result that cooperation can only evolve for intermediate
    benefit-to-cost ratios, while small and large benefit-to-cost ratios favor defection.
    Our paper is a step toward making a connection between computational learning
    theory and evolutionary game dynamics.
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Damien
  full_name: Zufferey, Damien
  id: 4397AC76-F248-11E8-B48F-1D18A9856A87
  last_name: Zufferey
  orcid: 0000-0002-3197-8736
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Chatterjee K, Zufferey D, Nowak M. Evolutionary game dynamics in populations
    with different learners. <i>Journal of Theoretical Biology</i>. 2012;301:161-173.
    doi:<a href="https://doi.org/10.1016/j.jtbi.2012.02.021">10.1016/j.jtbi.2012.02.021</a>
  apa: Chatterjee, K., Zufferey, D., &#38; Nowak, M. (2012). Evolutionary game dynamics
    in populations with different learners. <i>Journal of Theoretical Biology</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.jtbi.2012.02.021">https://doi.org/10.1016/j.jtbi.2012.02.021</a>
  chicago: Chatterjee, Krishnendu, Damien Zufferey, and Martin Nowak. “Evolutionary
    Game Dynamics in Populations with Different Learners.” <i>Journal of Theoretical
    Biology</i>. Elsevier, 2012. <a href="https://doi.org/10.1016/j.jtbi.2012.02.021">https://doi.org/10.1016/j.jtbi.2012.02.021</a>.
  ieee: K. Chatterjee, D. Zufferey, and M. Nowak, “Evolutionary game dynamics in populations
    with different learners,” <i>Journal of Theoretical Biology</i>, vol. 301. Elsevier,
    pp. 161–173, 2012.
  ista: Chatterjee K, Zufferey D, Nowak M. 2012. Evolutionary game dynamics in populations
    with different learners. Journal of Theoretical Biology. 301, 161–173.
  mla: Chatterjee, Krishnendu, et al. “Evolutionary Game Dynamics in Populations with
    Different Learners.” <i>Journal of Theoretical Biology</i>, vol. 301, Elsevier,
    2012, pp. 161–73, doi:<a href="https://doi.org/10.1016/j.jtbi.2012.02.021">10.1016/j.jtbi.2012.02.021</a>.
  short: K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301
    (2012) 161–173.
date_created: 2018-12-11T11:59:55Z
date_published: 2012-05-21T00:00:00Z
date_updated: 2021-01-12T07:00:12Z
day: '21'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.jtbi.2012.02.021
ec_funded: 1
external_id:
  pmid:
  - '22394652'
intvolume: '       301'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.ncbi.nlm.nih.gov/pmc/articles/PMC3322297/
month: '05'
oa: 1
oa_version: Submitted Version
page: 161 - 173
pmid: 1
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Journal of Theoretical Biology
publication_status: published
publisher: Elsevier
publist_id: '3946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Evolutionary game dynamics in populations with different learners
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 301
year: '2012'
...
---
_id: '2849'
author:
- first_name: Herbert
  full_name: Edelsbrunner, Herbert
  id: 3FB178DA-F248-11E8-B48F-1D18A9856A87
  last_name: Edelsbrunner
  orcid: 0000-0002-9823-6833
- first_name: Nataliya
  full_name: Strelkova, Nataliya
  last_name: Strelkova
citation:
  ama: Edelsbrunner H, Strelkova N. On the configuration space of Steiner minimal
    trees. <i>Russian Mathematical Surveys</i>. 2012;67(6):1167-1168. doi:<a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">10.1070/RM2012v067n06ABEH004820</a>
  apa: Edelsbrunner, H., &#38; Strelkova, N. (2012). On the configuration space of
    Steiner minimal trees. <i>Russian Mathematical Surveys</i>. IOP Publishing Ltd.
    <a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">https://doi.org/10.1070/RM2012v067n06ABEH004820</a>
  chicago: Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space
    of Steiner Minimal Trees.” <i>Russian Mathematical Surveys</i>. IOP Publishing
    Ltd., 2012. <a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">https://doi.org/10.1070/RM2012v067n06ABEH004820</a>.
  ieee: H. Edelsbrunner and N. Strelkova, “On the configuration space of Steiner minimal
    trees,” <i>Russian Mathematical Surveys</i>, vol. 67, no. 6. IOP Publishing Ltd.,
    pp. 1167–1168, 2012.
  ista: Edelsbrunner H, Strelkova N. 2012. On the configuration space of Steiner minimal
    trees. Russian Mathematical Surveys. 67(6), 1167–1168.
  mla: Edelsbrunner, Herbert, and Nataliya Strelkova. “On the Configuration Space
    of Steiner Minimal Trees.” <i>Russian Mathematical Surveys</i>, vol. 67, no. 6,
    IOP Publishing Ltd., 2012, pp. 1167–68, doi:<a href="https://doi.org/10.1070/RM2012v067n06ABEH004820">10.1070/RM2012v067n06ABEH004820</a>.
  short: H. Edelsbrunner, N. Strelkova, Russian Mathematical Surveys 67 (2012) 1167–1168.
date_created: 2018-12-11T11:59:55Z
date_published: 2012-01-01T00:00:00Z
date_updated: 2021-01-12T07:00:13Z
day: '01'
ddc:
- '000'
department:
- _id: HeEd
doi: 10.1070/RM2012v067n06ABEH004820
file:
- access_level: open_access
  checksum: 44ee8d173487e8ed41a51136816bbeb4
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:26Z
  date_updated: 2020-07-14T12:45:51Z
  file_id: '5078'
  file_name: IST-2016-546-v1+1_2014-J-05-SteinerMinTrees.pdf
  file_size: 392021
  relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: '        67'
issue: '6'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 1167 - 1168
publication: Russian Mathematical Surveys
publication_status: published
publisher: IOP Publishing Ltd.
publist_id: '3943'
pubrep_id: '546'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the configuration space of Steiner minimal trees
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 67
year: '2012'
...
---
_id: '2888'
abstract:
- lang: eng
  text: Formal verification aims to improve the quality of hardware and software by
    detecting errors before they do harm. At the basis of formal verification lies
    the logical notion of correctness, which purports to capture whether or not a
    circuit or program behaves as desired. We suggest that the boolean partition into
    correct and incorrect systems falls short of the practical need to assess the
    behavior of hardware and software in a more nuanced fashion against multiple criteria.
alternative_title:
- LNCS
author:
- 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: 'Henzinger TA. Quantitative reactive models. In: <i>Conference Proceedings
    MODELS 2012</i>. Vol 7590. Springer; 2012:1-2. doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_1">10.1007/978-3-642-33666-9_1</a>'
  apa: 'Henzinger, T. A. (2012). Quantitative reactive models. In <i>Conference proceedings
    MODELS 2012</i> (Vol. 7590, pp. 1–2). Innsbruck, Austria: Springer. <a href="https://doi.org/10.1007/978-3-642-33666-9_1">https://doi.org/10.1007/978-3-642-33666-9_1</a>'
  chicago: Henzinger, Thomas A. “Quantitative Reactive Models.” In <i>Conference Proceedings
    MODELS 2012</i>, 7590:1–2. Springer, 2012. <a href="https://doi.org/10.1007/978-3-642-33666-9_1">https://doi.org/10.1007/978-3-642-33666-9_1</a>.
  ieee: T. A. Henzinger, “Quantitative reactive models,” in <i>Conference proceedings
    MODELS 2012</i>, Innsbruck, Austria, 2012, vol. 7590, pp. 1–2.
  ista: 'Henzinger TA. 2012. Quantitative reactive models. Conference proceedings
    MODELS 2012. MODELS: Model-driven Engineering Languages and Systems, LNCS, vol.
    7590, 1–2.'
  mla: Henzinger, Thomas A. “Quantitative Reactive Models.” <i>Conference Proceedings
    MODELS 2012</i>, vol. 7590, Springer, 2012, pp. 1–2, doi:<a href="https://doi.org/10.1007/978-3-642-33666-9_1">10.1007/978-3-642-33666-9_1</a>.
  short: T.A. Henzinger, in:, Conference Proceedings MODELS 2012, Springer, 2012,
    pp. 1–2.
conference:
  end_date: 2012-10-05
  location: Innsbruck, Austria
  name: 'MODELS: Model-driven Engineering Languages and Systems'
  start_date: 2012-09-30
date_created: 2018-12-11T12:00:09Z
date_published: 2012-09-01T00:00:00Z
date_updated: 2021-01-12T07:00:29Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-33666-9_1
ec_funded: 1
intvolume: '      7590'
language:
- iso: eng
month: '09'
oa_version: None
page: 1 - 2
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Conference proceedings MODELS 2012
publication_status: published
publisher: Springer
publist_id: '3870'
quality_controlled: '1'
scopus_import: 1
status: public
title: Quantitative reactive models
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7590
year: '2012'
...
---
_id: '2890'
abstract:
- lang: eng
  text: 'Systems are often specified using multiple requirements on their behavior.
    In practice, these requirements can be contradictory. The classical approach to
    specification, verification, and synthesis demands more detailed specifications
    that resolve any contradictions in the requirements. These detailed specifications
    are usually large, cumbersome, and hard to maintain or modify. In contrast, quantitative
    frameworks allow the formalization of the intuitive idea that what is desired
    is an implementation that comes &quot;closest&quot; to satisfying the mutually
    incompatible requirements, according to a measure of fit that can be defined by
    the requirements engineer. One flexible framework for quantifying how &quot;well&quot;
    an implementation satisfies a specification is offered by simulation distances
    that are parameterized by an error model. We introduce this framework, study its
    properties, and provide an algorithmic solution for the following quantitative
    synthesis question: given two (or more) behavioral requirements specified by possibly
    incompatible finite-state machines, and an error model, find the finite-state
    implementation that minimizes the maximal simulation distance to the given requirements.
    Furthermore, we generalize the framework to handle infinite alphabets (for example,
    realvalued domains). We also demonstrate how quantitative specifications based
    on simulation distances might lead to smaller and easier to modify specifications.
    Finally, we illustrate our approach using case studies on error correcting codes
    and scheduler synthesis.'
author:
- first_name: Pavol
  full_name: Cerny, Pavol
  id: 4DCBEFFE-F248-11E8-B48F-1D18A9856A87
  last_name: Cerny
- first_name: Sivakanth
  full_name: Gopi, Sivakanth
  last_name: Gopi
- 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: Arjun
  full_name: Radhakrishna, Arjun
  id: 3B51CAC4-F248-11E8-B48F-1D18A9856A87
  last_name: Radhakrishna
- first_name: Nishant
  full_name: Totla, Nishant
  last_name: Totla
citation:
  ama: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. Synthesis from incompatible
    specifications. In: <i>Proceedings of the Tenth ACM International Conference on
    Embedded Software</i>. ACM; 2012:53-62. doi:<a href="https://doi.org/10.1145/2380356.2380371">10.1145/2380356.2380371</a>'
  apa: 'Cerny, P., Gopi, S., Henzinger, T. A., Radhakrishna, A., &#38; Totla, N. (2012).
    Synthesis from incompatible specifications. In <i>Proceedings of the tenth ACM
    international conference on Embedded software</i> (pp. 53–62). Tampere, Finland:
    ACM. <a href="https://doi.org/10.1145/2380356.2380371">https://doi.org/10.1145/2380356.2380371</a>'
  chicago: Cerny, Pavol, Sivakanth Gopi, Thomas A Henzinger, Arjun Radhakrishna, and
    Nishant Totla. “Synthesis from Incompatible Specifications.” In <i>Proceedings
    of the Tenth ACM International Conference on Embedded Software</i>, 53–62. ACM,
    2012. <a href="https://doi.org/10.1145/2380356.2380371">https://doi.org/10.1145/2380356.2380371</a>.
  ieee: P. Cerny, S. Gopi, T. A. Henzinger, A. Radhakrishna, and N. Totla, “Synthesis
    from incompatible specifications,” in <i>Proceedings of the tenth ACM international
    conference on Embedded software</i>, Tampere, Finland, 2012, pp. 53–62.
  ista: 'Cerny P, Gopi S, Henzinger TA, Radhakrishna A, Totla N. 2012. Synthesis from
    incompatible specifications. Proceedings of the tenth ACM international conference
    on Embedded software. EMSOFT: Embedded Software , 53–62.'
  mla: Cerny, Pavol, et al. “Synthesis from Incompatible Specifications.” <i>Proceedings
    of the Tenth ACM International Conference on Embedded Software</i>, ACM, 2012,
    pp. 53–62, doi:<a href="https://doi.org/10.1145/2380356.2380371">10.1145/2380356.2380371</a>.
  short: P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings
    of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp.
    53–62.
conference:
  end_date: 2012-10-12
  location: Tampere, Finland
  name: 'EMSOFT: Embedded Software '
  start_date: 2012-10-07
date_created: 2018-12-11T12:00:10Z
date_published: 2012-10-01T00:00:00Z
date_updated: 2021-01-12T07:00:30Z
day: '01'
department:
- _id: ToHe
doi: 10.1145/2380356.2380371
ec_funded: 1
language:
- iso: eng
month: '10'
oa_version: None
page: 53 - 62
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication: Proceedings of the tenth ACM international conference on Embedded software
publication_status: published
publisher: ACM
publist_id: '3868'
quality_controlled: '1'
scopus_import: 1
status: public
title: Synthesis from incompatible specifications
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2012'
...
