---
_id: '744'
abstract:
- lang: eng
  text: In evolutionary game theory interactions between individuals are often assumed
    obligatory. However, in many real-life situations, individuals can decide to opt
    out of an interaction depending on the information they have about the opponent.
    We consider a simple evolutionary game theoretic model to study such a scenario,
    where at each encounter between two individuals the type of the opponent (cooperator/defector)
    is known with some probability, and where each individual either accepts or opts
    out of the interaction. If the type of the opponent is unknown, a trustful individual
    accepts the interaction, whereas a suspicious individual opts out of the interaction.
    If either of the two individuals opt out both individuals remain without an interaction.
    We show that in the prisoners dilemma optional interactions along with suspicious
    behaviour facilitates the emergence of trustful cooperation.
article_processing_charge: No
article_type: original
author:
- first_name: Tadeas
  full_name: Priklopil, Tadeas
  id: 3C869AA0-F248-11E8-B48F-1D18A9856A87
  last_name: Priklopil
- 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: Priklopil T, Chatterjee K, Nowak M. Optional interactions and suspicious behaviour
    facilitates trustful cooperation in prisoners dilemma. <i> Journal of Theoretical
    Biology</i>. 2017;433:64-72. doi:<a href="https://doi.org/10.1016/j.jtbi.2017.08.025">10.1016/j.jtbi.2017.08.025</a>
  apa: Priklopil, T., Chatterjee, K., &#38; Nowak, M. (2017). Optional interactions
    and suspicious behaviour facilitates trustful cooperation in prisoners dilemma.
    <i> Journal of Theoretical Biology</i>. Elsevier. <a href="https://doi.org/10.1016/j.jtbi.2017.08.025">https://doi.org/10.1016/j.jtbi.2017.08.025</a>
  chicago: Priklopil, Tadeas, Krishnendu Chatterjee, and Martin Nowak. “Optional Interactions
    and Suspicious Behaviour Facilitates Trustful Cooperation in Prisoners Dilemma.”
    <i> Journal of Theoretical Biology</i>. Elsevier, 2017. <a href="https://doi.org/10.1016/j.jtbi.2017.08.025">https://doi.org/10.1016/j.jtbi.2017.08.025</a>.
  ieee: T. Priklopil, K. Chatterjee, and M. Nowak, “Optional interactions and suspicious
    behaviour facilitates trustful cooperation in prisoners dilemma,” <i> Journal
    of Theoretical Biology</i>, vol. 433. Elsevier, pp. 64–72, 2017.
  ista: Priklopil T, Chatterjee K, Nowak M. 2017. Optional interactions and suspicious
    behaviour facilitates trustful cooperation in prisoners dilemma.  Journal of Theoretical
    Biology. 433, 64–72.
  mla: Priklopil, Tadeas, et al. “Optional Interactions and Suspicious Behaviour Facilitates
    Trustful Cooperation in Prisoners Dilemma.” <i> Journal of Theoretical Biology</i>,
    vol. 433, Elsevier, 2017, pp. 64–72, doi:<a href="https://doi.org/10.1016/j.jtbi.2017.08.025">10.1016/j.jtbi.2017.08.025</a>.
  short: T. Priklopil, K. Chatterjee, M. Nowak,  Journal of Theoretical Biology 433
    (2017) 64–72.
date_created: 2018-12-11T11:48:16Z
date_published: 2017-11-21T00:00:00Z
date_updated: 2023-09-27T12:29:02Z
day: '21'
ddc:
- '000'
- '570'
department:
- _id: KrCh
doi: 10.1016/j.jtbi.2017.08.025
ec_funded: 1
external_id:
  isi:
  - '000412039800007'
  pmid:
  - '28867224'
file:
- access_level: open_access
  checksum: 4b43af1615ebf1a861840cb03d8a320c
  content_type: application/pdf
  creator: dernst
  date_created: 2019-11-19T07:57:39Z
  date_updated: 2020-07-14T12:47:58Z
  file_id: '7047'
  file_name: 2017_JournTheoretBio_Priklopil.pdf
  file_size: 537323
  relation: main_file
file_date_updated: 2020-07-14T12:47:58Z
has_accepted_license: '1'
intvolume: '       433'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc-nd/4.0/
month: '11'
oa: 1
oa_version: Submitted Version
page: 64 - 72
pmid: 1
project:
- _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: ' Journal of Theoretical Biology'
publication_identifier:
  issn:
  - '00225193'
publication_status: published
publisher: Elsevier
publist_id: '6923'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optional interactions and suspicious behaviour facilitates trustful cooperation
  in prisoners dilemma
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 433
year: '2017'
...
---
_id: '1407'
abstract:
- lang: eng
  text: We consider the problem of computing the set of initial states of a dynamical
    system such that there exists a control strategy to ensure that the trajectories
    satisfy a temporal logic specification with probability 1 (almost-surely). We
    focus on discrete-time, stochastic linear dynamics and specifications given as
    formulas of the Generalized Reactivity(1) fragment of Linear Temporal Logic over
    linear predicates in the states of the system. We propose a solution based on
    iterative abstraction-refinement, and turn-based 2-player probabilistic games.
    While the theoretical guarantee of our algorithm after any finite number of iterations
    is only a partial solution, we show that if our algorithm terminates, then the
    result is the set of all satisfying initial states. Moreover, for any (partial)
    solution our algorithm synthesizes witness control strategies to ensure almost-sure
    satisfaction of the temporal logic specification. While the proposed algorithm
    guarantees progress and soundness in every iteration, it is computationally demanding.
    We offer an alternative, more efficient solution for the reachability properties
    that decomposes the problem into a series of smaller problems of the same type.
    All algorithms are demonstrated on an illustrative case study.
article_processing_charge: No
arxiv: 1
author:
- first_name: Mária
  full_name: Svoreňová, Mária
  last_name: Svoreňová
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ivana
  full_name: Cěrná, Ivana
  last_name: Cěrná
- first_name: Cǎlin
  full_name: Belta, Cǎlin
  last_name: Belta
citation:
  ama: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. Temporal
    logic control for stochastic linear systems using abstraction refinement of probabilistic
    games. <i>Nonlinear Analysis: Hybrid Systems</i>. 2017;23(2):230-253. doi:<a href="https://doi.org/10.1016/j.nahs.2016.04.006">10.1016/j.nahs.2016.04.006</a>'
  apa: 'Svoreňová, M., Kretinsky, J., Chmelik, M., Chatterjee, K., Cěrná, I., &#38;
    Belta, C. (2017). Temporal logic control for stochastic linear systems using abstraction
    refinement of probabilistic games. <i>Nonlinear Analysis: Hybrid Systems</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.nahs.2016.04.006">https://doi.org/10.1016/j.nahs.2016.04.006</a>'
  chicago: 'Svoreňová, Mária, Jan Kretinsky, Martin Chmelik, Krishnendu Chatterjee,
    Ivana Cěrná, and Cǎlin Belta. “Temporal Logic Control for Stochastic Linear Systems
    Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid
    Systems</i>. Elsevier, 2017. <a href="https://doi.org/10.1016/j.nahs.2016.04.006">https://doi.org/10.1016/j.nahs.2016.04.006</a>.'
  ieee: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, and C. Belta,
    “Temporal logic control for stochastic linear systems using abstraction refinement
    of probabilistic games,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 23, no.
    2. Elsevier, pp. 230–253, 2017.'
  ista: 'Svoreňová M, Kretinsky J, Chmelik M, Chatterjee K, Cěrná I, Belta C. 2017.
    Temporal logic control for stochastic linear systems using abstraction refinement
    of probabilistic games. Nonlinear Analysis: Hybrid Systems. 23(2), 230–253.'
  mla: 'Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems
    Using Abstraction Refinement of Probabilistic Games.” <i>Nonlinear Analysis: Hybrid
    Systems</i>, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:<a href="https://doi.org/10.1016/j.nahs.2016.04.006">10.1016/j.nahs.2016.04.006</a>.'
  short: 'M. Svoreňová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cěrná, C. Belta,
    Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.'
date_created: 2018-12-11T11:51:50Z
date_published: 2017-02-01T00:00:00Z
date_updated: 2023-09-20T09:43:09Z
day: '01'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1016/j.nahs.2016.04.006
ec_funded: 1
external_id:
  arxiv:
  - '1410.5387'
  isi:
  - '000390637000014'
intvolume: '        23'
isi: 1
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1410.5387
month: '02'
oa: 1
oa_version: Preprint
page: 230 - 253
project:
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _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: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_status: published
publisher: Elsevier
publist_id: '5800'
quality_controlled: '1'
related_material:
  record:
  - id: '1689'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Temporal logic control for stochastic linear systems using abstraction refinement
  of probabilistic games
type: journal_article
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 23
year: '2017'
...
---
_id: '5455'
abstract:
- lang: eng
  text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
    reachability. The input is a graphwhere the edges are labeled with different types
    of opening and closing parentheses, and the reachabilityinformation is computed
    via paths whose parentheses are properly matched. We present new results for Dyckreachability
    problems with applications to alias analysis and data-dependence analysis. Our
    main contributions,that include improved upper bounds as well as lower bounds
    that establish optimality guarantees, are asfollows:First, we consider Dyck reachability
    on bidirected graphs, which is the standard way of performing field-sensitive
    points-to analysis. Given a bidirected graph withnnodes andmedges, we present:
    (i) an algorithmwith worst-case running timeO(m+n·α(n)), whereα(n)is the inverse
    Ackermann function, improving thepreviously knownO(n2)time bound; (ii) a matching
    lower bound that shows that our algorithm is optimalwrt to worst-case complexity;
    and (iii) an optimal average-case upper bound ofO(m)time, improving thepreviously
    knownO(m·logn)bound.Second, we consider the problem of context-sensitive data-dependence
    analysis, where the task is to obtainanalysis summaries of library code in the
    presence of callbacks. Our algorithm preprocesses libraries in almostlinear time,
    after which the contribution of the library in the complexity of the client analysis
    is only linear,and only wrt the number of call sites.Third, we prove that combinatorial
    algorithms for Dyck reachability on general graphs with truly sub-cubic bounds
    cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean
    MatrixMultiplication, which is a long-standing open problem. Thus we establish
    that the existing combinatorialalgorithms for Dyck reachability are (conditionally)
    optimal for general graphs. We also show that the samehardness holds for graphs
    of constant treewidth.Finally, we provide a prototype implementation of our algorithms
    for both alias analysis and data-dependenceanalysis. Our experimental evaluation
    demonstrates that the new algorithms significantly outperform allexisting methods
    on the two problems, over real-world benchmarks.'
