---
_id: '10417'
abstract:
- lang: eng
  text: "We present a new dynamic partial-order reduction method for stateless model
    checking of concurrent programs. A common approach for exploring program behaviors
    relies on enumerating the traces of the program, without storing the visited states
    (aka stateless exploration). As the number of distinct traces grows exponentially,
    dynamic partial-order reduction (DPOR) techniques have been successfully used
    to partition the space of traces into equivalence classes (Mazurkiewicz partitioning),
    with the goal of exploring only few representative traces from each class.\r\n\r\nWe
    introduce a new equivalence on traces under sequential consistency semantics,
    which we call the observation equivalence. Two traces are observationally equivalent
    if every read event observes the same write event in both traces. While the traditional
    Mazurkiewicz equivalence is control-centric, our new definition is data-centric.
    We show that our observation equivalence is coarser than the Mazurkiewicz equivalence,
    and in many cases even exponentially coarser. We devise a DPOR exploration of
    the trace space, called data-centric DPOR, based on the observation equivalence."
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant
  (279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061."
article_number: '31'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Marek
  full_name: Chalupa, Marek
  last_name: Chalupa
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
- first_name: Nishant
  full_name: Sinha, Nishant
  last_name: Sinha
- first_name: Kapil
  full_name: Vaidya, Kapil
  last_name: Vaidya
citation:
  ama: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic
    partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>.
    2017;2(POPL). doi:<a href="https://doi.org/10.1145/3158119">10.1145/3158119</a>
  apa: 'Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K.
    (2017). Data-centric dynamic partial order reduction. <i>Proceedings of the ACM
    on Programming Languages</i>. Los Angeles, CA, United States: Association for
    Computing Machinery. <a href="https://doi.org/10.1145/3158119">https://doi.org/10.1145/3158119</a>'
  chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
    and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings
    of the ACM on Programming Languages</i>. Association for Computing Machinery,
    2017. <a href="https://doi.org/10.1145/3158119">https://doi.org/10.1145/3158119</a>.
  ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric
    dynamic partial order reduction,” <i>Proceedings of the ACM on Programming Languages</i>,
    vol. 2, no. POPL. Association for Computing Machinery, 2017.
  ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
    dynamic partial order reduction. Proceedings of the ACM on Programming Languages.
    2(POPL), 31.
  mla: Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings
    of the ACM on Programming Languages</i>, vol. 2, no. POPL, 31, Association for
    Computing Machinery, 2017, doi:<a href="https://doi.org/10.1145/3158119">10.1145/3158119</a>.
  short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings
    of the ACM on Programming Languages 2 (2017).
conference:
  end_date: 2018-01-13
  location: Los Angeles, CA, United States
  name: 'POPL: Programming Languages'
  start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:16Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/3158119
ec_funded: 1
external_id:
  arxiv:
  - '1610.01188'
intvolume: '         2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://dl.acm.org/doi/10.1145/3158119
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
  eissn:
  - 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
related_material:
  record:
  - id: '5448'
    relation: earlier_version
    status: public
  - id: '5456'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Data-centric dynamic partial order reduction
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '10418'
abstract:
- lang: eng
  text: We present a new proof rule for proving almost-sure termination of probabilistic
    programs, including those that contain demonic non-determinism. An important question
    for a probabilistic program is whether the probability mass of all its diverging
    runs is zero, that is that it terminates "almost surely". Proving that can be
    hard, and this paper presents a new method for doing so. It applies directly to
    the program's source code, even if the program contains demonic choice. Like others,
    we use variant functions (a.k.a. "super-martingales") that are real-valued and
    decrease randomly on each loop iteration; but our key innovation is that the amount
    as well as the probability of the decrease are parametric. We prove the soundness
    of the new rule, indicate where its applicability goes beyond existing rules,
    and explain its connection to classical results on denumerable (non-demonic) Markov
    chains.
acknowledgement: "McIver and Morgan are grateful to David Basin and the Information
  Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during
  part of which this work began. And thanks particularly to Andreas Lochbihler, who
  shared with us the probabilistic termination problem that led to it. They acknowledge
  the support of ARC grant DP140101119. Part of this work was carried out during the
  Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs
  Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden.
  Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4."
article_number: '33'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Annabelle
  full_name: Mciver, Annabelle
  last_name: Mciver
- first_name: Carroll
  full_name: Morgan, Carroll
  last_name: Morgan
- first_name: Benjamin Lucien
  full_name: Kaminski, Benjamin Lucien
  last_name: Kaminski
- first_name: Joost P
  full_name: Katoen, Joost P
  id: 4524F760-F248-11E8-B48F-1D18A9856A87
  last_name: Katoen
citation:
  ama: Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure
    termination. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL).
    doi:<a href="https://doi.org/10.1145/3158121">10.1145/3158121</a>
  apa: 'Mciver, A., Morgan, C., Kaminski, B. L., &#38; Katoen, J. P. (2017). A new
    proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming
    Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery.
    <a href="https://doi.org/10.1145/3158121">https://doi.org/10.1145/3158121</a>'
  chicago: Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost
    P Katoen. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the
    ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a
    href="https://doi.org/10.1145/3158121">https://doi.org/10.1145/3158121</a>.
  ieee: A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule
    for almost-sure termination,” <i>Proceedings of the ACM on Programming Languages</i>,
    vol. 2, no. POPL. Association for Computing Machinery, 2017.
  ista: Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure
    termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.
  mla: Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings
    of the ACM on Programming Languages</i>, vol. 2, no. POPL, 33, Association for
    Computing Machinery, 2017, doi:<a href="https://doi.org/10.1145/3158121">10.1145/3158121</a>.
  short: A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM
    on Programming Languages 2 (2017).
conference:
  end_date: 2018-01-13
  location: Los Angeles, CA, United States
  name: 'POPL: Programming Languages'
  start_date: 2018-01-07
date_created: 2021-12-05T23:01:49Z
date_published: 2017-12-07T00:00:00Z
date_updated: 2021-12-07T08:04:14Z
day: '07'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3158121
external_id:
  arxiv:
  - '1711.03588'
intvolume: '         2'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://dl.acm.org/doi/10.1145/3158121
month: '12'
oa: 1
oa_version: Published Version
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
  eissn:
  - 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: A new proof rule for almost-sure termination
type: journal_article
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
---
_id: '1065'
abstract:
- lang: eng
  text: 'We consider the problem of reachability in pushdown graphs. We study the
    problem for pushdown graphs with constant treewidth. Even for pushdown graphs
    with treewidth 1, for the reachability problem we establish the following: (i)
    the problem is PTIME-complete, and (ii) any subcubic algorithm for the problem
    would contradict the k-clique conjecture and imply faster combinatorial algorithms
    for cliques in graphs.'
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Georg F
  full_name: Osang, Georg F
  id: 464B40D6-F248-11E8-B48F-1D18A9856A87
  last_name: Osang
  orcid: 0000-0002-8882-5116
citation:
  ama: Chatterjee K, Osang GF. Pushdown reachability with constant treewidth. <i>Information
    Processing Letters</i>. 2017;122:25-29. doi:<a href="https://doi.org/10.1016/j.ipl.2017.02.003">10.1016/j.ipl.2017.02.003</a>
  apa: Chatterjee, K., &#38; Osang, G. F. (2017). Pushdown reachability with constant
    treewidth. <i>Information Processing Letters</i>. Elsevier. <a href="https://doi.org/10.1016/j.ipl.2017.02.003">https://doi.org/10.1016/j.ipl.2017.02.003</a>
  chicago: Chatterjee, Krishnendu, and Georg F Osang. “Pushdown Reachability with
    Constant Treewidth.” <i>Information Processing Letters</i>. Elsevier, 2017. <a
    href="https://doi.org/10.1016/j.ipl.2017.02.003">https://doi.org/10.1016/j.ipl.2017.02.003</a>.
  ieee: K. Chatterjee and G. F. Osang, “Pushdown reachability with constant treewidth,”
    <i>Information Processing Letters</i>, vol. 122. Elsevier, pp. 25–29, 2017.
  ista: Chatterjee K, Osang GF. 2017. Pushdown reachability with constant treewidth.
    Information Processing Letters. 122, 25–29.
  mla: Chatterjee, Krishnendu, and Georg F. Osang. “Pushdown Reachability with Constant
    Treewidth.” <i>Information Processing Letters</i>, vol. 122, Elsevier, 2017, pp.
    25–29, doi:<a href="https://doi.org/10.1016/j.ipl.2017.02.003">10.1016/j.ipl.2017.02.003</a>.
  short: K. Chatterjee, G.F. Osang, Information Processing Letters 122 (2017) 25–29.
date_created: 2018-12-11T11:49:57Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:08:18Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
- _id: HeEd
doi: 10.1016/j.ipl.2017.02.003
ec_funded: 1
external_id:
  isi:
  - '000399506600005'
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:17Z
  date_updated: 2019-10-15T07:44:51Z
  file_id: '4998'
  file_name: IST-2018-991-v1+2_2018_Chatterjee_Pushdown_PREPRINT.pdf
  file_size: 247657
  relation: main_file
