---
_id: '2517'
abstract:
- lang: eng
  text: 'Traditional formal methods are based on a Boolean satisfaction notion: a
    reactive system satisfies, or not, a given specification. We generalize formal
    methods to also address the quality of systems. As an adequate specification formalism
    we introduce the linear temporal logic LTL[F]. The satisfaction value of an LTL[F]
    formula is a number between 0 and 1, describing the quality of the satisfaction.
    The logic generalizes traditional LTL by augmenting it with a (parameterized)
    set F of arbitrary functions over the interval [0,1]. For example, F may contain
    the maximum or minimum between the satisfaction values of subformulas, their product,
    and their average. The classical decision problems in formal methods, such as
    satisfiability, model checking, and synthesis, are generalized to search and optimization
    problems in the quantitative setting. For example, model checking asks for the
    quality in which a specification is satisfied, and synthesis returns a system
    satisfying the specification with the highest quality. Reasoning about quality
    gives rise to other natural questions, like the distance between specifications.
    We formalize these basic questions and study them for LTL[F]. By extending the
    automata-theoretic approach for LTL to a setting that takes quality into an account,
    we are able to solve the above problems and show that reasoning about LTL[F] has
    roughly the same complexity as reasoning about traditional LTL.'
acknowledgement: This work was supported in part by the Austrian Science Fund NFN
  RiSE (Rigorous Systems Engineering), by the ERC Advanced Grant QUAREM (Quantitative
  Reactive Modeling), and the ERC Grant QUALITY. The full version is available at
  the authors’ URLs.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Shaull
  full_name: Almagor, Shaull
  last_name: Almagor
- first_name: Udi
  full_name: Boker, Udi
  id: 31E297B6-F248-11E8-B48F-1D18A9856A87
  last_name: Boker
- first_name: Orna
  full_name: Kupferman, Orna
  last_name: Kupferman
citation:
  ama: Almagor S, Boker U, Kupferman O. Formalizing and reasoning about quality. 2013;7966(Part
    2):15-27. doi:<a href="https://doi.org/10.1007/978-3-642-39212-2_3">10.1007/978-3-642-39212-2_3</a>
  apa: 'Almagor, S., Boker, U., &#38; Kupferman, O. (2013). Formalizing and reasoning
    about quality. Presented at the ICALP: Automata, Languages and Programming, Riga,
    Latvia: Springer. <a href="https://doi.org/10.1007/978-3-642-39212-2_3">https://doi.org/10.1007/978-3-642-39212-2_3</a>'
  chicago: Almagor, Shaull, Udi Boker, and Orna Kupferman. “Formalizing and Reasoning
    about Quality.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-39212-2_3">https://doi.org/10.1007/978-3-642-39212-2_3</a>.
  ieee: S. Almagor, U. Boker, and O. Kupferman, “Formalizing and reasoning about quality,”
    vol. 7966, no. Part 2. Springer, pp. 15–27, 2013.
  ista: Almagor S, Boker U, Kupferman O. 2013. Formalizing and reasoning about quality.
    7966(Part 2), 15–27.
  mla: Almagor, Shaull, et al. <i>Formalizing and Reasoning about Quality</i>. Vol.
    7966, no. Part 2, Springer, 2013, pp. 15–27, doi:<a href="https://doi.org/10.1007/978-3-642-39212-2_3">10.1007/978-3-642-39212-2_3</a>.
  short: S. Almagor, U. Boker, O. Kupferman, 7966 (2013) 15–27.
conference:
  end_date: 2013-07-12
  location: Riga, Latvia
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2013-07-08
das_tickbox: '1'
date_created: 2018-12-11T11:58:08Z
date_published: 2013-07-01T00:00:00Z
date_updated: 2026-07-28T09:28:40Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-39212-2_3
ec_funded: 1
file:
- access_level: open_access
  checksum: 85afbf6c18a2c7e377c52c9410e2d824
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:16:12Z
  date_updated: 2020-07-14T12:45:42Z
  file_id: '7860'
  file_name: 2013_ICALP_Almagor.pdf
  file_size: 363031
  relation: main_file
file_date_updated: 2020-07-14T12:45:42Z
has_accepted_license: '1'
intvolume: '      7966'
issue: Part 2
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 15 - 27
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_status: published
publisher: Springer
publist_id: '4384'
quality_controlled: '1'
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Formalizing and reasoning about quality
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7966
year: '2013'
...
---
OA_type: free access
_id: '2443'
abstract:
- lang: eng
  text: The mode of action of auxin is based on its non-uniform distribution within
    tissues and organs. Despite the wide use of several auxin analogues in research
    and agriculture, little is known about the specificity of different auxin-related
    transport and signalling processes towards these compounds. Using seedlings of
    Arabidopsis thaliana and suspension-cultured cells of Nicotiana tabacum (BY-2),
    the physiological activity of several auxin analogues was investigated, together
    with their capacity to induce auxin-dependent gene expression, to inhibit endocytosis
    and to be transported across the plasma membrane. This study shows that the specificity
    criteria for different auxin-related processes vary widely. Notably, the special
    behaviour of some synthetic auxin analogues suggests that they might be useful
    tools in investigations of the molecular mechanism of auxin action. Thus, due
    to their differential stimulatory effects on DR5 expression, indole-3-propionic
    (IPA) and 2,4,5-trichlorophenoxy acetic (2,4,5-T) acids can serve in studies of
    TRANSPORT INHIBITOR RESPONSE 1/AUXIN SIGNALLING F-BOX (TIR1/AFB)-mediated auxin
    signalling, and 5-fluoroindole-3-acetic acid (5-F-IAA) can help to discriminate
    between transcriptional and non-transcriptional pathways of auxin signalling.
    The results demonstrate that the major determinants for the auxin-like physiological
    potential of a particular compound are very complex and involve its chemical and
    metabolic stability, its ability to distribute in tissues in a polar manner and
    its activity towards auxin signalling machinery.
acknowledgement: The authors thank Dr Christian Luschnig (University of Natural Resources
  and Life Sciences (BOKU), Vienna, Austria) for the anti-PIN2 antibody, Professor
  Mark Estelle (University of California, San Diego, CA, USA) for tir1-1 mutant seeds
  and, last but not least, to Dr David Morris for critical reading of the manuscript.
  We also thank Markéta Pařezová and Jana Stýblová for excellent technical assistance.
  This work was supported by the Grant Agency of the Czech Republic (P305/11/0797
  to E.Z. and 13-40637S to J.F.), the Central European Institute of Technology project
  CZ.1.05/1.1.00/02.0068 from the European Regional Development Fund and by a European
  Research Council starting independent research grant ERC-2011-StG-20101109-PSDP
  (to J.F.).
article_processing_charge: No
article_type: original
author:
- first_name: Sibu
  full_name: Simon, Sibu
  id: 4542EF9A-F248-11E8-B48F-1D18A9856A87
  last_name: Simon
  orcid: 0000-0002-1998-6741
- first_name: Martin
  full_name: Kubeš, Martin
  last_name: Kubeš
- first_name: Pawel
  full_name: Baster, Pawel
  id: 3028BD74-F248-11E8-B48F-1D18A9856A87
  last_name: Baster
- first_name: Stéphanie
  full_name: Robert, Stéphanie
  last_name: Robert
- first_name: Petre
  full_name: Dobrev, Petre
  last_name: Dobrev
- first_name: Jirí
  full_name: Friml, Jirí
  id: 4159519E-F248-11E8-B48F-1D18A9856A87
  last_name: Friml
  orcid: 0000-0002-8302-7596
- first_name: Jan
  full_name: Petrášek, Jan
  last_name: Petrášek
- first_name: Eva
  full_name: Zažímalová, Eva
  last_name: Zažímalová