alternative_title:
- IST Austria Technical Report
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Bhavya
  full_name: Choudhary, Bhavya
  last_name: Choudhary
- 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, Choudhary B, Pavlogiannis A. <i>Optimal Dyck Reachability for
    Data-Dependence and Alias Analysis</i>. IST Austria; 2017. doi:<a href="https://doi.org/10.15479/AT:IST-2017-870-v1-1">10.15479/AT:IST-2017-870-v1-1</a>
  apa: Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). <i>Optimal Dyck
    reachability for data-dependence and alias analysis</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2017-870-v1-1">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>
  chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. <i>Optimal
    Dyck Reachability for Data-Dependence and Alias Analysis</i>. IST Austria, 2017.
    <a href="https://doi.org/10.15479/AT:IST-2017-870-v1-1">https://doi.org/10.15479/AT:IST-2017-870-v1-1</a>.
  ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, <i>Optimal Dyck reachability
    for data-dependence and alias analysis</i>. IST Austria, 2017.
  ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
    for data-dependence and alias analysis, IST Austria, 37p.
  mla: Chatterjee, Krishnendu, et al. <i>Optimal Dyck Reachability for Data-Dependence
    and Alias Analysis</i>. IST Austria, 2017, doi:<a href="https://doi.org/10.15479/AT:IST-2017-870-v1-1">10.15479/AT:IST-2017-870-v1-1</a>.
  short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, Optimal Dyck Reachability for
    Data-Dependence and Alias Analysis, IST Austria, 2017.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-21T15:54:10Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-870-v1-1
file:
- access_level: open_access
  checksum: 177a84a46e3ac17e87b31534ad16a4c9
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:02Z
  date_updated: 2020-07-14T12:46:59Z
  file_id: '5524'
  file_name: IST-2017-870-v1+1_main.pdf
  file_size: 960491
  relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '37'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '870'
related_material:
  record:
  - id: '10416'
    relation: later_version
    status: public
status: public
title: Optimal Dyck reachability for data-dependence and alias analysis
type: technical_report
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2017'
...
---
_id: '5456'
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\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.\r\n1.
    For acyclic architectures, our algorithm is guaranteed to explore exactly one
    representative trace from each observation class, while spending polynomial time
    per class. Hence, our algorithm is optimal wrt the observation equivalence, and
    in several cases explores exponentially fewer traces than any enumerative method
    based on the Mazurkiewicz equivalence.\r\n2. For cyclic architectures, we consider
    an equivalence between traces which is finer than the observation equivalence;
    but coarser than the Mazurkiewicz equivalence, and in some cases is exponentially
    coarser. Our data-centric DPOR algorithm remains optimal under this trace equivalence.
    \r\nFinally, we perform a basic experimental comparison between the existing Mazurkiewicz-based
    DPOR and our data-centric DPOR on a set of academic benchmarks. Our results show
    a significant reduction in both running time and the number of explored equivalence
    classes."
alternative_title:
- IST Austria Technical Report
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. <i>Data-Centric
    Dynamic Partial Order Reduction</i>. IST Austria; 2017. doi:<a href="https://doi.org/10.15479/AT:IST-2017-872-v1-1">10.15479/AT:IST-2017-872-v1-1</a>
  apa: Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K.
    (2017). <i>Data-centric dynamic partial order reduction</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2017-872-v1-1">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>
  chicago: Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha,
    and Kapil Vaidya. <i>Data-Centric Dynamic Partial Order Reduction</i>. IST Austria,
    2017. <a href="https://doi.org/10.15479/AT:IST-2017-872-v1-1">https://doi.org/10.15479/AT:IST-2017-872-v1-1</a>.
  ieee: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, <i>Data-centric
    dynamic partial order reduction</i>. IST Austria, 2017.
  ista: Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2017. Data-centric
    dynamic partial order reduction, IST Austria, 36p.
  mla: Chalupa, Marek, et al. <i>Data-Centric Dynamic Partial Order Reduction</i>.
    IST Austria, 2017, doi:<a href="https://doi.org/10.15479/AT:IST-2017-872-v1-1">10.15479/AT:IST-2017-872-v1-1</a>.
  short: M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Data-Centric
    Dynamic Partial Order Reduction, IST Austria, 2017.
date_created: 2018-12-12T11:39:26Z
date_published: 2017-10-23T00:00:00Z
date_updated: 2023-02-23T12:26:54Z
day: '23'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-872-v1-1
file:
- access_level: open_access
  checksum: d2635c4cf013000f0a1b09e80f9e4ab7
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:26Z
  date_updated: 2020-07-14T12:46:59Z
  file_id: '5487'
  file_name: IST-2017-872-v1+1_main.pdf
  file_size: 910347
  relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '10'
oa: 1
oa_version: Published Version
page: '36'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '872'
related_material:
  record:
  - id: '10417'
    relation: later_version
    status: public
  - id: '5448'
    relation: earlier_version
    status: public
status: public
title: Data-centric dynamic partial order reduction
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '551'
abstract:
- lang: eng
  text: 'Evolutionary graph theory studies the evolutionary dynamics in a population
    structure given as a connected graph. Each node of the graph represents an individual
    of the population, and edges determine how offspring are placed. We consider the
    classical birth-death Moran process where there are two types of individuals,
    namely, the residents with fitness 1 and mutants with fitness r. The fitness indicates
    the reproductive strength. The evolutionary dynamics happens as follows: in the
    initial step, in a population of all resident individuals a mutant is introduced,
    and then at each step, an individual is chosen proportional to the fitness of
    its type to reproduce, and the offspring replaces a neighbor uniformly at random.
    The process stops when all individuals are either residents or mutants. The probability
    that all individuals in the end are mutants is called the fixation probability,
    which is a key factor in the rate of evolution. We consider the problem of approximating
    the fixation probability. The class of algorithms that is extremely relevant for
    approximation of the fixation probabilities is the Monte-Carlo simulation of the
    process. Previous results present a polynomial-time Monte-Carlo algorithm for
    undirected graphs when r is given in unary. First, we present a simple modification:
    instead of simulating each step, we discard ineffective steps, where no node changes
    type (i.e., either residents replace residents, or mutants replace mutants). Using
    the above simple modification and our result that the number of effective steps
    is concentrated around the expected number of effective steps, we present faster
    polynomial-time Monte-Carlo algorithms for undirected graphs. Our algorithms are
    always at least a factor O(n2/ log n) faster as compared to the previous algorithms,
    where n is the number of nodes, and is polynomial even if r is given in binary.
    We also present lower bounds showing that the upper bound on the expected number
    of effective steps we present is asymptotically tight for undirected graphs. '
alternative_title:
- LIPIcs
article_number: '61'
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: 'Chatterjee K, Ibsen-Jensen R, Nowak M. Faster Monte Carlo algorithms for fixation
    probability of the Moran process on undirected graphs. In: <i>Leibniz International
    Proceedings in Informatics</i>. Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik; 2017. doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.61">10.4230/LIPIcs.MFCS.2017.61</a>'
  apa: 'Chatterjee, K., Ibsen-Jensen, R., &#38; Nowak, M. (2017). Faster Monte Carlo
    algorithms for fixation probability of the Moran process on undirected graphs.
    In <i>Leibniz International Proceedings in Informatics</i> (Vol. 83). Aalborg,
    Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.61">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>'
  chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Martin Nowak. “Faster
    Monte Carlo Algorithms for Fixation Probability of the Moran Process on Undirected
    Graphs.” In <i>Leibniz International Proceedings in Informatics</i>, Vol. 83.
    Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.61">https://doi.org/10.4230/LIPIcs.MFCS.2017.61</a>.
  ieee: K. Chatterjee, R. Ibsen-Jensen, and M. Nowak, “Faster Monte Carlo algorithms
    for fixation probability of the Moran process on undirected graphs,” in <i>Leibniz
    International Proceedings in Informatics</i>, Aalborg, Denmark, 2017, vol. 83.
  ista: 'Chatterjee K, Ibsen-Jensen R, Nowak M. 2017. Faster Monte Carlo algorithms
    for fixation probability of the Moran process on undirected graphs. Leibniz International
    Proceedings in Informatics. MFCS: Mathematical Foundations of Computer Science
    (SG), LIPIcs, vol. 83, 61.'
  mla: Chatterjee, Krishnendu, et al. “Faster Monte Carlo Algorithms for Fixation
    Probability of the Moran Process on Undirected Graphs.” <i>Leibniz International
    Proceedings in Informatics</i>, vol. 83, 61, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2017, doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.61">10.4230/LIPIcs.MFCS.2017.61</a>.
  short: K. Chatterjee, R. Ibsen-Jensen, M. Nowak, in:, Leibniz International Proceedings
    in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
  end_date: 2017-08-25
  location: Aalborg, Denmark
  name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
  start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2021-01-12T08:02:34Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.61
file:
- access_level: open_access
  checksum: 2eed5224c0e4e259484a1d71acb8ba6a
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:04Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '5322'
  file_name: IST-2018-924-v1+1_LIPIcs-MFCS-2017-61.pdf
  file_size: 535077
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: '        83'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '11'
oa: 1
oa_version: Published Version
publication: Leibniz International Proceedings in Informatics
publication_identifier:
  isbn:
  - 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7263'