file_date_updated: 2019-10-15T07:44:51Z
has_accepted_license: '1'
intvolume: '       122'
isi: 1
language:
- iso: eng
month: '06'
oa: 1
oa_version: Submitted Version
page: 25 - 29
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'
publication: Information Processing Letters
publication_identifier:
  issn:
  - '00200190'
publication_status: published
publisher: Elsevier
publist_id: '6323'
pubrep_id: '991'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Pushdown reachability with constant treewidth
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 122
year: '2017'
...
---
_id: '1066'
abstract:
- lang: eng
  text: "Simulation is an attractive alternative to language inclusion for automata
    as it is an under-approximation of language inclusion, but usually has much lower
    complexity. Simulation has also been extended in two orthogonal directions, namely,
    (1) fair simulation, for simulation over specified set of infinite runs; and (2)
    quantitative simulation, for simulation between weighted automata. While fair
    trace inclusion is PSPACE-complete, fair simulation can be computed in polynomial
    time. For weighted automata, the (quantitative) language inclusion problem is
    undecidable in general, whereas the (quantitative) simulation reduces to quantitative
    games, which admit pseudo-polynomial time algorithms.\r\n\r\nIn this work, we
    study (quantitative) simulation for weighted automata with Büchi acceptance conditions,
    i.e., we generalize fair simulation from non-weighted automata to weighted automata.
    We show that imposing Büchi acceptance conditions on weighted automata changes
    many fundamental properties of the simulation games, yet they still admit pseudo-polynomial
    time algorithms."
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
- first_name: Yaron
  full_name: Velner, Yaron
  last_name: Velner
citation:
  ama: Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation
    games. <i>Information and Computation</i>. 2017;254(2):143-166. doi:<a href="https://doi.org/10.1016/j.ic.2016.10.006">10.1016/j.ic.2016.10.006</a>
  apa: Chatterjee, K., Henzinger, T. A., Otop, J., &#38; Velner, Y. (2017). Quantitative
    fair simulation games. <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1016/j.ic.2016.10.006">https://doi.org/10.1016/j.ic.2016.10.006</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Jan Otop, and Yaron Velner.
    “Quantitative Fair Simulation Games.” <i>Information and Computation</i>. Elsevier,
    2017. <a href="https://doi.org/10.1016/j.ic.2016.10.006">https://doi.org/10.1016/j.ic.2016.10.006</a>.
  ieee: K. Chatterjee, T. A. Henzinger, J. Otop, and Y. Velner, “Quantitative fair
    simulation games,” <i>Information and Computation</i>, vol. 254, no. 2. Elsevier,
    pp. 143–166, 2017.
  ista: Chatterjee K, Henzinger TA, Otop J, Velner Y. 2017. Quantitative fair simulation
    games. Information and Computation. 254(2), 143–166.
  mla: Chatterjee, Krishnendu, et al. “Quantitative Fair Simulation Games.” <i>Information
    and Computation</i>, vol. 254, no. 2, Elsevier, 2017, pp. 143–66, doi:<a href="https://doi.org/10.1016/j.ic.2016.10.006">10.1016/j.ic.2016.10.006</a>.
  short: K. Chatterjee, T.A. Henzinger, J. Otop, Y. Velner, Information and Computation
    254 (2017) 143–166.
date_created: 2018-12-11T11:49:58Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-09-20T12:07:48Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1016/j.ic.2016.10.006
ec_funded: 1
external_id:
  isi:
  - '000402025600002'
intvolume: '       254'
isi: 1
issue: '2'
language:
- iso: eng
month: '06'
oa_version: None
page: 143 - 166
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Information and Computation
publication_status: published
publisher: Elsevier
publist_id: '6322'
quality_controlled: '1'
related_material:
  record:
  - id: '5428'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Quantitative fair simulation games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 254
year: '2017'
...
---
_id: '1080'
abstract:
- lang: eng
  text: Reconstructing the evolutionary history of metastases is critical for understanding
    their basic biological principles and has profound clinical implications. Genome-wide
    sequencing data has enabled modern phylogenomic methods to accurately dissect
    subclones and their phylogenies from noisy and impure bulk tumour samples at unprecedented
    depth. However, existing methods are not designed to infer metastatic seeding
    patterns. Here we develop a tool, called Treeomics, to reconstruct the phylogeny
    of metastases and map subclones to their anatomic locations. Treeomics infers
    comprehensive seeding patterns for pancreatic, ovarian, and prostate cancers.
    Moreover, Treeomics correctly disambiguates true seeding patterns from sequencing
    artifacts; 7% of variants were misclassified by conventional statistical methods.
    These artifacts can skew phylogenies by creating illusory tumour heterogeneity
    among distinct samples. In silico benchmarking on simulated tumour phylogenies
    across a wide range of sample purities (15–95%) and sequencing depths (25-800
    × ) demonstrates the accuracy of Treeomics compared with existing methods.
article_number: '14114'
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: Alvin
  full_name: Makohon Moore, Alvin
  last_name: Makohon Moore
- first_name: Jeffrey
  full_name: Gerold, Jeffrey
  last_name: Gerold
- 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: Christine
  full_name: Iacobuzio Donahue, Christine
  last_name: Iacobuzio Donahue
- first_name: Bert
  full_name: Vogelstein, Bert
  last_name: Vogelstein
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Reiter J, Makohon Moore A, Gerold J, et al. Reconstructing metastatic seeding
    patterns of human cancers. <i>Nature Communications</i>. 2017;8. doi:<a href="https://doi.org/10.1038/ncomms14114">10.1038/ncomms14114</a>
  apa: Reiter, J., Makohon Moore, A., Gerold, J., Božić, I., Chatterjee, K., Iacobuzio
    Donahue, C., … Nowak, M. (2017). Reconstructing metastatic seeding patterns of
    human cancers. <i>Nature Communications</i>. Nature Publishing Group. <a href="https://doi.org/10.1038/ncomms14114">https://doi.org/10.1038/ncomms14114</a>
  chicago: Reiter, Johannes, Alvin Makohon Moore, Jeffrey Gerold, Ivana Božić, Krishnendu
    Chatterjee, Christine Iacobuzio Donahue, Bert Vogelstein, and Martin Nowak. “Reconstructing
    Metastatic Seeding Patterns of Human Cancers.” <i>Nature Communications</i>. Nature
    Publishing Group, 2017. <a href="https://doi.org/10.1038/ncomms14114">https://doi.org/10.1038/ncomms14114</a>.
  ieee: J. Reiter <i>et al.</i>, “Reconstructing metastatic seeding patterns of human
    cancers,” <i>Nature Communications</i>, vol. 8. Nature Publishing Group, 2017.
  ista: Reiter J, Makohon Moore A, Gerold J, Božić I, Chatterjee K, Iacobuzio Donahue
    C, Vogelstein B, Nowak M. 2017. Reconstructing metastatic seeding patterns of
    human cancers. Nature Communications. 8, 14114.
  mla: Reiter, Johannes, et al. “Reconstructing Metastatic Seeding Patterns of Human
    Cancers.” <i>Nature Communications</i>, vol. 8, 14114, Nature Publishing Group,
    2017, doi:<a href="https://doi.org/10.1038/ncomms14114">10.1038/ncomms14114</a>.
  short: J. Reiter, A. Makohon Moore, J. Gerold, I. Božić, K. Chatterjee, C. Iacobuzio
    Donahue, B. Vogelstein, M. Nowak, Nature Communications 8 (2017).
date_created: 2018-12-11T11:50:02Z
date_published: 2017-01-31T00:00:00Z
date_updated: 2023-09-20T11:55:31Z
day: '31'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1038/ncomms14114
ec_funded: 1
external_id:
  isi:
  - '000393096600001'
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:15:15Z
  date_updated: 2018-12-12T10:15:15Z
  file_id: '5133'
  file_name: IST-2017-786-v1+1_ncomms14114.pdf
  file_size: 897050
  relation: main_file
file_date_updated: 2018-12-12T10:15:15Z
has_accepted_license: '1'
intvolume: '         8'
isi: 1
language:
- iso: eng
month: '01'
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: 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
publication: Nature Communications
publication_identifier:
  issn:
  - '20411723'