citation:
  ama: 'Simon S, Kubeš M, Baster P, et al. Defining the selectivity of processes along
    the auxin response chain: A study using auxin analogues. <i>New Phytologist</i>.
    2013;200(4):1034-1048. doi:<a href="https://doi.org/10.1111/nph.12437">10.1111/nph.12437</a>'
  apa: 'Simon, S., Kubeš, M., Baster, P., Robert, S., Dobrev, P., Friml, J., … Zažímalová,
    E. (2013). Defining the selectivity of processes along the auxin response chain:
    A study using auxin analogues. <i>New Phytologist</i>. Wiley. <a href="https://doi.org/10.1111/nph.12437">https://doi.org/10.1111/nph.12437</a>'
  chicago: 'Simon, Sibu, Martin Kubeš, Pawel Baster, Stéphanie Robert, Petre Dobrev,
    Jiří Friml, Jan Petrášek, and Eva Zažímalová. “Defining the Selectivity of Processes
    along the Auxin Response Chain: A Study Using Auxin Analogues.” <i>New Phytologist</i>.
    Wiley, 2013. <a href="https://doi.org/10.1111/nph.12437">https://doi.org/10.1111/nph.12437</a>.'
  ieee: 'S. Simon <i>et al.</i>, “Defining the selectivity of processes along the
    auxin response chain: A study using auxin analogues,” <i>New Phytologist</i>,
    vol. 200, no. 4. Wiley, pp. 1034–1048, 2013.'
  ista: 'Simon S, Kubeš M, Baster P, Robert S, Dobrev P, Friml J, Petrášek J, Zažímalová
    E. 2013. Defining the selectivity of processes along the auxin response chain:
    A study using auxin analogues. New Phytologist. 200(4), 1034–1048.'
  mla: 'Simon, Sibu, et al. “Defining the Selectivity of Processes along the Auxin
    Response Chain: A Study Using Auxin Analogues.” <i>New Phytologist</i>, vol. 200,
    no. 4, Wiley, 2013, pp. 1034–48, doi:<a href="https://doi.org/10.1111/nph.12437">10.1111/nph.12437</a>.'
  short: S. Simon, M. Kubeš, P. Baster, S. Robert, P. Dobrev, J. Friml, J. Petrášek,
    E. Zažímalová, New Phytologist 200 (2013) 1034–1048.
das_tickbox: '1'
date_created: 2018-12-11T11:57:41Z
date_published: 2013-12-01T00:00:00Z
date_updated: 2026-07-28T09:29:45Z
day: '01'
ddc:
- '580'
department:
- _id: JiFr
doi: 10.1111/nph.12437
ec_funded: 1
external_id:
  isi:
  - '000330955300012'
intvolume: '       200'
isi: 1
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1111/nph.12437
month: '12'
oa: 1
oa_version: Published Version
page: 1034 - 1048
project:
- _id: 25716A02-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '282300'
  name: Polarity and subcellular dynamics in plants
publication: New Phytologist
publication_status: published
publisher: Wiley
publist_id: '4460'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Defining the selectivity of processes along the auxin response chain: A study
  using auxin analogues'
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 200
year: '2013'
...
---
_id: '2181'
abstract:
- lang: eng
  text: 'There is a trade-off between performance and correctness in implementing
    concurrent data structures. Better performance may be achieved at the expense
    of relaxing correctness, by redefining the semantics of data structures. We address
    such a redefinition of data structure semantics and present a systematic and formal
    framework for obtaining new data structures by quantitatively relaxing existing
    ones. We view a data structure as a sequential specification S containing all
    &quot;legal&quot; sequences over an alphabet of method calls. Relaxing the data
    structure corresponds to defining a distance from any sequence over the alphabet
    to the sequential specification: the k-relaxed sequential specification contains
    all sequences over the alphabet within distance k from the original specification.
    In contrast to other existing work, our relaxations are semantic (distance in
    terms of data structure states). As an instantiation of our framework, we present
    two simple yet generic relaxation schemes, called out-of-order and stuttering
    relaxation, along with several ways of computing distances. We show that the out-of-order
    relaxation, when further instantiated to stacks, queues, and priority queues,
    amounts to tolerating bounded out-of-order behavior, which cannot be captured
    by a purely syntactic relaxation (distance in terms of sequence manipulation,
    e.g. edit distance). We give concurrent implementations of relaxed data structures
    and demonstrate that bounded relaxations provide the means for trading correctness
    for performance in a controlled way. The relaxations are monotonic which further
    highlights the trade-off: increasing k increases the number of permitted sequences,
    which as we demonstrate can lead to better performance. Finally, since a relaxed
    stack or queue also implements a pool, we actually have new concurrent pool implementations
    that outperform the state-of-the-art ones.'
acknowledgement: "This work has been supported by the European Research Council\r\nadvanced
  grant QUAREM, the National Research Network RiSE\r\non Rigorous Systems Engineering
  (Austrian Science Fund S11404-\r\nN23), and an Elise Richter Fellowship (Austrian
  Science Fund\r\nV00125). We thank the anonymous referees for their constructive\r\nand
  inspiring comments and suggestions. Ana Sokolova wishes to\r\nthank Dexter Kozen
  and in particular Joel Ouaknine: had they not\r\nsaved her life, she would have
  missed a lot of the fun involved in\r\nworking on this paper and seeing it finished."
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Hannes
  full_name: Payer, Hannes
  last_name: Payer
- first_name: Ali
  full_name: Sezgin, Ali
  id: 4C7638DA-F248-11E8-B48F-1D18A9856A87
  last_name: Sezgin
- first_name: Ana
  full_name: Sokolova, Ana
  last_name: Sokolova
citation:
  ama: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. Quantitative relaxation
    of concurrent data structures. In: <i>Proceedings of the 40th Annual ACM SIGPLAN-SIGACT
    Symposium on Principles of Programming Language</i>. ACM; 2013:317-328. doi:<a
    href="https://doi.org/10.1145/2429069.2429109">10.1145/2429069.2429109</a>'
  apa: 'Henzinger, T. A., Kirsch, C., Payer, H., Sezgin, A., &#38; Sokolova, A. (2013).
    Quantitative relaxation of concurrent data structures. In <i>Proceedings of the
    40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming language</i>
    (pp. 317–328). Rome, Italy: ACM. <a href="https://doi.org/10.1145/2429069.2429109">https://doi.org/10.1145/2429069.2429109</a>'
  chicago: Henzinger, Thomas A, Christoph Kirsch, Hannes Payer, Ali Sezgin, and Ana
    Sokolova. “Quantitative Relaxation of Concurrent Data Structures.” In <i>Proceedings
    of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language</i>,
    317–28. ACM, 2013. <a href="https://doi.org/10.1145/2429069.2429109">https://doi.org/10.1145/2429069.2429109</a>.
  ieee: T. A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, and A. Sokolova, “Quantitative
    relaxation of concurrent data structures,” in <i>Proceedings of the 40th annual
    ACM SIGPLAN-SIGACT symposium on Principles of programming language</i>, Rome,
    Italy, 2013, pp. 317–328.
  ista: 'Henzinger TA, Kirsch C, Payer H, Sezgin A, Sokolova A. 2013. Quantitative
    relaxation of concurrent data structures. Proceedings of the 40th annual ACM SIGPLAN-SIGACT
    symposium on Principles of programming language. POPL: Principles of Programming
    Languages, 317–328.'
  mla: Henzinger, Thomas A., et al. “Quantitative Relaxation of Concurrent Data Structures.”
    <i>Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of
    Programming Language</i>, ACM, 2013, pp. 317–28, doi:<a href="https://doi.org/10.1145/2429069.2429109">10.1145/2429069.2429109</a>.
  short: T.A. Henzinger, C. Kirsch, H. Payer, A. Sezgin, A. Sokolova, in:, Proceedings
    of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language,
    ACM, 2013, pp. 317–328.
conference:
  end_date: 2013-01-25
  location: Rome, Italy
  name: 'POPL: Principles of Programming Languages'
  start_date: 2013-01-23
corr_author: '1'
date_created: 2018-12-11T11:56:11Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2026-07-28T11:18:47Z
day: '01'
ddc:
- '000'
- '004'
department:
- _id: ToHe
doi: 10.1145/2429069.2429109
ec_funded: 1
file:
- access_level: open_access
  checksum: adf465e70948f4e80e48057524516456
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:33Z
  date_updated: 2020-07-14T12:45:31Z
  file_id: '5086'
  file_name: IST-2014-198-v1+1_popl128-henzinger-clean.pdf
  file_size: 294689
  relation: main_file
file_date_updated: 2020-07-14T12:45:31Z
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 317 - 328
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
publication: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles
  of programming language
publication_identifier:
  isbn:
  - 978-1-4503-1832-7
publication_status: published
publisher: ACM
publist_id: '4801'
pubrep_id: '198'
quality_controlled: '1'
related_material:
  record:
  - id: '10901'
    relation: later_version
    status: deleted
scopus_import: '1'
status: public
title: Quantitative relaxation of concurrent data structures
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
OA_place: repository
OA_type: green
_id: '1385'
abstract:
- lang: eng
  text: It is often difficult to correctly implement a Boolean controller for a complex
    system, especially when concurrency is involved. Yet, it may be easy to formally
    specify a controller. For instance, for a pipelined processor it suffices to state
    that the visible behavior of the pipelined system should be identical to a non-pipelined
    reference system (Burch-Dill paradigm). We present a novel procedure to efficiently
    synthesize multiple Boolean control signals from a specification given as a quantified
    first-order formula (with a specific quantifier structure). Our approach uses
    uninterpreted functions to abstract details of the design. We construct an unsatisfiable
    SMT formula from the given specification. Then, from just one proof of unsatisfiability,
    we use a variant of Craig interpolation to compute multiple coordinated interpolants
    that implement the Boolean control signals. Our method avoids iterative learning
    and back-substitution of the control functions. We applied our approach to synthesize
    a controller for a simple two-stage pipelined processor, and present first experimental
    results.
