---
_id: '3343'
abstract:
- lang: eng
  text: 'We present faster and dynamic algorithms for the following problems arising
    in probabilistic verification: Computation of the maximal end-component (mec)
    decomposition of Markov decision processes (MDPs), and of the almost sure winning
    set for reachability and parity objectives in MDPs. We achieve the following running
    time for static algorithms in MDPs with graphs of n vertices and m edges: (1)
    O(m · min{ √m, n2/3 }) for the mec decomposition, improving the longstanding O(m·n)
    bound; (2) O(m·n2/3) for reachability objectives, improving the previous O(m ·
    √m) bound for m &gt; n4/3; and (3) O(m · min{ √m, n2/3 } · log(d)) for parity
    objectives with d priorities, improving the previous O(m · √m · d) bound. We also
    give incremental and decremental algorithms in linear time for mec decomposition
    and reachability objectives and O(m · log d) time for parity ob jectives.'
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: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
citation:
  ama: 'Chatterjee K, Henzinger MH. Faster and dynamic algorithms for maximal end-component
    decomposition and related graph problems in probabilistic verification. In: SIAM;
    2011:1318-1336. doi:<a href="https://doi.org/10.1137/1.9781611973082.101">10.1137/1.9781611973082.101</a>'
  apa: 'Chatterjee, K., &#38; Henzinger, M. H. (2011). Faster and dynamic algorithms
    for maximal end-component decomposition and related graph problems in probabilistic
    verification (pp. 1318–1336). Presented at the SODA: Symposium on Discrete Algorithms,
    San Francisco, SA, United States: SIAM. <a href="https://doi.org/10.1137/1.9781611973082.101">https://doi.org/10.1137/1.9781611973082.101</a>'
  chicago: Chatterjee, Krishnendu, and Monika H Henzinger. “Faster and Dynamic Algorithms
    for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic
    Verification,” 1318–36. SIAM, 2011. <a href="https://doi.org/10.1137/1.9781611973082.101">https://doi.org/10.1137/1.9781611973082.101</a>.
  ieee: 'K. Chatterjee and M. H. Henzinger, “Faster and dynamic algorithms for maximal
    end-component decomposition and related graph problems in probabilistic verification,”
    presented at the SODA: Symposium on Discrete Algorithms, San Francisco, SA, United
    States, 2011, pp. 1318–1336.'
  ista: 'Chatterjee K, Henzinger MH. 2011. Faster and dynamic algorithms for maximal
    end-component decomposition and related graph problems in probabilistic verification.
    SODA: Symposium on Discrete Algorithms, 1318–1336.'
  mla: Chatterjee, Krishnendu, and Monika H. Henzinger. <i>Faster and Dynamic Algorithms
    for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic
    Verification</i>. SIAM, 2011, pp. 1318–36, doi:<a href="https://doi.org/10.1137/1.9781611973082.101">10.1137/1.9781611973082.101</a>.
  short: K. Chatterjee, M.H. Henzinger, in:, SIAM, 2011, pp. 1318–1336.
conference:
  end_date: 2011-01-25
  location: San Francisco, SA, United States
  name: 'SODA: Symposium on Discrete Algorithms'
  start_date: 2011-01-23
date_created: 2018-12-11T12:02:47Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2023-02-14T10:36:10Z
day: '01'
department:
- _id: KrCh
doi: 10.1137/1.9781611973082.101
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://eprints.cs.univie.ac.at/21/
month: '01'
oa: 1
oa_version: Submitted Version
page: 1318 - 1336
publication_status: published
publisher: SIAM
publist_id: '3278'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster and dynamic algorithms for maximal end-component decomposition and related
  graph problems in probabilistic verification
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '3344'
abstract:
- lang: eng
  text: 'Games played on graphs provide the mathematical framework to analyze several
    important problems in computer science as well as mathematics, such as the synthesis
    problem of Church, model checking of open reactive systems and many others. On
    the basis of mode of interaction of the players these games can be classified
    as follows: (a) turn-based (players make moves in turns); and (b) concurrent (players
    make moves simultaneously). On the basis of the information available to the players
    these games can be classified as follows: (a) perfect-information (players have
    perfect view of the game); and (b) partial-information (players have partial view
    of the game). In this talk we will consider all these classes of games with reachability
    objectives, where the goal of one player is to reach a set of target vertices
    of the graph, and the goal of the opponent player is to prevent the player from
    reaching the target. We will survey the results for various classes of games,
    and the results range from linear time decision algorithms to EXPTIME-complete
    problems to undecidable problems.'
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
citation:
  ama: 'Chatterjee K. Graph games with reachability objectives. In: Delzanno G, Potapov
    I, eds. Vol 6945. Springer; 2011:1-1. doi:<a href="https://doi.org/10.1007/978-3-642-24288-5_1">10.1007/978-3-642-24288-5_1</a>'
  apa: 'Chatterjee, K. (2011). Graph games with reachability objectives. In G. Delzanno
    &#38; I. Potapov (Eds.) (Vol. 6945, pp. 1–1). Presented at the RP: Reachability
    Problems, Genoa, Italy: Springer. <a href="https://doi.org/10.1007/978-3-642-24288-5_1">https://doi.org/10.1007/978-3-642-24288-5_1</a>'
  chicago: Chatterjee, Krishnendu. “Graph Games with Reachability Objectives.” edited
    by Giorgo Delzanno and Igor Potapov, 6945:1–1. Springer, 2011. <a href="https://doi.org/10.1007/978-3-642-24288-5_1">https://doi.org/10.1007/978-3-642-24288-5_1</a>.
  ieee: 'K. Chatterjee, “Graph games with reachability objectives,” presented at the
    RP: Reachability Problems, Genoa, Italy, 2011, vol. 6945, pp. 1–1.'
  ista: 'Chatterjee K. 2011. Graph games with reachability objectives. RP: Reachability
    Problems, LNCS, vol. 6945, 1–1.'
  mla: Chatterjee, Krishnendu. <i>Graph Games with Reachability Objectives</i>. Edited
    by Giorgo Delzanno and Igor Potapov, vol. 6945, Springer, 2011, pp. 1–1, doi:<a
    href="https://doi.org/10.1007/978-3-642-24288-5_1">10.1007/978-3-642-24288-5_1</a>.
  short: K. Chatterjee, in:, G. Delzanno, I. Potapov (Eds.), Springer, 2011, pp. 1–1.
conference:
  end_date: 2011-09-30
  location: Genoa, Italy
  name: 'RP: Reachability Problems'
  start_date: 2011-09-28
date_created: 2018-12-11T12:02:47Z
date_published: 2011-10-15T00:00:00Z
date_updated: 2021-01-12T07:42:48Z
day: '15'
department:
- _id: KrCh
doi: 10.1007/978-3-642-24288-5_1
editor:
- first_name: Giorgo
  full_name: Delzanno, Giorgo
  last_name: Delzanno
- first_name: Igor
  full_name: Potapov, Igor
  last_name: Potapov
intvolume: '      6945'
language:
- iso: eng
month: '10'
oa_version: None
page: 1 - 1
publication_status: published
publisher: Springer
publist_id: '3277'
quality_controlled: '1'
status: public
title: Graph games with reachability objectives
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 6945
year: '2011'
...
---
_id: '10907'
abstract:
- lang: eng
  text: This paper presents a method to create a model of an articulated object using
    the planar motion in an initialization video. The model consists of rigid parts
    connected by points of articulation. The rigid parts are described by the positions
    of salient feature-points tracked throughout the video. Following a filtering
    step that identifies points that belong to different objects, rigid parts are
    found by a grouping process in a graph pyramid. Valid articulation points are
    selected by verifying multiple hypotheses for each pair of parts.
acknowledgement: This work has been partially supported by the Austrian Science Fund
  under grants S9103-N13 and P18716-N13.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Nicole M.
  full_name: Artner, Nicole M.
  last_name: Artner
- first_name: Adrian
  full_name: Ion, Adrian
  id: 29F89302-F248-11E8-B48F-1D18A9856A87
  last_name: Ion
- first_name: Walter G.
  full_name: Kropatsch, Walter G.
  last_name: Kropatsch
citation:
  ama: 'Artner NM, Ion A, Kropatsch WG. Spatio-temporal extraction of articulated
    models in a graph pyramid. In: Jiang X, Ferrer M, Torsello A, eds. <i>Graph-Based
    Representations in Pattern Recognition</i>. Vol 6658. LNIP. Berlin, Heidelberg:
    Springer; 2011:215-224. doi:<a href="https://doi.org/10.1007/978-3-642-20844-7_22">10.1007/978-3-642-20844-7_22</a>'
  apa: 'Artner, N. M., Ion, A., &#38; Kropatsch, W. G. (2011). Spatio-temporal extraction
    of articulated models in a graph pyramid. In X. Jiang, M. Ferrer, &#38; A. Torsello
    (Eds.), <i>Graph-Based Representations in Pattern Recognition</i> (Vol. 6658,
    pp. 215–224). Berlin, Heidelberg: Springer. <a href="https://doi.org/10.1007/978-3-642-20844-7_22">https://doi.org/10.1007/978-3-642-20844-7_22</a>'
  chicago: 'Artner, Nicole M., Adrian Ion, and Walter G. Kropatsch. “Spatio-Temporal
    Extraction of Articulated Models in a Graph Pyramid.” In <i>Graph-Based Representations
    in Pattern Recognition</i>, edited by Xiaoyi Jiang, Miquel Ferrer, and Andrea
    Torsello, 6658:215–24. LNIP. Berlin, Heidelberg: Springer, 2011. <a href="https://doi.org/10.1007/978-3-642-20844-7_22">https://doi.org/10.1007/978-3-642-20844-7_22</a>.'
  ieee: N. M. Artner, A. Ion, and W. G. Kropatsch, “Spatio-temporal extraction of
    articulated models in a graph pyramid,” in <i>Graph-Based Representations in Pattern
    Recognition</i>, Münster, Germany, 2011, vol. 6658, pp. 215–224.
  ista: 'Artner NM, Ion A, Kropatsch WG. 2011. Spatio-temporal extraction of articulated
    models in a graph pyramid. Graph-Based Representations in Pattern Recognition.
    GbRPR: Graph-based Representations in Pattern RecognitionLNIP, LNCS, vol. 6658,
    215–224.'
  mla: Artner, Nicole M., et al. “Spatio-Temporal Extraction of Articulated Models
    in a Graph Pyramid.” <i>Graph-Based Representations in Pattern Recognition</i>,
    edited by Xiaoyi Jiang et al., vol. 6658, Springer, 2011, pp. 215–24, doi:<a href="https://doi.org/10.1007/978-3-642-20844-7_22">10.1007/978-3-642-20844-7_22</a>.
  short: N.M. Artner, A. Ion, W.G. Kropatsch, in:, X. Jiang, M. Ferrer, A. Torsello
    (Eds.), Graph-Based Representations in Pattern Recognition, Springer, Berlin,
    Heidelberg, 2011, pp. 215–224.