publication_status: published
publisher: Nature Publishing Group
publist_id: '6301'
pubrep_id: '786'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reconstructing metastatic seeding patterns of human cancers
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: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 8
year: '2017'
...
---
_id: '949'
abstract:
- lang: eng
  text: The notion of treewidth of graphs has been exploited for faster algorithms
    for several problems arising in verification and program analysis. Moreover, various
    notions of balanced tree decompositions have been used for improved algorithms
    supporting dynamic updates and analysis of concurrent programs. In this work,
    we present a tool for constructing tree-decompositions of CFGs obtained from Java
    methods, which is implemented as an extension to the widely used Soot framework.
    The experimental results show that our implementation on real-world Java benchmarks
    is very efficient. Our tool also provides the first implementation for balancing
    tree-decompositions. In summary, we present the first tool support for exploiting
    treewidth in the static analysis problems on Java programs.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Amir
  full_name: Goharshady, Amir
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
citation:
  ama: 'Chatterjee K, Goharshady AK, Pavlogiannis A. JTDec: A tool for tree decompositions
    in soot. In: D’Souza D, ed. Vol 10482. Springer; 2017:59-66. doi:<a href="https://doi.org/10.1007/978-3-319-68167-2_4">10.1007/978-3-319-68167-2_4</a>'
  apa: 'Chatterjee, K., Goharshady, A. K., &#38; Pavlogiannis, A. (2017). JTDec: A
    tool for tree decompositions in soot. In D. D’Souza (Ed.) (Vol. 10482, pp. 59–66).
    Presented at the ATVA: Automated Technology for Verification and Analysis, Pune,
    India: Springer. <a href="https://doi.org/10.1007/978-3-319-68167-2_4">https://doi.org/10.1007/978-3-319-68167-2_4</a>'
  chicago: 'Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Andreas Pavlogiannis.
    “JTDec: A Tool for Tree Decompositions in Soot.” edited by Deepak D’Souza, 10482:59–66.
    Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-68167-2_4">https://doi.org/10.1007/978-3-319-68167-2_4</a>.'
  ieee: 'K. Chatterjee, A. K. Goharshady, and A. Pavlogiannis, “JTDec: A tool for
    tree decompositions in soot,” presented at the ATVA: Automated Technology for
    Verification and Analysis, Pune, India, 2017, vol. 10482, pp. 59–66.'
  ista: 'Chatterjee K, Goharshady AK, Pavlogiannis A. 2017. JTDec: A tool for tree
    decompositions in soot. ATVA: Automated Technology for Verification and Analysis,
    LNCS, vol. 10482, 59–66.'
  mla: 'Chatterjee, Krishnendu, et al. <i>JTDec: A Tool for Tree Decompositions in
    Soot</i>. Edited by Deepak D’Souza, vol. 10482, Springer, 2017, pp. 59–66, doi:<a
    href="https://doi.org/10.1007/978-3-319-68167-2_4">10.1007/978-3-319-68167-2_4</a>.'
  short: K. Chatterjee, A.K. Goharshady, A. Pavlogiannis, in:, D. D’Souza (Ed.), Springer,
    2017, pp. 59–66.
conference:
  end_date: 2017-10-06
  location: Pune, India
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2017-10-03
date_created: 2018-12-11T11:49:22Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2024-03-25T23:30:19Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.1007/978-3-319-68167-2_4
ec_funded: 1
editor:
- first_name: Deepak
  full_name: D'Souza, Deepak
  last_name: D'Souza
external_id:
  isi:
  - '000723567800004'
file:
- access_level: open_access
  checksum: a0d9f5f94dc594c4e71e78525c9942f1
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:10:45Z
  date_updated: 2020-07-14T12:48:16Z
  file_id: '4835'
  file_name: IST-2017-845-v1+1_2017_Chatterjee_JTDec.pdf
  file_size: 948514
  relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: '     10482'
isi: 1
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 59 - 66
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
  issn:
  - '03029743'
publication_status: published
publisher: Springer
publist_id: '6468'
pubrep_id: '845'
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: 'JTDec: A tool for tree decompositions in soot'
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10482
year: '2017'
...
---
_id: '950'
abstract:
- lang: eng
  text: "Two-player games on graphs are widely studied in formal methods as they model
    the interaction between a system and its environment. The game is played by moving
    a token throughout a graph to produce an infinite path. There are several common
    modes to determine how the players move the token through the graph; e.g., in
    turn-based games the players alternate turns in moving the token. We study the
    bidding mode of moving the token, which, to the best of our knowledge, has never
    been studied in infinite-duration games. Both players have separate budgets, which
    sum up to $1$. In each turn, a bidding takes place. Both players submit bids simultaneously,
    and a bid is legal if it does not exceed the available budget. The winner of the
    bidding pays his bid to the other player and moves the token. For reachability
    objectives, repeated bidding games have been studied and are called Richman games.
    There, a central question is the existence and computation of threshold budgets;
    namely, a value t\\in [0,1] such that if\\PO's budget exceeds $t$, he can win
    the game, and if\\PT's budget exceeds 1-t, he can win the game. We focus on parity
    games and mean-payoff games. We show the existence of threshold budgets in these
    games, and reduce the problem of finding them to Richman games. We also determine
    the strategy-complexity of an optimal strategy. Our most interesting result shows
    that memoryless strategies suffice for mean-payoff bidding games. \r\n"
alternative_title:
- LIPIcs
article_number: '17'
arxiv: 1
author:
- first_name: Guy
  full_name: Avni, Guy
  id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
  last_name: Avni
  orcid: 0000-0001-5588-8287
- 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: Ventsislav K
  full_name: Chonev, Ventsislav K
  id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
  last_name: Chonev
citation:
  ama: 'Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol
    85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2017.21">10.4230/LIPIcs.CONCUR.2017.21</a>'
  apa: 'Avni, G., Henzinger, T. A., &#38; Chonev, V. K. (2017). Infinite-duration
    bidding games (Vol. 85). Presented at the CONCUR: Concurrency Theory, Berlin,
    Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2017.21">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>'
  chicago: Avni, Guy, Thomas A Henzinger, and Ventsislav K Chonev. “Infinite-Duration
    Bidding Games,” Vol. 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
    <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2017.21">https://doi.org/10.4230/LIPIcs.CONCUR.2017.21</a>.
  ieee: 'G. Avni, T. A. Henzinger, and V. K. Chonev, “Infinite-duration bidding games,”
    presented at the CONCUR: Concurrency Theory, Berlin, Germany, 2017, vol. 85.'
  ista: 'Avni G, Henzinger TA, Chonev VK. 2017. Infinite-duration bidding games. CONCUR:
    Concurrency Theory, LIPIcs, vol. 85, 17.'
  mla: Avni, Guy, et al. <i>Infinite-Duration Bidding Games</i>. Vol. 85, 17, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2017.21">10.4230/LIPIcs.CONCUR.2017.21</a>.
  short: G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2017.
conference:
  end_date: 2017-09-07
  location: Berlin, Germany
  name: 'CONCUR: Concurrency Theory'
  start_date: 2017-09-05
date_created: 2018-12-11T11:49:22Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-08-29T07:02:13Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2017.21
external_id:
  arxiv:
  - '1705.01433'
file:
- access_level: open_access
  checksum: 6d5cccf755207b91ccbef95d8275b013
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:00Z
  date_updated: 2020-07-14T12:48:16Z
  file_id: '5318'
  file_name: IST-2017-844-v1+1_concur-cr.pdf
  file_size: 335170
  relation: main_file
file_date_updated: 2020-07-14T12:48:16Z
has_accepted_license: '1'
intvolume: '        85'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication_identifier:
  issn:
  - 1868-8969
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6466'
pubrep_id: '844'
quality_controlled: '1'
related_material:
  record:
  - id: '6752'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Infinite-duration bidding games
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: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 85
year: '2017'
...
---
_id: '1194'
abstract:
- lang: eng
  text: 'Termination is one of the basic liveness properties, and we study the termination
    problem for probabilistic programs with real-valued variables. Previous works
    focused on the qualitative problem that asks whether an input program terminates
    with probability~1 (almost-sure termination). A powerful approach for this qualitative
    problem is the notion of ranking supermartingales with respect to a given set
    of invariants. The quantitative problem (probabilistic termination) asks for bounds
    on the termination probability. A fundamental and conceptual drawback of the existing
    approaches to address probabilistic termination is that even though the supermartingales
    consider the probabilistic behavior of the programs, the invariants are obtained
    completely ignoring the probabilistic aspect. In this work we address the probabilistic
    termination problem for linear-arithmetic probabilistic programs with nondeterminism.
    We define the notion of {\em stochastic invariants}, which are constraints along
    with a probability bound that the constraints hold. We introduce a concept of
    {\em repulsing supermartingales}. First, we show that repulsing supermartingales
    can be used to obtain bounds on the probability of the stochastic invariants.
    Second, we show the effectiveness of repulsing supermartingales in the following
    three ways: (1)~With a combination of ranking and repulsing supermartingales we
    can compute lower bounds on the probability of termination; (2)~repulsing supermartingales
    provide witnesses for refutation of almost-sure termination; and (3)~with a combination
    of ranking and repulsing supermartingales we can establish persistence properties
    of probabilistic programs. We also present results on related computational problems
    and an experimental evaluation of our approach on academic examples. '
alternative_title:
- ACM SIGPLAN Notices
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
- first_name: Djordje
  full_name: Zikelic, Djordje
  last_name: Zikelic
citation:
  ama: 'Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic
    termination. In: Vol 52. ACM; 2017:145-160. doi:<a href="https://doi.org/10.1145/3009837.3009873">10.1145/3009837.3009873</a>'
  apa: 'Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants
    for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles
    of Programming Languages, Paris, France: ACM. <a href="https://doi.org/10.1145/3009837.3009873">https://doi.org/10.1145/3009837.3009873</a>'
  chicago: Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic
    Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href="https://doi.org/10.1145/3009837.3009873">https://doi.org/10.1145/3009837.3009873</a>.
  ieee: 'K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic
    termination,” presented at the POPL: Principles of Programming Languages, Paris,
    France, 2017, vol. 52, no. 1, pp. 145–160.'
  ista: 'Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic
    termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol.
    52, 145–160.'
  mla: Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>.
    Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href="https://doi.org/10.1145/3009837.3009873">10.1145/3009837.3009873</a>.
  short: K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.