acknowledgement: "This research was supported by the European Commission through project\r\nDIAMOND
  (FP7-2009-IST-4-248613), the Austrian Science Fund (FWF)\r\nthrough projects RiSE
  (S11406-N23) and QUAINT (I774-N23), and ERC\r\nAdvanced Grant QUAREM (Quantitative
  Reactive Modeling)"
article_processing_charge: No
arxiv: 1
author:
- first_name: Georg
  full_name: Hofferek, Georg
  last_name: Hofferek
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Bettina
  full_name: Könighofer, Bettina
  last_name: Könighofer
- first_name: Jie
  full_name: Jiang, Jie
  last_name: Jiang
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
citation:
  ama: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. Synthesizing multiple
    boolean functions using interpolation on a single proof. In: <i>2013 Formal Methods
    in Computer-Aided Design</i>. IEEE; 2013:77-84. doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a>'
  apa: 'Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., &#38; Bloem, R. (2013).
    Synthesizing multiple boolean functions using interpolation on a single proof.
    In <i>2013 Formal Methods in Computer-Aided Design</i> (pp. 77–84). Portland,
    OR, United States: IEEE. <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a>'
  chicago: Hofferek, Georg, Ashutosh Gupta, Bettina Könighofer, Jie Jiang, and Roderick
    Bloem. “Synthesizing Multiple Boolean Functions Using Interpolation on a Single
    Proof.” In <i>2013 Formal Methods in Computer-Aided Design</i>, 77–84. IEEE, 2013.
    <a href="https://doi.org/10.1109/FMCAD.2013.6679394">https://doi.org/10.1109/FMCAD.2013.6679394</a>.
  ieee: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, and R. Bloem, “Synthesizing
    multiple boolean functions using interpolation on a single proof,” in <i>2013
    Formal Methods in Computer-Aided Design</i>, Portland, OR, United States, 2013,
    pp. 77–84.
  ista: 'Hofferek G, Gupta A, Könighofer B, Jiang J, Bloem R. 2013. Synthesizing multiple
    boolean functions using interpolation on a single proof. 2013 Formal Methods in
    Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 77–84.'
  mla: Hofferek, Georg, et al. “Synthesizing Multiple Boolean Functions Using Interpolation
    on a Single Proof.” <i>2013 Formal Methods in Computer-Aided Design</i>, IEEE,
    2013, pp. 77–84, doi:<a href="https://doi.org/10.1109/FMCAD.2013.6679394">10.1109/FMCAD.2013.6679394</a>.
  short: G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal
    Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
conference:
  end_date: 2013-10-23
  location: Portland, OR, United States
  name: 'FMCAD: Formal Methods in Computer-Aided Design'
  start_date: 2013-10-20
das_tickbox: '1'
date_created: 2018-12-11T11:51:43Z
date_published: 2013-12-11T00:00:00Z
date_updated: 2026-07-28T11:20:30Z
day: '11'
department:
- _id: ToHe
doi: 10.1109/FMCAD.2013.6679394
ec_funded: 1
external_id:
  arxiv:
  - '1308.4767'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1308.4767
month: '12'
oa: 1
oa_version: Preprint
page: 77 - 84
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: 2013 Formal Methods in Computer-Aided Design
publication_status: published
publisher: IEEE
publist_id: '5825'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesizing multiple boolean functions using interpolation on a single proof
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2013'
...
---
OA_place: publisher
OA_type: free access
_id: '11087'
abstract:
- lang: eng
  text: Intracellular proteins with long lifespans have recently been linked to age-dependent
    defects, ranging from decreased fertility to the functional decline of neurons.
    Why long-lived proteins exist in metabolically active cellular environments and
    how they are maintained over time remains poorly understood. Here, we provide
    a system-wide identification of proteins with exceptional lifespans in the rat
    brain. These proteins are inefficiently replenished despite being translated robustly
    throughout adulthood. Using nucleoporins as a paradigm for long-term protein persistence,
    we found that nuclear pore complexes (NPCs) are maintained over a cell’s life
    through slow but finite exchange of even its most stable subcomplexes. This maintenance
    is limited, however, as some nucleoporin levels decrease during aging, providing
    a rationale for the previously observed age-dependent deterioration of NPC function.
    Our identification of a long-lived proteome reveals cellular components that are
    at increased risk for damage accumulation, linking long-term protein persistence
    to the cellular aging process.
article_processing_charge: No
article_type: original
author:
- first_name: Brandon H.
  full_name: Toyama, Brandon H.
  last_name: Toyama
- first_name: Jeffrey N.
  full_name: Savas, Jeffrey N.
  last_name: Savas
- first_name: Sung Kyu
  full_name: Park, Sung Kyu
  last_name: Park
- first_name: Michael S.
  full_name: Harris, Michael S.
  last_name: Harris
- first_name: Nicholas T.
  full_name: Ingolia, Nicholas T.
  last_name: Ingolia
- first_name: John R.
  full_name: Yates, John R.
  last_name: Yates
- first_name: Martin W
  full_name: HETZER, Martin W
  id: 86c0d31b-b4eb-11ec-ac5a-eae7b2e135ed
  last_name: HETZER
  orcid: 0000-0002-2111-992X
citation:
  ama: Toyama BH, Savas JN, Park SK, et al. Identification of long-lived proteins
    reveals exceptional stability of essential cellular structures. <i>Cell</i>. 2013;154(5):971-982.
    doi:<a href="https://doi.org/10.1016/j.cell.2013.07.037">10.1016/j.cell.2013.07.037</a>
  apa: Toyama, B. H., Savas, J. N., Park, S. K., Harris, M. S., Ingolia, N. T., Yates,
    J. R., &#38; Hetzer, M. (2013). Identification of long-lived proteins reveals
    exceptional stability of essential cellular structures. <i>Cell</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.cell.2013.07.037">https://doi.org/10.1016/j.cell.2013.07.037</a>
  chicago: Toyama, Brandon H., Jeffrey N. Savas, Sung Kyu Park, Michael S. Harris,
    Nicholas T. Ingolia, John R. Yates, and Martin Hetzer. “Identification of Long-Lived
    Proteins Reveals Exceptional Stability of Essential Cellular Structures.” <i>Cell</i>.
    Elsevier, 2013. <a href="https://doi.org/10.1016/j.cell.2013.07.037">https://doi.org/10.1016/j.cell.2013.07.037</a>.
  ieee: B. H. Toyama <i>et al.</i>, “Identification of long-lived proteins reveals
    exceptional stability of essential cellular structures,” <i>Cell</i>, vol. 154,
    no. 5. Elsevier, pp. 971–982, 2013.
  ista: Toyama BH, Savas JN, Park SK, Harris MS, Ingolia NT, Yates JR, Hetzer M. 2013.
    Identification of long-lived proteins reveals exceptional stability of essential
    cellular structures. Cell. 154(5), 971–982.
  mla: Toyama, Brandon H., et al. “Identification of Long-Lived Proteins Reveals Exceptional
    Stability of Essential Cellular Structures.” <i>Cell</i>, vol. 154, no. 5, Elsevier,
    2013, pp. 971–82, doi:<a href="https://doi.org/10.1016/j.cell.2013.07.037">10.1016/j.cell.2013.07.037</a>.
  short: B.H. Toyama, J.N. Savas, S.K. Park, M.S. Harris, N.T. Ingolia, J.R. Yates,
    M. Hetzer, Cell 154 (2013) 971–982.
das_tickbox: '1'
date_created: 2022-04-07T07:51:08Z
date_published: 2013-08-29T00:00:00Z
date_updated: 2026-07-28T10:15:26Z
day: '29'
department:
- _id: MaHe
doi: 10.1016/j.cell.2013.07.037
extern: '1'
external_id:
  pmid:
  - '23993091'
intvolume: '       154'
issue: '5'
keyword:
- General Biochemistry
- Genetics and Molecular Biology
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1016/j.cell.2013.07.037
month: '08'
oa: 1
oa_version: Published Version
page: 971-982
pmid: 1
publication: Cell
publication_identifier:
  issn:
  - 0092-8674
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Identification of long-lived proteins reveals exceptional stability of essential
  cellular structures
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 154
year: '2013'
...
---
_id: '2237'
abstract:
- lang: eng
  text: We describe new extensions of the Vampire theorem prover for computing tree
    interpolants. These extensions generalize Craig interpolation in Vampire, and
    can also be used to derive sequence interpolants. We evaluated our implementation
    on a large number of examples over the theory of linear integer arithmetic and
    integer-indexed arrays, with and without quantifiers. When compared to other methods,
    our experiments show that some examples could only be solved by our implementation.