pubrep_id: '924'
quality_controlled: '1'
scopus_import: 1
status: public
title: Faster Monte Carlo algorithms for fixation probability of the Moran process
  on undirected graphs
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: 83
year: '2017'
...
---
_id: '552'
abstract:
- lang: eng
  text: 'Graph games provide the foundation for modeling and synthesis of reactive
    processes. Such games are played over graphs where the vertices are controlled
    by two adversarial players. We consider graph games where the objective of the
    first player is the conjunction of a qualitative objective (specified as a parity
    condition) and a quantitative objective (specified as a meanpayoff condition).
    There are two variants of the problem, namely, the threshold problem where the
    quantitative goal is to ensure that the mean-payoff value is above a threshold,
    and the value problem where the quantitative goal is to ensure the optimal mean-payoff
    value; in both cases ensuring the qualitative parity objective. The previous best-known
    algorithms for game graphs with n vertices, m edges, parity objectives with d
    priorities, and maximal absolute reward value W for mean-payoff objectives, are
    as follows: O(nd+1 . m . w) for the threshold problem, and O(nd+2 · m · W) for
    the value problem. Our main contributions are faster algorithms, and the running
    times of our algorithms are as follows: O(nd-1 · m ·W) for the threshold problem,
    and O(nd · m · W · log(n · W)) for the value problem. For mean-payoff parity objectives
    with two priorities, our algorithms match the best-known bounds of the algorithms
    for mean-payoff games (without conjunction with parity objectives). Our results
    are relevant in synthesis of reactive systems with both functional requirement
    (given as a qualitative objective) and performance requirement (given as a quantitative
    objective).'
alternative_title:
- LIPIcs
article_number: '39'
article_processing_charge: No
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Monika H
  full_name: Henzinger, Monika H
  id: 540c9bbd-f2de-11ec-812d-d04a5be85630
  last_name: Henzinger
  orcid: 0000-0002-5008-6530
- first_name: Alexander
  full_name: Svozil, Alexander
  last_name: Svozil
citation:
  ama: 'Chatterjee K, Henzinger MH, Svozil A. Faster algorithms for mean-payoff parity
    games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol 83. Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.39">10.4230/LIPIcs.MFCS.2017.39</a>'
  apa: 'Chatterjee, K., Henzinger, M. H., &#38; Svozil, A. (2017). Faster algorithms
    for mean-payoff parity games. In <i>Leibniz International Proceedings in Informatics</i>
    (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
    <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.39">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>'
  chicago: Chatterjee, Krishnendu, Monika H Henzinger, and Alexander Svozil. “Faster
    Algorithms for Mean-Payoff Parity Games.” In <i>Leibniz International Proceedings
    in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2017. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.39">https://doi.org/10.4230/LIPIcs.MFCS.2017.39</a>.
  ieee: K. Chatterjee, M. H. Henzinger, and A. Svozil, “Faster algorithms for mean-payoff
    parity games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg,
    Denmark, 2017, vol. 83.
  ista: 'Chatterjee K, Henzinger MH, Svozil A. 2017. Faster algorithms for mean-payoff
    parity games. Leibniz International Proceedings in Informatics. MFCS: Mathematical
    Foundations of Computer Science (SG), LIPIcs, vol. 83, 39.'
  mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Mean-Payoff Parity Games.”
    <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 39, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.39">10.4230/LIPIcs.MFCS.2017.39</a>.
  short: K. Chatterjee, M.H. Henzinger, A. Svozil, in:, Leibniz International Proceedings
    in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
  end_date: 2017-08-25
  location: Aalborg, Denmark
  name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
  start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2023-02-14T10:06:46Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.39
ec_funded: 1
file:
- access_level: open_access
  checksum: c67f4866ddbfd555afef1f63ae9a8fc7
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:57Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '5248'
  file_name: IST-2018-923-v1+1_LIPIcs-MFCS-2017-39.pdf
  file_size: 610339
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: '        83'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/3.0/
month: '11'
oa: 1
oa_version: Published Version
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: Leibniz International Proceedings in Informatics
publication_identifier:
  isbn:
  - 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7262'
pubrep_id: '923'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for mean-payoff parity games
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
  name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
  short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 83
year: '2017'
...
---
_id: '553'
abstract:
- lang: eng
  text: 'We consider two player, zero-sum, finite-state concurrent reachability games,
    played for an infinite number of rounds, where in every round, each player simultaneously
    and independently of the other players chooses an action, whereafter the successor
    state is determined by a probability distribution given by the current state and
    the chosen actions. Player 1 wins iff a designated goal state is eventually visited.
    We are interested in the complexity of stationary strategies measured by their
    patience, which is defined as the inverse of the smallest non-zero probability
    employed. Our main results are as follows: We show that: (i) the optimal bound
    on the patience of optimal and -optimal strategies, for both players is doubly
    exponential; and (ii) even in games with a single non-absorbing state exponential
    (in the number of actions) patience is necessary. '
alternative_title:
- LIPIcs
article_number: '55'
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Kristofer
  full_name: Hansen, Kristofer
  last_name: Hansen
- first_name: Rasmus
  full_name: Ibsen-Jensen, Rasmus
  id: 3B699956-F248-11E8-B48F-1D18A9856A87
  last_name: Ibsen-Jensen
  orcid: 0000-0003-4783-0389
citation:
  ama: 'Chatterjee K, Hansen K, Ibsen-Jensen R. Strategy complexity of concurrent
    safety games. In: <i>Leibniz International Proceedings in Informatics</i>. Vol
    83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.55">10.4230/LIPIcs.MFCS.2017.55</a>'
  apa: 'Chatterjee, K., Hansen, K., &#38; Ibsen-Jensen, R. (2017). Strategy complexity
    of concurrent safety games. In <i>Leibniz International Proceedings in Informatics</i>
    (Vol. 83). Aalborg, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
    <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.55">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>'
  chicago: Chatterjee, Krishnendu, Kristofer Hansen, and Rasmus Ibsen-Jensen. “Strategy
    Complexity of Concurrent Safety Games.” In <i>Leibniz International Proceedings
    in Informatics</i>, Vol. 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2017. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.55">https://doi.org/10.4230/LIPIcs.MFCS.2017.55</a>.
  ieee: K. Chatterjee, K. Hansen, and R. Ibsen-Jensen, “Strategy complexity of concurrent
    safety games,” in <i>Leibniz International Proceedings in Informatics</i>, Aalborg,
    Denmark, 2017, vol. 83.
  ista: 'Chatterjee K, Hansen K, Ibsen-Jensen R. 2017. Strategy complexity of concurrent
    safety games. Leibniz International Proceedings in Informatics. MFCS: Mathematical
    Foundations of Computer Science (SG), LIPIcs, vol. 83, 55.'
  mla: Chatterjee, Krishnendu, et al. “Strategy Complexity of Concurrent Safety Games.”
    <i>Leibniz International Proceedings in Informatics</i>, vol. 83, 55, Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik, 2017, doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2017.55">10.4230/LIPIcs.MFCS.2017.55</a>.
  short: K. Chatterjee, K. Hansen, R. Ibsen-Jensen, in:, Leibniz International Proceedings
    in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
conference:
  end_date: 2017-08-25
  location: Aalborg, Denmark
  name: 'MFCS: Mathematical Foundations of Computer Science (SG)'
  start_date: 2017-08-21
date_created: 2018-12-11T11:47:08Z
date_published: 2017-11-01T00:00:00Z
date_updated: 2021-01-12T08:02:35Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2017.55
file:
- access_level: open_access
  checksum: 7101facb56ade363205c695d72dbd173
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:09:29Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '4753'
  file_name: IST-2018-922-v1+1_LIPIcs-MFCS-2017-55.pdf
  file_size: 549967
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
intvolume: '        83'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1506.02434
month: '11'
oa: 1
oa_version: Published Version
publication: Leibniz International Proceedings in Informatics
publication_identifier:
  isbn:
  - 978-395977046-0
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '7261'
pubrep_id: '922'
quality_controlled: '1'
scopus_import: 1
status: public
title: Strategy complexity of concurrent safety 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: 83
year: '2017'
...
---
_id: '5559'
abstract:
- lang: eng
  text: Strong amplifiers of natural selection
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. Strong amplifiers of natural
    selection. 2017. doi:<a href="https://doi.org/10.15479/AT:ISTA:51">10.15479/AT:ISTA:51</a>
  apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak , M. (2017). Strong
    amplifiers of natural selection. Institute of Science and Technology Austria.
    <a href="https://doi.org/10.15479/AT:ISTA:51">https://doi.org/10.15479/AT:ISTA:51</a>
  chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak . “Strong Amplifiers of Natural Selection.” Institute of Science and Technology
    Austria, 2017. <a href="https://doi.org/10.15479/AT:ISTA:51">https://doi.org/10.15479/AT:ISTA:51</a>.
  ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak , “Strong amplifiers
    of natural selection.” Institute of Science and Technology Austria, 2017.
  ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak  M. 2017. Strong amplifiers
    of natural selection, Institute of Science and Technology Austria, <a href="https://doi.org/10.15479/AT:ISTA:51">10.15479/AT:ISTA:51</a>.
  mla: Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>.
    Institute of Science and Technology Austria, 2017, doi:<a href="https://doi.org/10.15479/AT:ISTA:51">10.15479/AT:ISTA:51</a>.
  short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak , (2017).
datarep_id: '51'
date_created: 2018-12-12T12:31:32Z
date_published: 2017-01-02T00:00:00Z
date_updated: 2024-02-21T13:48:42Z
day: '02'
ddc:
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:ISTA:51
ec_funded: 1
file:
- access_level: open_access
  checksum: b427dd46a30096a1911b245640c47af8
  content_type: video/mp4
  creator: system
  date_created: 2018-12-12T13:05:18Z
  date_updated: 2020-07-14T12:47:02Z
  file_id: '5644'
  file_name: IST-2017-51-v1+2_illustration.mp4
  file_size: 32987015
  relation: main_file
file_date_updated: 2020-07-14T12:47:02Z
has_accepted_license: '1'
keyword:
- natural selection
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'
publisher: Institute of Science and Technology Austria
related_material:
  record:
  - id: '5452'
    relation: research_paper
    status: public
  - id: '5751'
    relation: research_paper
    status: public
status: public
title: Strong amplifiers of natural selection
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2017'
...
---
_id: '625'
abstract:
- lang: eng
  text: In the analysis of reactive systems a quantitative objective assigns a real
    value to every trace of the system. The value decision problem for a quantitative
    objective requires a trace whose value is at least a given threshold, and the
    exact value decision problem requires a trace whose value is exactly the threshold.
    We compare the computational complexity of the value and exact value decision
    problems for classical quantitative objectives, such as sum, discounted sum, energy,
    and mean-payoff for two standard models of reactive systems, namely, graphs and
    graph games.
acknowledgement: 'This research was supported in part by the Austrian Science Fund
  (FWF) under grants S11402-N23 and S11407-N23 (RiSE/SHiNE), and Z211-N23 (Wittgenstein
  Award), ERC Start grant (279307: Graph Games), Vienna Science and Technology Fund
  (WWTF) through project ICT15-003.'
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: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Chatterjee K, Doyen L, Henzinger TA. The cost of exactness in quantitative
    reachability. In: Aceto L, Bacci G, Ingólfsdóttir A, Legay A, Mardare R, eds.
    <i>Models, Algorithms, Logics and Tools</i>. Vol 10460. Theoretical Computer Science
    and General Issues. Springer; 2017:367-381. doi:<a href="https://doi.org/10.1007/978-3-319-63121-9_18">10.1007/978-3-319-63121-9_18</a>'
  apa: Chatterjee, K., Doyen, L., &#38; Henzinger, T. A. (2017). The cost of exactness
    in quantitative reachability. In L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay,
    &#38; R. Mardare (Eds.), <i>Models, Algorithms, Logics and Tools</i> (Vol. 10460,
    pp. 367–381). Springer. <a href="https://doi.org/10.1007/978-3-319-63121-9_18">https://doi.org/10.1007/978-3-319-63121-9_18</a>
  chicago: Chatterjee, Krishnendu, Laurent Doyen, and Thomas A Henzinger. “The Cost
    of Exactness in Quantitative Reachability.” In <i>Models, Algorithms, Logics and
    Tools</i>, edited by Luca Aceto, Giorgio Bacci, Anna Ingólfsdóttir, Axel Legay,
    and Radu Mardare, 10460:367–81. Theoretical Computer Science and General Issues.
    Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-63121-9_18">https://doi.org/10.1007/978-3-319-63121-9_18</a>.
  ieee: K. Chatterjee, L. Doyen, and T. A. Henzinger, “The cost of exactness in quantitative
    reachability,” in <i>Models, Algorithms, Logics and Tools</i>, vol. 10460, L.
    Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, and R. Mardare, Eds. Springer, 2017,
    pp. 367–381.
  ista: 'Chatterjee K, Doyen L, Henzinger TA. 2017.The cost of exactness in quantitative
    reachability. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, 367–381.'
  mla: Chatterjee, Krishnendu, et al. “The Cost of Exactness in Quantitative Reachability.”
    <i>Models, Algorithms, Logics and Tools</i>, edited by Luca Aceto et al., vol.
    10460, Springer, 2017, pp. 367–81, doi:<a href="https://doi.org/10.1007/978-3-319-63121-9_18">10.1007/978-3-319-63121-9_18</a>.
  short: K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir,
    A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017,
    pp. 367–381.