conference:
  end_date: 2011-05-20
  location: Münster, Germany
  name: 'GbRPR: Graph-based Representations in Pattern Recognition'
  start_date: 2011-05-18
date_created: 2022-03-21T08:08:35Z
date_published: 2011-06-01T00:00:00Z
date_updated: 2023-09-05T14:10:15Z
day: '01'
department:
- _id: HeEd
doi: 10.1007/978-3-642-20844-7_22
editor:
- first_name: Xiaoyi
  full_name: Jiang, Xiaoyi
  last_name: Jiang
- first_name: Miquel
  full_name: Ferrer, Miquel
  last_name: Ferrer
- first_name: Andrea
  full_name: Torsello, Andrea
  last_name: Torsello
intvolume: '      6658'
language:
- iso: eng
month: '06'
oa_version: None
page: 215-224
place: Berlin, Heidelberg
publication: Graph-Based Representations in Pattern Recognition
publication_identifier:
  eisbn:
  - '9783642208447'
  eissn:
  - 1611-3349
  isbn:
  - '9783642208430'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
series_title: LNIP
status: public
title: Spatio-temporal extraction of articulated models in a graph pyramid
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 6658
year: '2011'
...
---
_id: '469'
abstract:
- lang: eng
  text: 'Spontaneous release of glutamate is important for maintaining synaptic strength
    and controlling spike timing in the brain. Mechanisms regulating spontaneous exocytosis
    remain poorly understood. Extracellular calcium concentration ([Ca2+]o) regulates
    Ca2+ entry through voltage-activated calcium channels (VACCs) and consequently
    is a pivotal determinant of action potential-evoked vesicle fusion. Extracellular
    Ca 2+ also enhances spontaneous release, but via unknown mechanisms. Here we report
    that external Ca2+ triggers spontaneous glutamate release more weakly than evoked
    release in mouse neocortical neurons. Blockade of VACCs has no effect on the spontaneous
    release rate or its dependence on [Ca2+]o. Intracellular [Ca2+] slowly increases
    in a minority of neurons following increases in [Ca2+]o. Furthermore, the enhancement
    of spontaneous release by extracellular calcium is insensitive to chelation of
    intracellular calcium by BAPTA. Activation of the calcium-sensing receptor (CaSR),
    a G-protein-coupled receptor present in nerve terminals, by several specific agonists
    increased spontaneous glutamate release. The frequency of spontaneous synaptic
    transmission was decreased in CaSR mutant neurons. The concentration-effect relationship
    for extracellular calcium regulation of spontaneous release was well described
    by a combination of CaSR-dependent and CaSR-independent mechanisms. Overall these
    results indicate that extracellular Ca2+ does not trigger spontaneous glutamate
    release by simply increasing calcium influx but stimulates CaSR and thereby promotes
    resting spontaneous glutamate release. '
author:
- first_name: Nicholas
  full_name: Vyleta, Nicholas
  id: 36C4978E-F248-11E8-B48F-1D18A9856A87
  last_name: Vyleta
- first_name: Stephen
  full_name: Smith, Stephen
  last_name: Smith
citation:
  ama: Vyleta N, Smith S. Spontaneous glutamate release is independent of calcium
    influx and tonically activated by the calcium-sensing receptor. <i>European Journal
    of Neuroscience</i>. 2011;31(12):4593-4606. doi:<a href="https://doi.org/10.1523/JNEUROSCI.6398-10.2011">10.1523/JNEUROSCI.6398-10.2011</a>
  apa: Vyleta, N., &#38; Smith, S. (2011). Spontaneous glutamate release is independent
    of calcium influx and tonically activated by the calcium-sensing receptor. <i>European
    Journal of Neuroscience</i>. Wiley-Blackwell. <a href="https://doi.org/10.1523/JNEUROSCI.6398-10.2011">https://doi.org/10.1523/JNEUROSCI.6398-10.2011</a>
  chicago: Vyleta, Nicholas, and Stephen Smith. “Spontaneous Glutamate Release Is
    Independent of Calcium Influx and Tonically Activated by the Calcium-Sensing Receptor.”
    <i>European Journal of Neuroscience</i>. Wiley-Blackwell, 2011. <a href="https://doi.org/10.1523/JNEUROSCI.6398-10.2011">https://doi.org/10.1523/JNEUROSCI.6398-10.2011</a>.
  ieee: N. Vyleta and S. Smith, “Spontaneous glutamate release is independent of calcium
    influx and tonically activated by the calcium-sensing receptor,” <i>European Journal
    of Neuroscience</i>, vol. 31, no. 12. Wiley-Blackwell, pp. 4593–4606, 2011.
  ista: Vyleta N, Smith S. 2011. Spontaneous glutamate release is independent of calcium
    influx and tonically activated by the calcium-sensing receptor. European Journal
    of Neuroscience. 31(12), 4593–4606.
  mla: Vyleta, Nicholas, and Stephen Smith. “Spontaneous Glutamate Release Is Independent
    of Calcium Influx and Tonically Activated by the Calcium-Sensing Receptor.” <i>European
    Journal of Neuroscience</i>, vol. 31, no. 12, Wiley-Blackwell, 2011, pp. 4593–606,
    doi:<a href="https://doi.org/10.1523/JNEUROSCI.6398-10.2011">10.1523/JNEUROSCI.6398-10.2011</a>.
  short: N. Vyleta, S. Smith, European Journal of Neuroscience 31 (2011) 4593–4606.
date_created: 2018-12-11T11:46:39Z
date_published: 2011-03-23T00:00:00Z
date_updated: 2021-01-12T08:00:49Z
day: '23'
department:
- _id: PeJo
doi: 10.1523/JNEUROSCI.6398-10.2011
intvolume: '        31'
issue: '12'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3097128/
month: '03'
oa: 1
oa_version: Submitted Version
page: 4593 - 4606
publication: European Journal of Neuroscience
publication_status: published
publisher: Wiley-Blackwell
publist_id: '7353'
quality_controlled: '1'
scopus_import: 1
status: public
title: Spontaneous glutamate release is independent of calcium influx and tonically
  activated by the calcium-sensing receptor
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 31
year: '2011'
...
---
_id: '490'
abstract:
- lang: eng
  text: 'BioSig is an open source software library for biomedical signal processing.
    The aim of the BioSig project is to foster research in biomedical signal processing
    by providing free and open source software tools for many different application
    areas. Some of the areas where BioSig can be employed are neuroinformatics, brain-computer
    interfaces, neurophysiology, psychology, cardiovascular systems, and sleep research.
    Moreover, the analysis of biosignals such as the electroencephalogram (EEG), electrocorticogram
    (ECoG), electrocardiogram (ECG), electrooculogram (EOG), electromyogram (EMG),
    or respiration signals is a very relevant element of the BioSig project. Specifically,
    BioSig provides solutions for data acquisition, artifact processing, quality control,
    feature extraction, classification, modeling, and data visualization, to name
    a few. In this paper, we highlight several methods to help students and researchers
    to work more efficiently with biomedical signals. '
article_number: '935364'
author:
- first_name: Alois
  full_name: Schlögl, Alois
  id: 45BF87EE-F248-11E8-B48F-1D18A9856A87
  last_name: Schlögl
  orcid: 0000-0002-5621-8100
- first_name: Carmen
  full_name: Vidaurre, Carmen
  last_name: Vidaurre
- first_name: Tilmann
  full_name: Sander, Tilmann
  last_name: Sander