acknowledgement: This research was partly supported by the Austrian National Research
  Network RiSE (FWF grants S11402-N23 and S11410-N23) and the WWTF PROSEED grant (ICT
  C-050).
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Régis
  full_name: Blanc, Régis
  last_name: Blanc
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
citation:
  ama: Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181.
    doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a>
  apa: 'Blanc, R., Gupta, A., Kovács, L., &#38; Kragl, B. (2013). Tree interpolation
    in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence,
    and Reasoning, Stellenbosch, South Africa: Springer. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a>'
  chicago: Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation
    in Vampire.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a>.
  ieee: R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,”
    vol. 8312. Springer, pp. 173–181, 2013.
  ista: Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire.
    8312, 173–181.
  mla: Blanc, Régis, et al. <i>Tree Interpolation in Vampire</i>. Vol. 8312, Springer,
    2013, pp. 173–81, doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a>.
  short: R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
conference:
  end_date: 2013-12-19
  location: Stellenbosch, South Africa
  name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
  start_date: 2013-12-14
das_tickbox: '1'
date_created: 2018-12-11T11:56:29Z
date_published: 2013-01-14T00:00:00Z
date_updated: 2026-07-28T10:10:38Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-45221-5_13
file:
- access_level: open_access
  checksum: 9cebaafca032e6769d273f393305c705
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:10:40Z
  date_updated: 2020-07-14T12:45:34Z
  file_id: '7858'
  file_name: 2013_LPAR_Blanc.pdf
  file_size: 279206
  relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: '      8312'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 173 - 181
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '4724'
quality_controlled: '1'
scopus_import: '1'
series_title: Lecture Notes in Computer Science
status: public
title: Tree interpolation in Vampire
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8312
year: '2013'
...
---
OA_place: publisher
_id: '1406'
abstract:
- lang: eng
  text: Epithelial spreading is a critical part of various developmental and wound
    repair processes. Here we use zebrafish epiboly as a model system to study the
    cellular and molecular mechanisms underlying the spreading of epithelial sheets.
    During zebrafish epiboly the enveloping cell layer (EVL), a simple squamous epithelium,
    spreads over the embryo to eventually cover the entire yolk cell by the end of
    gastrulation. The EVL leading edge is anchored through tight junctions to the
    yolk syncytial layer (YSL), where directly adjacent to the EVL margin a contractile
    actomyosin ring is formed that is thought to drive EVL epiboly. The prevalent
    view in the field was that the contractile ring exerts a pulling force on the
    EVL margin, which pulls the EVL towards the vegetal pole. However, how this force
    is generated and how it affects EVL morphology still remains elusive. Moreover,
    the cellular mechanisms mediating the increase in EVL surface area, while maintaining
    tissue integrity and function are still unclear. Here we show that the YSL actomyosin
    ring pulls on the EVL margin by two distinct force-generating mechanisms. One
    mechanism is based on contraction of the ring around its circumference, as previously
    proposed. The second mechanism is based on actomyosin retrogade flows, generating
    force through resistance against the substrate. The latter can function at any
    epiboly stage even in situations where the contraction-based mechanism is unproductive.
    Additionally, we demonstrate that during epiboly the EVL is subjected to anisotropic
    tension, which guides the orientation of EVL cell division along the main axis
    (animal-vegetal) of tension. The influence of tension in cell division orientation
    involves cell elongation and requires myosin-2 activity for proper spindle alignment.
    Strikingly, we reveal that tension-oriented cell divisions release anisotropic
    tension within the EVL and that in the absence of such divisions, EVL cells undergo
    ectopic fusions. We conclude that forces applied to the EVL by the action of the
    YSL actomyosin ring generate a tension anisotropy in the EVL that orients cell
    divisions, which in turn limit tissue tension increase thereby facilitating tissue
    spreading.
acknowledged_ssus:
- _id: Bio
- _id: PreCl
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Pedro
  full_name: Campinho, Pedro
  id: 3AFBBC42-F248-11E8-B48F-1D18A9856A87
  last_name: Campinho
  orcid: 0000-0002-8526-5416
citation:
  ama: 'Campinho P. Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading. 2013.'
  apa: 'Campinho, P. (2013). <i>Mechanics of zebrafish epiboly: Tension-oriented cell
    divisions limit anisotropic tissue tension in epithelial spreading</i>. Institute
    of Science and Technology Austria.'
  chicago: 'Campinho, Pedro. “Mechanics of Zebrafish Epiboly: Tension-Oriented Cell
    Divisions Limit Anisotropic Tissue Tension in Epithelial Spreading.” Institute
    of Science and Technology Austria, 2013.'
  ieee: 'P. Campinho, “Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading,” Institute of Science
    and Technology Austria, 2013.'
  ista: 'Campinho P. 2013. Mechanics of zebrafish epiboly: Tension-oriented cell divisions
    limit anisotropic tissue tension in epithelial spreading. Institute of Science
    and Technology Austria.'
  mla: 'Campinho, Pedro. <i>Mechanics of Zebrafish Epiboly: Tension-Oriented Cell
    Divisions Limit Anisotropic Tissue Tension in Epithelial Spreading</i>. Institute
    of Science and Technology Austria, 2013.'
  short: 'P. Campinho, Mechanics of Zebrafish Epiboly: Tension-Oriented Cell Divisions
    Limit Anisotropic Tissue Tension in Epithelial Spreading, Institute of Science
    and Technology Austria, 2013.'
corr_author: '1'
date_created: 2018-12-11T11:51:50Z
date_published: 2013-10-01T00:00:00Z
date_updated: 2026-07-29T10:00:09Z
day: '01'
degree_awarded: PhD
department:
- _id: CaHe
- _id: GradSch
doi_confirm: '1'
language:
- iso: eng
month: '10'
oa_version: None
page: '123'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5801'
status: public
supervisor:
- first_name: Carl-Philipp J
  full_name: Heisenberg, Carl-Philipp J
  id: 39427864-F248-11E8-B48F-1D18A9856A87
  last_name: Heisenberg
  orcid: 0000-0002-0912-4566
title: 'Mechanics of zebrafish epiboly: Tension-oriented cell divisions limit anisotropic
  tissue tension in epithelial spreading'
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2013'
...
---
_id: '2282'
abstract:
- lang: eng
  text: Epithelial spreading is a common and fundamental aspect of various developmental
    and disease-related processes such as epithelial closure and wound healing. A
    key challenge for epithelial tissues undergoing spreading is to increase their
    surface area without disrupting epithelial integrity. Here we show that orienting
    cell divisions by tension constitutes an efficient mechanism by which the enveloping
    cell layer (EVL) releases anisotropic tension while undergoing spreading during
    zebrafish epiboly. The control of EVL cell-division orientation by tension involves
    cell elongation and requires myosin II activity to align the mitotic spindle with
    the main tension axis. We also found that in the absence of tension-oriented cell
    divisions and in the presence of increased tissue tension, EVL cells undergo ectopic
    fusions, suggesting that the reduction of tension anisotropy by oriented cell
    divisions is required to prevent EVL cells from fusing. We conclude that cell-division
    orientation by tension constitutes a key mechanism for limiting tension anisotropy
    and thus promoting tissue spreading during EVL epiboly.
acknowledged_ssus:
- _id: PreCl
- _id: Bio
acknowledgement: 'This work was supported by the IST Austria and MPI-CBG '
article_processing_charge: No
author:
- first_name: Pedro
  full_name: Campinho, Pedro
  id: 3AFBBC42-F248-11E8-B48F-1D18A9856A87
  last_name: Campinho
  orcid: 0000-0002-8526-5416
- first_name: Martin
  full_name: Behrndt, Martin
  id: 3ECECA3A-F248-11E8-B48F-1D18A9856A87
  last_name: Behrndt
- first_name: Jonas
  full_name: Ranft, Jonas
  last_name: Ranft
- first_name: Thomas
  full_name: Risler, Thomas
  last_name: Risler
- first_name: Nicolas
  full_name: Minc, Nicolas
  last_name: Minc
- first_name: Carl-Philipp J
  full_name: Heisenberg, Carl-Philipp J
  id: 39427864-F248-11E8-B48F-1D18A9856A87
  last_name: Heisenberg
  orcid: 0000-0002-0912-4566