date_created: 2018-12-11T11:47:34Z
date_published: 2017-07-25T00:00:00Z
date_updated: 2025-06-02T08:53:45Z
day: '25'
ddc:
- '000'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-63121-9_18
ec_funded: 1
editor:
- first_name: Luca
  full_name: Aceto, Luca
  last_name: Aceto
- first_name: Giorgio
  full_name: Bacci, Giorgio
  last_name: Bacci
- first_name: Anna
  full_name: Ingólfsdóttir, Anna
  last_name: Ingólfsdóttir
- first_name: Axel
  full_name: Legay, Axel
  last_name: Legay
- first_name: Radu
  full_name: Mardare, Radu
  last_name: Mardare
file:
- access_level: open_access
  checksum: b2402766ec02c79801aac634bd8f9f6c
  content_type: application/pdf
  creator: dernst
  date_created: 2019-11-19T08:06:50Z
  date_updated: 2020-07-14T12:47:25Z
  file_id: '7048'
  file_name: 2017_ModelsAlgorithms_Chatterjee.pdf
  file_size: 192826
  relation: main_file
file_date_updated: 2020-07-14T12:47:25Z
has_accepted_license: '1'
intvolume: '     10460'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Submitted Version
page: 367 - 381
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
publication: Models, Algorithms, Logics and Tools
publication_identifier:
  isbn:
  - 978-3-319-63120-2
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
publist_id: '7170'
quality_controlled: '1'
scopus_import: '1'
series_title: Theoretical Computer Science and General Issues
status: public
title: The cost of exactness in quantitative reachability
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10460
year: '2017'
...
---
_id: '628'
abstract:
- lang: eng
  text: We consider the problem of developing automated techniques for solving recurrence
    relations to aid the expected-runtime analysis of programs. The motivation is
    that several classical textbook algorithms have quite efficient expected-runtime
    complexity, whereas the corresponding worst-case bounds are either inefficient
    (e.g., Quick-Sort), or completely ineffective (e.g., Coupon-Collector). Since
    the main focus of expected-runtime analysis is to obtain efficient bounds, we
    consider bounds that are either logarithmic, linear or almost-linear (O(log n),
    O(n), O(n · log n), respectively, where n represents the input size). Our main
    contribution is an efficient (simple linear-time algorithm) sound approach for
    deriving such expected-runtime bounds for the analysis of recurrence relations
    induced by randomized algorithms. The experimental results show that our approach
    can efficiently derive asymptotically optimal expected-runtime bounds for recurrences
    of classical randomized algorithms, including Randomized-Search, Quick-Sort, Quick-Select,
    Coupon-Collector, where the worst-case bounds are either inefficient (such as
    linear as compared to logarithmic expected-runtime complexity, or quadratic as
    compared to linear or almost-linear expected-runtime complexity), or ineffective.
alternative_title:
- LNCS
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  last_name: Fu
- first_name: Aniket
  full_name: Murhekar, Aniket
  last_name: Murhekar
citation:
  ama: 'Chatterjee K, Fu H, Murhekar A. Automated recurrence analysis for almost linear
    expected runtime bounds. In: Majumdar R, Kunčak V, eds. Vol 10426. Springer; 2017:118-139.
    doi:<a href="https://doi.org/10.1007/978-3-319-63387-9_6">10.1007/978-3-319-63387-9_6</a>'
  apa: 'Chatterjee, K., Fu, H., &#38; Murhekar, A. (2017). Automated recurrence analysis
    for almost linear expected runtime bounds. In R. Majumdar &#38; V. Kunčak (Eds.)
    (Vol. 10426, pp. 118–139). Presented at the CAV: Computer Aided Verification,
    Heidelberg, Germany: Springer. <a href="https://doi.org/10.1007/978-3-319-63387-9_6">https://doi.org/10.1007/978-3-319-63387-9_6</a>'
  chicago: Chatterjee, Krishnendu, Hongfei Fu, and Aniket Murhekar. “Automated Recurrence
    Analysis for Almost Linear Expected Runtime Bounds.” edited by Rupak Majumdar
    and Viktor Kunčak, 10426:118–39. Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-63387-9_6">https://doi.org/10.1007/978-3-319-63387-9_6</a>.
  ieee: 'K. Chatterjee, H. Fu, and A. Murhekar, “Automated recurrence analysis for
    almost linear expected runtime bounds,” presented at the CAV: Computer Aided Verification,
    Heidelberg, Germany, 2017, vol. 10426, pp. 118–139.'
  ista: 'Chatterjee K, Fu H, Murhekar A. 2017. Automated recurrence analysis for almost
    linear expected runtime bounds. CAV: Computer Aided Verification, LNCS, vol. 10426,
    118–139.'
  mla: Chatterjee, Krishnendu, et al. <i>Automated Recurrence Analysis for Almost
    Linear Expected Runtime Bounds</i>. Edited by Rupak Majumdar and Viktor Kunčak,
    vol. 10426, Springer, 2017, pp. 118–39, doi:<a href="https://doi.org/10.1007/978-3-319-63387-9_6">10.1007/978-3-319-63387-9_6</a>.
  short: K. Chatterjee, H. Fu, A. Murhekar, in:, R. Majumdar, V. Kunčak (Eds.), Springer,
    2017, pp. 118–139.
conference:
  end_date: 2017-07-28
  location: Heidelberg, Germany
  name: 'CAV: Computer Aided Verification'
  start_date: 2017-07-24
date_created: 2018-12-11T11:47:35Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2021-01-12T08:06:55Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_6
ec_funded: 1
editor:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Viktor
  full_name: Kunčak, Viktor
  last_name: Kunčak
intvolume: '     10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1705.00314
month: '01'
oa: 1
oa_version: Submitted Version
page: 118 - 139
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided 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_identifier:
  isbn:
  - 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7166'
quality_controlled: '1'
scopus_import: 1
status: public
title: Automated recurrence analysis for almost linear expected runtime bounds
type: conference
user_id: 4435EBFC-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '639'
abstract:
- lang: eng
  text: We study the problem of developing efficient approaches for proving worst-case
    bounds of non-deterministic recursive programs. Ranking functions are sound and
    complete for proving termination and worst-case bounds of non-recursive programs.
    First, we apply ranking functions to recursion, resulting in measure functions,
    and show that they provide a sound and complete approach to prove worst-case bounds
    of non-deterministic recursive programs. Our second contribution is the synthesis
    of measure functions in non-polynomial forms. We show that non-polynomial measure
    functions with logarithm and exponentiation can be synthesized through abstraction
    of logarithmic or exponentiation terms, Farkas’ Lemma, and Handelman’s Theorem
    using linear programming. While previous methods obtain worst-case polynomial
    bounds, our approach can synthesize bounds of the form O(n log n) as well as O(nr)
    where r is not an integer. We present experimental results to demonstrate that
    our approach can efficiently obtain worst-case bounds of classical recursive algorithms
    such as Merge-Sort, Closest-Pair, Karatsuba’s algorithm and Strassen’s algorithm.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Hongfei
  full_name: Fu, Hongfei
  last_name: Fu
- first_name: Amir
  full_name: Goharshady, Amir
  id: 391365CE-F248-11E8-B48F-1D18A9856A87
  last_name: Goharshady
  orcid: 0000-0003-1702-6584