conference:
  end_date: 2017-01-21
  location: Paris, France
  name: 'POPL: Principles of Programming Languages'
  start_date: 2017-01-15
date_created: 2018-12-11T11:50:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-07-14T09:09:58Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/3009837.3009873
ec_funded: 1
external_id:
  isi:
  - '000408311200013'
intvolume: '        52'
isi: 1
issue: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1611.01063
month: '01'
oa: 1
oa_version: Submitted Version
page: 145 - 160
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_identifier:
  issn:
  - '07308566'
publication_status: published
publisher: ACM
publist_id: '6157'
quality_controlled: '1'
related_material:
  record:
  - id: '14539'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Stochastic invariants for probabilistic termination
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 52
year: '2017'
...
---
_id: '464'
abstract:
- lang: eng
  text: The computation of the winning set for parity objectives and for Streett objectives
    in graphs as well as in game graphs are central problems in computer-aided verification,
    with application to the verification of closed systems with strong fairness conditions,
    the verification of open systems, checking interface compatibility, well-formedness
    of specifications, and the synthesis of reactive systems. We show how to compute
    the winning set on n vertices for (1) parity-3 (aka one-pair Streett) objectives
    in game graphs in time O(n5/2) and for (2) k-pair Streett objectives in graphs
    in time O(n2+nklogn). For both problems this gives faster algorithms for dense
    graphs and represents the first improvement in asymptotic running time in 15 years.
article_number: '26'
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Veronika
  full_name: Loitzenbauer, Veronika
  last_name: Loitzenbauer
citation:
  ama: Chatterjee K, Henzinger MH, Loitzenbauer V. Improved algorithms for parity
    and Streett objectives. <i>Logical Methods in Computer Science</i>. 2017;13(3).
    doi:<a href="https://doi.org/10.23638/LMCS-13(3:26)2017">10.23638/LMCS-13(3:26)2017</a>
  apa: Chatterjee, K., Henzinger, M. H., &#38; Loitzenbauer, V. (2017). Improved algorithms
    for parity and Streett objectives. <i>Logical Methods in Computer Science</i>.
    International Federation of Computational Logic. <a href="https://doi.org/10.23638/LMCS-13(3:26)2017">https://doi.org/10.23638/LMCS-13(3:26)2017</a>
  chicago: Chatterjee, Krishnendu, Monika H Henzinger, and Veronika Loitzenbauer.
    “Improved Algorithms for Parity and Streett Objectives.” <i>Logical Methods in
    Computer Science</i>. International Federation of Computational Logic, 2017. <a
    href="https://doi.org/10.23638/LMCS-13(3:26)2017">https://doi.org/10.23638/LMCS-13(3:26)2017</a>.
  ieee: K. Chatterjee, M. H. Henzinger, and V. Loitzenbauer, “Improved algorithms
    for parity and Streett objectives,” <i>Logical Methods in Computer Science</i>,
    vol. 13, no. 3. International Federation of Computational Logic, 2017.
  ista: Chatterjee K, Henzinger MH, Loitzenbauer V. 2017. Improved algorithms for
    parity and Streett objectives. Logical Methods in Computer Science. 13(3), 26.
  mla: Chatterjee, Krishnendu, et al. “Improved Algorithms for Parity and Streett
    Objectives.” <i>Logical Methods in Computer Science</i>, vol. 13, no. 3, 26, International
    Federation of Computational Logic, 2017, doi:<a href="https://doi.org/10.23638/LMCS-13(3:26)2017">10.23638/LMCS-13(3:26)2017</a>.
  short: K. Chatterjee, M.H. Henzinger, V. Loitzenbauer, Logical Methods in Computer
    Science 13 (2017).
date_created: 2018-12-11T11:46:37Z
date_published: 2017-09-26T00:00:00Z
date_updated: 2025-06-02T08:53:41Z
day: '26'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(3:26)2017
ec_funded: 1
external_id:
  arxiv:
  - '1410.0833'
file:
- access_level: open_access
  checksum: 12d469ae69b80361333d7dead965cf5d
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:13:27Z
  date_updated: 2020-07-14T12:46:32Z
  file_id: '5010'
  file_name: IST-2018-956-v1+1_2017_Chatterjee_Improved_algorithms.pdf
  file_size: 582940
  relation: main_file
file_date_updated: 2020-07-14T12:46:32Z
has_accepted_license: '1'
intvolume: '        13'
issue: '3'
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nd/4.0/
month: '09'
oa: 1
oa_version: Published Version
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: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Logical Methods in Computer Science
publication_identifier:
  issn:
  - 1860-5974
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7357'
pubrep_id: '956'
quality_controlled: '1'
related_material:
  record:
  - id: '1661'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Improved algorithms for parity and Streett objectives
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '465'
abstract:
- lang: eng
  text: 'The edit distance between two words w 1 , w 2 is the minimal number of word
    operations (letter insertions, deletions, and substitutions) necessary to transform
    w 1 to w 2 . The edit distance generalizes to languages L 1 , L 2 , where the
    edit distance from L 1 to L 2 is the minimal number k such that for every word
    from L 1 there exists a word in L 2 with edit distance at most k . We study the
    edit distance computation problem between pushdown automata and their subclasses.
    The problem of computing edit distance to a pushdown automaton is undecidable,
    and in practice, the interesting question is to compute the edit distance from
    a pushdown automaton (the implementation, a standard model for programs with recursion)
    to a regular language (the specification). In this work, we present a complete
    picture of decidability and complexity for the following problems: (1) deciding
    whether, for a given threshold k , the edit distance from a pushdown automaton
    to a finite automaton is at most k , and (2) deciding whether the edit distance
    from a pushdown automaton to a finite automaton is finite. '
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
- first_name: Jan
  full_name: Otop, Jan
  last_name: Otop
citation:
  ama: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown
    automata. <i>Logical Methods in Computer Science</i>. 2017;13(3). doi:<a href="https://doi.org/10.23638/LMCS-13(3:23)2017">10.23638/LMCS-13(3:23)2017</a>
  apa: Chatterjee, K., Henzinger, T. A., Ibsen-Jensen, R., &#38; Otop, J. (2017).
    Edit distance for pushdown automata. <i>Logical Methods in Computer Science</i>.
    International Federation of Computational Logic. <a href="https://doi.org/10.23638/LMCS-13(3:23)2017">https://doi.org/10.23638/LMCS-13(3:23)2017</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, Rasmus Ibsen-Jensen, and Jan
    Otop. “Edit Distance for Pushdown Automata.” <i>Logical Methods in Computer Science</i>.
    International Federation of Computational Logic, 2017. <a href="https://doi.org/10.23638/LMCS-13(3:23)2017">https://doi.org/10.23638/LMCS-13(3:23)2017</a>.
  ieee: K. Chatterjee, T. A. Henzinger, R. Ibsen-Jensen, and J. Otop, “Edit distance
    for pushdown automata,” <i>Logical Methods in Computer Science</i>, vol. 13, no.
    3. International Federation of Computational Logic, 2017.
  ista: Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. 2017. Edit distance for
    pushdown automata. Logical Methods in Computer Science. 13(3).
  mla: Chatterjee, Krishnendu, et al. “Edit Distance for Pushdown Automata.” <i>Logical
    Methods in Computer Science</i>, vol. 13, no. 3, International Federation of Computational
    Logic, 2017, doi:<a href="https://doi.org/10.23638/LMCS-13(3:23)2017">10.23638/LMCS-13(3:23)2017</a>.
  short: K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods
    in Computer Science 13 (2017).
date_created: 2018-12-11T11:46:37Z
date_published: 2017-09-13T00:00:00Z
date_updated: 2023-02-23T12:26:25Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.23638/LMCS-13(3:23)2017
ec_funded: 1
file:
- access_level: open_access
  checksum: 08041379ba408d40664f449eb5907a8f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:37Z
  date_updated: 2020-07-14T12:46:33Z
  file_id: '5090'
  file_name: IST-2015-321-v1+1_main.pdf
  file_size: 279071
  relation: main_file
- access_level: open_access
  checksum: 08041379ba408d40664f449eb5907a8f
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:38Z
  date_updated: 2020-07-14T12:46:33Z
  file_id: '5091'
  file_name: IST-2018-955-v1+1_2017_Chatterjee_Edit_distance.pdf
  file_size: 279071
  relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: '        13'
issue: '3'
language:
- iso: eng
month: '09'
oa: 1
oa_version: Published Version
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _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: Logical Methods in Computer Science
publication_identifier:
  issn:
  - '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7356'
pubrep_id: '955'
quality_controlled: '1'
related_material:
  record:
  - id: '1610'
    relation: earlier_version
    status: public
  - id: '5438'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Edit distance for pushdown automata
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '466'
abstract:
- lang: eng
  text: 'We consider Markov decision processes (MDPs) with multiple limit-average
    (or mean-payoff) objectives. There exist two different views: (i) the expectation
    semantics, where the goal is to optimize the expected mean-payoff objective, and
    (ii) the satisfaction semantics, where the goal is to maximize the probability
    of runs such that the mean-payoff value stays above a given vector. We consider
    optimization with respect to both objectives at once, thus unifying the existing
    semantics. Precisely, the goal is to optimize the expectation while ensuring the
    satisfaction constraint. Our problem captures the notion of optimization with
    respect to strategies that are risk-averse (i.e., ensure certain probabilistic
    guarantee). Our main results are as follows: First, we present algorithms for
    the decision problems which are always polynomial in the size of the MDP. We also
    show that an approximation of the Pareto-curve can be computed in time polynomial
    in the size of the MDP, and the approximation factor, but exponential in the number
    of dimensions. Second, we present a complete characterization of the strategy
    complexity (in terms of memory bounds and randomization) required to solve our
    problem. '