citation:
  ama: Campinho P, Behrndt M, Ranft J, Risler T, Minc N, Heisenberg C-PJ. Tension-oriented
    cell divisions limit anisotropic tissue tension in epithelial spreading during
    zebrafish epiboly. <i>Nature Cell Biology</i>. 2013;15:1405-1414. doi:<a href="https://doi.org/10.1038/ncb2869">10.1038/ncb2869</a>
  apa: Campinho, P., Behrndt, M., Ranft, J., Risler, T., Minc, N., &#38; Heisenberg,
    C.-P. J. (2013). Tension-oriented cell divisions limit anisotropic tissue tension
    in epithelial spreading during zebrafish epiboly. <i>Nature Cell Biology</i>.
    Nature Publishing Group. <a href="https://doi.org/10.1038/ncb2869">https://doi.org/10.1038/ncb2869</a>
  chicago: Campinho, Pedro, Martin Behrndt, Jonas Ranft, Thomas Risler, Nicolas Minc,
    and Carl-Philipp J Heisenberg. “Tension-Oriented Cell Divisions Limit Anisotropic
    Tissue Tension in Epithelial Spreading during Zebrafish Epiboly.” <i>Nature Cell
    Biology</i>. Nature Publishing Group, 2013. <a href="https://doi.org/10.1038/ncb2869">https://doi.org/10.1038/ncb2869</a>.
  ieee: P. Campinho, M. Behrndt, J. Ranft, T. Risler, N. Minc, and C.-P. J. Heisenberg,
    “Tension-oriented cell divisions limit anisotropic tissue tension in epithelial
    spreading during zebrafish epiboly,” <i>Nature Cell Biology</i>, vol. 15. Nature
    Publishing Group, pp. 1405–1414, 2013.
  ista: Campinho P, Behrndt M, Ranft J, Risler T, Minc N, Heisenberg C-PJ. 2013. Tension-oriented
    cell divisions limit anisotropic tissue tension in epithelial spreading during
    zebrafish epiboly. Nature Cell Biology. 15, 1405–1414.
  mla: Campinho, Pedro, et al. “Tension-Oriented Cell Divisions Limit Anisotropic
    Tissue Tension in Epithelial Spreading during Zebrafish Epiboly.” <i>Nature Cell
    Biology</i>, vol. 15, Nature Publishing Group, 2013, pp. 1405–14, doi:<a href="https://doi.org/10.1038/ncb2869">10.1038/ncb2869</a>.
  short: P. Campinho, M. Behrndt, J. Ranft, T. Risler, N. Minc, C.-P.J. Heisenberg,
    Nature Cell Biology 15 (2013) 1405–1414.
corr_author: '1'
date_created: 2018-12-11T11:56:45Z
date_published: 2013-11-10T00:00:00Z
date_updated: 2026-07-29T10:07:18Z
day: '10'
department:
- _id: CaHe
doi: 10.1038/ncb2869
external_id:
  isi:
  - '000327944200005'
intvolume: '        15'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://hal.upmc.fr/hal-00983313/
month: '11'
oa: 1
oa_version: Submitted Version
page: 1405 - 1414
project:
- _id: 252ABD0A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: I930-B20
  name: Control of Epithelial Cell Layer Spreading in Zebrafish
publication: Nature Cell Biology
publication_status: published
publisher: Nature Publishing Group
publist_id: '4652'
quality_controlled: '1'
related_material:
  record:
  - id: '1403'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Tension-oriented cell divisions limit anisotropic tissue tension in epithelial
  spreading during zebrafish epiboly
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 15
year: '2013'
...
---
_id: '2247'
abstract:
- lang: eng
  text: Cooperative behavior, where one individual incurs a cost to help another,
    is a wide spread phenomenon. Here we study direct reciprocity in the context of
    the alternating Prisoner's Dilemma. We consider all strategies that can be implemented
    by one and two-state automata. We calculate the payoff matrix of all pairwise
    encounters in the presence of noise. We explore deterministic selection dynamics
    with and without mutation. Using different error rates and payoff values, we observe
    convergence to a small number of distinct equilibria. Two of them are uncooperative
    strict Nash equilibria representing always-defect (ALLD) and Grim. The third equilibrium
    is mixed and represents a cooperative alliance of several strategies, dominated
    by a strategy which we call Forgiver. Forgiver cooperates whenever the opponent
    has cooperated; it defects once when the opponent has defected, but subsequently
    Forgiver attempts to re-establish cooperation even if the opponent has defected
    again. Forgiver is not an evolutionarily stable strategy, but the alliance, which
    it rules, is asymptotically stable. For a wide range of parameter values the most
    commonly observed outcome is convergence to the mixed equilibrium, dominated by
    Forgiver. Our results show that although forgiving might incur a short-term loss
    it can lead to a long-term gain. Forgiveness facilitates stable cooperation in
    the presence of exploitation and noise.
article_number: e80814
article_processing_charge: No
author:
- first_name: Benjamin
  full_name: Zagorsky, Benjamin
  last_name: Zagorsky
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Zagorsky B, Reiter J, Chatterjee K, Nowak M. Forgiver triumphs in alternating
    prisoner’s dilemma . <i>PLoS One</i>. 2013;8(12). doi:<a href="https://doi.org/10.1371/journal.pone.0080814">10.1371/journal.pone.0080814</a>
  apa: Zagorsky, B., Reiter, J., Chatterjee, K., &#38; Nowak, M. (2013). Forgiver
    triumphs in alternating prisoner’s dilemma . <i>PLoS One</i>. Public Library of
    Science. <a href="https://doi.org/10.1371/journal.pone.0080814">https://doi.org/10.1371/journal.pone.0080814</a>
  chicago: Zagorsky, Benjamin, Johannes Reiter, Krishnendu Chatterjee, and Martin
    Nowak. “Forgiver Triumphs in Alternating Prisoner’s Dilemma .” <i>PLoS One</i>.
    Public Library of Science, 2013. <a href="https://doi.org/10.1371/journal.pone.0080814">https://doi.org/10.1371/journal.pone.0080814</a>.
  ieee: B. Zagorsky, J. Reiter, K. Chatterjee, and M. Nowak, “Forgiver triumphs in
    alternating prisoner’s dilemma ,” <i>PLoS One</i>, vol. 8, no. 12. Public Library
    of Science, 2013.
  ista: Zagorsky B, Reiter J, Chatterjee K, Nowak M. 2013. Forgiver triumphs in alternating
    prisoner’s dilemma . PLoS One. 8(12), e80814.
  mla: Zagorsky, Benjamin, et al. “Forgiver Triumphs in Alternating Prisoner’s Dilemma
    .” <i>PLoS One</i>, vol. 8, no. 12, e80814, Public Library of Science, 2013, doi:<a
    href="https://doi.org/10.1371/journal.pone.0080814">10.1371/journal.pone.0080814</a>.
  short: B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, PLoS One 8 (2013).
date_created: 2018-12-11T11:56:33Z
date_published: 2013-12-12T00:00:00Z
date_updated: 2026-07-29T10:15:25Z
day: '12'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0080814
ec_funded: 1
external_id:
  isi:
  - '000328731800009'
file:
- access_level: open_access
  checksum: 808e8b9e6e89658bee4ffbbfac1bd19d
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:11:15Z
  date_updated: 2020-07-14T12:45:34Z
  file_id: '4868'
  file_name: IST-2016-409-v1+1_journal.pone.0080814.pdf
  file_size: 1050042
  relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: '         8'
isi: 1
issue: '12'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
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: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '4702'
pubrep_id: '409'
quality_controlled: '1'
related_material:
  record:
  - id: '9749'
    relation: research_data
    status: public
  - id: '1400'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: 'Forgiver triumphs in alternating prisoner''s dilemma '
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2013'
...
---
_id: '2858'
abstract:
- lang: eng
  text: Tumor growth is caused by the acquisition of driver mutations, which enhance
    the net reproductive rate of cells. Driver mutations may increase cell division,
    reduce cell death, or allow cells to overcome density-limiting effects. We study
    the dynamics of tumor growth as one additional driver mutation is acquired. Our
    models are based on two-type branching processes that terminate in either tumor
    disappearance or tumor detection. In our first model, both cell types grow exponentially,
    with a faster rate for cells carrying the additional driver. We find that the
    additional driver mutation does not affect the survival probability of the lesion,
    but can substantially reduce the time to reach the detectable size if the lesion
    is slow growing. In our second model, cells lacking the additional driver cannot
    exceed a fixed carrying capacity, due to density limitations. In this case, the
    time to detection depends strongly on this carrying capacity. Our model provides
    a quantitative framework for studying tumor dynamics during different stages of
    progression. We observe that early, small lesions need additional drivers, while
    late stage metastases are only marginally affected by them. These results help
    to explain why additional driver mutations are typically not detected in fast-growing
    metastases.