citation:
  ama: 'Chatterjee K, Fu H, Goharshady AK. Non-polynomial worst case analysis of recursive
    programs. In: Majumdar R, Kunčak V, eds. Vol 10427. Springer; 2017:41-63. doi:<a
    href="https://doi.org/10.1007/978-3-319-63390-9_3">10.1007/978-3-319-63390-9_3</a>'
  apa: 'Chatterjee, K., Fu, H., &#38; Goharshady, A. K. (2017). Non-polynomial worst
    case analysis of recursive programs. In R. Majumdar &#38; V. Kunčak (Eds.) (Vol.
    10427, pp. 41–63). Presented at the CAV: Computer Aided Verification, Heidelberg,
    Germany: Springer. <a href="https://doi.org/10.1007/978-3-319-63390-9_3">https://doi.org/10.1007/978-3-319-63390-9_3</a>'
  chicago: Chatterjee, Krishnendu, Hongfei Fu, and Amir Kafshdar Goharshady. “Non-Polynomial
    Worst Case Analysis of Recursive Programs.” edited by Rupak Majumdar and Viktor
    Kunčak, 10427:41–63. Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-63390-9_3">https://doi.org/10.1007/978-3-319-63390-9_3</a>.
  ieee: 'K. Chatterjee, H. Fu, and A. K. Goharshady, “Non-polynomial worst case analysis
    of recursive programs,” presented at the CAV: Computer Aided Verification, Heidelberg,
    Germany, 2017, vol. 10427, pp. 41–63.'
  ista: 'Chatterjee K, Fu H, Goharshady AK. 2017. Non-polynomial worst case analysis
    of recursive programs. CAV: Computer Aided Verification, LNCS, vol. 10427, 41–63.'
  mla: Chatterjee, Krishnendu, et al. <i>Non-Polynomial Worst Case Analysis of Recursive
    Programs</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10427, Springer,
    2017, pp. 41–63, doi:<a href="https://doi.org/10.1007/978-3-319-63390-9_3">10.1007/978-3-319-63390-9_3</a>.
  short: K. Chatterjee, H. Fu, A.K. Goharshady, in:, R. Majumdar, V. Kunčak (Eds.),
    Springer, 2017, pp. 41–63.
conference:
  end_date: 2017-07-28
  location: Heidelberg, Germany
  name: 'CAV: Computer Aided Verification'
  start_date: 2017-07-24
date_created: 2018-12-11T11:47:39Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-06-02T08:53:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63390-9_3
ec_funded: 1
editor:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Viktor
  full_name: Kunčak, Viktor
  last_name: Kunčak
external_id:
  arxiv:
  - '1705.00317'
intvolume: '     10427'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1705.00317
month: '01'
oa: 1
oa_version: Submitted Version
page: 41 - 63
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:
  isbn:
  - 978-331963389-3
publication_status: published
publisher: Springer
publist_id: '7149'
quality_controlled: '1'
related_material:
  record:
  - id: '8934'
    relation: dissertation_contains
    status: public
  - id: '7014'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Non-polynomial worst case analysis of recursive programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10427
year: '2017'
...
---
_id: '645'
abstract:
- lang: eng
  text: Markov decision processes (MDPs) are standard models for probabilistic systems
    with non-deterministic behaviours. Long-run average rewards provide a mathematically
    elegant formalism for expressing long term performance. Value iteration (VI) is
    one of the simplest and most efficient algorithmic approaches to MDPs with other
    properties, such as reachability objectives. Unfortunately, a naive extension
    of VI does not work for MDPs with long-run average rewards, as there is no known
    stopping criterion. In this work our contributions are threefold. (1) We refute
    a conjecture related to stopping criteria for MDPs with long-run average rewards.
    (2) We present two practical algorithms for MDPs with long-run average rewards
    based on VI. First, we show that a combination of applying VI locally for each
    maximal end-component (MEC) and VI for reachability objectives can provide approximation
    guarantees. Second, extending the above approach with a simulation-guided on-demand
    variant of VI, we present an anytime algorithm that is able to deal with very
    large models. (3) Finally, we present experimental results showing that our methods
    significantly outperform the standard approaches on several benchmarks.
alternative_title:
- LNCS
author:
- first_name: Pranav
  full_name: Ashok, Pranav
  last_name: Ashok
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Przemyslaw
  full_name: Daca, Przemyslaw
  id: 49351290-F248-11E8-B48F-1D18A9856A87
  last_name: Daca
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  last_name: Meggendorfer
citation:
  ama: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. Value iteration
    for long run average reward in markov decision processes. In: Majumdar R, Kunčak
    V, eds. Vol 10426. Springer; 2017:201-221. doi:<a href="https://doi.org/10.1007/978-3-319-63387-9_10">10.1007/978-3-319-63387-9_10</a>'
  apa: 'Ashok, P., Chatterjee, K., Daca, P., Kretinsky, J., &#38; Meggendorfer, T.
    (2017). Value iteration for long run average reward in markov decision processes.
    In R. Majumdar &#38; V. Kunčak (Eds.) (Vol. 10426, pp. 201–221). Presented at
    the CAV: Computer Aided Verification, Heidelberg, Germany: Springer. <a href="https://doi.org/10.1007/978-3-319-63387-9_10">https://doi.org/10.1007/978-3-319-63387-9_10</a>'
  chicago: Ashok, Pranav, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretinsky, and
    Tobias Meggendorfer. “Value Iteration for Long Run Average Reward in Markov Decision
    Processes.” edited by Rupak Majumdar and Viktor Kunčak, 10426:201–21. Springer,
    2017. <a href="https://doi.org/10.1007/978-3-319-63387-9_10">https://doi.org/10.1007/978-3-319-63387-9_10</a>.
  ieee: 'P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, and T. Meggendorfer, “Value
    iteration for long run average reward in markov decision processes,” presented
    at the CAV: Computer Aided Verification, Heidelberg, Germany, 2017, vol. 10426,
    pp. 201–221.'
  ista: 'Ashok P, Chatterjee K, Daca P, Kretinsky J, Meggendorfer T. 2017. Value iteration
    for long run average reward in markov decision processes. CAV: Computer Aided
    Verification, LNCS, vol. 10426, 201–221.'
  mla: Ashok, Pranav, et al. <i>Value Iteration for Long Run Average Reward in Markov
    Decision Processes</i>. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426,
    Springer, 2017, pp. 201–21, doi:<a href="https://doi.org/10.1007/978-3-319-63387-9_10">10.1007/978-3-319-63387-9_10</a>.
  short: P. Ashok, K. Chatterjee, P. Daca, J. Kretinsky, T. Meggendorfer, in:, R.
    Majumdar, V. Kunčak (Eds.), Springer, 2017, pp. 201–221.
conference:
  end_date: 2017-07-28
  location: Heidelberg, Germany
  name: 'CAV: Computer Aided Verification'
  start_date: 2017-07-24
date_created: 2018-12-11T11:47:41Z
date_published: 2017-07-13T00:00:00Z
date_updated: 2021-01-12T08:07:32Z
day: '13'
department:
- _id: KrCh
doi: 10.1007/978-3-319-63387-9_10
ec_funded: 1
editor:
- first_name: Rupak
  full_name: Majumdar, Rupak
  last_name: Majumdar
- first_name: Viktor
  full_name: Kunčak, Viktor
  last_name: Kunčak
intvolume: '     10426'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1705.02326
month: '07'
oa: 1
oa_version: Submitted Version
page: 201 - 221
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided 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_identifier:
  isbn:
  - 978-331963386-2
publication_status: published
publisher: Springer
publist_id: '7135'
quality_controlled: '1'
scopus_import: 1
status: public
title: Value iteration for long run average reward in markov decision processes
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10426
year: '2017'
...
---
_id: '6519'
abstract:
- lang: eng
  text: 'Graph games with omega-regular winning conditions provide a mathematical
    framework to analyze a wide range of problems in the analysis of reactive systems
    and programs (such as the synthesis of reactive systems, program repair, and the
    verification of branching time properties). Parity conditions are canonical forms
    to specify omega-regular winning conditions. Graph games with parity conditions
    are equivalent to mu-calculus model checking, and thus a very important algorithmic
    problem. Symbolic algorithms are of great significance because they provide scalable
    algorithms for the analysis of large finite-state systems, as well as algorithms
    for the analysis of infinite-state systems with finite quotient. A set-based symbolic
    algorithm uses the basic set operations and the one-step predecessor operators.
    We consider graph games with n vertices and parity conditions with c priorities
    (equivalently, a mu-calculus formula with c alternations of least and greatest
    fixed points). While many explicit algorithms exist for graph games with parity
    conditions, for set-based symbolic algorithms there are only two algorithms (notice
    that we use space to refer to the number of sets stored by a symbolic algorithm):
    (a) the basic algorithm that requires O(n^c) symbolic operations and linear space;
    and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but
    also O(n^{c/2+1}) space (i.e., exponential space). In this work we present two
    set-based symbolic algorithms for parity games: (a) our first algorithm requires
    O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing
    on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic
    operations and only linear space. We also present the first linear space set-based
    symbolic algorithm for parity games that requires at most a sub-exponential number
    of symbolic operations. '
article_number: '18'
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: Wolfgang
  full_name: Dvorák, Wolfgang
  last_name: Dvorák
- 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, Dvorák W, Henzinger MH, Loitzenbauer V. Improved set-based symbolic
    algorithms for parity games. In: Vol 82. Schloss Dagstuhl -Leibniz-Zentrum fuer
    Informatik; 2017. doi:<a href="https://doi.org/10.4230/LIPICS.CSL.2017.18">10.4230/LIPICS.CSL.2017.18</a>'
  apa: 'Chatterjee, K., Dvorák, W., Henzinger, M. H., &#38; Loitzenbauer, V. (2017).
    Improved set-based symbolic algorithms for parity games (Vol. 82). Presented at
    the CSL: Conference on Computer Science Logic, Stockholm, Sweden: Schloss Dagstuhl
    -Leibniz-Zentrum fuer Informatik. <a href="https://doi.org/10.4230/LIPICS.CSL.2017.18">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika H Henzinger, and Veronika
    Loitzenbauer. “Improved Set-Based Symbolic Algorithms for Parity Games,” Vol.
    82. Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, 2017. <a href="https://doi.org/10.4230/LIPICS.CSL.2017.18">https://doi.org/10.4230/LIPICS.CSL.2017.18</a>.
  ieee: 'K. Chatterjee, W. Dvorák, M. H. Henzinger, and V. Loitzenbauer, “Improved
    set-based symbolic algorithms for parity games,” presented at the CSL: Conference
    on Computer Science Logic, Stockholm, Sweden, 2017, vol. 82.'
  ista: 'Chatterjee K, Dvorák W, Henzinger MH, Loitzenbauer V. 2017. Improved set-based
    symbolic algorithms for parity games. CSL: Conference on Computer Science Logic
    vol. 82, 18.'
  mla: Chatterjee, Krishnendu, et al. <i>Improved Set-Based Symbolic Algorithms for
    Parity Games</i>. Vol. 82, 18, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik,
    2017, doi:<a href="https://doi.org/10.4230/LIPICS.CSL.2017.18">10.4230/LIPICS.CSL.2017.18</a>.
  short: K. Chatterjee, W. Dvorák, M.H. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
    -Leibniz-Zentrum fuer Informatik, 2017.