citation:
  ama: 'Schlögl A, Vidaurre C, Sander T. BioSig: The free and open source software
    library for biomedical signal processing. <i>Computational Intelligence and Neuroscience</i>.
    2011;2011. doi:<a href="https://doi.org/10.1155/2011/935364">10.1155/2011/935364</a>'
  apa: 'Schlögl, A., Vidaurre, C., &#38; Sander, T. (2011). BioSig: The free and open
    source software library for biomedical signal processing. <i>Computational Intelligence
    and Neuroscience</i>. Hindawi Publishing Corporation. <a href="https://doi.org/10.1155/2011/935364">https://doi.org/10.1155/2011/935364</a>'
  chicago: 'Schlögl, Alois, Carmen Vidaurre, and Tilmann Sander. “BioSig: The Free
    and Open Source Software Library for Biomedical Signal Processing.” <i>Computational
    Intelligence and Neuroscience</i>. Hindawi Publishing Corporation, 2011. <a href="https://doi.org/10.1155/2011/935364">https://doi.org/10.1155/2011/935364</a>.'
  ieee: 'A. Schlögl, C. Vidaurre, and T. Sander, “BioSig: The free and open source
    software library for biomedical signal processing,” <i>Computational Intelligence
    and Neuroscience</i>, vol. 2011. Hindawi Publishing Corporation, 2011.'
  ista: 'Schlögl A, Vidaurre C, Sander T. 2011. BioSig: The free and open source software
    library for biomedical signal processing. Computational Intelligence and Neuroscience.
    2011, 935364.'
  mla: 'Schlögl, Alois, et al. “BioSig: The Free and Open Source Software Library
    for Biomedical Signal Processing.” <i>Computational Intelligence and Neuroscience</i>,
    vol. 2011, 935364, Hindawi Publishing Corporation, 2011, doi:<a href="https://doi.org/10.1155/2011/935364">10.1155/2011/935364</a>.'
  short: A. Schlögl, C. Vidaurre, T. Sander, Computational Intelligence and Neuroscience
    2011 (2011).
date_created: 2018-12-11T11:46:45Z
date_published: 2011-01-01T00:00:00Z
date_updated: 2021-01-12T08:01:02Z
day: '01'
ddc:
- '005'
department:
- _id: ScienComp
- _id: PeJo
doi: 10.1155/2011/935364
file:
- access_level: open_access
  checksum: 8263bbf255171f2054f43f3db5f53b6e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:07:44Z
  date_updated: 2020-07-14T12:46:35Z
  file_id: '4642'
  file_name: IST-2018-947-v1+1_2011_Schloegl_BioSig.pdf
  file_size: 2863551
  relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: '      2011'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '01'
oa: 1
oa_version: Published Version
publication: Computational Intelligence and Neuroscience
publication_status: published
publisher: Hindawi Publishing Corporation
publist_id: '7330'
pubrep_id: '947'
quality_controlled: '1'
scopus_import: 1
status: public
title: 'BioSig: The free and open source software library for biomedical signal processing'
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 2011
year: '2011'
...
---
_id: '491'
abstract:
- lang: eng
  text: In their search for antigens, lymphocytes continuously shuttle among blood
    vessels, lymph vessels, and lymphatic tissues. Chemokines mediate entry of lymphocytes
    into lymphatic tissues, and sphingosine 1-phosphate (S1P) promotes localization
    of lymphocytes to the vasculature. Both signals are sensed through G protein-coupled
    receptors (GPCRs). Most GPCRs undergo ligand-dependent homologous receptor desensitization,
    a process that decreases their signaling output after previous exposure to high
    ligand concentration. Such desensitization can explain why lymphocytes do not
    take an intermediate position between two signals but rather oscillate between
    them. The desensitization of S1P receptor 1 (S1PR1) is mediated by GPCR kinase
    2 (GRK2). Deletion of GRK2 in lymphocytes compromises desensitization by high
    vascular S1P concentrations, thereby reducing responsiveness to the chemokine
    signal and trapping the cells in the vascular compartment. The desensitization
    kinetics of S1PR1 allows lymphocytes to dynamically shuttle between vasculature
    and lymphatic tissue, although the positional information in both compartments
    is static.
article_number: pe43
author:
- first_name: Alexander
  full_name: Eichner, Alexander
  id: 4DFA52AE-F248-11E8-B48F-1D18A9856A87
  last_name: Eichner
- first_name: Michael K
  full_name: Sixt, Michael K
  id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
  last_name: Sixt
  orcid: 0000-0002-6620-9179
citation:
  ama: Eichner A, Sixt MK. Setting the clock for recirculating lymphocytes. <i>Science
    Signaling</i>. 2011;4(198). doi:<a href="https://doi.org/10.1126/scisignal.2002617">10.1126/scisignal.2002617</a>
  apa: Eichner, A., &#38; Sixt, M. K. (2011). Setting the clock for recirculating
    lymphocytes. <i>Science Signaling</i>. American Association for the Advancement
    of Science. <a href="https://doi.org/10.1126/scisignal.2002617">https://doi.org/10.1126/scisignal.2002617</a>
  chicago: Eichner, Alexander, and Michael K Sixt. “Setting the Clock for Recirculating
    Lymphocytes.” <i>Science Signaling</i>. American Association for the Advancement
    of Science, 2011. <a href="https://doi.org/10.1126/scisignal.2002617">https://doi.org/10.1126/scisignal.2002617</a>.
  ieee: A. Eichner and M. K. Sixt, “Setting the clock for recirculating lymphocytes,”
    <i>Science Signaling</i>, vol. 4, no. 198. American Association for the Advancement
    of Science, 2011.
  ista: Eichner A, Sixt MK. 2011. Setting the clock for recirculating lymphocytes.
    Science Signaling. 4(198), pe43.
  mla: Eichner, Alexander, and Michael K. Sixt. “Setting the Clock for Recirculating
    Lymphocytes.” <i>Science Signaling</i>, vol. 4, no. 198, pe43, American Association
    for the Advancement of Science, 2011, doi:<a href="https://doi.org/10.1126/scisignal.2002617">10.1126/scisignal.2002617</a>.
  short: A. Eichner, M.K. Sixt, Science Signaling 4 (2011).
date_created: 2018-12-11T11:46:46Z
date_published: 2011-11-08T00:00:00Z
date_updated: 2021-01-12T08:01:02Z
day: '08'
department:
- _id: MiSi
doi: 10.1126/scisignal.2002617
intvolume: '         4'
issue: '198'
language:
- iso: eng
month: '11'
oa_version: None
publication: Science Signaling
publication_status: published
publisher: American Association for the Advancement of Science
publist_id: '7329'
quality_controlled: '1'
scopus_import: 1
status: public
title: Setting the clock for recirculating lymphocytes
type: journal_article
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 4
year: '2011'
...
---
_id: '518'
abstract:
- lang: eng
  text: Cancer stem cells or cancer initiating cells are believed to contribute to
    cancer recurrence after therapy. MicroRNAs (miRNAs) are short RNA molecules with
    fundamental roles in gene regulation. The role of miRNAs in cancer stem cells
    is only poorly understood. Here, we report miRNA expression profiles of glioblastoma
    stem cell-containing CD133 + cell populations. We find that miR-9, miR-9 * (referred
    to as miR-9/9 *), miR-17 and miR-106b are highly abundant in CD133 + cells. Furthermore,
    inhibition of miR-9/9 * or miR-17 leads to reduced neurosphere formation and stimulates
    cell differentiation. Calmodulin-binding transcription activator 1 (CAMTA1) is
    a putative transcription factor, which induces the expression of the anti-proliferative
    cardiac hormone natriuretic peptide A (NPPA). We identify CAMTA1 as an miR-9/9
    * and miR-17 target. CAMTA1 expression leads to reduced neurosphere formation
    and tumour growth in nude mice, suggesting that CAMTA1 can function as tumour
    suppressor. Consistently, CAMTA1 and NPPA expression correlate with patient survival.
    Our findings could provide a basis for novel strategies of glioblastoma therapy.
article_processing_charge: No
article_type: original
author:
- first_name: Daniel
  full_name: Schraivogel, Daniel
  last_name: Schraivogel
- first_name: Lasse
  full_name: Weinmann, Lasse
  last_name: Weinmann
- first_name: Dagmar
  full_name: Beier, Dagmar
  last_name: Beier
- first_name: Ghazaleh
  full_name: Tabatabai, Ghazaleh
  last_name: Tabatabai
- first_name: Alexander
  full_name: Eichner, Alexander
  id: 4DFA52AE-F248-11E8-B48F-1D18A9856A87
  last_name: Eichner
- first_name: Jia
  full_name: Zhu, Jia
  last_name: Zhu
- first_name: Martina
  full_name: Anton, Martina
  last_name: Anton
- first_name: Michael K
  full_name: Sixt, Michael K
  id: 41E9FBEA-F248-11E8-B48F-1D18A9856A87
  last_name: Sixt
  orcid: 0000-0002-6620-9179
- first_name: Michael
  full_name: Weller, Michael
  last_name: Weller
- first_name: Christoph
  full_name: Beier, Christoph
  last_name: Beier
- first_name: Gunter
  full_name: Meister, Gunter
  last_name: Meister
citation:
  ama: Schraivogel D, Weinmann L, Beier D, et al. CAMTA1 is a novel tumour suppressor
    regulated by miR-9/9 * in glioblastoma stem cells. <i>EMBO Journal</i>. 2011;30(20):4309-4322.
    doi:<a href="https://doi.org/10.1038/emboj.2011.301">10.1038/emboj.2011.301</a>
  apa: Schraivogel, D., Weinmann, L., Beier, D., Tabatabai, G., Eichner, A., Zhu,
    J., … Meister, G. (2011). CAMTA1 is a novel tumour suppressor regulated by miR-9/9
    * in glioblastoma stem cells. <i>EMBO Journal</i>. Wiley-Blackwell. <a href="https://doi.org/10.1038/emboj.2011.301">https://doi.org/10.1038/emboj.2011.301</a>
  chicago: Schraivogel, Daniel, Lasse Weinmann, Dagmar Beier, Ghazaleh Tabatabai,
    Alexander Eichner, Jia Zhu, Martina Anton, et al. “CAMTA1 Is a Novel Tumour Suppressor
    Regulated by MiR-9/9 * in Glioblastoma Stem Cells.” <i>EMBO Journal</i>. Wiley-Blackwell,
    2011. <a href="https://doi.org/10.1038/emboj.2011.301">https://doi.org/10.1038/emboj.2011.301</a>.
  ieee: D. Schraivogel <i>et al.</i>, “CAMTA1 is a novel tumour suppressor regulated
    by miR-9/9 * in glioblastoma stem cells,” <i>EMBO Journal</i>, vol. 30, no. 20.
    Wiley-Blackwell, pp. 4309–4322, 2011.
  ista: Schraivogel D, Weinmann L, Beier D, Tabatabai G, Eichner A, Zhu J, Anton M,
    Sixt MK, Weller M, Beier C, Meister G. 2011. CAMTA1 is a novel tumour suppressor
    regulated by miR-9/9 * in glioblastoma stem cells. EMBO Journal. 30(20), 4309–4322.
  mla: Schraivogel, Daniel, et al. “CAMTA1 Is a Novel Tumour Suppressor Regulated
    by MiR-9/9 * in Glioblastoma Stem Cells.” <i>EMBO Journal</i>, vol. 30, no. 20,
    Wiley-Blackwell, 2011, pp. 4309–22, doi:<a href="https://doi.org/10.1038/emboj.2011.301">10.1038/emboj.2011.301</a>.
  short: D. Schraivogel, L. Weinmann, D. Beier, G. Tabatabai, A. Eichner, J. Zhu,
    M. Anton, M.K. Sixt, M. Weller, C. Beier, G. Meister, EMBO Journal 30 (2011) 4309–4322.