article_processing_charge: No
author:
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Ivana
  full_name: Božić, Ivana
  last_name: Božić
- first_name: Benjamin
  full_name: Allen, Benjamin
  id: 135B5B70-E9D2-11E9-BD74-BB415DA2B523
  last_name: Allen
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. The effect of one additional
    driver mutation on tumor progression. <i>Evolutionary Applications</i>. 2013;6(1):34-45.
    doi:<a href="https://doi.org/10.1111/eva.12020">10.1111/eva.12020</a>
  apa: Reiter, J., Božić, I., Allen, B., Chatterjee, K., &#38; Nowak, M. (2013). The
    effect of one additional driver mutation on tumor progression. <i>Evolutionary
    Applications</i>. Wiley-Blackwell. <a href="https://doi.org/10.1111/eva.12020">https://doi.org/10.1111/eva.12020</a>
  chicago: Reiter, Johannes, Ivana Božić, Benjamin Allen, Krishnendu Chatterjee, and
    Martin Nowak. “The Effect of One Additional Driver Mutation on Tumor Progression.”
    <i>Evolutionary Applications</i>. Wiley-Blackwell, 2013. <a href="https://doi.org/10.1111/eva.12020">https://doi.org/10.1111/eva.12020</a>.
  ieee: J. Reiter, I. Božić, B. Allen, K. Chatterjee, and M. Nowak, “The effect of
    one additional driver mutation on tumor progression,” <i>Evolutionary Applications</i>,
    vol. 6, no. 1. Wiley-Blackwell, pp. 34–45, 2013.
  ista: Reiter J, Božić I, Allen B, Chatterjee K, Nowak M. 2013. The effect of one
    additional driver mutation on tumor progression. Evolutionary Applications. 6(1),
    34–45.
  mla: Reiter, Johannes, et al. “The Effect of One Additional Driver Mutation on Tumor
    Progression.” <i>Evolutionary Applications</i>, vol. 6, no. 1, Wiley-Blackwell,
    2013, pp. 34–45, doi:<a href="https://doi.org/10.1111/eva.12020">10.1111/eva.12020</a>.
  short: J. Reiter, I. Božić, B. Allen, K. Chatterjee, M. Nowak, Evolutionary Applications
    6 (2013) 34–45.
corr_author: '1'
date_created: 2018-12-11T11:59:58Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2026-07-29T10:15:25Z
day: '01'
ddc:
- '570'
department:
- _id: KrCh
doi: 10.1111/eva.12020
ec_funded: 1
external_id:
  isi:
  - '000313878800004'
file:
- access_level: open_access
  checksum: e2955b3889f8a823c3d5a72cb16f8957
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:15:50Z
  date_updated: 2020-07-14T12:45:51Z
  file_id: '5173'
  file_name: IST-2016-415-v1+1_Reiter_et_al-2013-Evolutionary_Applications.pdf
  file_size: 1172037
  relation: main_file
file_date_updated: 2020-07-14T12:45:51Z
has_accepted_license: '1'
intvolume: '         6'
isi: 1
issue: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 34 - 45
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
publication: Evolutionary Applications
publication_status: published
publisher: Wiley-Blackwell
publist_id: '3931'
pubrep_id: '415'
quality_controlled: '1'
related_material:
  record:
  - id: '1400'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: The effect of one additional driver mutation on tumor progression
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2013'
...
---
_id: '2816'
abstract:
- lang: eng
  text: In solid tumors, targeted treatments can lead to dramatic regressions, but
    responses are often short-lived because resistant cancer cells arise. The major
    strategy proposed for overcoming resistance is combination therapy. We present
    a mathematical model describing the evolutionary dynamics of lesions in response
    to treatment. We first studied 20 melanoma patients receiving vemurafenib. We
    then applied our model to an independent set of pancreatic, colorectal, and melanoma
    cancer patients with metastatic disease. We find that dual therapy results in
    long-term disease control for most patients, if there are no single mutations
    that cause cross-resistance to both drugs; in patients with large disease burden,
    triple therapy is needed. We also find that simultaneous therapy with two drugs
    is much more effective than sequential therapy. Our results provide realistic
    expectations for the efficacy of new drug combinations and inform the design of
    trials for new cancer therapeutics.
article_number: e00747
article_processing_charge: No
author:
- first_name: Ivana
  full_name: Božić, Ivana
  last_name: Božić
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Benjamin
  full_name: Allen, Benjamin
  last_name: Allen
- first_name: Tibor
  full_name: Antal, Tibor
  last_name: Antal
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Preya
  full_name: Shah, Preya
  last_name: Shah
- first_name: Yo
  full_name: Moon, Yo
  last_name: Moon
- first_name: Amin
  full_name: Yaqubie, Amin
  last_name: Yaqubie
- first_name: Nicole
  full_name: Kelly, Nicole
  last_name: Kelly
- first_name: Dung
  full_name: Le, Dung
  last_name: Le
- first_name: Evan
  full_name: Lipson, Evan
  last_name: Lipson
- first_name: Paul
  full_name: Chapman, Paul
  last_name: Chapman
- first_name: Luis
  full_name: Diaz, Luis
  last_name: Diaz
- first_name: Bert
  full_name: Vogelstein, Bert
  last_name: Vogelstein
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Božić I, Reiter J, Allen B, et al. Evolutionary dynamics of cancer in response
    to targeted combination therapy. <i>eLife</i>. 2013;2. doi:<a href="https://doi.org/10.7554/eLife.00747">10.7554/eLife.00747</a>
  apa: Božić, I., Reiter, J., Allen, B., Antal, T., Chatterjee, K., Shah, P., … Nowak,
    M. (2013). Evolutionary dynamics of cancer in response to targeted combination
    therapy. <i>ELife</i>. eLife Sciences Publications. <a href="https://doi.org/10.7554/eLife.00747">https://doi.org/10.7554/eLife.00747</a>
  chicago: Božić, Ivana, Johannes Reiter, Benjamin Allen, Tibor Antal, Krishnendu
    Chatterjee, Preya Shah, Yo Moon, et al. “Evolutionary Dynamics of Cancer in Response
    to Targeted Combination Therapy.” <i>ELife</i>. eLife Sciences Publications, 2013.
    <a href="https://doi.org/10.7554/eLife.00747">https://doi.org/10.7554/eLife.00747</a>.
  ieee: I. Božić <i>et al.</i>, “Evolutionary dynamics of cancer in response to targeted
    combination therapy,” <i>eLife</i>, vol. 2. eLife Sciences Publications, 2013.
  ista: Božić I, Reiter J, Allen B, Antal T, Chatterjee K, Shah P, Moon Y, Yaqubie
    A, Kelly N, Le D, Lipson E, Chapman P, Diaz L, Vogelstein B, Nowak M. 2013. Evolutionary
    dynamics of cancer in response to targeted combination therapy. eLife. 2, e00747.
  mla: Božić, Ivana, et al. “Evolutionary Dynamics of Cancer in Response to Targeted
    Combination Therapy.” <i>ELife</i>, vol. 2, e00747, eLife Sciences Publications,
    2013, doi:<a href="https://doi.org/10.7554/eLife.00747">10.7554/eLife.00747</a>.
  short: I. Božić, J. Reiter, B. Allen, T. Antal, K. Chatterjee, P. Shah, Y. Moon,
    A. Yaqubie, N. Kelly, D. Le, E. Lipson, P. Chapman, L. Diaz, B. Vogelstein, M.
    Nowak, ELife 2 (2013).
date_created: 2018-12-11T11:59:45Z
date_published: 2013-06-25T00:00:00Z
date_updated: 2026-07-29T10:15:25Z
day: '25'
ddc:
- '570'
- '610'
department:
- _id: KrCh
doi: 10.7554/eLife.00747
external_id:
  isi:
  - '000328619300005'
file:
- access_level: open_access
  checksum: 2c38c47815eacd8fa66cb8b404cf7c61
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:12:48Z
  date_updated: 2020-07-14T12:45:49Z
  file_id: '4967'
  file_name: IST-2013-134-v1+1_e00747.full.pdf
  file_size: 3358321
  relation: main_file
file_date_updated: 2020-07-14T12:45:49Z
has_accepted_license: '1'
intvolume: '         2'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
publication: eLife
publication_status: published
publisher: eLife Sciences Publications
publist_id: '3985'
pubrep_id: '134'
quality_controlled: '1'
related_material:
  record:
  - id: '1400'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Evolutionary dynamics of cancer in response to targeted combination therapy
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 2
year: '2013'
...
---
_id: '2000'
abstract:
- lang: eng
  text: In this work we present a flexible tool for tumor progression, which simulates
    the evolutionary dynamics of cancer. Tumor progression implements a multi-type
    branching process where the key parameters are the fitness landscape, the mutation
    rate, and the average time of cell division. The fitness of a cancer cell depends
    on the mutations it has accumulated. The input to our tool could be any fitness
    landscape, mutation rate, and cell division time, and the tool produces the growth
    dynamics and all relevant statistics.