conference:
  end_date: 2017-08-24
  location: Stockholm, Sweden
  name: 'CSL: Conference on Computer Science Logic'
  start_date: 2017-08-20
date_created: 2019-06-04T12:42:43Z
date_published: 2017-08-01T00:00:00Z
date_updated: 2025-06-02T08:53:46Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.4230/LIPICS.CSL.2017.18
ec_funded: 1
file:
- access_level: open_access
  checksum: 7c2c9d09970af79026d7e37d9b632ef8
  content_type: application/pdf
  creator: kschuh
  date_created: 2019-06-04T12:56:52Z
  date_updated: 2020-07-14T12:47:33Z
  file_id: '6520'
  file_name: 2017_LIPIcs-Chatterjee.pdf
  file_size: 710185
  relation: main_file
file_date_updated: 2020-07-14T12:47:33Z
has_accepted_license: '1'
intvolume: '        82'
language:
- iso: eng
month: '08'
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: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
publication_status: published
publisher: Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik
quality_controlled: '1'
scopus_import: '1'
status: public
title: Improved set-based symbolic algorithms for parity games
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/3.0/legalcode
  name: Creative Commons Attribution 3.0 Unported (CC BY 3.0)
  short: CC BY (3.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2017'
...
---
_id: '653'
abstract:
- lang: eng
  text: The extent of heterogeneity among driver gene mutations present in naturally
    occurring metastases - that is, treatment-naive metastatic disease - is largely
    unknown. To address this issue, we carried out 60× whole-genome sequencing of
    26 metastases from four patients with pancreatic cancer. We found that identical
    mutations in known driver genes were present in every metastatic lesion for each
    patient studied. Passenger gene mutations, which do not have known or predicted
    functional consequences, accounted for all intratumoral heterogeneity. Even with
    respect to these passenger mutations, our analysis suggests that the genetic similarity
    among the founding cells of metastases was higher than that expected for any two
    cells randomly taken from a normal tissue. The uniformity of known driver gene
    mutations among metastases in the same patient has critical and encouraging implications
    for the success of future targeted therapies in advanced-stage disease.
acknowledgement: 'We thank the Memorial Sloan Kettering Cancer Center Molecular Cytology
  core facility for immunohistochemistry staining. This work was supported by Office
  of Naval Research grant N00014-16-1-2914, the Bill and Melinda Gates Foundation
  (OPP1148627), and a gift from B. Wu and E. Larson (M.A.N.), National Institutes
  of Health grants CA179991 (C.A.I.-D. and I.B.), F31 CA180682 (A.P.M.-M.), CA43460
  (B.V.), and P50 CA62924, the Monastra Foundation, the Virginia and D.K. Ludwig Fund
  for Cancer Research, the Lustgarten Foundation for Pancreatic Cancer Research, the
  Sol Goldman Center for Pancreatic Cancer Research, the Sol Goldman Sequencing Center,
  ERC Start grant 279307: Graph Games (J.G.R., D.K., and C.K.), Austrian Science Fund
  (FWF) grant P23499-N23 (J.G.R., D.K., and C.K.), and FWF NFN grant S11407-N23 RiSE/SHiNE
  (J.G.R., D.K., and C.K.).'
article_processing_charge: No
article_type: original
author:
- first_name: Alvin
  full_name: Makohon Moore, Alvin
  last_name: Makohon Moore
- first_name: Ming
  full_name: Zhang, Ming
  last_name: Zhang
- first_name: Johannes
  full_name: Reiter, Johannes
  id: 4A918E98-F248-11E8-B48F-1D18A9856A87
  last_name: Reiter
  orcid: 0000-0002-0170-7353
- first_name: Ivana
  full_name: Božić, Ivana
  last_name: Božić
- first_name: Benjamin
  full_name: Allen, Benjamin
  last_name: Allen
- first_name: Deepanjan
  full_name: Kundu, Deepanjan
  id: 1d4c0f4f-e8a3-11ec-a351-e36772758c45
  last_name: Kundu
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Fay
  full_name: Wong, Fay
  last_name: Wong
- first_name: Yuchen
  full_name: Jiao, Yuchen
  last_name: Jiao
- first_name: Zachary
  full_name: Kohutek, Zachary
  last_name: Kohutek
- first_name: Jungeui
  full_name: Hong, Jungeui
  last_name: Hong
- first_name: Marc
  full_name: Attiyeh, Marc
  last_name: Attiyeh
- first_name: Breanna
  full_name: Javier, Breanna
  last_name: Javier
- first_name: Laura
  full_name: Wood, Laura
  last_name: Wood
- first_name: Ralph
  full_name: Hruban, Ralph
  last_name: Hruban
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
- first_name: Nickolas
  full_name: Papadopoulos, Nickolas
  last_name: Papadopoulos
- first_name: Kenneth
  full_name: Kinzler, Kenneth
  last_name: Kinzler
- first_name: Bert
  full_name: Vogelstein, Bert
  last_name: Vogelstein
- first_name: Christine
  full_name: Iacobuzio Donahue, Christine
  last_name: Iacobuzio Donahue
citation:
  ama: Makohon Moore A, Zhang M, Reiter J, et al. Limited heterogeneity of known driver
    gene mutations among the metastases of individual patients with pancreatic cancer.
    <i>Nature Genetics</i>. 2017;49(3):358-366. doi:<a href="https://doi.org/10.1038/ng.3764">10.1038/ng.3764</a>
  apa: Makohon Moore, A., Zhang, M., Reiter, J., Božić, I., Allen, B., Kundu, D.,
    … Iacobuzio Donahue, C. (2017). Limited heterogeneity of known driver gene mutations
    among the metastases of individual patients with pancreatic cancer. <i>Nature
    Genetics</i>. Nature Publishing Group. <a href="https://doi.org/10.1038/ng.3764">https://doi.org/10.1038/ng.3764</a>
  chicago: Makohon Moore, Alvin, Ming Zhang, Johannes Reiter, Ivana Božić, Benjamin
    Allen, Deepanjan Kundu, Krishnendu Chatterjee, et al. “Limited Heterogeneity of
    Known Driver Gene Mutations among the Metastases of Individual Patients with Pancreatic
    Cancer.” <i>Nature Genetics</i>. Nature Publishing Group, 2017. <a href="https://doi.org/10.1038/ng.3764">https://doi.org/10.1038/ng.3764</a>.
  ieee: A. Makohon Moore <i>et al.</i>, “Limited heterogeneity of known driver gene
    mutations among the metastases of individual patients with pancreatic cancer,”
    <i>Nature Genetics</i>, vol. 49, no. 3. Nature Publishing Group, pp. 358–366,
    2017.
  ista: Makohon Moore A, Zhang M, Reiter J, Božić I, Allen B, Kundu D, Chatterjee
    K, Wong F, Jiao Y, Kohutek Z, Hong J, Attiyeh M, Javier B, Wood L, Hruban R, Nowak
    M, Papadopoulos N, Kinzler K, Vogelstein B, Iacobuzio Donahue C. 2017. Limited
    heterogeneity of known driver gene mutations among the metastases of individual
    patients with pancreatic cancer. Nature Genetics. 49(3), 358–366.
  mla: Makohon Moore, Alvin, et al. “Limited Heterogeneity of Known Driver Gene Mutations
    among the Metastases of Individual Patients with Pancreatic Cancer.” <i>Nature
    Genetics</i>, vol. 49, no. 3, Nature Publishing Group, 2017, pp. 358–66, doi:<a
    href="https://doi.org/10.1038/ng.3764">10.1038/ng.3764</a>.
  short: A. Makohon Moore, M. Zhang, J. Reiter, I. Božić, B. Allen, D. Kundu, K. Chatterjee,
    F. Wong, Y. Jiao, Z. Kohutek, J. Hong, M. Attiyeh, B. Javier, L. Wood, R. Hruban,
    M. Nowak, N. Papadopoulos, K. Kinzler, B. Vogelstein, C. Iacobuzio Donahue, Nature
    Genetics 49 (2017) 358–366.
date_created: 2018-12-11T11:47:43Z
date_published: 2017-03-01T00:00:00Z
date_updated: 2022-06-10T09:55:08Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/ng.3764
ec_funded: 1
external_id:
  pmid:
  - '28092682'
file:
- access_level: open_access
  checksum: e442dc3b7420a36ec805e9bb45cc1a2e
  content_type: application/pdf
  creator: dernst
  date_created: 2019-11-19T08:13:50Z
  date_updated: 2020-07-14T12:47:33Z
  file_id: '7050'
  file_name: 2017_NatureGenetics_Makohon.pdf
  file_size: 908099
  relation: main_file
file_date_updated: 2020-07-14T12:47:33Z
has_accepted_license: '1'
intvolume: '        49'
issue: '3'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Submitted Version
page: 358 - 366
pmid: 1
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 Genetics
publication_identifier:
  issn:
  - '10614036'
publication_status: published
publisher: Nature Publishing Group
publist_id: '7092'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Limited heterogeneity of known driver gene mutations among the metastases of
  individual patients with pancreatic cancer
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 49
year: '2017'
...
---
_id: '671'
abstract:
- lang: eng
  text: Humans routinely use conditionally cooperative strategies when interacting
    in repeated social dilemmas. They are more likely to cooperate if others cooperated
    before, and are ready to retaliate if others defected. To capture the emergence
    of reciprocity, most previous models consider subjects who can only choose from
    a restricted set of representative strategies, or who react to the outcome of
    the very last round only. As players memorize more rounds, the dimension of the
    strategy space increases exponentially. This increasing computational complexity
    renders simulations for individuals with higher cognitive abilities infeasible,
    especially if multiplayer interactions are taken into account. Here, we take an
    axiomatic approach instead. We propose several properties that a robust cooperative
    strategy for a repeated multiplayer dilemma should have. These properties naturally
    lead to a unique class of cooperative strategies, which contains the classical
    Win-Stay Lose-Shift rule as a special case. A comprehensive numerical analysis
    for the prisoner's dilemma and for the public goods game suggests that strategies
    of this class readily evolve across various memory-n spaces. Our results reveal
    that successful strategies depend not only on how cooperative others were in the
    past but also on the respective context of cooperation.
article_processing_charge: Yes (in subscription journal)
author:
- first_name: Christian
  full_name: Hilbe, Christian
  id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
  last_name: Hilbe
  orcid: 0000-0001-5116-955X
- first_name: Vaquero
  full_name: Martinez, Vaquero
  last_name: Martinez
- 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: Hilbe C, Martinez V, Chatterjee K, Nowak M. Memory-n strategies of direct reciprocity.
    <i>PNAS</i>. 2017;114(18):4715-4720. doi:<a href="https://doi.org/10.1073/pnas.1621239114">10.1073/pnas.1621239114</a>
  apa: Hilbe, C., Martinez, V., Chatterjee, K., &#38; Nowak, M. (2017). Memory-n strategies
    of direct reciprocity. <i>PNAS</i>. National Academy of Sciences. <a href="https://doi.org/10.1073/pnas.1621239114">https://doi.org/10.1073/pnas.1621239114</a>
  chicago: Hilbe, Christian, Vaquero Martinez, Krishnendu Chatterjee, and Martin Nowak.
    “Memory-n Strategies of Direct Reciprocity.” <i>PNAS</i>. National Academy of
    Sciences, 2017. <a href="https://doi.org/10.1073/pnas.1621239114">https://doi.org/10.1073/pnas.1621239114</a>.
  ieee: C. Hilbe, V. Martinez, K. Chatterjee, and M. Nowak, “Memory-n strategies of
    direct reciprocity,” <i>PNAS</i>, vol. 114, no. 18. National Academy of Sciences,
    pp. 4715–4720, 2017.
  ista: Hilbe C, Martinez V, Chatterjee K, Nowak M. 2017. Memory-n strategies of direct
    reciprocity. PNAS. 114(18), 4715–4720.
  mla: Hilbe, Christian, et al. “Memory-n Strategies of Direct Reciprocity.” <i>PNAS</i>,
    vol. 114, no. 18, National Academy of Sciences, 2017, pp. 4715–20, doi:<a href="https://doi.org/10.1073/pnas.1621239114">10.1073/pnas.1621239114</a>.
  short: C. Hilbe, V. Martinez, K. Chatterjee, M. Nowak, PNAS 114 (2017) 4715–4720.
date_created: 2018-12-11T11:47:50Z
date_published: 2017-05-02T00:00:00Z
date_updated: 2021-01-12T08:08:37Z
day: '02'
department:
- _id: KrCh
doi: 10.1073/pnas.1621239114
ec_funded: 1
external_id:
  pmid:
  - '28420786'
intvolume: '       114'
issue: '18'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5422766/
month: '05'
oa: 1
oa_version: Published Version
page: 4715 - 4720
pmid: 1
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: PNAS
publication_identifier:
  issn:
  - '00278424'
publication_status: published
publisher: National Academy of Sciences
publist_id: '7053'
quality_controlled: '1'
scopus_import: 1
status: public
title: Memory-n strategies of direct reciprocity
type: journal_article
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 114
year: '2017'
...
---
_id: '681'
abstract:
- lang: eng
  text: Two-player games on graphs provide the theoretical framework for many important
    problems such as reactive synthesis. While the traditional study of two-player
    zero-sum games has been extended to multi-player games with several notions of
    equilibria, they are decidable only for perfect-information games, whereas several
    applications require imperfect-information. In this paper we propose a new notion
    of equilibria, called doomsday equilibria, which is a strategy profile where all
    players satisfy their own objective, and if any coalition of players deviates
    and violates even one of the players' objective, then the objective of every player
    is violated. We present algorithms and complexity results for deciding the existence
    of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information
    games, and for perfect-information games. We provide optimal complexity bounds
    for imperfect-information games, and in most cases for perfect-information games.
article_processing_charge: No
article_type: original
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: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Emmanuel
  full_name: Filiot, Emmanuel
  last_name: Filiot
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
citation:
  ama: Chatterjee K, Doyen L, Filiot E, Raskin J. Doomsday equilibria for omega-regular
    games. <i>Information and Computation</i>. 2017;254:296-315. doi:<a href="https://doi.org/10.1016/j.ic.2016.10.012">10.1016/j.ic.2016.10.012</a>
  apa: Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J. (2017). Doomsday equilibria
    for omega-regular games. <i>Information and Computation</i>. Elsevier. <a href="https://doi.org/10.1016/j.ic.2016.10.012">https://doi.org/10.1016/j.ic.2016.10.012</a>
  chicago: Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean Raskin.
    “Doomsday Equilibria for Omega-Regular Games.” <i>Information and Computation</i>.
    Elsevier, 2017. <a href="https://doi.org/10.1016/j.ic.2016.10.012">https://doi.org/10.1016/j.ic.2016.10.012</a>.
  ieee: K. Chatterjee, L. Doyen, E. Filiot, and J. Raskin, “Doomsday equilibria for
    omega-regular games,” <i>Information and Computation</i>, vol. 254. Elsevier,
    pp. 296–315, 2017.
  ista: Chatterjee K, Doyen L, Filiot E, Raskin J. 2017. Doomsday equilibria for omega-regular
    games. Information and Computation. 254, 296–315.
  mla: Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.”
    <i>Information and Computation</i>, vol. 254, Elsevier, 2017, pp. 296–315, doi:<a
    href="https://doi.org/10.1016/j.ic.2016.10.012">10.1016/j.ic.2016.10.012</a>.
  short: K. Chatterjee, L. Doyen, E. Filiot, J. Raskin, Information and Computation
    254 (2017) 296–315.
date_created: 2018-12-11T11:47:53Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2023-02-21T16:06:02Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.ic.2016.10.012
ec_funded: 1
external_id:
  arxiv:
  - '1311.3238'
intvolume: '       254'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1311.3238
month: '06'
oa: 1
oa_version: Submitted Version
page: 296 - 315
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication: Information and Computation
publication_identifier:
  issn:
  - '08905401'
publication_status: published
publisher: Elsevier
publist_id: '7036'
quality_controlled: '1'
related_material:
  record:
  - id: '10885'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Doomsday equilibria for omega-regular games
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 254
year: '2017'
...
---
_id: '684'
abstract:
- lang: eng
  text: We generalize winning conditions in two-player games by adding a structural
    acceptance condition called obligations. Obligations are orthogonal to the linear
    winning conditions that define whether a play is winning. Obligations are a declaration
    that player 0 can achieve a certain value from a configuration. If the obligation
    is met, the value of that configuration for player 0 is 1. We define the value
    in such games and show that obligation games are determined. For Markov chains
    with Borel objectives and obligations, and finite turn-based stochastic parity
    games with obligations we give an alternative and simpler characterization of
    the value function. Based on this simpler definition we show that the decision
    problem of winning finite turn-based stochastic parity games with obligations
    is in NP∩co-NP. We also show that obligation games provide a game framework for
    reasoning about p-automata. © 2017 The Association for Symbolic Logic.
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: Nir
  full_name: Piterman, Nir
  last_name: Piterman
citation:
  ama: Chatterjee K, Piterman N. Obligation blackwell games and p-automata. <i>Journal
    of Symbolic Logic</i>. 2017;82(2):420-452. doi:<a href="https://doi.org/10.1017/jsl.2016.71">10.1017/jsl.2016.71</a>
  apa: Chatterjee, K., &#38; Piterman, N. (2017). Obligation blackwell games and p-automata.
    <i>Journal of Symbolic Logic</i>. Cambridge University Press. <a href="https://doi.org/10.1017/jsl.2016.71">https://doi.org/10.1017/jsl.2016.71</a>
  chicago: Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and
    P-Automata.” <i>Journal of Symbolic Logic</i>. Cambridge University Press, 2017.
    <a href="https://doi.org/10.1017/jsl.2016.71">https://doi.org/10.1017/jsl.2016.71</a>.
  ieee: K. Chatterjee and N. Piterman, “Obligation blackwell games and p-automata,”
    <i>Journal of Symbolic Logic</i>, vol. 82, no. 2. Cambridge University Press,
    pp. 420–452, 2017.
  ista: Chatterjee K, Piterman N. 2017. Obligation blackwell games and p-automata.
    Journal of Symbolic Logic. 82(2), 420–452.
  mla: Chatterjee, Krishnendu, and Nir Piterman. “Obligation Blackwell Games and P-Automata.”
    <i>Journal of Symbolic Logic</i>, vol. 82, no. 2, Cambridge University Press,
    2017, pp. 420–52, doi:<a href="https://doi.org/10.1017/jsl.2016.71">10.1017/jsl.2016.71</a>.
  short: K. Chatterjee, N. Piterman, Journal of Symbolic Logic 82 (2017) 420–452.
date_created: 2018-12-11T11:47:54Z
date_published: 2017-06-01T00:00:00Z
date_updated: 2021-04-16T12:10:53Z
day: '01'
department:
- _id: KrCh
doi: 10.1017/jsl.2016.71
intvolume: '        82'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1206.5174
month: '06'
oa: 1
oa_version: Submitted Version
page: 420 - 452
publication: Journal of Symbolic Logic
publication_identifier:
  eissn:
  - 1943-5886
  issn:
  - 0022-4812
publication_status: published
publisher: Cambridge University Press
publist_id: '7026'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Obligation blackwell games and p-automata
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 82
year: '2017'
...
---
_id: '1009'
abstract:
- lang: eng
  text: A standard objective in partially-observable Markov decision processes (POMDPs)
    is to find a policy that maximizes the expected discounted-sum payoff. However,
    such policies may still permit unlikely but highly undesirable outcomes, which
    is problematic especially in safety-critical applications. Recently, there has
    been a surge of interest in POMDPs where the goal is to maximize the probability
    to ensure that the payoff is at least a given threshold, but these approaches
    do not consider any optimization beyond satisfying this threshold constraint.
    In this work we go beyond both the “expectation” and “threshold” approaches and
    consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we
    are given a threshold t and the objective is to find a policy σ such that a) each
    possible outcome of σ yields a discounted-sum payoff of at least t, and b) the
    expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies
    satisfying a). We present a practical approach to tackle the GPO problem and evaluate
    it on standard POMDP benchmarks.