article_number: '15'
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Zuzana
  full_name: Křetínská, Zuzana
  last_name: Křetínská
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
citation:
  ama: Chatterjee K, Křetínská Z, Kretinsky J. Unifying two views on multiple mean-payoff
    objectives in Markov decision processes. <i>Logical Methods in Computer Science</i>.
    2017;13(2). doi:<a href="https://doi.org/10.23638/LMCS-13(2:15)2017">10.23638/LMCS-13(2:15)2017</a>
  apa: Chatterjee, K., Křetínská, Z., &#38; Kretinsky, J. (2017). Unifying two views
    on multiple mean-payoff objectives in Markov decision processes. <i>Logical Methods
    in Computer Science</i>. International Federation of Computational Logic. <a href="https://doi.org/10.23638/LMCS-13(2:15)2017">https://doi.org/10.23638/LMCS-13(2:15)2017</a>
  chicago: Chatterjee, Krishnendu, Zuzana Křetínská, and Jan Kretinsky. “Unifying
    Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.” <i>Logical
    Methods in Computer Science</i>. International Federation of Computational Logic,
    2017. <a href="https://doi.org/10.23638/LMCS-13(2:15)2017">https://doi.org/10.23638/LMCS-13(2:15)2017</a>.
  ieee: K. Chatterjee, Z. Křetínská, and J. Kretinsky, “Unifying two views on multiple
    mean-payoff objectives in Markov decision processes,” <i>Logical Methods in Computer
    Science</i>, vol. 13, no. 2. International Federation of Computational Logic,
    2017.
  ista: Chatterjee K, Křetínská Z, Kretinsky J. 2017. Unifying two views on multiple
    mean-payoff objectives in Markov decision processes. Logical Methods in Computer
    Science. 13(2), 15.
  mla: Chatterjee, Krishnendu, et al. “Unifying Two Views on Multiple Mean-Payoff
    Objectives in Markov Decision Processes.” <i>Logical Methods in Computer Science</i>,
    vol. 13, no. 2, 15, International Federation of Computational Logic, 2017, doi:<a
    href="https://doi.org/10.23638/LMCS-13(2:15)2017">10.23638/LMCS-13(2:15)2017</a>.
  short: K. Chatterjee, Z. Křetínská, J. Kretinsky, Logical Methods in Computer Science
    13 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-07-03T00:00:00Z
date_updated: 2023-02-23T12:26:16Z
day: '03'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.23638/LMCS-13(2:15)2017
ec_funded: 1
file:
- access_level: open_access
  checksum: bfa405385ec6229ad5ead89ab5751639
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:32Z
  date_updated: 2020-07-14T12:46:33Z
  file_id: '5354'
  file_name: IST-2018-957-v1+1_2017_Chatterjee_Unifying_two.pdf
  file_size: 511832
  relation: main_file
file_date_updated: 2020-07-14T12:46:33Z
has_accepted_license: '1'
intvolume: '        13'
issue: '2'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2590DB08-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '701309'
  name: Atomic-Resolution Structures of Mitochondrial Respiratory Chain Supercomplexes
    (H2020)
publication: Logical Methods in Computer Science
publication_identifier:
  issn:
  - '18605974'
publication_status: published
publisher: International Federation of Computational Logic
publist_id: '7355'
pubrep_id: '957'
quality_controlled: '1'
related_material:
  record:
  - id: '1657'
    relation: earlier_version
    status: public
  - id: '5429'
    relation: earlier_version
    status: public
  - id: '5435'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Unifying two views on multiple mean-payoff objectives in Markov decision processes
tmp:
  image: /image/cc_by_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode
  name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)
  short: CC BY-ND (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13
year: '2017'
...
---
_id: '467'
abstract:
- lang: eng
  text: Recently there has been a significant effort to handle quantitative properties
    in formal verification and synthesis. While weighted automata over finite and
    infinite words provide a natural and flexible framework to express quantitative
    properties, perhaps surprisingly, some basic system properties such as average
    response time cannot be expressed using weighted automata or in any other known
    decidable formalism. In this work, we introduce nested weighted automata as a
    natural extension of weighted automata, which makes it possible to express important
    quantitative properties such as average response time. In nested weighted automata,
    a master automaton spins off and collects results from weighted slave automata,
    each of which computes a quantity along a finite portion of an infinite word.
    Nested weighted automata can be viewed as the quantitative analogue of monitor
    automata, which are used in runtime verification. We establish an almost-complete
    decidability picture for the basic decision problems about nested weighted automata
    and illustrate their applicability in several domains. In particular, nested weighted
    automata can be used to decide average response time properties.
article_number: '31'
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jan
  full_name: Otop, Jan
  id: 2FC5DA74-F248-11E8-B48F-1D18A9856A87
  last_name: Otop
citation:
  ama: Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. <i>ACM Transactions
    on Computational Logic (TOCL)</i>. 2017;18(4). doi:<a href="https://doi.org/10.1145/3152769">10.1145/3152769</a>
  apa: Chatterjee, K., Henzinger, T. A., &#38; Otop, J. (2017). Nested weighted automata.
    <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM. <a href="https://doi.org/10.1145/3152769">https://doi.org/10.1145/3152769</a>
  chicago: Chatterjee, Krishnendu, Thomas A Henzinger, and Jan Otop. “Nested Weighted
    Automata.” <i>ACM Transactions on Computational Logic (TOCL)</i>. ACM, 2017. <a
    href="https://doi.org/10.1145/3152769">https://doi.org/10.1145/3152769</a>.
  ieee: K. Chatterjee, T. A. Henzinger, and J. Otop, “Nested weighted automata,” <i>ACM
    Transactions on Computational Logic (TOCL)</i>, vol. 18, no. 4. ACM, 2017.
  ista: Chatterjee K, Henzinger TA, Otop J. 2017. Nested weighted automata. ACM Transactions
    on Computational Logic (TOCL). 18(4), 31.
  mla: Chatterjee, Krishnendu, et al. “Nested Weighted Automata.” <i>ACM Transactions
    on Computational Logic (TOCL)</i>, vol. 18, no. 4, 31, ACM, 2017, doi:<a href="https://doi.org/10.1145/3152769">10.1145/3152769</a>.
  short: K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational
    Logic (TOCL) 18 (2017).
date_created: 2018-12-11T11:46:38Z
date_published: 2017-12-01T00:00:00Z
date_updated: 2023-02-23T12:26:19Z
day: '01'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1145/3152769
ec_funded: 1
external_id:
  arxiv:
  - '1606.03598'
intvolume: '        18'
issue: '4'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1606.03598
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _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: ACM Transactions on Computational Logic (TOCL)
publication_identifier:
  issn:
  - '15293785'
publication_status: published
publisher: ACM
publist_id: '7354'
quality_controlled: '1'
related_material:
  record:
  - id: '1656'
    relation: earlier_version
    status: public
  - id: '5415'
    relation: earlier_version
    status: public
  - id: '5436'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: Nested weighted automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 18
year: '2017'
...
---
_id: '512'
abstract:
- lang: eng
  text: 'The fixation probability is the probability that a new mutant introduced
    in a homogeneous population eventually takes over the entire population. The fixation
    probability is a fundamental quantity of natural selection, and known to depend
    on the population structure. Amplifiers of natural selection are population structures
    which increase the fixation probability of advantageous mutants, as compared to
    the baseline case of well-mixed populations. In this work we focus on symmetric
    population structures represented as undirected graphs. In the regime of undirected
    graphs, the strongest amplifier known has been the Star graph, and the existence
    of undirected graphs with stronger amplification properties has remained open
    for over a decade. In this work we present the Comet and Comet-swarm families
    of undirected graphs. We show that for a range of fitness values of the mutants,
    the Comet and Cometswarm graphs have fixation probability strictly larger than
    the fixation probability of the Star graph, for fixed population size and at the
    limit of large populations, respectively. '
article_number: '82'
article_processing_charge: No
author:
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
- first_name: Josef
  full_name: Tkadlec, Josef
  id: 3F24CCC8-F248-11E8-B48F-1D18A9856A87
  last_name: Tkadlec
  orcid: 0000-0002-1097-9684
- 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: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. Amplification on undirected
    population structures: Comets beat stars. <i>Scientific Reports</i>. 2017;7(1).
    doi:<a href="https://doi.org/10.1038/s41598-017-00107-w">10.1038/s41598-017-00107-w</a>'
  apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2017). Amplification
    on undirected population structures: Comets beat stars. <i>Scientific Reports</i>.
    Nature Publishing Group. <a href="https://doi.org/10.1038/s41598-017-00107-w">https://doi.org/10.1038/s41598-017-00107-w</a>'
  chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak. “Amplification on Undirected Population Structures: Comets Beat Stars.”
    <i>Scientific Reports</i>. Nature Publishing Group, 2017. <a href="https://doi.org/10.1038/s41598-017-00107-w">https://doi.org/10.1038/s41598-017-00107-w</a>.'
  ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, “Amplification
    on undirected population structures: Comets beat stars,” <i>Scientific Reports</i>,
    vol. 7, no. 1. Nature Publishing Group, 2017.'
  ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2017. Amplification on
    undirected population structures: Comets beat stars. Scientific Reports. 7(1),
    82.'
  mla: 'Pavlogiannis, Andreas, et al. “Amplification on Undirected Population Structures:
    Comets Beat Stars.” <i>Scientific Reports</i>, vol. 7, no. 1, 82, Nature Publishing
    Group, 2017, doi:<a href="https://doi.org/10.1038/s41598-017-00107-w">10.1038/s41598-017-00107-w</a>.'
  short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Scientific Reports
    7 (2017).