alternative_title:
- LNCS
arxiv: 1
author:
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Ivana
  full_name: Božić, Ivana
  last_name: Božić
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: 'Reiter J, Božić I, Chatterjee K, Nowak M. TTP: Tool for tumor progression.
    In: <i>Proceedings of 25th Int. Conf. on Computer Aided Verification</i>. Vol
    8044. Lecture Notes in Computer Science. Springer; 2013:101-106. doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_6">10.1007/978-3-642-39799-8_6</a>'
  apa: 'Reiter, J., Božić, I., Chatterjee, K., &#38; Nowak, M. (2013). TTP: Tool for
    tumor progression. In <i>Proceedings of 25th Int. Conf. on Computer Aided Verification</i>
    (Vol. 8044, pp. 101–106). St. Petersburg, Russia: Springer. <a href="https://doi.org/10.1007/978-3-642-39799-8_6">https://doi.org/10.1007/978-3-642-39799-8_6</a>'
  chicago: 'Reiter, Johannes, Ivana Božić, Krishnendu Chatterjee, and Martin Nowak.
    “TTP: Tool for Tumor Progression.” In <i>Proceedings of 25th Int. Conf. on Computer
    Aided Verification</i>, 8044:101–6. Lecture Notes in Computer Science. Springer,
    2013. <a href="https://doi.org/10.1007/978-3-642-39799-8_6">https://doi.org/10.1007/978-3-642-39799-8_6</a>.'
  ieee: 'J. Reiter, I. Božić, K. Chatterjee, and M. Nowak, “TTP: Tool for tumor progression,”
    in <i>Proceedings of 25th Int. Conf. on Computer Aided Verification</i>, St. Petersburg,
    Russia, 2013, vol. 8044, pp. 101–106.'
  ista: 'Reiter J, Božić I, Chatterjee K, Nowak M. 2013. TTP: Tool for tumor progression.
    Proceedings of 25th Int. Conf. on Computer Aided Verification. CAV: Computer Aided
    VerificationLecture Notes in Computer Science, LNCS, vol. 8044, 101–106.'
  mla: 'Reiter, Johannes, et al. “TTP: Tool for Tumor Progression.” <i>Proceedings
    of 25th Int. Conf. on Computer Aided Verification</i>, vol. 8044, Springer, 2013,
    pp. 101–06, doi:<a href="https://doi.org/10.1007/978-3-642-39799-8_6">10.1007/978-3-642-39799-8_6</a>.'
  short: J. Reiter, I. Božić, K. Chatterjee, M. Nowak, in:, Proceedings of 25th Int.
    Conf. on Computer Aided Verification, Springer, 2013, pp. 101–106.
conference:
  end_date: 2013-07-19
  location: St. Petersburg, Russia
  name: 'CAV: Computer Aided Verification'
  start_date: 2013-07-13
date_created: 2018-12-11T11:55:08Z
date_published: 2013-01-01T00:00:00Z
date_updated: 2026-07-29T10:15:25Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-642-39799-8_6
ec_funded: 1
external_id:
  arxiv:
  - '1303.5251'
intvolume: '      8044'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1303.5251
month: '01'
oa: 1
oa_version: Preprint
page: 101 - 106
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: Proceedings of 25th Int. Conf. on Computer Aided Verification
publication_status: published
publisher: Springer
publist_id: '5077'
quality_controlled: '1'
related_material:
  record:
  - id: '5399'
    relation: earlier_version
    status: public
  - id: '1400'
    relation: dissertation_contains
    status: public
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: 'TTP: Tool for tumor progression'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8044
year: '2013'
...
---
_id: '450'
abstract:
- lang: eng
  text: Understanding the relative importance of heterosis and outbreeding depression
    over multiple generations is a key question in evolutionary biology and is essential
    for identifying appropriate genetic sources for population and ecosystem restoration.
    Here we use 2455 experimental crosses between 12 population pairs of the rare
    perennial plant Rutidosis leptorrhynchoides (Asteraceae) to investigate the multi-generational
    (F1, F2, F3) fitness outcomes of inter-population hybridization. We detected no
    evidence of outbreeding depression, with inter-population hybrids and backcrosses
    showing either similar fitness or significant heterosis for fitness components
    across the three generations. Variation in heterosis among population pairs was
    best explained by characteristics of the foreign source or home population, and
    was greatest when the source population was large, with high genetic diversity
    and low inbreeding, and the home population was small and inbred. Our results
    indicate that the primary consideration for maximizing progeny fitness following
    population augmentation or restoration is the use of seed from large, genetically
    diverse populations.
article_number: '2058'
article_processing_charge: No
author:
- first_name: Melinda
  full_name: Pickup, Melinda
  id: 2C78037E-F248-11E8-B48F-1D18A9856A87
  last_name: Pickup
  orcid: 0000-0001-6118-0541
- first_name: David
  full_name: Field, David
  id: 419049E2-F248-11E8-B48F-1D18A9856A87
  last_name: Field
  orcid: 0000-0002-4014-8478
- first_name: David
  full_name: Rowell, David
  last_name: Rowell
- first_name: Andrew
  full_name: Young, Andrew
  last_name: Young
citation:
  ama: Pickup M, Field D, Rowell D, Young A. Source population characteristics affect
    heterosis following genetic rescue of fragmented plant populations. <i>Proceedings
    of the Royal Society of London Series B Biological Sciences</i>. 2013;280(1750).
    doi:<a href="https://doi.org/10.1098/rspb.2012.2058">10.1098/rspb.2012.2058</a>
  apa: Pickup, M., Field, D., Rowell, D., &#38; Young, A. (2013). Source population
    characteristics affect heterosis following genetic rescue of fragmented plant
    populations. <i>Proceedings of the Royal Society of London Series B Biological
    Sciences</i>. Royal Society. <a href="https://doi.org/10.1098/rspb.2012.2058">https://doi.org/10.1098/rspb.2012.2058</a>
  chicago: Pickup, Melinda, David Field, David Rowell, and Andrew Young. “Source Population
    Characteristics Affect Heterosis Following Genetic Rescue of Fragmented Plant
    Populations.” <i>Proceedings of the Royal Society of London Series B Biological
    Sciences</i>. Royal Society, 2013. <a href="https://doi.org/10.1098/rspb.2012.2058">https://doi.org/10.1098/rspb.2012.2058</a>.
  ieee: M. Pickup, D. Field, D. Rowell, and A. Young, “Source population characteristics
    affect heterosis following genetic rescue of fragmented plant populations,” <i>Proceedings
    of the Royal Society of London Series B Biological Sciences</i>, vol. 280, no.
    1750. Royal Society, 2013.
  ista: Pickup M, Field D, Rowell D, Young A. 2013. Source population characteristics
    affect heterosis following genetic rescue of fragmented plant populations. Proceedings
    of the Royal Society of London Series B Biological Sciences. 280(1750), 2058.
  mla: Pickup, Melinda, et al. “Source Population Characteristics Affect Heterosis
    Following Genetic Rescue of Fragmented Plant Populations.” <i>Proceedings of the
    Royal Society of London Series B Biological Sciences</i>, vol. 280, no. 1750,
    2058, Royal Society, 2013, doi:<a href="https://doi.org/10.1098/rspb.2012.2058">10.1098/rspb.2012.2058</a>.
  short: M. Pickup, D. Field, D. Rowell, A. Young, Proceedings of the Royal Society
    of London Series B Biological Sciences 280 (2013).
corr_author: '1'
date_created: 2018-12-11T11:46:32Z
date_published: 2013-01-07T00:00:00Z
date_updated: 2026-08-12T06:25:53Z
day: '07'
department:
- _id: NiBa
doi: 10.1098/rspb.2012.2058
external_id:
  isi:
  - '000311943100012'
  pmid:
  - '23173202'