acknowledgement: 'he research leading to these results was supported by the Austrian
  Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants
  (279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund
  (WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions)
  of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant
  agreement no. [291734].'
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: Guillermo
  full_name: Pérez, Guillermo
  last_name: Pérez
- first_name: Jean
  full_name: Raskin, Jean
  last_name: Raskin
- first_name: Djordje
  full_name: Zikelic, Djordje
  last_name: Zikelic
citation:
  ama: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation
    with guarantees in POMDPs. In: <i>Proceedings of the 31st AAAI Conference on Artificial
    Intelligence</i>. Vol 5. AAAI Press; 2017:3725-3732.'
  apa: 'Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., &#38; Zikelic, D. (2017).
    Optimizing expectation with guarantees in POMDPs. In <i>Proceedings of the 31st
    AAAI Conference on Artificial Intelligence</i> (Vol. 5, pp. 3725–3732). San Francisco,
    CA, United States: AAAI Press.'
  chicago: Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and
    Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In <i>Proceedings
    of the 31st AAAI Conference on Artificial Intelligence</i>, 5:3725–32. AAAI Press,
    2017.
  ieee: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing
    expectation with guarantees in POMDPs,” in <i>Proceedings of the 31st AAAI Conference
    on Artificial Intelligence</i>, San Francisco, CA, United States, 2017, vol. 5,
    pp. 3725–3732.
  ista: 'Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation
    with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial
    Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.'
  mla: Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.”
    <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, vol.
    5, AAAI Press, 2017, pp. 3725–32.
  short: K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings
    of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp.
    3725–3732.
conference:
  end_date: 2017-02-10
  location: San Francisco, CA, United States
  name: 'AAAI: Conference on Artificial Intelligence'
  start_date: 2017-02-04
date_created: 2018-12-11T11:49:40Z
date_published: 2017-01-01T00:00:00Z
date_updated: 2025-06-02T08:53:49Z
day: '01'
department:
- _id: KrCh
ec_funded: 1
external_id:
  isi:
  - '000485630703107'
intvolume: '         5'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092
month: '01'
oa: 1
oa_version: Submitted Version
page: 3725 - 3732
project:
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
publication: Proceedings of the 31st AAAI Conference on Artificial Intelligence
publication_status: published
publisher: AAAI Press
publist_id: '6387'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Optimizing expectation with guarantees in POMDPs
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 5
year: '2017'
...
---
_id: '1011'
abstract:
- lang: eng
  text: Pushdown systems (PDSs) and recursive state machines (RSMs), which are linearly
    equivalent, are standard models for interprocedural analysis. Yet RSMs are more
    convenient as they (a) explicitly model function calls and returns, and (b) specify
    many natural parameters for algorithmic analysis, e.g., the number of entries
    and exits. We consider a general framework where RSM transitions are labeled from
    a semiring and path properties are algebraic with semiring operations, which can
    model, e.g., interprocedural reachability and dataflow analysis problems. Our
    main contributions are new algorithms for several fundamental problems. As compared
    to a direct translation of RSMs to PDSs and the best-known existing bounds of
    PDSs, our analysis algorithm improves the complexity for finite-height semirings
    (that subsumes reachability and standard dataflow properties). We further consider
    the problem of extracting distance values from the representation structures computed
    by our algorithm, and give efficient algorithms that distinguish the complexity
    of a one-time preprocessing from the complexity of each individual query. Another
    advantage of our algorithm is that our improvements carry over to the concurrent
    setting, where we improve the bestknown complexity for the context-bounded analysis
    of concurrent RSMs. Finally, we provide a prototype implementation that gives
    a significant speed-up on several benchmarks from the SLAM/SDV project.
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: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
- first_name: Samarth
  full_name: Mishra, Samarth
  last_name: Mishra
- 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, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted
    recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:<a
    href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>'
  apa: 'Chatterjee, K., Kragl, B., Mishra, S., &#38; Pavlogiannis, A. (2017). Faster
    algorithms for weighted recursive state machines. In H. Yang (Ed.) (Vol. 10201,
    pp. 287–313). Presented at the ESOP: European Symposium on Programming, Uppsala,
    Sweden: Springer. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>'
  chicago: Chatterjee, Krishnendu, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis.
    “Faster Algorithms for Weighted Recursive State Machines.” edited by Hongseok
    Yang, 10201:287–313. Springer, 2017. <a href="https://doi.org/10.1007/978-3-662-54434-1_11">https://doi.org/10.1007/978-3-662-54434-1_11</a>.
  ieee: 'K. Chatterjee, B. Kragl, S. Mishra, and A. Pavlogiannis, “Faster algorithms
    for weighted recursive state machines,” presented at the ESOP: European Symposium
    on Programming, Uppsala, Sweden, 2017, vol. 10201, pp. 287–313.'
  ista: 'Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. 2017. Faster algorithms
    for weighted recursive state machines. ESOP: European Symposium on Programming,
    LNCS, vol. 10201, 287–313.'
  mla: Chatterjee, Krishnendu, et al. <i>Faster Algorithms for Weighted Recursive
    State Machines</i>. Edited by Hongseok Yang, vol. 10201, Springer, 2017, pp. 287–313,
    doi:<a href="https://doi.org/10.1007/978-3-662-54434-1_11">10.1007/978-3-662-54434-1_11</a>.
  short: K. Chatterjee, B. Kragl, S. Mishra, A. Pavlogiannis, in:, H. Yang (Ed.),
    Springer, 2017, pp. 287–313.
conference:
  end_date: 2017-04-29
  location: Uppsala, Sweden
  name: 'ESOP: European Symposium on Programming'
  start_date: 2017-04-22
date_created: 2018-12-11T11:49:41Z
date_published: 2017-03-19T00:00:00Z
date_updated: 2023-09-22T09:44:50Z
day: '19'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-662-54434-1_11
ec_funded: 1
editor:
- first_name: Hongseok
  full_name: Yang, Hongseok
  last_name: Yang
external_id:
  isi:
  - '000681702400011'
intvolume: '     10201'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1701.04914
month: '03'
oa: 1
oa_version: Submitted Version
page: 287 - 313
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _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: 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: '6384'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for weighted recursive state machines
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 10201
year: '2017'
...
---
_id: '10416'
abstract:
- lang: eng
  text: 'A fundamental algorithmic problem at the heart of static analysis is Dyck
    reachability. The input is a graph where the edges are labeled with different
    types of opening and closing parentheses, and the reachability information is
    computed via paths whose parentheses are properly matched. We present new results
    for Dyck reachability problems with applications to alias analysis and data-dependence
    analysis. Our main contributions, that include improved upper bounds as well as
    lower bounds that establish optimality guarantees, are as follows: First, we consider
    Dyck reachability on bidirected graphs, which is the standard way of performing
    field-sensitive points-to analysis. Given a bidirected graph with n nodes and
    m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)),
    where α(n) is the inverse Ackermann function, improving the previously known O(n2)
    time bound; (ii) a matching lower bound that shows that our algorithm is optimal
    wrt to worst-case complexity; and (iii) an optimal average-case upper bound of
    O(m) time, improving the previously known O(m · logn) bound. Second, we consider
    the problem of context-sensitive data-dependence analysis, where the task is to
    obtain analysis summaries of library code in the presence of callbacks. Our algorithm
    preprocesses libraries in almost linear time, after which the contribution of
    the library in the complexity of the client analysis is only linear, and only
    wrt the number of call sites. Third, we prove that combinatorial algorithms for
    Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained
    without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication,
    which is a long-standing open problem. Thus we establish that the existing combinatorial
    algorithms for Dyck reachability are (conditionally) optimal for general graphs.
    We also show that the same hardness holds for graphs of constant treewidth. Finally,
    we provide a prototype implementation of our algorithms for both alias analysis
    and data-dependence analysis. Our experimental evaluation demonstrates that the
    new algorithms significantly outperform all existing methods on the two problems,
    over real-world benchmarks.'