date_created: 2018-12-11T11:46:53Z
date_published: 2017-03-06T00:00:00Z
date_updated: 2023-02-23T12:26:57Z
day: '06'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.1038/s41598-017-00107-w
ec_funded: 1
file:
- access_level: open_access
  checksum: 7d05cbdd914e194a019c0f91fb64e9a8
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:35Z
  date_updated: 2020-07-14T12:46:36Z
  file_id: '5357'
  file_name: IST-2018-938-v1+1_2017_Pavlogiannis_Amplification_on.pdf
  file_size: 1536783
  relation: main_file
file_date_updated: 2020-07-14T12:46:36Z
has_accepted_license: '1'
intvolume: '         7'
issue: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
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'
publication: Scientific Reports
publication_identifier:
  issn:
  - '20452322'
publication_status: published
publisher: Nature Publishing Group
publist_id: '7307'
pubrep_id: '938'
quality_controlled: '1'
related_material:
  record:
  - id: '5449'
    relation: earlier_version
    status: public
scopus_import: 1
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2017'
...
---
_id: '1245'
abstract:
- lang: eng
  text: 'To facilitate collaboration in massive online classrooms, instructors must
    make many decisions. For instance, the following parameters need to be decided
    when designing a peer-feedback system where students review each others'' essays:
    the number of students each student must provide feedback to, an algorithm to
    map feedback providers to receivers, constraints that ensure students do not become
    free-riders (receiving feedback but not providing it), the best times to receive
    feedback to improve learning etc. While instructors can answer these questions
    by running experiments or invoking past experience, game-theoretic models with
    data from online learning platforms can identify better initial designs for further
    improvements. As an example, we explore the design space of a peer feedback system
    by modeling it using game theory. Our simulations show that incentivizing students
    to provide feedback requires the value obtained from receiving a feedback to exceed
    the cost of providing it by a large factor (greater than 7). Furthermore, hiding
    feedback from low-effort students incentivizes them to provide more feedback.'
acknowledgement: 'ERC Start Grant Graph Games 279307 supported this  research. '
author:
- first_name: Vineet
  full_name: Pandey, Vineet
  last_name: Pandey
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
citation:
  ama: 'Pandey V, Chatterjee K. Game-theoretic models identify useful principles for
    peer collaboration in online learning platforms. In: <i>Proceedings of the ACM
    Conference on Computer Supported Cooperative Work</i>. Vol 26. ACM; 2016:365-368.
    doi:<a href="https://doi.org/10.1145/2818052.2869122">10.1145/2818052.2869122</a>'
  apa: 'Pandey, V., &#38; Chatterjee, K. (2016). Game-theoretic models identify useful
    principles for peer collaboration in online learning platforms. In <i>Proceedings
    of the ACM Conference on Computer Supported Cooperative Work</i> (Vol. 26, pp.
    365–368). San Francisco, CA, USA: ACM. <a href="https://doi.org/10.1145/2818052.2869122">https://doi.org/10.1145/2818052.2869122</a>'
  chicago: Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify
    Useful Principles for Peer Collaboration in Online Learning Platforms.” In <i>Proceedings
    of the ACM Conference on Computer Supported Cooperative Work</i>, 26:365–68. ACM,
    2016. <a href="https://doi.org/10.1145/2818052.2869122">https://doi.org/10.1145/2818052.2869122</a>.
  ieee: V. Pandey and K. Chatterjee, “Game-theoretic models identify useful principles
    for peer collaboration in online learning platforms,” in <i>Proceedings of the
    ACM Conference on Computer Supported Cooperative Work</i>, San Francisco, CA,
    USA, 2016, vol. 26, no. Februar-2016, pp. 365–368.
  ista: 'Pandey V, Chatterjee K. 2016. Game-theoretic models identify useful principles
    for peer collaboration in online learning platforms. Proceedings of the ACM Conference
    on Computer Supported Cooperative Work. CSCW: Computer Supported Cooperative Work
    and Social Computing vol. 26, 365–368.'
  mla: Pandey, Vineet, and Krishnendu Chatterjee. “Game-Theoretic Models Identify
    Useful Principles for Peer Collaboration in Online Learning Platforms.” <i>Proceedings
    of the ACM Conference on Computer Supported Cooperative Work</i>, vol. 26, no.
    Februar-2016, ACM, 2016, pp. 365–68, doi:<a href="https://doi.org/10.1145/2818052.2869122">10.1145/2818052.2869122</a>.
  short: V. Pandey, K. Chatterjee, in:, Proceedings of the ACM Conference on Computer
    Supported Cooperative Work, ACM, 2016, pp. 365–368.
conference:
  end_date: 2016-03-02
  location: San Francisco, CA, USA
  name: 'CSCW: Computer Supported Cooperative Work and Social Computing'
  start_date: 2016-02-26
date_created: 2018-12-11T11:50:55Z
date_published: 2016-02-27T00:00:00Z
date_updated: 2021-01-12T06:49:22Z
day: '27'
department:
- _id: KrCh
doi: 10.1145/2818052.2869122
ec_funded: 1
intvolume: '        26'
issue: Februar-2016
language:
- iso: eng
month: '02'
oa_version: None
page: 365 - 368
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the ACM Conference on Computer Supported Cooperative Work
publication_status: published
publisher: ACM
publist_id: '6083'
quality_controlled: '1'
scopus_import: 1
status: public
title: Game-theoretic models identify useful principles for peer collaboration in
  online learning platforms
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 26
year: '2016'
...
---
_id: '1322'
abstract:
- lang: eng
  text: Direct reciprocity is a major mechanism for the evolution of cooperation.
    Several classical studies have suggested that humans should quickly learn to adopt
    reciprocal strategies to establish mutual cooperation in repeated interactions.
    On the other hand, the recently discovered theory of ZD strategies has found that
    subjects who use extortionate strategies are able to exploit and subdue cooperators.
    Although such extortioners have been predicted to succeed in any population of
    adaptive opponents, theoretical follow-up studies questioned whether extortion
    can evolve in reality. However, most of these studies presumed that individuals
    have similar strategic possibilities and comparable outside options, whereas asymmetries
    are ubiquitous in real world applications. Here we show with a model and an economic
    experiment that extortionate strategies readily emerge once subjects differ in
    their strategic power. Our experiment combines a repeated social dilemma with
    asymmetric partner choice. In our main treatment there is one randomly chosen
    group member who is unilaterally allowed to exchange one of the other group members
    after every ten rounds of the social dilemma. We find that this asymmetric replacement
    opportunity generally promotes cooperation, but often the resulting payoff distribution
    reflects the underlying power structure. Almost half of the subjects in a better
    strategic position turn into extortioners, who quickly proceed to exploit their
    peers. By adapting their cooperation probabilities consistent with ZD theory,
    extortioners force their co-players to cooperate without being similarly cooperative
    themselves. Comparison to non-extortionate players under the same conditions indicates
    a substantial net gain to extortion. Our results thus highlight how power asymmetries
    can endanger mutually beneficial interactions, and transform them into exploitative
    relationships. In particular, our results indicate that the extortionate strategies
    predicted from ZD theory could play a more prominent role in our daily interactions
    than previously thought.
acknowledgement: 'CH was funded by the Schrödinger program of the Austrian Science
  Fund (FWF) J3475. '
article_number: e0163867
author:
- first_name: Christian
  full_name: Hilbe, Christian
  id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
  last_name: Hilbe
  orcid: 0000-0001-5116-955X
- first_name: Kristin
  full_name: Hagel, Kristin
  last_name: Hagel
- first_name: Manfred
  full_name: Milinski, Manfred
  last_name: Milinski