intvolume: '       280'
isi: 1
issue: '1750'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC3574427/
month: '01'
oa: 1
oa_version: Submitted Version
pmid: 1
publication: Proceedings of the Royal Society of London Series B Biological Sciences
publication_status: published
publisher: Royal Society
publist_id: '7372'
quality_controlled: '1'
status: public
title: Source population characteristics affect heterosis following genetic rescue
  of fragmented plant populations
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 280
year: '2013'
...
---
_id: '2811'
abstract:
- lang: eng
  text: 'In pipe, channel, and boundary layer flows turbulence first occurs intermittently
    in space and time: at moderate Reynolds numbers domains of disordered turbulent
    motion are separated by quiescent laminar regions. Based on direct numerical simulations
    of pipe flow we argue here that the spatial intermittency has its origin in a
    nearest neighbor interaction between turbulent regions. We further show that in
    this regime turbulent flows are intrinsically intermittent with a well-defined
    equilibrium turbulent fraction but without ever assuming a steady pattern. This
    transition scenario is analogous to that found in simple models such as coupled
    map lattices. The scaling observed implies that laminar intermissions of the turbulent
    flow will persist to arbitrarily large Reynolds numbers.'
article_number: '063012'
article_processing_charge: No
arxiv: 1
author:
- first_name: Marc
  full_name: Avila, Marc
  last_name: Avila
- first_name: Björn
  full_name: Hof, Björn
  id: 3A374330-F248-11E8-B48F-1D18A9856A87
  last_name: Hof
  orcid: 0000-0003-2057-2754
citation:
  ama: Avila M, Hof B. Nature of laminar-turbulence intermittency in shear flows.
    <i>Physical Review E</i>. 2013;87(6). doi:<a href="https://doi.org/10.1103/PhysRevE.87.063012">10.1103/PhysRevE.87.063012</a>
  apa: Avila, M., &#38; Hof, B. (2013). Nature of laminar-turbulence intermittency
    in shear flows. <i>Physical Review E</i>. American Physical Society. <a href="https://doi.org/10.1103/PhysRevE.87.063012">https://doi.org/10.1103/PhysRevE.87.063012</a>
  chicago: Avila, Marc, and Björn Hof. “Nature of Laminar-Turbulence Intermittency
    in Shear Flows.” <i>Physical Review E</i>. American Physical Society, 2013. <a
    href="https://doi.org/10.1103/PhysRevE.87.063012">https://doi.org/10.1103/PhysRevE.87.063012</a>.
  ieee: M. Avila and B. Hof, “Nature of laminar-turbulence intermittency in shear
    flows,” <i>Physical Review E</i>, vol. 87, no. 6. American Physical Society, 2013.
  ista: Avila M, Hof B. 2013. Nature of laminar-turbulence intermittency in shear
    flows. Physical Review E. 87(6), 063012.
  mla: Avila, Marc, and Björn Hof. “Nature of Laminar-Turbulence Intermittency in
    Shear Flows.” <i>Physical Review E</i>, vol. 87, no. 6, 063012, American Physical
    Society, 2013, doi:<a href="https://doi.org/10.1103/PhysRevE.87.063012">10.1103/PhysRevE.87.063012</a>.
  short: M. Avila, B. Hof, Physical Review E 87 (2013).
date_created: 2018-12-11T11:59:43Z
date_published: 2013-06-18T00:00:00Z
date_updated: 2026-08-12T14:29:19Z
day: '18'
department:
- _id: BjHo
doi: 10.1103/PhysRevE.87.063012
ec_funded: 1
external_id:
  arxiv:
  - '1306.5890'
  isi:
  - '000320645700009'
intvolume: '        87'
isi: 1
issue: '6'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1306.5890
month: '06'
oa: 1
oa_version: Preprint
project:
- _id: 25152F3A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '306589'
  name: Decoding the complexity of turbulence at its origin
publication: Physical Review E
publication_status: published
publisher: American Physical Society
publist_id: '4074'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Nature of laminar-turbulence intermittency in shear flows
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 87
year: '2013'
...
---
_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
corr_author: '1'
date_created: 2022-03-21T07:58:39Z
date_published: 2012-10-15T00:00:00Z
date_updated: 2024-10-09T21:02:34Z
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: '11092'
abstract:
- lang: eng
  text: To combat the functional decline of the proteome, cells use the process of
    protein turnover to replace potentially impaired polypeptides with new functional
    copies. We found that extremely long-lived proteins (ELLPs) did not turn over
    in postmitotic cells of the rat central nervous system. These ELLPs were associated
    with chromatin and the nuclear pore complex, the central transport channels that
    mediate all molecular trafficking in and out of the nucleus. The longevity of
    these proteins would be expected to expose them to potentially harmful metabolites,
    putting them at risk of accumulating damage over extended periods of time. Thus,
    it is possible that failure to maintain proper levels and functional integrity
    of ELLPs in nonproliferative cells might contribute to age-related deterioration
    in cell and tissue function.
article_processing_charge: No
article_type: letter_note
author:
- first_name: Jeffrey N.
  full_name: Savas, Jeffrey N.
  last_name: Savas
- first_name: Brandon H.
  full_name: Toyama, Brandon H.
  last_name: Toyama
- first_name: Tao
  full_name: Xu, Tao
  last_name: Xu
- first_name: John R.
  full_name: Yates, John R.
  last_name: Yates
- first_name: Martin W
  full_name: HETZER, Martin W
  id: 86c0d31b-b4eb-11ec-ac5a-eae7b2e135ed
  last_name: HETZER
  orcid: 0000-0002-2111-992X
citation:
  ama: Savas JN, Toyama BH, Xu T, Yates JR, Hetzer M. Extremely long-lived nuclear
    pore proteins in the rat brain. <i>Science</i>. 2012;335(6071):942-942. doi:<a
    href="https://doi.org/10.1126/science.1217421">10.1126/science.1217421</a>
  apa: Savas, J. N., Toyama, B. H., Xu, T., Yates, J. R., &#38; Hetzer, M. (2012).
    Extremely long-lived nuclear pore proteins in the rat brain. <i>Science</i>. American
    Association for the Advancement of Science. <a href="https://doi.org/10.1126/science.1217421">https://doi.org/10.1126/science.1217421</a>
  chicago: Savas, Jeffrey N., Brandon H. Toyama, Tao Xu, John R. Yates, and Martin
    Hetzer. “Extremely Long-Lived Nuclear Pore Proteins in the Rat Brain.” <i>Science</i>.
    American Association for the Advancement of Science, 2012. <a href="https://doi.org/10.1126/science.1217421">https://doi.org/10.1126/science.1217421</a>.
  ieee: J. N. Savas, B. H. Toyama, T. Xu, J. R. Yates, and M. Hetzer, “Extremely long-lived
    nuclear pore proteins in the rat brain,” <i>Science</i>, vol. 335, no. 6071. American
    Association for the Advancement of Science, pp. 942–942, 2012.
  ista: Savas JN, Toyama BH, Xu T, Yates JR, Hetzer M. 2012. Extremely long-lived
    nuclear pore proteins in the rat brain. Science. 335(6071), 942–942.
  mla: Savas, Jeffrey N., et al. “Extremely Long-Lived Nuclear Pore Proteins in the
    Rat Brain.” <i>Science</i>, vol. 335, no. 6071, American Association for the Advancement
    of Science, 2012, pp. 942–942, doi:<a href="https://doi.org/10.1126/science.1217421">10.1126/science.1217421</a>.
  short: J.N. Savas, B.H. Toyama, T. Xu, J.R. Yates, M. Hetzer, Science 335 (2012)
    942–942.
date_created: 2022-04-07T07:52:01Z
date_published: 2012-02-02T00:00:00Z
date_updated: 2025-12-15T10:03:06Z
day: '02'
department:
- _id: MaHe
doi: 10.1126/science.1217421
extern: '1'
external_id:
  pmid:
  - '22300851'
intvolume: '       335'
issue: '6071'
language:
- iso: eng
month: '02'
oa_version: None
page: 942-942
pmid: 1
publication: Science
publication_identifier:
  eissn:
  - 1095-9203
  issn:
  - 0036-8075
publication_status: published
publisher: American Association for the Advancement of Science
quality_controlled: '1'
scopus_import: '1'
status: public
title: Extremely long-lived nuclear pore proteins in the rat brain
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 335
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.'
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: 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.
corr_author: '1'
date_created: 2018-12-11T11:56:52Z
date_published: 2012-07-03T00:00:00Z
date_updated: 2025-09-29T14:17:43Z
day: '03'
department:
- _id: ToHe
- _id: CaGu
doi: 10.1109/TCBB.2012.91
ec_funded: 1
external_id:
  isi:
  - '000323504100006'
  pmid:
  - '22778152'
intvolume: '        10'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 10
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.
article_processing_charge: No
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: 2025-09-30T08:21:34Z
day: '01'
ddc:
- '570'
- '576'
department:
- _id: JoBo
doi: 10.1093/molbev/msr285
external_id:
  isi:
  - '000303603300004'
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'
isi: 1
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: 317138e5-6ab7-11ef-aa6d-ffef3953e345
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: 2025-09-23T08:00:31Z
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'
...