date_created: 2018-12-11T11:46:55Z
date_published: 2011-10-19T00:00:00Z
date_updated: 2021-01-12T08:01:19Z
day: '19'
department:
- _id: MiSi
doi: 10.1038/emboj.2011.301
external_id:
  pmid:
  - '21857646'
intvolume: '        30'
issue: '20'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3199389/
month: '10'
oa: 1
oa_version: Submitted Version
page: 4309 - 4322
pmid: 1
publication: EMBO Journal
publication_status: published
publisher: Wiley-Blackwell
publist_id: '7301'
quality_controlled: '1'
scopus_import: 1
status: public
title: CAMTA1 is a novel tumour suppressor regulated by miR-9/9 * in glioblastoma
  stem cells
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 30
year: '2011'
...
---
_id: '531'
abstract:
- lang: eng
  text: Software transactional memories (STM) are described in the literature with
    assumptions of sequentially consistent program execution and atomicity of high
    level operations like read, write, and abort. However, in a realistic setting,
    processors use relaxed memory models to optimize hardware performance. Moreover,
    the atomicity of operations depends on the underlying 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 describe RML, a
    simple language for expressing concurrent programs. We develop a semantics of
    RML parametrized by a relaxed memory model. We then present our tool, FOIL, which
    takes as input the RML description of an STM algorithm restricted to two threads
    and two variables, and the description of a memory model, and automatically determines
    the locations of fences, which if inserted, ensure the correctness of the restricted
    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 for two threads and two variables.
    Finally, we extend the verification results for DSTM and TL2 to an arbitrary number
    of threads and variables by manually proving that the structural properties of
    STMs are satisfied at the hardware level of atomicity under the considered relaxed
    memory models.
article_processing_charge: No
article_type: original
author:
- first_name: Rachid
  full_name: Guerraoui, Rachid
  last_name: Guerraoui
- 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: Vasu
  full_name: Singh, Vasu
  id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
  last_name: Singh
citation:
  ama: Guerraoui R, Henzinger TA, Singh V. Verification of STM on relaxed memory models.
    <i>Formal Methods in System Design</i>. 2011;39(3):297-331. doi:<a href="https://doi.org/10.1007/s10703-011-0131-3">10.1007/s10703-011-0131-3</a>
  apa: Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2011). Verification of STM
    on relaxed memory models. <i>Formal Methods in System Design</i>. Springer. <a
    href="https://doi.org/10.1007/s10703-011-0131-3">https://doi.org/10.1007/s10703-011-0131-3</a>
  chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Verification of
    STM on Relaxed Memory Models.” <i>Formal Methods in System Design</i>. Springer,
    2011. <a href="https://doi.org/10.1007/s10703-011-0131-3">https://doi.org/10.1007/s10703-011-0131-3</a>.
  ieee: R. Guerraoui, T. A. Henzinger, and V. Singh, “Verification of STM on relaxed
    memory models,” <i>Formal Methods in System Design</i>, vol. 39, no. 3. Springer,
    pp. 297–331, 2011.
  ista: Guerraoui R, Henzinger TA, Singh V. 2011. Verification of STM on relaxed memory
    models. Formal Methods in System Design. 39(3), 297–331.
  mla: Guerraoui, Rachid, et al. “Verification of STM on Relaxed Memory Models.” <i>Formal
    Methods in System Design</i>, vol. 39, no. 3, Springer, 2011, pp. 297–331, doi:<a
    href="https://doi.org/10.1007/s10703-011-0131-3">10.1007/s10703-011-0131-3</a>.
  short: R. Guerraoui, T.A. Henzinger, V. Singh, Formal Methods in System Design 39
    (2011) 297–331.