citation:
  ama: Hilbe C, Hagel K, Milinski M. Asymmetric power boosts extortion in an economic
    experiment. <i>PLoS One</i>. 2016;11(10). doi:<a href="https://doi.org/10.1371/journal.pone.0163867">10.1371/journal.pone.0163867</a>
  apa: Hilbe, C., Hagel, K., &#38; Milinski, M. (2016). Asymmetric power boosts extortion
    in an economic experiment. <i>PLoS One</i>. Public Library of Science. <a href="https://doi.org/10.1371/journal.pone.0163867">https://doi.org/10.1371/journal.pone.0163867</a>
  chicago: Hilbe, Christian, Kristin Hagel, and Manfred Milinski. “Asymmetric Power
    Boosts Extortion in an Economic Experiment.” <i>PLoS One</i>. Public Library of
    Science, 2016. <a href="https://doi.org/10.1371/journal.pone.0163867">https://doi.org/10.1371/journal.pone.0163867</a>.
  ieee: C. Hilbe, K. Hagel, and M. Milinski, “Asymmetric power boosts extortion in
    an economic experiment,” <i>PLoS One</i>, vol. 11, no. 10. Public Library of Science,
    2016.
  ista: Hilbe C, Hagel K, Milinski M. 2016. Asymmetric power boosts extortion in an
    economic experiment. PLoS One. 11(10), e0163867.
  mla: Hilbe, Christian, et al. “Asymmetric Power Boosts Extortion in an Economic
    Experiment.” <i>PLoS One</i>, vol. 11, no. 10, e0163867, Public Library of Science,
    2016, doi:<a href="https://doi.org/10.1371/journal.pone.0163867">10.1371/journal.pone.0163867</a>.
  short: C. Hilbe, K. Hagel, M. Milinski, PLoS One 11 (2016).
date_created: 2018-12-11T11:51:22Z
date_published: 2016-10-04T00:00:00Z
date_updated: 2023-02-23T14:11:27Z
day: '04'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.1371/journal.pone.0163867
file:
- access_level: open_access
  checksum: 6b33e394003dfe8b4ca6be1858aaa8e3
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:08Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '4668'
  file_name: IST-2016-716-v1+1_journal.pone.0163867.PDF
  file_size: 2077905
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '        11'
issue: '10'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
publication: PLoS One
publication_status: published
publisher: Public Library of Science
publist_id: '5948'
pubrep_id: '716'
quality_controlled: '1'
related_material:
  record:
  - id: '9867'
    relation: research_data
    status: public
  - id: '9868'
    relation: research_data
    status: public
scopus_import: 1
status: public
title: Asymmetric power boosts extortion in an economic experiment
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 11
year: '2016'
...
---
_id: '1324'
abstract:
- lang: eng
  text: 'DEC-POMDPs extend POMDPs to a multi-agent setting, where several agents operate
    in an uncertain environment independently to achieve a joint objective. DEC-POMDPs
    have been studied with finite-horizon and infinite-horizon discounted-sum objectives,
    and there exist solvers both for exact and approximate solutions. In this work
    we consider Goal-DEC-POMDPs, where given a set of target states, the objective
    is to ensure that the target set is reached with minimal cost. We consider the
    indefinite-horizon (infinite-horizon with either discounted-sum, or undiscounted-sum,
    where absorbing goal states have zero-cost) problem. We present a new and novel
    method to solve the problem that extends methods for finite-horizon DEC-POMDPs
    and the RTDP-Bel approach for POMDPs. We present experimental results on several
    examples, and show that our approach presents promising results. Copyright '
author:
- 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: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
citation:
  ama: 'Chatterjee K, Chmelik M. Indefinite-horizon reachability in Goal-DEC-POMDPs.
    In: <i>Proceedings of the Twenty-Sixth International Conference on International
    Conference on Automated Planning and Scheduling</i>. Vol 2016-January. AAAI Press;
    2016:88-96.'
  apa: 'Chatterjee, K., &#38; Chmelik, M. (2016). Indefinite-horizon reachability
    in Goal-DEC-POMDPs. In <i>Proceedings of the Twenty-Sixth International Conference
    on International Conference on Automated Planning and Scheduling</i> (Vol. 2016–January,
    pp. 88–96). London, United Kingdom: AAAI Press.'
  chicago: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
    in Goal-DEC-POMDPs.” In <i>Proceedings of the Twenty-Sixth International Conference
    on International Conference on Automated Planning and Scheduling</i>, 2016–January:88–96.
    AAAI Press, 2016.
  ieee: K. Chatterjee and M. Chmelik, “Indefinite-horizon reachability in Goal-DEC-POMDPs,”
    in <i>Proceedings of the Twenty-Sixth International Conference on International
    Conference on Automated Planning and Scheduling</i>, London, United Kingdom, 2016,
    vol. 2016–January, pp. 88–96.
  ista: 'Chatterjee K, Chmelik M. 2016. Indefinite-horizon reachability in Goal-DEC-POMDPs.
    Proceedings of the Twenty-Sixth International Conference on International Conference
    on Automated Planning and Scheduling. ICAPS: International Conference on Automated
    Planning and Scheduling vol. 2016–January, 88–96.'
  mla: Chatterjee, Krishnendu, and Martin Chmelik. “Indefinite-Horizon Reachability
    in Goal-DEC-POMDPs.” <i>Proceedings of the Twenty-Sixth International Conference
    on International Conference on Automated Planning and Scheduling</i>, vol. 2016–January,
    AAAI Press, 2016, pp. 88–96.
  short: K. Chatterjee, M. Chmelik, in:, Proceedings of the Twenty-Sixth International
    Conference on International Conference on Automated Planning and Scheduling, AAAI
    Press, 2016, pp. 88–96.
conference:
  end_date: 2016-06-17
  location: London, United Kingdom
  name: 'ICAPS: International Conference on Automated Planning and Scheduling'
  start_date: 2016-06-12
date_created: 2018-12-11T11:51:22Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- url: http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/12999
month: '01'
oa_version: None
page: 88 - 96
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _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
publication: Proceedings of the Twenty-Sixth International Conference on International
  Conference on Automated Planning and Scheduling
publication_status: published
publisher: AAAI Press
publist_id: '5946'
quality_controlled: '1'
scopus_import: 1
status: public
title: Indefinite-horizon reachability in Goal-DEC-POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 2016-January
year: '2016'
...
---
_id: '1325'
abstract:
- lang: eng
  text: We study graphs and two-player games in which rewards are assigned to states,
    and the goal of the players is to satisfy or dissatisfy certain property of the
    generated outcome, given as a mean payoff property. Since the notion of mean-payoff
    does not reflect possible fluctuations from the mean-payoff along a run, we propose
    definitions and algorithms for capturing the stability of the system, and give
    algorithms for deciding if a given mean payoff and stability objective can be
    ensured in the system.
acknowledgement: "The work has been supported by the Czech Science Foundation, grant
  No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie
  Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013)
  under REA grant agreement no [291734]"
alternative_title:
- LIPIcs
article_number: '10'
author:
- first_name: Tomáš
  full_name: Brázdil, Tomáš
  last_name: Brázdil
- first_name: Vojtěch
  full_name: Forejt, Vojtěch
  last_name: Forejt
- first_name: Antonín
  full_name: Kučera, Antonín
  last_name: Kučera
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
citation:
  ama: 'Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In:
    Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.10">10.4230/LIPIcs.CONCUR.2016.10</a>'
  apa: 'Brázdil, T., Forejt, V., Kučera, A., &#38; Novotný, P. (2016). Stability in
    graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec
    City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.10">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>'
  chicago: Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability
    in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.10">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>.
  ieee: 'T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and
    games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016,
    vol. 59.'
  ista: 'Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games.
    CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.'
  mla: Brázdil, Tomáš, et al. <i>Stability in Graphs and Games</i>. Vol. 59, 10, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2016.10">10.4230/LIPIcs.CONCUR.2016.10</a>.
  short: T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2016.
conference:
  end_date: 2016-08-26
  location: Quebec City, Canada
  name: 'CONCUR: Concurrency Theory'
  start_date: 2016-08-23
date_created: 2018-12-11T11:51:23Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.CONCUR.2016.10
ec_funded: 1
file:
- access_level: open_access
  checksum: 3c2dc6ab0358f8aa8f7aa7d6c1293159
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:40Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '5229'
  file_name: IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf
  file_size: 553648
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '        59'
language:
- iso: eng
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '5944'
pubrep_id: '665'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stability in graphs and games
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: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 59
year: '2016'
...
---
_id: '1326'
abstract:
- lang: eng
  text: 'Energy Markov Decision Processes (EMDPs) are finite-state Markov decision
    processes where each transition is assigned an integer counter update and a rational
    payoff. An EMDP configuration is a pair s(n), where s is a control state and n
    is the current counter value. The configurations are changed by performing transitions
    in the standard way. We consider the problem of computing a safe strategy (i.e.,
    a strategy that keeps the counter non-negative) which maximizes the expected mean
    payoff. '
acknowledgement: The research was funded by the Czech Science Foundation Grant No.
  P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s
  Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].
alternative_title:
- LNCS
author:
- first_name: Tomáš
  full_name: Brázdil, Tomáš
  last_name: Brázdil