acknowledgement: "The research was partly supported by Austrian Science Fund (FWF)
  Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant
  (279307: Graph Games).\r\n"
article_number: '30'
article_processing_charge: No
article_type: original
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: Bhavya
  full_name: Choudhary, Bhavya
  last_name: Choudhary
- 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, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence
    and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL).
    doi:<a href="https://doi.org/10.1145/3158118">10.1145/3158118</a>
  apa: 'Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). Optimal Dyck
    reachability for data-dependence and Alias analysis. <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/3158118">https://doi.org/10.1145/3158118</a>'
  chicago: Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal
    Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the
    ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a
    href="https://doi.org/10.1145/3158118">https://doi.org/10.1145/3158118</a>.
  ieee: K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability
    for data-dependence and Alias analysis,” <i>Proceedings of the ACM on Programming
    Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.
  ista: Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability
    for data-dependence and Alias analysis. Proceedings of the ACM on Programming
    Languages. 2(POPL), 30.
  mla: Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence
    and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>, vol.
    2, no. POPL, 30, Association for Computing Machinery, 2017, doi:<a href="https://doi.org/10.1145/3158118">10.1145/3158118</a>.
  short: K. Chatterjee, B. Choudhary, A. Pavlogiannis, 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:48Z
date_published: 2017-12-27T00:00:00Z
date_updated: 2023-02-23T12:27:13Z
day: '27'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1145/3158118
ec_funded: 1
external_id:
  arxiv:
  - '1910.00241'
file:
- access_level: open_access
  checksum: faa3f7b3fe8aab84b50ed805c26a0ee5
  content_type: application/pdf
  creator: cchlebak
  date_created: 2021-12-07T08:06:28Z
  date_updated: 2021-12-07T08:06:28Z
  file_id: '10421'
  file_name: 2017_ACMProgLang_Chatterjee.pdf
  file_size: 460188
  relation: main_file
  success: 1
file_date_updated: 2021-12-07T08:06:28Z
has_accepted_license: '1'
intvolume: '         2'
issue: POPL
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 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
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: '5455'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Optimal Dyck reachability for data-dependence and Alias analysis
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: 8b945eb4-e2f2-11eb-945a-df72226e66a9
volume: 2
year: '2017'
...