date_created: 2018-12-11T11:47:00Z
date_published: 2011-12-01T00:00:00Z
date_updated: 2021-01-12T08:01:27Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/s10703-011-0131-3
intvolume: '        39'
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://infoscience.epfl.ch/record/178042/files/art3A10.10072Fs10703-011-0131-3.pdf
month: '12'
oa: 1
oa_version: Published Version
page: 297 - 331
publication: Formal Methods in System Design
publication_status: published
publisher: Springer
publist_id: '7288'
quality_controlled: '1'
scopus_import: 1
status: public
title: Verification of STM on relaxed memory models
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 39
year: '2011'
...
---
_id: '5379'
abstract:
- lang: eng
  text: Computing the winning set for Büchi objectives in alternating games on graphs
    is a central problem in computer aided verification with a large number of applications.
    The long standing best known upper bound for solving the problem is ̃O(n·m), where
    n is the number of vertices and m is the number of edges in the graph. We are
    the first to break the ̃O(n·m) boundary by presenting a new technique that reduces
    the running time to O(n2). This bound also leads to O(n2) time algorithms for
    computing the set of almost-sure winning vertices for Büchi objectives (1) in
    alternating games with probabilistic transitions (improving an earlier bound of
    O(n·m)), (2) in concurrent graph games with constant actions (improving an earlier
    bound of O(n3)), and (3) in Markov decision processes (improving for m > n4/3
    an earlier bound of O(min(m1.5, m·n2/3)). We also show that the same technique
    can be used to compute the maximal end-component decomposition of a graph in time
    O(n2), which is an improvement over earlier bounds for m > n4/3. Finally, we show
    how to maintain the winning set for Büchi objectives in alternating games under
    a sequence of edge insertions or a sequence of edge deletions in O(n) amortized
    time per operation. This is the first dynamic algorithm for this problem.
alternative_title:
- IST Austria Technical Report
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: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
citation:
  ama: Chatterjee K, Henzinger MH. <i>An O(N2) Time Algorithm for Alternating Büchi
    Games</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0009">10.15479/AT:IST-2011-0009</a>
  apa: Chatterjee, K., &#38; Henzinger, M. H. (2011). <i>An O(n2) time algorithm for
    alternating Büchi games</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0009">https://doi.org/10.15479/AT:IST-2011-0009</a>
  chicago: Chatterjee, Krishnendu, and Monika H Henzinger. <i>An O(N2) Time Algorithm
    for Alternating Büchi Games</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0009">https://doi.org/10.15479/AT:IST-2011-0009</a>.
  ieee: K. Chatterjee and M. H. Henzinger, <i>An O(n2) time algorithm for alternating
    Büchi games</i>. IST Austria, 2011.
  ista: Chatterjee K, Henzinger MH. 2011. An O(n2) time algorithm for alternating
    Büchi games, IST Austria, 20p.
  mla: Chatterjee, Krishnendu, and Monika H. Henzinger. <i>An O(N2) Time Algorithm
    for Alternating Büchi Games</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0009">10.15479/AT:IST-2011-0009</a>.
  short: K. Chatterjee, M.H. Henzinger, An O(N2) Time Algorithm for Alternating Büchi
    Games, IST Austria, 2011.
date_created: 2018-12-12T11:38:59Z
date_published: 2011-07-11T00:00:00Z
date_updated: 2023-02-23T11:15:12Z
day: '11'
ddc:
- '000'
- '004'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0009
file:
- access_level: open_access
  checksum: 0b354264229045d982332fd2cb5b9a26
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:43Z
  date_updated: 2020-07-14T12:46:39Z
  file_id: '5504'
  file_name: IST-2011-0009_IST-2011-0009.pdf
  file_size: 388665
  relation: main_file
file_date_updated: 2020-07-14T12:46:39Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '15'
related_material:
  record:
  - id: '3165'
    relation: later_version
    status: public
status: public
title: An O(n2) time algorithm for alternating Büchi games
type: technical_report
user_id: 6785fbc1-c503-11eb-8a32-93094b40e1cf
year: '2011'
...
---
_id: '5380'
abstract:
- lang: eng
  text: 'We consider 2-player games played on a finite state space for an infinite
    number of rounds.  The games are concurrent: in each round, the two players (player
    1 and player 2) choose their moves independently and simultaneously; the current
    state and the two moves determine the successor state. We study concurrent games
    with ω-regular winning conditions specified as parity objectives.  We consider
    the qualitative analysis problems: the computation of the almost-sure and limit-sure
    winning set of states, where player 1 can ensure to win with probability 1 and
    with probability arbitrarily close to 1, respectively. In general the almost-sure
    and limit-sure winning strategies require both infinite-memory as well as infinite-precision
    (to describe probabilities). We study the bounded-rationality problem for qualitative
    analysis of concurrent parity games, where the strategy set for player 1 is restricted
    to bounded-resource strategies.  In terms of precision, strategies can be deterministic,
    uniform, finite-precision or infinite-precision;  and in terms of memory, strategies
    can be memoryless, finite-memory or infinite-memory. We present a precise and
    complete characterization of the qualitative winning sets for all combinations
    of classes of strategies. In particular, we show that uniform memoryless strategies
    are as powerful as finite-precision infinite-memory strategies, and infinite-precision
    memoryless strategies are as powerful as infinite-precision finite-memory strategies.  We
    show that the winning sets can be computed in O(n2d+3) time, where n is the size
    of the game structure and 2d is the number of priorities (or colors), and our
    algorithms are symbolic. The membership problem of whether a state belongs to
    a winning set can be decided in NP ∩ coNP. While this complexity is the same as
    for the simpler class of turn-based parity games, where in each state only one
    of the two players has a choice of moves, our algorithms,that are obtained by
    characterization of the winning sets as μ-calculus formulas, are considerably
    more involved than those for turn-based games.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
citation:
  ama: Chatterjee K. <i>Bounded Rationality in Concurrent Parity Games</i>. IST Austria;
    2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0008">10.15479/AT:IST-2011-0008</a>
  apa: Chatterjee, K. (2011). <i>Bounded rationality in concurrent parity games</i>.
    IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0008">https://doi.org/10.15479/AT:IST-2011-0008</a>
  chicago: Chatterjee, Krishnendu. <i>Bounded Rationality in Concurrent Parity Games</i>.
    IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0008">https://doi.org/10.15479/AT:IST-2011-0008</a>.
  ieee: K. Chatterjee, <i>Bounded rationality in concurrent parity games</i>. IST
    Austria, 2011.
  ista: Chatterjee K. 2011. Bounded rationality in concurrent parity games, IST Austria,
    53p.
  mla: Chatterjee, Krishnendu. <i>Bounded Rationality in Concurrent Parity Games</i>.
    IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0008">10.15479/AT:IST-2011-0008</a>.
  short: K. Chatterjee, Bounded Rationality in Concurrent Parity Games, IST Austria,
    2011.
date_created: 2018-12-12T11:39:00Z
date_published: 2011-07-11T00:00:00Z
date_updated: 2023-02-23T11:22:53Z
day: '11'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0008
file:
- access_level: open_access
  checksum: 0fd38186409be819a911c4990fa79d1f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:22Z
  date_updated: 2020-07-14T12:46:39Z
  file_id: '5544'
  file_name: IST-2011-0008_IST-2011-0008.pdf
  file_size: 500399
  relation: main_file
file_date_updated: 2020-07-14T12:46:39Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '53'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '16'
related_material:
  record:
  - id: '3338'
    relation: later_version
    status: public
status: public
title: Bounded rationality in concurrent parity games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5381'
abstract:
- lang: eng
  text: "In two-player finite-state stochastic games of partial obser- vation on graphs,
    in every state of the graph, the players simultaneously choose an action, and
    their joint actions determine a probability distri- bution over the successor
    states. The game is played for infinitely many rounds and thus the players construct
    an infinite path in the graph. We consider reachability objectives where the first
    player tries to ensure a target state to be visited almost-surely (i.e., with
    probability 1) or pos- itively (i.e., with positive probability), no matter the
    strategy of the second player.\r\n\r\nWe classify such games according to the
    information and to the power of randomization available to the players. On the
    basis of information, the game can be one-sided with either (a) player 1, or (b)
    player 2 having partial observation (and the other player has perfect observation),
    or two- sided with (c) both players having partial observation. On the basis of
    randomization, (a) the players may not be allowed to use randomization (pure strategies),
    or (b) they may choose a probability distribution over actions but the actual
    random choice is external and not visible to the player (actions invisible), or
    (c) they may use full randomization.\r\n\r\nOur main results for pure strategies
    are as follows: (1) For one-sided games with player 2 perfect observation we show
    that (in contrast to full randomized strategies) belief-based (subset-construction
    based) strate- gies are not sufficient, and present an exponential upper bound
    on mem- ory both for almost-sure and positive winning strategies; we show that
    the problem of deciding the existence of almost-sure and positive winning strategies
    for player 1 is EXPTIME-complete and present symbolic algo- rithms that avoid
    the explicit exponential construction. (2) For one-sided games with player 1 perfect
    observation we show that non-elementary memory is both necessary and sufficient
    for both almost-sure and posi- tive winning strategies. (3) We show that for the
    general (two-sided) case finite-memory strategies are sufficient for both positive
    and almost-sure winning, and at least non-elementary memory is required. We establish
    the equivalence of the almost-sure winning problems for pure strategies and for
    randomized strategies with actions invisible. Our equivalence re- sult exhibit
    serious flaws in previous results in the literature: we show a non-elementary
    memory lower bound for almost-sure winning whereas an exponential upper bound
    was previously claimed."
alternative_title:
- IST Austria Technical Report
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
citation:
  ama: 'Chatterjee K, Doyen L. <i>Partial-Observation Stochastic Games: How to Win
    When Belief Fails</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0007">10.15479/AT:IST-2011-0007</a>'
  apa: 'Chatterjee, K., &#38; Doyen, L. (2011). <i>Partial-observation stochastic
    games: How to win when belief fails</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0007">https://doi.org/10.15479/AT:IST-2011-0007</a>'
  chicago: 'Chatterjee, Krishnendu, and Laurent Doyen. <i>Partial-Observation Stochastic
    Games: How to Win When Belief Fails</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0007">https://doi.org/10.15479/AT:IST-2011-0007</a>.'
  ieee: 'K. Chatterjee and L. Doyen, <i>Partial-observation stochastic games: How
    to win when belief fails</i>. IST Austria, 2011.'
  ista: 'Chatterjee K, Doyen L. 2011. Partial-observation stochastic games: How to
    win when belief fails, IST Austria, 43p.'
  mla: 'Chatterjee, Krishnendu, and Laurent Doyen. <i>Partial-Observation Stochastic
    Games: How to Win When Belief Fails</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0007">10.15479/AT:IST-2011-0007</a>.'
  short: 'K. Chatterjee, L. Doyen, Partial-Observation Stochastic Games: How to Win
    When Belief Fails, IST Austria, 2011.'
date_created: 2018-12-12T11:39:00Z
date_published: 2011-07-05T00:00:00Z
date_updated: 2023-02-23T11:05:48Z
day: '05'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0007
file:
- access_level: open_access
  checksum: 06bf6dfc97f6006e3fd0e9a3f31bc961
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:27Z
  date_updated: 2020-07-14T12:46:39Z
  file_id: '5488'
  file_name: IST-2011-0007_IST-2011-0007.pdf
  file_size: 574055
  relation: main_file
file_date_updated: 2020-07-14T12:46:39Z
has_accepted_license: '1'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: '43'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '17'
related_material:
  record:
  - id: '1903'
    relation: later_version
    status: public
  - id: '2211'
    relation: later_version
    status: public
  - id: '2955'
    relation: later_version
    status: public
status: public
title: 'Partial-observation stochastic games: How to win when belief fails'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5382'
abstract:
- lang: eng
  text: 'We consider two-player stochastic games played on a finite state space for
    an infinite num- ber of rounds. The games are concurrent: in each round, the two
    players (player 1 and player 2) choose their moves independently and simultaneously;
    the current state and the two moves determine a probability distribution over
    the successor states. We also consider the important special case of turn-based
    stochastic games where players make moves in turns, rather than concurrently.
    We study concurrent games with ω-regular winning conditions specified as parity
    objectives. The value for player 1 for a parity objective is the maximal probability
    with which the player can guarantee the satisfaction of the objective against
    all strategies of the opponent. We study the problem of continuity and robustness
    of the value function in concurrent and turn-based stochastic parity games with
    respect to imprecision in the transition probabilities. We present quantitative
    bounds on the difference of the value function (in terms of the imprecision of
    the transition probabilities) and show the value continuity for structurally equivalent
    concurrent games (two games are structurally equivalent if the support of the
    transition func- tion is same and the probabilities differ). We also show robustness
    of optimal strategies for structurally equivalent turn-based stochastic parity
    games. Finally we show that the value continuity property breaks without the structurally
    equivalent assumption (even for Markov chains) and show that our quantitative
    bound is asymptotically optimal. Hence our results are tight (the assumption is
    both necessary and sufficient) and optimal (our quantitative bound is asymptotically
    optimal).'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
citation:
  ama: Chatterjee K. <i>Robustness of Structurally Equivalent Concurrent Parity Games</i>.
    IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0006">10.15479/AT:IST-2011-0006</a>
  apa: Chatterjee, K. (2011). <i>Robustness of structurally equivalent concurrent
    parity games</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0006">https://doi.org/10.15479/AT:IST-2011-0006</a>
  chicago: Chatterjee, Krishnendu. <i>Robustness of Structurally Equivalent Concurrent
    Parity Games</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0006">https://doi.org/10.15479/AT:IST-2011-0006</a>.
  ieee: K. Chatterjee, <i>Robustness of structurally equivalent concurrent parity
    games</i>. IST Austria, 2011.
  ista: Chatterjee K. 2011. Robustness of structurally equivalent concurrent parity
    games, IST Austria, 18p.
  mla: Chatterjee, Krishnendu. <i>Robustness of Structurally Equivalent Concurrent
    Parity Games</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0006">10.15479/AT:IST-2011-0006</a>.
  short: K. Chatterjee, Robustness of Structurally Equivalent Concurrent Parity Games,
    IST Austria, 2011.
date_created: 2018-12-12T11:39:00Z
date_published: 2011-06-27T00:00:00Z
date_updated: 2023-02-23T11:23:01Z
day: '27'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0006
file:
- access_level: open_access
  checksum: 1322b652d6ab07eb5248298a3f91c1cf
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:24Z
  date_updated: 2020-07-14T12:46:40Z
  file_id: '5546'
  file_name: IST-2011-0006_IST-2011-0006.pdf
  file_size: 335997
  relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: '18'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '18'
related_material:
  record:
  - id: '3341'
    relation: later_version
    status: public
status: public
title: Robustness of structurally equivalent concurrent parity games
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5383'
abstract:
- lang: eng
  text: We present a new decidable logic called TREX for expressing constraints about
    imperative tree data structures. In particular, TREX supports a transitive closure
    operator that can express reachability constraints, which often appear in data
    structure invariants. We show that our logic is closed under weakest precondition
    computation, which enables its use for automated software verification. We further
    show that satisfiability of formulas in TREX is decidable in NP. The low complexity
    makes it an attractive alternative to more expensive logics such as monadic second-order
    logic (MSOL) over trees, which have been traditionally used for reasoning about
    tree data structures.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Thomas
  full_name: Wies, Thomas
  id: 447BFB88-F248-11E8-B48F-1D18A9856A87
  last_name: Wies
- first_name: Marco
  full_name: Muñiz, Marco
  last_name: Muñiz
- first_name: Viktor
  full_name: Kuncak, Viktor
  last_name: Kuncak
citation:
  ama: Wies T, Muñiz M, Kuncak V. <i>On an Efficient Decision Procedure for Imperative
    Tree Data Structures</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0005">10.15479/AT:IST-2011-0005</a>
  apa: Wies, T., Muñiz, M., &#38; Kuncak, V. (2011). <i>On an efficient decision procedure
    for imperative tree data structures</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0005">https://doi.org/10.15479/AT:IST-2011-0005</a>
  chicago: Wies, Thomas, Marco Muñiz, and Viktor Kuncak. <i>On an Efficient Decision
    Procedure for Imperative Tree Data Structures</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0005">https://doi.org/10.15479/AT:IST-2011-0005</a>.
  ieee: T. Wies, M. Muñiz, and V. Kuncak, <i>On an efficient decision procedure for
    imperative tree data structures</i>. IST Austria, 2011.
  ista: Wies T, Muñiz M, Kuncak V. 2011. On an efficient decision procedure for imperative
    tree data structures, IST Austria, 25p.
  mla: Wies, Thomas, et al. <i>On an Efficient Decision Procedure for Imperative Tree
    Data Structures</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0005">10.15479/AT:IST-2011-0005</a>.
  short: T. Wies, M. Muñiz, V. Kuncak, On an Efficient Decision Procedure for Imperative
    Tree Data Structures, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-26T00:00:00Z
date_updated: 2023-02-23T11:22:16Z
day: '26'
ddc:
- '000'
- '006'
department:
- _id: ToHe
doi: 10.15479/AT:IST-2011-0005
file:
- access_level: open_access
  checksum: b20029184c4a819c5f4466a4a3d238b5
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:01Z
  date_updated: 2020-07-14T12:46:40Z
  file_id: '5462'
  file_name: IST-2011-0005_IST-2011-0005.pdf
  file_size: 619053
  relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '25'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '19'
related_material:
  record:
  - id: '3323'
    relation: later_version
    status: public
status: public
title: On an efficient decision procedure for imperative tree data structures
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5384'
abstract:
- lang: eng
  text: 'We consider probabilistic automata on infinite words with acceptance defined
    by parity conditions. We consider three qualitative decision problems: (i) the
    positive decision problem asks whether there is a word that is accepted with positive
    probability; (ii) the almost decision problem asks whether there is a word that
    is accepted with probability 1; and (iii) the limit decision problem asks whether
    for every ε > 0 there is a word that is accepted with probability at least 1 −
    ε. We unify and generalize several decidability results for probabilistic automata
    over infinite words, and identify a robust (closed under union and intersection)
    subclass of probabilistic automata for which all the qualitative decision problems
    are decidable for parity conditions. We also show that if the input words are
    restricted to lasso shape words, then the positive and almost problems are decidable
    for all probabilistic automata with parity conditions.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Tracol M. <i>Decidable Problems for Probabilistic Automata on
    Infinite Words</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0004">10.15479/AT:IST-2011-0004</a>
  apa: Chatterjee, K., &#38; Tracol, M. (2011). <i>Decidable problems for probabilistic
    automata on infinite words</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0004">https://doi.org/10.15479/AT:IST-2011-0004</a>
  chicago: Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic
    Automata on Infinite Words</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0004">https://doi.org/10.15479/AT:IST-2011-0004</a>.
  ieee: K. Chatterjee and M. Tracol, <i>Decidable problems for probabilistic automata
    on infinite words</i>. IST Austria, 2011.
  ista: Chatterjee K, Tracol M. 2011. Decidable problems for probabilistic automata
    on infinite words, IST Austria, 30p.
  mla: Chatterjee, Krishnendu, and Mathieu Tracol. <i>Decidable Problems for Probabilistic
    Automata on Infinite Words</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0004">10.15479/AT:IST-2011-0004</a>.
  short: K. Chatterjee, M. Tracol, Decidable Problems for Probabilistic Automata on
    Infinite Words, IST Austria, 2011.
date_created: 2018-12-12T11:39:01Z
date_published: 2011-04-11T00:00:00Z
date_updated: 2023-02-23T11:05:53Z
day: '11'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0004
file:
- access_level: open_access
  checksum: f5a0f664fadc335990f5fcf138df19f1
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:23Z
  date_updated: 2020-07-14T12:46:40Z
  file_id: '5545'
  file_name: IST-2011-004_IST-2011-0004.pdf
  file_size: 570827
  relation: main_file
file_date_updated: 2020-07-14T12:46:40Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '30'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '20'
related_material:
  record:
  - id: '2957'
    relation: later_version
    status: public
status: public
title: Decidable problems for probabilistic automata on infinite words
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5385'
abstract:
- lang: eng
  text: There is recently a significant effort to add quantitative objectives to formal
    verification and synthesis. We introduce and investigate the extension of temporal
    logics with quantitative atomic assertions, aiming for a general and flexible
    framework for quantitative-oriented specifications. In the heart of quantitative
    objectives lies the accumulation of values along a computation. It is either the
    accumulated summation, as with the energy objectives, or the accumulated average,
    as with the mean-payoff objectives. We investigate the extension of temporal logics
    with the prefix-accumulation assertions Sum(v) ≥ c and Avg(v) ≥ c, where v is
    a numeric variable of the system, c is a constant rational number, and Sum(v)
    and Avg(v) denote the accumulated sum and average of the values of v from the
    beginning of the computation up to the current point of time. We also allow the
    path-accumulation assertions LimInfAvg(v) ≥ c and LimSupAvg(v) ≥ c, referring
    to the average value along an entire computation. We study the border of decidability
    for extensions of various temporal logics. In particular, we show that extending
    the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by
    prefix-accumulation assertions and extending LTL with path-accumulation assertions,
    result in temporal logics whose model-checking problem is decidable. The extended
    logics allow to significantly extend the currently known energy and mean-payoff
    objectives. Moreover, the prefix-accumulation assertions may be refined with “controlled-accumulation”,
    allowing, for example, to specify constraints on the average waiting time between
    a request and a grant. On the negative side, we show that the fragment we point
    to is, in a sense, the maximal logic whose extension with prefix-accumulation
    assertions permits a decidable model-checking procedure. Extending a temporal
    logic that has the EG or EU modalities, and in particular CTL and LTL, makes the
    problem undecidable.
alternative_title:
- IST Austria Technical Report
author:
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- 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: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: Boker U, Chatterjee K, Henzinger TA, Kupferman O. <i>Temporal Specifications
    with Accumulative Values</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0003">10.15479/AT:IST-2011-0003</a>
  apa: Boker, U., Chatterjee, K., Henzinger, T. A., &#38; Kupferman, O. (2011). <i>Temporal
    specifications with accumulative values</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0003">https://doi.org/10.15479/AT:IST-2011-0003</a>
  chicago: Boker, Udi, Krishnendu Chatterjee, Thomas A Henzinger, and Orna Kupferman.
    <i>Temporal Specifications with Accumulative Values</i>. IST Austria, 2011. <a
    href="https://doi.org/10.15479/AT:IST-2011-0003">https://doi.org/10.15479/AT:IST-2011-0003</a>.
  ieee: U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, <i>Temporal specifications
    with accumulative values</i>. IST Austria, 2011.
  ista: Boker U, Chatterjee K, Henzinger TA, Kupferman O. 2011. Temporal specifications
    with accumulative values, IST Austria, 14p.
  mla: Boker, Udi, et al. <i>Temporal Specifications with Accumulative Values</i>.
    IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0003">10.15479/AT:IST-2011-0003</a>.
  short: U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications
    with Accumulative Values, IST Austria, 2011.
date_created: 2018-12-12T11:39:02Z
date_published: 2011-04-04T00:00:00Z
date_updated: 2023-02-23T11:23:41Z
day: '04'
ddc:
- '000'
- '004'
department:
- _id: ToHe
- _id: KrCh
doi: 10.15479/AT:IST-2011-0003
ec_funded: 1
file:
- access_level: open_access
  checksum: 8491d0d48c4911620ecd5350b413c11e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:00Z
  date_updated: 2020-07-14T12:46:41Z
  file_id: '5461'
  file_name: IST-2011-0003_IST-2011-0003.pdf
  file_size: 366281
  relation: main_file
file_date_updated: 2020-07-14T12:46:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '04'
oa: 1
oa_version: Published Version
page: '14'
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EFB36C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '215543'
  name: COMponent-Based Embedded Systems design Techniques
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F1337C-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '214373'
  name: Design for Embedded Systems
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '21'
related_material:
  record:
  - id: '2038'
    relation: later_version
    status: public
  - id: '3356'
    relation: later_version
    status: public
status: public
title: Temporal specifications with accumulative values
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5386'
abstract:
- lang: eng
  text: 'We introduce TopoCut: a new way to integrate knowledge about topological
    properties (TPs) into random field image segmentation model. Instead of including
    TPs as additional constraints during minimization of the energy function, we devise
    an efficient algorithm for modifying the unary potentials such that the resulting
    segmentation is guaranteed with the desired properties. Our method is more flexible
    in the sense that it handles more topology constraints than previous methods,
    which were only able to enforce pairwise or global connectivity. In particular,
    our method is very fast, making it for the first time possible to enforce global
    topological properties in practical image segmentation tasks.'
alternative_title:
- IST Austria Technical Report
author:
- first_name: Chao
  full_name: Chen, Chao
  id: 3E92416E-F248-11E8-B48F-1D18A9856A87
  last_name: Chen
- first_name: Daniel
  full_name: Freedman, Daniel
  last_name: Freedman
- first_name: Christoph
  full_name: Lampert, Christoph
  id: 40C20FD2-F248-11E8-B48F-1D18A9856A87
  last_name: Lampert
  orcid: 0000-0001-8622-7887
citation:
  ama: Chen C, Freedman D, Lampert C. <i>Enforcing Topological Constraints in Random
    Field Image Segmentation</i>. IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0002">10.15479/AT:IST-2011-0002</a>
  apa: Chen, C., Freedman, D., &#38; Lampert, C. (2011). <i>Enforcing topological
    constraints in random field image segmentation</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0002">https://doi.org/10.15479/AT:IST-2011-0002</a>
  chicago: Chen, Chao, Daniel Freedman, and Christoph Lampert. <i>Enforcing Topological
    Constraints in Random Field Image Segmentation</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0002">https://doi.org/10.15479/AT:IST-2011-0002</a>.
  ieee: C. Chen, D. Freedman, and C. Lampert, <i>Enforcing topological constraints
    in random field image segmentation</i>. IST Austria, 2011.
  ista: Chen C, Freedman D, Lampert C. 2011. Enforcing topological constraints in
    random field image segmentation, IST Austria, 69p.
  mla: Chen, Chao, et al. <i>Enforcing Topological Constraints in Random Field Image
    Segmentation</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0002">10.15479/AT:IST-2011-0002</a>.
  short: C. Chen, D. Freedman, C. Lampert, Enforcing Topological Constraints in Random
    Field Image Segmentation, IST Austria, 2011.
date_created: 2018-12-12T11:39:02Z
date_published: 2011-03-28T00:00:00Z
date_updated: 2023-02-23T11:22:48Z
day: '28'
ddc:
- '000'
department:
- _id: ChLa
doi: 10.15479/AT:IST-2011-0002
file:
- access_level: open_access
  checksum: ad64c2add5fe2ad10e9d5c669f3f9526
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:34Z
  date_updated: 2020-07-14T12:46:41Z
  file_id: '5495'
  file_name: IST-2011-0002_IST-2011-0002.pdf
  file_size: 26390601
  relation: main_file
file_date_updated: 2020-07-14T12:46:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '69'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '22'
related_material:
  record:
  - id: '3336'
    relation: later_version
    status: public
status: public
title: Enforcing topological constraints in random field image segmentation
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '5387'
abstract:
- lang: eng
  text: We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy
    parity objectives. In system design, the parity objective is used to encode ω-regular
    specifications, and the mean-payoff and energy objectives can be used to model
    quantitative resource constraints. The energy condition re- quires that the resource
    level never drops below 0, and the mean-payoff condi- tion requires that the limit-average
    value of the resource consumption is within a threshold. While these two (energy
    and mean-payoff) classical conditions are equivalent for two-player games, we
    show that they differ for MDPs. We show that the problem of deciding whether a
    state is almost-sure winning (i.e., winning with probability 1) in energy parity
    MDPs is in NP ∩ coNP, while for mean- payoff parity MDPs, the problem is solvable
    in polynomial time, improving a recent PSPACE bound.
alternative_title:
- IST Austria Technical Report
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
citation:
  ama: Chatterjee K, Doyen L. <i>Energy and Mean-Payoff Parity Markov Decision Processes</i>.
    IST Austria; 2011. doi:<a href="https://doi.org/10.15479/AT:IST-2011-0001">10.15479/AT:IST-2011-0001</a>
  apa: Chatterjee, K., &#38; Doyen, L. (2011). <i>Energy and mean-payoff parity Markov
    decision processes</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2011-0001">https://doi.org/10.15479/AT:IST-2011-0001</a>
  chicago: Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity
    Markov Decision Processes</i>. IST Austria, 2011. <a href="https://doi.org/10.15479/AT:IST-2011-0001">https://doi.org/10.15479/AT:IST-2011-0001</a>.
  ieee: K. Chatterjee and L. Doyen, <i>Energy and mean-payoff parity Markov decision
    processes</i>. IST Austria, 2011.
  ista: Chatterjee K, Doyen L. 2011. Energy and mean-payoff parity Markov decision
    processes, IST Austria, 20p.
  mla: Chatterjee, Krishnendu, and Laurent Doyen. <i>Energy and Mean-Payoff Parity
    Markov Decision Processes</i>. IST Austria, 2011, doi:<a href="https://doi.org/10.15479/AT:IST-2011-0001">10.15479/AT:IST-2011-0001</a>.
  short: K. Chatterjee, L. Doyen, Energy and Mean-Payoff Parity Markov Decision Processes,
    IST Austria, 2011.
date_created: 2018-12-12T11:39:02Z
date_published: 2011-02-16T00:00:00Z
date_updated: 2023-02-23T11:23:11Z
day: '16'
ddc:
- '000'
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2011-0001
file:
- access_level: open_access
  checksum: 824d6c70e6d3feb3e836b009e0b3cf73
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:52:57Z
  date_updated: 2020-07-14T12:46:41Z
  file_id: '5458'
  file_name: IST-2011-0001_IST-2011-0001.pdf
  file_size: 329976
  relation: main_file
file_date_updated: 2020-07-14T12:46:41Z
has_accepted_license: '1'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Published Version
page: '20'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '23'
related_material:
  record:
  - id: '3345'
    relation: later_version
    status: public
status: public
title: Energy and mean-payoff parity Markov decision processes
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2011'
...
---
_id: '6496'
abstract:
- lang: eng
  text: We report the switching behavior of the full bacterial flagellum system that
    includes the filament and the motor in wild-type Escherichia coli cells. In sorting
    the motor behavior by the clockwise bias, we find that the distributions of the
    clockwise (CW) and counterclockwise (CCW) intervals are either exponential or
    nonexponential with long tails. At low bias, CW intervals are exponentially distributed
    and CCW intervals exhibit long tails. At intermediate CW bias (0.5) both CW and
    CCW intervals are mainly exponentially distributed. A simple model suggests that
    these two distinct switching behaviors are governed by the presence of signaling
    noise within the chemotaxis network. Low noise yields exponentially distributed
    intervals, whereas large noise yields nonexponential behavior with long tails.
    These drastically different motor statistics may play a role in optimizing bacterial
    behavior for a wide range of environmental conditions.
article_processing_charge: No
author:
- first_name: Heungwon
  full_name: Park, Heungwon
  last_name: Park
- first_name: Panos
  full_name: Oikonomou, Panos
  last_name: Oikonomou
- first_name: Calin C
  full_name: Guet, Calin C
  id: 47F8433E-F248-11E8-B48F-1D18A9856A87
  last_name: Guet
  orcid: 0000-0001-6220-2052
- first_name: Philippe
  full_name: Cluzel, Philippe
  last_name: Cluzel
citation:
  ama: Park H, Oikonomou P, Guet CC, Cluzel P. Noise underlies switching behavior
    of the bacterial flagellum. <i>Biophysical Journal</i>. 2011;101(10):2336-2340.
    doi:<a href="https://doi.org/10.1016/j.bpj.2011.09.040">10.1016/j.bpj.2011.09.040</a>
  apa: Park, H., Oikonomou, P., Guet, C. C., &#38; Cluzel, P. (2011). Noise underlies
    switching behavior of the bacterial flagellum. <i>Biophysical Journal</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.bpj.2011.09.040">https://doi.org/10.1016/j.bpj.2011.09.040</a>
  chicago: Park, Heungwon, Panos Oikonomou, Calin C Guet, and Philippe Cluzel. “Noise
    Underlies Switching Behavior of the Bacterial Flagellum.” <i>Biophysical Journal</i>.
    Elsevier, 2011. <a href="https://doi.org/10.1016/j.bpj.2011.09.040">https://doi.org/10.1016/j.bpj.2011.09.040</a>.
  ieee: H. Park, P. Oikonomou, C. C. Guet, and P. Cluzel, “Noise underlies switching
    behavior of the bacterial flagellum,” <i>Biophysical Journal</i>, vol. 101, no.
    10. Elsevier, pp. 2336–2340, 2011.
  ista: Park H, Oikonomou P, Guet CC, Cluzel P. 2011. Noise underlies switching behavior
    of the bacterial flagellum. Biophysical Journal. 101(10), 2336–2340.
  mla: Park, Heungwon, et al. “Noise Underlies Switching Behavior of the Bacterial
    Flagellum.” <i>Biophysical Journal</i>, vol. 101, no. 10, Elsevier, 2011, pp.
    2336–40, doi:<a href="https://doi.org/10.1016/j.bpj.2011.09.040">10.1016/j.bpj.2011.09.040</a>.
  short: H. Park, P. Oikonomou, C.C. Guet, P. Cluzel, Biophysical Journal 101 (2011)
    2336–2340.
date_created: 2019-05-28T11:54:29Z
date_published: 2011-11-16T00:00:00Z
date_updated: 2021-04-16T11:54:49Z
day: '16'
department:
- _id: CaGu
doi: 10.1016/j.bpj.2011.09.040
external_id:
  pmid:
  - '22098731'
intvolume: '       101'
issue: '10'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3218319/
month: '11'
oa: 1
oa_version: Published Version
page: 2336-2340
pmid: 1
publication: Biophysical Journal
publication_identifier:
  issn:
  - 0006-3495
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Noise underlies switching behavior of the bacterial flagellum
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 101
year: '2011'
...
---
_id: '9483'
abstract:
- lang: eng
  text: Imprinted genes are expressed primarily or exclusively from either the maternal
    or paternal allele, a phenomenon that occurs in flowering plants and mammals.
    Flowering plant imprinted gene expression has been described primarily in endosperm,
    a terminal nutritive tissue consumed by the embryo during seed development or
    after germination. Imprinted expression in Arabidopsis thaliana endosperm is orchestrated
    by differences in cytosine DNA methylation between the paternal and maternal genomes
    as well as by Polycomb group proteins. Currently, only 11 imprinted A. thaliana
    genes are known. Here, we use extensive sequencing of cDNA libraries to identify
    9 paternally expressed and 34 maternally expressed imprinted genes in A. thaliana
    endosperm that are regulated by the DNA-demethylating glycosylase DEMETER, the
    DNA methyltransferase MET1, and/or the core Polycomb group protein FIE. These
    genes encode transcription factors, proteins involved in hormone signaling, components
    of the ubiquitin protein degradation pathway, regulators of histone and DNA methylation,
    and small RNA pathway proteins. We also identify maternally expressed genes that
    may be regulated by unknown mechanisms or deposited from maternal tissues. We
    did not detect any imprinted genes in the embryo. Our results show that imprinted
    gene expression is an extensive mechanistically complex phenomenon that likely
    affects multiple aspects of seed development.
article_processing_charge: No
article_type: original
author:
- first_name: Tzung-Fu
  full_name: Hsieh, Tzung-Fu
  last_name: Hsieh
- first_name: Juhyun
  full_name: Shin, Juhyun
  last_name: Shin
- first_name: Rie
  full_name: Uzawa, Rie
  last_name: Uzawa
- first_name: Pedro
  full_name: Silva, Pedro
  last_name: Silva
- first_name: Stephanie
  full_name: Cohen, Stephanie
  last_name: Cohen
- first_name: Matthew J.
  full_name: Bauer, Matthew J.
  last_name: Bauer
- first_name: Meryl
  full_name: Hashimoto, Meryl
  last_name: Hashimoto
- first_name: Ryan C.
  full_name: Kirkbride, Ryan C.
  last_name: Kirkbride
- first_name: John J.
  full_name: Harada, John J.
  last_name: Harada
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
- first_name: Robert L.
  full_name: Fischer, Robert L.
  last_name: Fischer
citation:
  ama: Hsieh T-F, Shin J, Uzawa R, et al. Regulation of imprinted gene expression
    in Arabidopsis endosperm. <i>Proceedings of the National Academy of Sciences</i>.
    2011;108(5):1755-1762. doi:<a href="https://doi.org/10.1073/pnas.1019273108">10.1073/pnas.1019273108</a>
  apa: Hsieh, T.-F., Shin, J., Uzawa, R., Silva, P., Cohen, S., Bauer, M. J., … Fischer,
    R. L. (2011). Regulation of imprinted gene expression in Arabidopsis endosperm.
    <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences.
    <a href="https://doi.org/10.1073/pnas.1019273108">https://doi.org/10.1073/pnas.1019273108</a>
  chicago: Hsieh, Tzung-Fu, Juhyun Shin, Rie Uzawa, Pedro Silva, Stephanie Cohen,
    Matthew J. Bauer, Meryl Hashimoto, et al. “Regulation of Imprinted Gene Expression
    in Arabidopsis Endosperm.” <i>Proceedings of the National Academy of Sciences</i>.
    National Academy of Sciences, 2011. <a href="https://doi.org/10.1073/pnas.1019273108">https://doi.org/10.1073/pnas.1019273108</a>.
  ieee: T.-F. Hsieh <i>et al.</i>, “Regulation of imprinted gene expression in Arabidopsis
    endosperm,” <i>Proceedings of the National Academy of Sciences</i>, vol. 108,
    no. 5. National Academy of Sciences, pp. 1755–1762, 2011.
  ista: Hsieh T-F, Shin J, Uzawa R, Silva P, Cohen S, Bauer MJ, Hashimoto M, Kirkbride
    RC, Harada JJ, Zilberman D, Fischer RL. 2011. Regulation of imprinted gene expression
    in Arabidopsis endosperm. Proceedings of the National Academy of Sciences. 108(5),
    1755–1762.
  mla: Hsieh, Tzung-Fu, et al. “Regulation of Imprinted Gene Expression in Arabidopsis
    Endosperm.” <i>Proceedings of the National Academy of Sciences</i>, vol. 108,
    no. 5, National Academy of Sciences, 2011, pp. 1755–62, doi:<a href="https://doi.org/10.1073/pnas.1019273108">10.1073/pnas.1019273108</a>.
  short: T.-F. Hsieh, J. Shin, R. Uzawa, P. Silva, S. Cohen, M.J. Bauer, M. Hashimoto,
    R.C. Kirkbride, J.J. Harada, D. Zilberman, R.L. Fischer, Proceedings of the National
    Academy of Sciences 108 (2011) 1755–1762.
date_created: 2021-06-07T07:40:38Z
date_published: 2011-02-01T00:00:00Z
date_updated: 2021-12-14T08:33:49Z
day: '01'
department:
- _id: DaZi
doi: 10.1073/pnas.1019273108
extern: '1'
external_id:
  pmid:
  - '21257907'
intvolume: '       108'
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1073/pnas.1019273108
month: '02'
oa: 1
oa_version: Published Version
page: 1755-1762
pmid: 1
publication: Proceedings of the National Academy of Sciences
publication_identifier:
  eissn:
  - 1091-6490
  issn:
  - 0027-8424
publication_status: published
publisher: National Academy of Sciences
quality_controlled: '1'
scopus_import: '1'
status: public
title: Regulation of imprinted gene expression in Arabidopsis endosperm
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 108
year: '2011'
...
---
_id: '9522'
abstract:
- lang: eng
  text: Little is known about chromatin remodeling events immediately after fertilization.
    A recent report by Autran et al. (2011) in Cell now shows that chromatin regulatory
    pathways that silence transposable elements are responsible for global delayed
    activation of gene expression in the early Arabidopsis embryo.
article_processing_charge: No
author:
- first_name: Daniel
  full_name: Zilberman, Daniel
  id: 6973db13-dd5f-11ea-814e-b3e5455e9ed1
  last_name: Zilberman
  orcid: 0000-0002-0123-8649
citation:
  ama: Zilberman D. <i>Balancing Parental Contributions in Plant Embryonic Gene Activation</i>.
    Vol 20. Elsevier; 2011:735-736. doi:<a href="https://doi.org/10.1016/j.devcel.2011.05.018">10.1016/j.devcel.2011.05.018</a>
  apa: Zilberman, D. (2011). <i>Balancing parental contributions in plant embryonic
    gene activation</i>. <i>Developmental Cell</i> (Vol. 20, pp. 735–736). Elsevier.
    <a href="https://doi.org/10.1016/j.devcel.2011.05.018">https://doi.org/10.1016/j.devcel.2011.05.018</a>
  chicago: Zilberman, Daniel. <i>Balancing Parental Contributions in Plant Embryonic
    Gene Activation</i>. <i>Developmental Cell</i>. Vol. 20. Elsevier, 2011. <a href="https://doi.org/10.1016/j.devcel.2011.05.018">https://doi.org/10.1016/j.devcel.2011.05.018</a>.
  ieee: D. Zilberman, <i>Balancing parental contributions in plant embryonic gene
    activation</i>, vol. 20, no. 6. Elsevier, 2011, pp. 735–736.
  ista: Zilberman D. 2011. Balancing parental contributions in plant embryonic gene
    activation, Elsevier,p.
  mla: Zilberman, Daniel. “Balancing Parental Contributions in Plant Embryonic Gene
    Activation.” <i>Developmental Cell</i>, vol. 20, no. 6, Elsevier, 2011, pp. 735–36,
    doi:<a href="https://doi.org/10.1016/j.devcel.2011.05.018">10.1016/j.devcel.2011.05.018</a>.
  short: D. Zilberman, Balancing Parental Contributions in Plant Embryonic Gene Activation,
    Elsevier, 2011.
date_created: 2021-06-08T06:23:39Z
date_published: 2011-06-14T00:00:00Z
date_updated: 2021-12-14T08:34:37Z
day: '14'
department:
- _id: DaZi
doi: 10.1016/j.devcel.2011.05.018
extern: '1'
external_id:
  pmid:
  - '21664571'
intvolume: '        20'
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1016/j.devcel.2011.05.018
month: '06'
oa: 1
oa_version: Published Version
page: 735-736
pmid: 1
publication: Developmental Cell
publication_identifier:
  eissn:
  - 1878-1551
  issn:
  - 1534-5807
publication_status: published
publisher: Elsevier
quality_controlled: '1'
status: public
title: Balancing parental contributions in plant embryonic gene activation
type: other_academic_publication
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 20
year: '2011'
...