- first_name: Antonín
  full_name: Kučera, Antonín
  last_name: Kučera
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
citation:
  ama: 'Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy
    Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:<a href="https://doi.org/10.1007/978-3-319-46520-3_3">10.1007/978-3-319-46520-3_3</a>'
  apa: 'Brázdil, T., Kučera, A., &#38; Novotný, P. (2016). Optimizing the expected
    mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented
    at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan:
    Springer. <a href="https://doi.org/10.1007/978-3-319-46520-3_3">https://doi.org/10.1007/978-3-319-46520-3_3</a>'
  chicago: Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected
    Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016.
    <a href="https://doi.org/10.1007/978-3-319-46520-3_3">https://doi.org/10.1007/978-3-319-46520-3_3</a>.
  ieee: 'T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff
    in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology
    for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.'
  ista: 'Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff
    in Energy Markov Decision Processes. ATVA: Automated Technology for Verification
    and Analysis, LNCS, vol. 9938, 32–49.'
  mla: Brázdil, Tomáš, et al. <i>Optimizing the Expected Mean Payoff in Energy Markov
    Decision Processes</i>. Vol. 9938, Springer, 2016, pp. 32–49, doi:<a href="https://doi.org/10.1007/978-3-319-46520-3_3">10.1007/978-3-319-46520-3_3</a>.
  short: T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.
conference:
  end_date: 2016-10-20
  location: Chiba, Japan
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2016-10-17
date_created: 2018-12-11T11:51:23Z
date_published: 2016-09-22T00:00:00Z
date_updated: 2021-01-12T06:49:53Z
day: '22'
department:
- _id: KrCh
doi: 10.1007/978-3-319-46520-3_3
ec_funded: 1
intvolume: '      9938'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1607.00678
month: '09'
oa: 1
oa_version: Preprint
page: 32 - 49
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: Springer
publist_id: '5943'
quality_controlled: '1'
scopus_import: 1
status: public
title: Optimizing the expected mean payoff in Energy Markov Decision Processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 9938
year: '2016'
...
---
_id: '1327'
abstract:
- lang: eng
  text: 'We consider partially observable Markov decision processes (POMDPs) with
    a set of target states and positive integer costs associated with every transition.
    The traditional optimization objective (stochastic shortest path) asks to minimize
    the expected total cost until the target set is reached. We extend the traditional
    framework of POMDPs to model energy consumption, which represents a hard constraint.
    The energy levels may increase and decrease with transitions, and the hard constraint
    requires that the energy level must remain positive in all steps till the target
    is reached. First, we present a novel algorithm for solving POMDPs with energy
    levels, developing on existing POMDP solvers and using RTDP as its main method.
    Our second contribution is related to policy representation. For larger POMDP
    instances the policies computed by existing solvers are too large to be understandable.
    We present an automated procedure based on machine learning techniques that automatically
    extracts important decisions of the policy allowing us to compute succinct human
    readable policies. Finally, we show experimentally that our algorithm performs
    well and computes succinct policies on a number of POMDP instances from the literature
    that were naturally enhanced with energy levels. '
author:
- first_name: Tomáš
  full_name: Brázdil, Tomáš
  last_name: Brázdil
- 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: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Anchit
  full_name: Gupta, Anchit
  last_name: Gupta
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
citation:
  ama: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest
    path with energy constraints in POMDPs. In: <i>Proceedings of the 15th International
    Conference on Autonomous Agents and Multiagent Systems</i>. ACM; 2016:1465-1466.'
  apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., &#38; Novotný, P. (2016).
    Stochastic shortest path with energy constraints in POMDPs. In <i>Proceedings
    of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>
    (pp. 1465–1466). Singapore: ACM.'
  chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and
    Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In
    <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent
    Systems</i>, 1465–66. ACM, 2016.
  ieee: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic
    shortest path with energy constraints in POMDPs,” in <i>Proceedings of the 15th
    International Conference on Autonomous Agents and Multiagent Systems</i>, Singapore,
    2016, pp. 1465–1466.
  ista: 'Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic
    shortest path with energy constraints in POMDPs. Proceedings of the 15th International
    Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents
    &#38; Multiagent Systems, 1465–1466.'
  mla: Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in
    POMDPs.” <i>Proceedings of the 15th International Conference on Autonomous Agents
    and Multiagent Systems</i>, ACM, 2016, pp. 1465–66.
  short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings
    of the 15th International Conference on Autonomous Agents and Multiagent Systems,
    ACM, 2016, pp. 1465–1466.
conference:
  end_date: 2016-05-13
  location: Singapore
  name: 'AAMAS: Autonomous Agents & Multiagent Systems'
  start_date: 2016-05-09
date_created: 2018-12-11T11:51:23Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2021-01-12T06:49:54Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1602.07565
month: '01'
oa: 1
oa_version: Preprint
page: 1465 - 1466
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Proceedings of the 15th International Conference on Autonomous Agents
  and Multiagent Systems
publication_status: published
publisher: ACM
publist_id: '5942'
quality_controlled: '1'
scopus_import: 1
status: public
title: Stochastic shortest path with energy constraints in POMDPs
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1333'
abstract:
- lang: eng
  text: Social dilemmas force players to balance between personal and collective gain.
    In many dilemmas, such as elected governments negotiating climate-change mitigation
    measures, the decisions are made not by individual players but by their representatives.
    However, the behaviour of representatives in social dilemmas has not been investigated
    experimentally. Here inspired by the negotiations for greenhouse-gas emissions
    reductions, we experimentally study a collective-risk social dilemma that involves
    representatives deciding on behalf of their fellow group members. Representatives
    can be re-elected or voted out after each consecutive collective-risk game. Selfish
    players are preferentially elected and are hence found most frequently in the
    &quot;representatives&quot; treatment. Across all treatments, we identify the
    selfish players as extortioners. As predicted by our mathematical model, their
    steadfast strategies enforce cooperation from fair players who finally compensate
    almost completely the deficit caused by the extortionate co-players. Everybody
    gains, but the extortionate representatives and their groups gain the most.
acknowledgement: We thank the students for participation; H.-J. Krambeck for writing
  the software for the game; H. Arndt, T. Bakker, L. Becks, H. Brendelberger, S. Dobler
  and T. Reusch for support; and the Max Planck Society for the Advancement of Science
  for funding.
article_number: '10915'
author:
- first_name: Manfred
  full_name: Milinski, Manfred
  last_name: Milinski
- first_name: Christian
  full_name: Hilbe, Christian
  id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
  last_name: Hilbe
  orcid: 0000-0001-5116-955X
- first_name: Dirk
  full_name: Semmann, Dirk
  last_name: Semmann
- first_name: Ralf
  full_name: Sommerfeld, Ralf
  last_name: Sommerfeld
- first_name: Jochem
  full_name: Marotzke, Jochem
  last_name: Marotzke
citation:
  ama: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. Humans choose representatives
    who enforce cooperation in social dilemmas through extortion. <i>Nature Communications</i>.
    2016;7. doi:<a href="https://doi.org/10.1038/ncomms10915">10.1038/ncomms10915</a>
  apa: Milinski, M., Hilbe, C., Semmann, D., Sommerfeld, R., &#38; Marotzke, J. (2016).
    Humans choose representatives who enforce cooperation in social dilemmas through
    extortion. <i>Nature Communications</i>. Nature Publishing Group. <a href="https://doi.org/10.1038/ncomms10915">https://doi.org/10.1038/ncomms10915</a>
  chicago: Milinski, Manfred, Christian Hilbe, Dirk Semmann, Ralf Sommerfeld, and
    Jochem Marotzke. “Humans Choose Representatives Who Enforce Cooperation in Social
    Dilemmas through Extortion.” <i>Nature Communications</i>. Nature Publishing Group,
    2016. <a href="https://doi.org/10.1038/ncomms10915">https://doi.org/10.1038/ncomms10915</a>.
  ieee: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, and J. Marotzke, “Humans
    choose representatives who enforce cooperation in social dilemmas through extortion,”
    <i>Nature Communications</i>, vol. 7. Nature Publishing Group, 2016.
  ista: Milinski M, Hilbe C, Semmann D, Sommerfeld R, Marotzke J. 2016. Humans choose
    representatives who enforce cooperation in social dilemmas through extortion.
    Nature Communications. 7, 10915.
  mla: Milinski, Manfred, et al. “Humans Choose Representatives Who Enforce Cooperation
    in Social Dilemmas through Extortion.” <i>Nature Communications</i>, vol. 7, 10915,
    Nature Publishing Group, 2016, doi:<a href="https://doi.org/10.1038/ncomms10915">10.1038/ncomms10915</a>.
  short: M. Milinski, C. Hilbe, D. Semmann, R. Sommerfeld, J. Marotzke, Nature Communications
    7 (2016).
date_created: 2018-12-11T11:51:25Z
date_published: 2016-03-07T00:00:00Z
date_updated: 2021-01-12T06:49:57Z
day: '07'
ddc:
- '519'
- '530'
- '599'
department:
- _id: KrCh
doi: 10.1038/ncomms10915
file:
- access_level: open_access
  checksum: 9ea0d7ce59a555a1cb8353d5559407cb
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:10:44Z
  date_updated: 2020-07-14T12:44:44Z
  file_id: '4834'
  file_name: IST-2016-661-v1+1_ncomms10915.pdf
  file_size: 1432577
  relation: main_file
file_date_updated: 2020-07-14T12:44:44Z
has_accepted_license: '1'
intvolume: '         7'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
publication: Nature Communications
publication_status: published
publisher: Nature Publishing Group
publist_id: '5935'
pubrep_id: '661'
quality_controlled: '1'
scopus_import: 1
status: public
title: Humans choose representatives who enforce cooperation in social dilemmas through
  extortion
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: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 7
year: '2016'
...
