---
_id: '1340'
abstract:
- lang: eng
  text: We study repeated games with absorbing states, a type of two-player, zero-sum
    concurrent mean-payoff games with the prototypical example being the Big Match
    of Gillete (1957). These games may not allow optimal strategies but they always
    have ε-optimal strategies. In this paper we design ε-optimal strategies for Player
    1 in these games that use only O(log log T) space. Furthermore, we construct strategies
    for Player 1 that use space s(T), for an arbitrary small unbounded non-decreasing
    function s, and which guarantee an ε-optimal value for Player 1 in the limit superior
    sense. The previously known strategies use space Ω(log T) and it was known that
    no strategy can use constant space if it is ε-optimal even in the limit superior
    sense. We also give a complementary lower bound. Furthermore, we also show that
    no Markov strategy, even extended with finite memory, can ensure value greater
    than 0 in the Big Match, answering a question posed by Neyman [11].
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Kristoffer
  full_name: Hansen, Kristoffer
  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
- first_name: Michal
  full_name: Koucký, Michal
  last_name: Koucký
citation:
  ama: 'Hansen K, Ibsen-Jensen R, Koucký M. The big match in small space. In: Vol
    9928. Springer; 2016:64-76. doi:<a href="https://doi.org/10.1007/978-3-662-53354-3_6">10.1007/978-3-662-53354-3_6</a>'
  apa: 'Hansen, K., Ibsen-Jensen, R., &#38; Koucký, M. (2016). The big match in small
    space (Vol. 9928, pp. 64–76). Presented at the SAGT: Symposium on Algorithmic
    Game Theory, Liverpool, United Kingdom: Springer. <a href="https://doi.org/10.1007/978-3-662-53354-3_6">https://doi.org/10.1007/978-3-662-53354-3_6</a>'
  chicago: Hansen, Kristoffer, Rasmus Ibsen-Jensen, and Michal Koucký. “The Big Match
    in Small Space,” 9928:64–76. Springer, 2016. <a href="https://doi.org/10.1007/978-3-662-53354-3_6">https://doi.org/10.1007/978-3-662-53354-3_6</a>.
  ieee: 'K. Hansen, R. Ibsen-Jensen, and M. Koucký, “The big match in small space,”
    presented at the SAGT: Symposium on Algorithmic Game Theory, Liverpool, United
    Kingdom, 2016, vol. 9928, pp. 64–76.'
  ista: 'Hansen K, Ibsen-Jensen R, Koucký M. 2016. The big match in small space. SAGT:
    Symposium on Algorithmic Game Theory, LNCS, vol. 9928, 64–76.'
  mla: Hansen, Kristoffer, et al. <i>The Big Match in Small Space</i>. Vol. 9928,
    Springer, 2016, pp. 64–76, doi:<a href="https://doi.org/10.1007/978-3-662-53354-3_6">10.1007/978-3-662-53354-3_6</a>.
  short: K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.
conference:
  end_date: 2016-09-21
  location: Liverpool, United Kingdom
  name: 'SAGT: Symposium on Algorithmic Game Theory'
  start_date: 2016-09-19
date_created: 2018-12-11T11:51:28Z
date_published: 2016-09-01T00:00:00Z
date_updated: 2025-09-22T08:18:27Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/978-3-662-53354-3_6
ec_funded: 1
external_id:
  arxiv:
  - '1604.07634'
  isi:
  - '000389020400006'
intvolume: '      9928'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1604.07634
month: '09'
oa: 1
oa_version: Preprint
page: 64 - 76
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Springer
publist_id: '5927'
quality_controlled: '1'
scopus_import: '1'
status: public
title: The big match in small space
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 9928
year: '2016'
...
---
_id: '1380'
abstract:
- lang: eng
  text: We consider higher-dimensional versions of Kannan and Lipton's Orbit Problem
    - determining whether a target vector space V may be reached from a starting point
    x under repeated applications of a linear transformation A. Answering two questions
    posed by Kannan and Lipton in the 1980s, we show that when V has dimension one,
    this problem is solvable in polynomial time, and when V has dimension two or three,
    the problem is in NPRP.
article_number: '23'
article_processing_charge: No
arxiv: 1
author:
- first_name: Ventsislav K
  full_name: Chonev, Ventsislav K
  id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
  last_name: Chonev
- first_name: Joël
  full_name: Ouaknine, Joël
  last_name: Ouaknine
- first_name: James
  full_name: Worrell, James
  last_name: Worrell
citation:
  ama: Chonev VK, Ouaknine J, Worrell J. On the complexity of the orbit problem. <i>Journal
    of the ACM</i>. 2016;63(3). doi:<a href="https://doi.org/10.1145/2857050">10.1145/2857050</a>
  apa: Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On the complexity of
    the orbit problem. <i>Journal of the ACM</i>. ACM. <a href="https://doi.org/10.1145/2857050">https://doi.org/10.1145/2857050</a>
  chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Complexity
    of the Orbit Problem.” <i>Journal of the ACM</i>. ACM, 2016. <a href="https://doi.org/10.1145/2857050">https://doi.org/10.1145/2857050</a>.
  ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On the complexity of the orbit
    problem,” <i>Journal of the ACM</i>, vol. 63, no. 3. ACM, 2016.
  ista: Chonev VK, Ouaknine J, Worrell J. 2016. On the complexity of the orbit problem.
    Journal of the ACM. 63(3), 23.
  mla: Chonev, Ventsislav K., et al. “On the Complexity of the Orbit Problem.” <i>Journal
    of the ACM</i>, vol. 63, no. 3, 23, ACM, 2016, doi:<a href="https://doi.org/10.1145/2857050">10.1145/2857050</a>.
  short: V.K. Chonev, J. Ouaknine, J. Worrell, Journal of the ACM 63 (2016).
date_created: 2018-12-11T11:51:41Z
date_published: 2016-06-01T00:00:00Z
date_updated: 2025-09-22T07:33:47Z
day: '01'
department:
- _id: KrCh
doi: 10.1145/2857050
external_id:
  arxiv:
  - '1303.2981'
  isi:
  - '000382753300004'
intvolume: '        63'
isi: 1
issue: '3'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1303.2981
month: '06'
oa: 1
oa_version: Preprint
publication: Journal of the ACM
publication_status: published
publisher: ACM
publist_id: '5831'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the complexity of the orbit problem
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 63
year: '2016'
...
---
_id: '1389'
abstract:
- lang: eng
  text: "The continuous evolution of a wide variety of systems, including continous-time
    Markov chains and linear hybrid automata, can be\r\ndescribed in terms of linear
    differential equations. In this paper we study the decision problem of whether
    the solution x(t) of a system of linear differential equations dx/dt = Ax reaches
    a target halfspace infinitely often. This recurrent reachability problem can\r\nequivalently
    be formulated as the following Infinite Zeros Problem: does a real-valued function
    f:R≥0 --&gt; R satisfying a given linear\r\ndifferential equation have infinitely
    many zeros? Our main decidability result is that if the differential equation
    has order at most 7, then the Infinite Zeros Problem is decidable. On the other
    hand, we show that a decision procedure for the Infinite Zeros Problem at order
    9 (and above) would entail a major breakthrough in Diophantine Approximation,
    specifically an algorithm for computing the Lagrange constants of arbitrary real
    algebraic numbers to arbitrary precision."
article_processing_charge: No
arxiv: 1
author:
- first_name: Ventsislav K
  full_name: Chonev, Ventsislav K
  id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
  last_name: Chonev
- first_name: Joël
  full_name: Ouaknine, Joël
  last_name: Ouaknine
- first_name: James
  full_name: Worrell, James
  last_name: Worrell
citation:
  ama: 'Chonev VK, Ouaknine J, Worrell J. On recurrent reachability for continuous
    linear dynamical systems. In: <i>LICS ’16</i>. IEEE; 2016:515-524. doi:<a href="https://doi.org/10.1145/2933575.2934548">10.1145/2933575.2934548</a>'
  apa: 'Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On recurrent reachability
    for continuous linear dynamical systems. In <i>LICS ’16</i> (pp. 515–524). New
    York, NY, USA: IEEE. <a href="https://doi.org/10.1145/2933575.2934548">https://doi.org/10.1145/2933575.2934548</a>'
  chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On Recurrent Reachability
    for Continuous Linear Dynamical Systems.” In <i>LICS ’16</i>, 515–24. IEEE, 2016.
    <a href="https://doi.org/10.1145/2933575.2934548">https://doi.org/10.1145/2933575.2934548</a>.
  ieee: V. K. Chonev, J. Ouaknine, and J. Worrell, “On recurrent reachability for
    continuous linear dynamical systems,” in <i>LICS ’16</i>, New York, NY, USA, 2016,
    pp. 515–524.
  ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On recurrent reachability for continuous
    linear dynamical systems. LICS ’16. LICS: Logic in Computer Science, 515–524.'
  mla: Chonev, Ventsislav K., et al. “On Recurrent Reachability for Continuous Linear
    Dynamical Systems.” <i>LICS ’16</i>, IEEE, 2016, pp. 515–24, doi:<a href="https://doi.org/10.1145/2933575.2934548">10.1145/2933575.2934548</a>.
  short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.
conference:
  end_date: 2018-07-08
  location: New York, NY, USA
  name: 'LICS: Logic in Computer Science'
  start_date: 2018-07-05
date_created: 2018-12-11T11:51:44Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2025-09-22T07:31:08Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934548
ec_funded: 1
external_id:
  arxiv:
  - '1507.03632'
  isi:
  - '000387609200052'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1507.03632
month: '07'
oa: 1
oa_version: Preprint
page: 515 - 524
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication: LICS '16
publication_status: published
publisher: IEEE
publist_id: '5820'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On recurrent reachability for continuous linear dynamical systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2016'
...
---
OA_place: publisher
_id: '1397'
abstract:
- lang: eng
  text: 'We study partially observable Markov decision processes (POMDPs) with objectives
    used in verification and artificial intelligence. The qualitative analysis problem
    given a POMDP and an objective asks whether there is a strategy (policy) to ensure
    that the objective is satisfied almost surely (with probability 1), resp. with
    positive probability (with probability greater than 0). For POMDPs with limit-average
    payoff, where a reward value in the interval [0,1] is associated to every transition,
    and the payoff of an infinite path is the long-run average of the rewards, we
    consider two types of path constraints: (i) a quantitative limit-average constraint
    defines the set of paths where the payoff is at least a given threshold L1 = 1.
    Our main results for qualitative limit-average constraint under almost-sure winning
    are as follows: (i) the problem of deciding the existence of a finite-memory controller
    is EXPTIME-complete; and (ii) the problem of deciding the existence of an infinite-memory
    controller is undecidable. For quantitative limit-average constraints we show
    that the problem of deciding the existence of a finite-memory controller is undecidable.
    We present a prototype implementation of our EXPTIME algorithm. For POMDPs with
    w-regular conditions specified as parity objectives, while the qualitative analysis
    problems are known to be undecidable even for very special case of parity objectives,
    we establish decidability (with optimal complexity) of the qualitative analysis
    problems for POMDPs with parity objectives under finite-memory strategies. We
    establish optimal (exponential) memory bounds and EXPTIME-completeness of the
    qualitative analysis problems under finite-memory strategies for POMDPs with parity
    objectives. Based on our theoretical algorithms we also present a practical approach,
    where we design heuristics to deal with the exponential complexity, and have applied
    our implementation on a number of well-known POMDP examples for robotics applications.
    For POMDPs with a set of target states and an integer cost associated with every
    transition, we study the optimization objective that asks to minimize the expected
    total cost of reaching a state in the target set, while ensuring that the target
    set is reached almost surely. We show that for general integer costs approximating
    the optimal cost is undecidable. For positive costs, our results are as follows:
    (i) we establish matching lower and upper bounds for the optimal cost, both double
    and exponential in the POMDP state space size; (ii) we show that the problem of
    approximating the optimal cost is decidable and present approximation algorithms
    that extend existing algorithms for POMDPs with finite-horizon objectives. We
    show experimentally that it performs well in many examples of interest. We study
    more deeply the problem of almost-sure reachability, where  given a set of target
    states, the question is to decide whether there is a strategy to ensure that the
    target set is reached almost surely. While in general the problem EXPTIME-complete,
    in many practical cases strategies with a small amount of memory suffice. Moreover,
    the existing solution to the problem is explicit, which first requires to construct
    explicitly an exponential reduction to a belief-support MDP. We first study the
    existence of observation-stationary strategies, which is NP-complete, and then
    small-memory strategies. We present a symbolic algorithm by an efficient encoding
    to SAT and using a SAT solver for the problem. We report experimental results
    demonstrating the scalability of our symbolic (SAT-based) approach. Decentralized
    POMDPs (DEC-POMDPs) extend POMDPs to a multi-agent setting, where several agents
    operate in an uncertain environment independently to achieve a joint objective.
    In this work we consider Goal DEC-POMDPs, where given a set of target states,
    the objective is to ensure that the target set is reached with minimal cost. We
    consider the indefinite-horizon (infinite-horizon with either discounted-sum,
    or undiscounted-sum, where absorbing goal states have zero-cost) problem. We present
    a new and novel method to solve the problem that extends methods for finite-horizon
    DEC-POMDPs and the real-time dynamic programming approach for POMDPs. We present
    experimental results on several examples, and show that our approach presents
    promising results. In the end we present a short summary of a few other results
    related to verification of MDPs and POMDPs.'
alternative_title:
- ISTA Thesis
article_processing_charge: No
author:
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
citation:
  ama: Chmelik M. Algorithms for partially observable markov decision processes. 2016.
  apa: Chmelik, M. (2016). <i>Algorithms for partially observable markov decision
    processes</i>. Institute of Science and Technology Austria.
  chicago: Chmelik, Martin. “Algorithms for Partially Observable Markov Decision Processes.”
    Institute of Science and Technology Austria, 2016.
  ieee: M. Chmelik, “Algorithms for partially observable markov decision processes,”
    Institute of Science and Technology Austria, 2016.
  ista: Chmelik M. 2016. Algorithms for partially observable markov decision processes.
    Institute of Science and Technology Austria.
  mla: Chmelik, Martin. <i>Algorithms for Partially Observable Markov Decision Processes</i>.
    Institute of Science and Technology Austria, 2016.
  short: M. Chmelik, Algorithms for Partially Observable Markov Decision Processes,
    Institute of Science and Technology Austria, 2016.
corr_author: '1'
date_created: 2018-12-11T11:51:47Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2026-04-08T14:23:19Z
day: '01'
degree_awarded: PhD
department:
- _id: KrCh
language:
- iso: eng
month: '02'
oa_version: None
page: '232'
publication_identifier:
  issn:
  - 2663-337X
publication_status: published
publisher: Institute of Science and Technology Austria
publist_id: '5810'
status: public
supervisor:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
title: Algorithms for partially observable markov decision processes
type: dissertation
user_id: ba8df636-2132-11f1-aed0-ed93e2281fdd
year: '2016'
...
---
_id: '1423'
abstract:
- lang: eng
  text: 'Direct reciprocity is a mechanism for the evolution of cooperation based
    on repeated interactions. When individuals meet repeatedly, they can use conditional
    strategies to enforce cooperative outcomes that would not be feasible in one-shot
    social dilemmas. Direct reciprocity requires that individuals keep track of their
    past interactions and find the right response. However, there are natural bounds
    on strategic complexity: Humans find it difficult to remember past interactions
    accurately, especially over long timespans. Given these limitations, it is natural
    to ask how complex strategies need to be for cooperation to evolve. Here, we study
    stochastic evolutionary game dynamics in finite populations to systematically
    compare the evolutionary performance of reactive strategies, which only respond
    to the co-player''s previous move, and memory-one strategies, which take into
    account the own and the co-player''s previous move. In both cases, we compare
    deterministic strategy and stochastic strategy spaces. For reactive strategies
    and small costs, we find that stochasticity benefits cooperation, because it allows
    for generous-tit-for-tat. For memory one strategies and small costs, we find that
    stochasticity does not increase the propensity for cooperation, because the deterministic
    rule of win-stay, lose-shift works best. For memory one strategies and large costs,
    however, stochasticity can augment cooperation.'
acknowledgement: C.H. acknowledges generous funding from the Schrödinger scholarship
  of the Austrian Science Fund (FWF), J3475.
article_number: '25676'
article_processing_charge: No
author:
- first_name: Seung
  full_name: Baek, Seung
  last_name: Baek
- first_name: Hyeongchai
  full_name: Jeong, Hyeongchai
  last_name: Jeong
- first_name: Christian
  full_name: Hilbe, Christian
  id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
  last_name: Hilbe
  orcid: 0000-0001-5116-955X
- first_name: Martin
  full_name: Nowak, Martin
  last_name: Nowak
citation:
  ama: Baek S, Jeong H, Hilbe C, Nowak M. Comparing reactive and memory-one strategies
    of direct reciprocity. <i>Scientific Reports</i>. 2016;6. doi:<a href="https://doi.org/10.1038/srep25676">10.1038/srep25676</a>
  apa: Baek, S., Jeong, H., Hilbe, C., &#38; Nowak, M. (2016). Comparing reactive
    and memory-one strategies of direct reciprocity. <i>Scientific Reports</i>. Nature
    Publishing Group. <a href="https://doi.org/10.1038/srep25676">https://doi.org/10.1038/srep25676</a>
  chicago: Baek, Seung, Hyeongchai Jeong, Christian Hilbe, and Martin Nowak. “Comparing
    Reactive and Memory-One Strategies of Direct Reciprocity.” <i>Scientific Reports</i>.
    Nature Publishing Group, 2016. <a href="https://doi.org/10.1038/srep25676">https://doi.org/10.1038/srep25676</a>.
  ieee: S. Baek, H. Jeong, C. Hilbe, and M. Nowak, “Comparing reactive and memory-one
    strategies of direct reciprocity,” <i>Scientific Reports</i>, vol. 6. Nature Publishing
    Group, 2016.
  ista: Baek S, Jeong H, Hilbe C, Nowak M. 2016. Comparing reactive and memory-one
    strategies of direct reciprocity. Scientific Reports. 6, 25676.
  mla: Baek, Seung, et al. “Comparing Reactive and Memory-One Strategies of Direct
    Reciprocity.” <i>Scientific Reports</i>, vol. 6, 25676, Nature Publishing Group,
    2016, doi:<a href="https://doi.org/10.1038/srep25676">10.1038/srep25676</a>.
  short: S. Baek, H. Jeong, C. Hilbe, M. Nowak, Scientific Reports 6 (2016).
corr_author: '1'
date_created: 2018-12-11T11:51:56Z
date_published: 2016-05-10T00:00:00Z
date_updated: 2025-09-18T14:15:33Z
day: '10'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1038/srep25676
external_id:
  isi:
  - '000375448500002'
file:
- access_level: open_access
  checksum: ee17c482370d2e1b3add393710d3c696
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:18:08Z
  date_updated: 2020-07-14T12:44:53Z
  file_id: '5327'
  file_name: IST-2016-590-v1+1_srep25676.pdf
  file_size: 1349915
  relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: '         6'
isi: 1
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
publication: Scientific Reports
publication_status: published
publisher: Nature Publishing Group
publist_id: '5784'
pubrep_id: '590'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Comparing reactive and memory-one strategies of direct reciprocity
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2016'
...
---
_id: '1426'
abstract:
- lang: eng
  text: 'Brood parasites exploit their host in order to increase their own fitness.
    Typically, this results in an arms race between parasite trickery and host defence.
    Thus, it is puzzling to observe hosts that accept parasitism without any resistance.
    The ‘mafia’ hypothesis suggests that these hosts accept parasitism to avoid retaliation.
    Retaliation has been shown to evolve when the hosts condition their response to
    mafia parasites, who use depredation as a targeted response to rejection. However,
    it is unclear if acceptance would also emerge when ‘farming’ parasites are present
    in the population. Farming parasites use depredation to synchronize the timing
    with the host, destroying mature clutches to force the host to re-nest. Herein,
    we develop an evolutionary model to analyse the interaction between depredatory
    parasites and their hosts. We show that coevolutionary cycles between farmers
    and mafia can still induce host acceptance of brood parasites. However, this equilibrium
    is unstable and in the long-run the dynamics of this host–parasite interaction
    exhibits strong oscillations: when farmers are the majority, accepters conditional
    to mafia (the host will reject first and only accept after retaliation by the
    parasite) have a higher fitness than unconditional accepters (the host always
    accepts parasitism). This leads to an increase in mafia parasites’ fitness and
    in turn induce an optimal environment for accepter hosts.'
acknowledgement: C.H. gratefully acknowledges funding by the Schrödinger scholarship
  of the Austrian Science Fund (FWF) J3475.
article_number: '160036'
article_processing_charge: No
author:
- first_name: Maria
  full_name: Chakra, Maria
  last_name: Chakra
- first_name: Christian
  full_name: Hilbe, Christian
  id: 2FDF8F3C-F248-11E8-B48F-1D18A9856A87
  last_name: Hilbe
  orcid: 0000-0001-5116-955X
- first_name: Arne
  full_name: Traulsen, Arne
  last_name: Traulsen
citation:
  ama: Chakra M, Hilbe C, Traulsen A. Coevolutionary interactions between farmers
    and mafia induce host acceptance of avian brood parasites. <i>Royal Society Open
    Science</i>. 2016;3(5). doi:<a href="https://doi.org/10.1098/rsos.160036">10.1098/rsos.160036</a>
  apa: Chakra, M., Hilbe, C., &#38; Traulsen, A. (2016). Coevolutionary interactions
    between farmers and mafia induce host acceptance of avian brood parasites. <i>Royal
    Society Open Science</i>. Royal Society, The. <a href="https://doi.org/10.1098/rsos.160036">https://doi.org/10.1098/rsos.160036</a>
  chicago: Chakra, Maria, Christian Hilbe, and Arne Traulsen. “Coevolutionary Interactions
    between Farmers and Mafia Induce Host Acceptance of Avian Brood Parasites.” <i>Royal
    Society Open Science</i>. Royal Society, The, 2016. <a href="https://doi.org/10.1098/rsos.160036">https://doi.org/10.1098/rsos.160036</a>.
  ieee: M. Chakra, C. Hilbe, and A. Traulsen, “Coevolutionary interactions between
    farmers and mafia induce host acceptance of avian brood parasites,” <i>Royal Society
    Open Science</i>, vol. 3, no. 5. Royal Society, The, 2016.
  ista: Chakra M, Hilbe C, Traulsen A. 2016. Coevolutionary interactions between farmers
    and mafia induce host acceptance of avian brood parasites. Royal Society Open
    Science. 3(5), 160036.
  mla: Chakra, Maria, et al. “Coevolutionary Interactions between Farmers and Mafia
    Induce Host Acceptance of Avian Brood Parasites.” <i>Royal Society Open Science</i>,
    vol. 3, no. 5, 160036, Royal Society, The, 2016, doi:<a href="https://doi.org/10.1098/rsos.160036">10.1098/rsos.160036</a>.
  short: M. Chakra, C. Hilbe, A. Traulsen, Royal Society Open Science 3 (2016).
date_created: 2018-12-11T11:51:57Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2025-09-18T14:14:59Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1098/rsos.160036
external_id:
  isi:
  - '000377969800008'
file:
- access_level: open_access
  checksum: bf84211b31fe87451e738ba301d729c3
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:49Z
  date_updated: 2020-07-14T12:44:53Z
  file_id: '5104'
  file_name: IST-2016-589-v1+1_160036.full.pdf
  file_size: 937002
  relation: main_file
file_date_updated: 2020-07-14T12:44:53Z
has_accepted_license: '1'
intvolume: '         3'
isi: 1
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
publication: Royal Society Open Science
publication_status: published
publisher: Royal Society, The
publist_id: '5776'
pubrep_id: '589'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Coevolutionary interactions between farmers and mafia induce host acceptance
  of avian brood parasites
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 3
year: '2016'
...
---
_id: '1438'
abstract:
- lang: eng
  text: 'In this paper, we consider termination of probabilistic programs with real-valued
    variables. The questions concerned are: (a) qualitative ones that ask (i) whether
    the program terminates with probability 1 (almost-sure termination) and (ii) whether
    the expected termination time is finite (finite termination); (b) quantitative
    ones that ask (i) to approximate the expected termination time (expectation problem)
    and (ii) to compute a bound B such that the probability to terminate after B steps
    decreases exponentially (concentration problem). To solve these questions, we
    utilize the notion of ranking supermartingales which is a powerful approach for
    proving termination of probabilistic programs. In detail, we focus on algorithmic
    synthesis of linear ranking-supermartingales over affine probabilistic programs
    (APP''s) with both angelic and demonic non-determinism. An important subclass
    of APP''s is LRAPP which is defined as the class of all APP''s over which a linear
    ranking-supermartingale exists. Our main contributions are as follows. Firstly,
    we show that the membership problem of LRAPP (i) can be decided in polynomial
    time for APP''s with at most demonic non-determinism, and (ii) is NP-hard and
    in PSPACE for APP''s with angelic non-determinism; moreover, the NP-hardness result
    holds already for APP''s without probability and demonic non-determinism. Secondly,
    we show that the concentration problem over LRAPP can be solved in the same complexity
    as for the membership problem of LRAPP. Finally, we show that the expectation
    problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP''s
    without probability and non-determinism (i.e., deterministic programs). Our experimental
    results demonstrate the effectiveness of our approach to answer the qualitative
    and quantitative questions over APP''s with at most demonic non-determinism.'
acknowledgement: 'Supported by the Natural Science Foundation of China (NSFC) under
  Grant No. 61532019 '
alternative_title:
- POPL
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
  id: 3AAD03D6-F248-11E8-B48F-1D18A9856A87
  last_name: Fu
- first_name: Petr
  full_name: Novotny, Petr
  id: 3CC3B868-F248-11E8-B48F-1D18A9856A87
  last_name: Novotny
- first_name: Rouzbeh
  full_name: Hasheminezhad, Rouzbeh
  last_name: Hasheminezhad
citation:
  ama: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative
    and quantitative termination problems for affine probabilistic programs. In: Vol
    20-22. ACM; 2016:327-342. doi:<a href="https://doi.org/10.1145/2837614.2837639">10.1145/2837614.2837639</a>'
  apa: 'Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2016). Algorithmic
    analysis of qualitative and quantitative termination problems for affine probabilistic
    programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming
    Languages, St. Petersburg, FL, USA: ACM. <a href="https://doi.org/10.1145/2837614.2837639">https://doi.org/10.1145/2837614.2837639</a>'
  chicago: Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad.
    “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for
    Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. <a href="https://doi.org/10.1145/2837614.2837639">https://doi.org/10.1145/2837614.2837639</a>.
  ieee: 'K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis
    of qualitative and quantitative termination problems for affine probabilistic
    programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg,
    FL, USA, 2016, vol. 20–22, pp. 327–342.'
  ista: 'Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis
    of qualitative and quantitative termination problems for affine probabilistic
    programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.'
  mla: Chatterjee, Krishnendu, et al. <i>Algorithmic Analysis of Qualitative and Quantitative
    Termination Problems for Affine Probabilistic Programs</i>. Vol. 20–22, ACM, 2016,
    pp. 327–42, doi:<a href="https://doi.org/10.1145/2837614.2837639">10.1145/2837614.2837639</a>.
  short: K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.
conference:
  end_date: 2016-01-22
  location: St. Petersburg, FL, USA
  name: 'POPL: Principles of Programming Languages'
  start_date: 2016-01-20
date_created: 2018-12-11T11:52:01Z
date_published: 2016-01-11T00:00:00Z
date_updated: 2025-04-15T08:12:22Z
day: '11'
department:
- _id: KrCh
doi: 10.1145/2837614.2837639
ec_funded: 1
external_id:
  arxiv:
  - '1510.08517'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1510.08517
month: '01'
oa: 1
oa_version: Preprint
page: 327 - 342
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_status: published
publisher: ACM
publist_id: '5760'
quality_controlled: '1'
related_material:
  record:
  - id: '5993'
    relation: later_version
    status: public
scopus_import: 1
status: public
title: Algorithmic analysis of qualitative and quantitative termination problems for
  affine probabilistic programs
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 20-22
year: '2016'
...
---
_id: '1477'
abstract:
- lang: eng
  text: We consider partially observable Markov decision processes (POMDPs) with ω-regular
    conditions specified as parity objectives. The class of ω-regular languages provides
    a robust specification language to express properties in verification, and parity
    objectives are canonical forms to express them. The qualitative analysis problem
    given a POMDP and a parity objective asks whether there is a strategy to ensure
    that the objective is satisfied with probability 1 (resp. positive probability).
    While the qualitative analysis problems are undecidable even for special cases
    of parity objectives, we establish decidability (with optimal complexity) for
    POMDPs with all parity objectives under finite-memory strategies. We establish
    optimal (exponential) memory bounds and EXPTIME-completeness of the qualitative
    analysis problems under finite-memory strategies for POMDPs with parity objectives.
    We also present a practical approach, where we design heuristics to deal with
    the exponential complexity, and have applied our implementation on a number of
    POMDP examples.
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: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Mathieu
  full_name: Tracol, Mathieu
  id: 3F54FA38-F248-11E8-B48F-1D18A9856A87
  last_name: Tracol
citation:
  ama: Chatterjee K, Chmelik M, Tracol M. What is decidable about partially observable
    Markov decision processes with ω-regular objectives. <i>Journal of Computer and
    System Sciences</i>. 2016;82(5):878-911. doi:<a href="https://doi.org/10.1016/j.jcss.2016.02.009">10.1016/j.jcss.2016.02.009</a>
  apa: Chatterjee, K., Chmelik, M., &#38; Tracol, M. (2016). What is decidable about
    partially observable Markov decision processes with ω-regular objectives. <i>Journal
    of Computer and System Sciences</i>. Elsevier. <a href="https://doi.org/10.1016/j.jcss.2016.02.009">https://doi.org/10.1016/j.jcss.2016.02.009</a>
  chicago: Chatterjee, Krishnendu, Martin Chmelik, and Mathieu Tracol. “What Is Decidable
    about Partially Observable Markov Decision Processes with ω-Regular Objectives.”
    <i>Journal of Computer and System Sciences</i>. Elsevier, 2016. <a href="https://doi.org/10.1016/j.jcss.2016.02.009">https://doi.org/10.1016/j.jcss.2016.02.009</a>.
  ieee: K. Chatterjee, M. Chmelik, and M. Tracol, “What is decidable about partially
    observable Markov decision processes with ω-regular objectives,” <i>Journal of
    Computer and System Sciences</i>, vol. 82, no. 5. Elsevier, pp. 878–911, 2016.
  ista: Chatterjee K, Chmelik M, Tracol M. 2016. What is decidable about partially
    observable Markov decision processes with ω-regular objectives. Journal of Computer
    and System Sciences. 82(5), 878–911.
  mla: Chatterjee, Krishnendu, et al. “What Is Decidable about Partially Observable
    Markov Decision Processes with ω-Regular Objectives.” <i>Journal of Computer and
    System Sciences</i>, vol. 82, no. 5, Elsevier, 2016, pp. 878–911, doi:<a href="https://doi.org/10.1016/j.jcss.2016.02.009">10.1016/j.jcss.2016.02.009</a>.
  short: K. Chatterjee, M. Chmelik, M. Tracol, Journal of Computer and System Sciences
    82 (2016) 878–911.
corr_author: '1'
date_created: 2018-12-11T11:52:15Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-09-18T11:38:39Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.jcss.2016.02.009
ec_funded: 1
external_id:
  arxiv:
  - '1309.2802'
  isi:
  - '000374425900015'
intvolume: '        82'
isi: 1
issue: '5'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1309.2802
month: '08'
oa: 1
oa_version: Preprint
page: 878 - 911
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
  name: Microsoft Research Faculty Fellowship
publication: Journal of Computer and System Sciences
publication_status: published
publisher: Elsevier
publist_id: '5718'
quality_controlled: '1'
related_material:
  record:
  - id: '2295'
    relation: earlier_version
    status: public
  - id: '5400'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: What is decidable about partially observable Markov decision processes with
  ω-regular objectives
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 82
year: '2016'
...
---
_id: '1518'
abstract:
- lang: eng
  text: The inference of demographic history from genome data is hindered by a lack
    of efficient computational approaches. In particular, it has proved difficult
    to exploit the information contained in the distribution of genealogies across
    the genome. We have previously shown that the generating function (GF) of genealogies
    can be used to analytically compute likelihoods of demographic models from configurations
    of mutations in short sequence blocks (Lohse et al. 2011). Although the GF has
    a simple, recursive form, the size of such likelihood calculations explodes quickly
    with the number of individuals and applications of this framework have so far
    been mainly limited to small samples (pairs and triplets) for which the GF can
    be written by hand. Here we investigate several strategies for exploiting the
    inherent symmetries of the coalescent. In particular, we show that the GF of genealogies
    can be decomposed into a set of equivalence classes that allows likelihood calculations
    from nontrivial samples. Using this strategy, we automated blockwise likelihood
    calculations for a general set of demographic scenarios in Mathematica. These
    histories may involve population size changes, continuous migration, discrete
    divergence, and admixture between multiple populations. To give a concrete example,
    we calculate the likelihood for a model of isolation with migration (IM), assuming
    two diploid samples without phase and outgroup information. We demonstrate the
    new inference scheme with an analysis of two individual butterfly genomes from
    the sister species Heliconius melpomene rosina and H. cydno.
acknowledgement: "We thank Lynsey Bunnefeld for discussions throughout the project
  and Joshua Schraiber and one anonymous reviewer\r\nfor constructive comments on
  an earlier version of this manuscript. This work was supported by funding from the\r\nUnited
  Kingdom Natural Environment Research Council (to K.L.) (NE/I020288/1) and a grant
  from the European\r\nResearch Council (250152) (to N.H.B.)."
article_processing_charge: No
article_type: original
author:
- first_name: Konrad
  full_name: Lohse, Konrad
  last_name: Lohse
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Simon
  full_name: Martin, Simon
  last_name: Martin
- first_name: Nicholas H
  full_name: Barton, Nicholas H
  id: 4880FE40-F248-11E8-B48F-1D18A9856A87
  last_name: Barton
  orcid: 0000-0002-8548-5240
citation:
  ama: Lohse K, Chmelik M, Martin S, Barton NH. Efficient strategies for calculating
    blockwise likelihoods under the coalescent. <i>Genetics</i>. 2016;202(2):775-786.
    doi:<a href="https://doi.org/10.1534/genetics.115.183814">10.1534/genetics.115.183814</a>
  apa: Lohse, K., Chmelik, M., Martin, S., &#38; Barton, N. H. (2016). Efficient strategies
    for calculating blockwise likelihoods under the coalescent. <i>Genetics</i>. Genetics
    Society of America. <a href="https://doi.org/10.1534/genetics.115.183814">https://doi.org/10.1534/genetics.115.183814</a>
  chicago: Lohse, Konrad, Martin Chmelik, Simon Martin, and Nicholas H Barton. “Efficient
    Strategies for Calculating Blockwise Likelihoods under the Coalescent.” <i>Genetics</i>.
    Genetics Society of America, 2016. <a href="https://doi.org/10.1534/genetics.115.183814">https://doi.org/10.1534/genetics.115.183814</a>.
  ieee: K. Lohse, M. Chmelik, S. Martin, and N. H. Barton, “Efficient strategies for
    calculating blockwise likelihoods under the coalescent,” <i>Genetics</i>, vol.
    202, no. 2. Genetics Society of America, pp. 775–786, 2016.
  ista: Lohse K, Chmelik M, Martin S, Barton NH. 2016. Efficient strategies for calculating
    blockwise likelihoods under the coalescent. Genetics. 202(2), 775–786.
  mla: Lohse, Konrad, et al. “Efficient Strategies for Calculating Blockwise Likelihoods
    under the Coalescent.” <i>Genetics</i>, vol. 202, no. 2, Genetics Society of America,
    2016, pp. 775–86, doi:<a href="https://doi.org/10.1534/genetics.115.183814">10.1534/genetics.115.183814</a>.
  short: K. Lohse, M. Chmelik, S. Martin, N.H. Barton, Genetics 202 (2016) 775–786.
date_created: 2018-12-11T11:52:29Z
date_published: 2016-02-01T00:00:00Z
date_updated: 2025-09-18T11:09:34Z
day: '01'
ddc:
- '570'
department:
- _id: KrCh
- _id: NiBa
doi: 10.1534/genetics.115.183814
ec_funded: 1
external_id:
  isi:
  - '000371304600032'
  pmid:
  - '26715666'
file:
- access_level: open_access
  checksum: 41c9b5d72e7fe4624dd22dfe622337d5
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:51Z
  date_updated: 2020-07-14T12:45:00Z
  file_id: '5241'
  file_name: IST-2016-561-v1+1_Lohse_et_al_Genetics_2015.pdf
  file_size: 957466
  relation: main_file
file_date_updated: 2020-07-14T12:45:00Z
has_accepted_license: '1'
intvolume: '       202'
isi: 1
issue: '2'
language:
- iso: eng
month: '02'
oa: 1
oa_version: Preprint
page: 775 - 786
pmid: 1
project:
- _id: 25B07788-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '250152'
  name: Limits to selection in biology and in evolutionary computation
publication: Genetics
publication_status: published
publisher: Genetics Society of America
publist_id: '5658'
pubrep_id: '561'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Efficient strategies for calculating blockwise likelihoods under the coalescent
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 202
year: '2016'
...
---
_id: '1529'
abstract:
- lang: eng
  text: 'We consider partially observable Markov decision processes (POMDPs) with
    a set of target states and an integer cost associated with every transition. The
    optimization objective we study asks to minimize the expected total cost of reaching
    a state in the target set, while ensuring that the target set is reached almost
    surely (with probability 1). We show that for integer costs approximating the
    optimal cost is undecidable. For positive costs, our results are as follows: (i)
    we establish matching lower and upper bounds for the optimal cost, both double
    exponential in the POMDP state space size; (ii) we show that the problem of approximating
    the optimal cost is decidable and present approximation algorithms developing
    on the existing algorithms for POMDPs with finite-horizon objectives. While the
    worst-case running time of our algorithm is double exponential, we also present
    efficient stopping criteria for the algorithm and show experimentally that it
    performs well in many examples of interest.'
acknowledgement: 'We thank Blai Bonet for helping us with RTDP-Bel. The research was
  partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant
  No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft faculty
  fellows award.'
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: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Raghav
  full_name: Gupta, Raghav
  last_name: Gupta
- first_name: Ayush
  full_name: Kanodia, Ayush
  last_name: Kanodia
citation:
  ama: Chatterjee K, Chmelik M, Gupta R, Kanodia A. Optimal cost almost-sure reachability
    in POMDPs. <i>Artificial Intelligence</i>. 2016;234:26-48. doi:<a href="https://doi.org/10.1016/j.artint.2016.01.007">10.1016/j.artint.2016.01.007</a>
  apa: Chatterjee, K., Chmelik, M., Gupta, R., &#38; Kanodia, A. (2016). Optimal cost
    almost-sure reachability in POMDPs. <i>Artificial Intelligence</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.artint.2016.01.007">https://doi.org/10.1016/j.artint.2016.01.007</a>
  chicago: Chatterjee, Krishnendu, Martin Chmelik, Raghav Gupta, and Ayush Kanodia.
    “Optimal Cost Almost-Sure Reachability in POMDPs.” <i>Artificial Intelligence</i>.
    Elsevier, 2016. <a href="https://doi.org/10.1016/j.artint.2016.01.007">https://doi.org/10.1016/j.artint.2016.01.007</a>.
  ieee: K. Chatterjee, M. Chmelik, R. Gupta, and A. Kanodia, “Optimal cost almost-sure
    reachability in POMDPs,” <i>Artificial Intelligence</i>, vol. 234. Elsevier, pp.
    26–48, 2016.
  ista: Chatterjee K, Chmelik M, Gupta R, Kanodia A. 2016. Optimal cost almost-sure
    reachability in POMDPs. Artificial Intelligence. 234, 26–48.
  mla: Chatterjee, Krishnendu, et al. “Optimal Cost Almost-Sure Reachability in POMDPs.”
    <i>Artificial Intelligence</i>, vol. 234, Elsevier, 2016, pp. 26–48, doi:<a href="https://doi.org/10.1016/j.artint.2016.01.007">10.1016/j.artint.2016.01.007</a>.
  short: K. Chatterjee, M. Chmelik, R. Gupta, A. Kanodia, Artificial Intelligence
    234 (2016) 26–48.
corr_author: '1'
date_created: 2018-12-11T11:52:33Z
date_published: 2016-05-01T00:00:00Z
date_updated: 2025-09-18T11:05:09Z
day: '01'
department:
- _id: KrCh
doi: 10.1016/j.artint.2016.01.007
ec_funded: 1
external_id:
  arxiv:
  - '1411.3880'
  isi:
  - '000372683700002'
intvolume: '       234'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1411.3880
month: '05'
oa: 1
oa_version: Preprint
page: 26 - 48
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Artificial Intelligence
publication_status: published
publisher: Elsevier
publist_id: '5642'
quality_controlled: '1'
related_material:
  record:
  - id: '5425'
    relation: earlier_version
    status: public
  - id: '1820'
    relation: earlier_version
    status: public
scopus_import: '1'
status: public
title: Optimal cost almost-sure reachability in POMDPs
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 234
year: '2016'
...
---
_id: '478'
abstract:
- lang: eng
  text: 'Magic: the Gathering is a game about magical combat for any number of players.
    Formally it is a zero-sum, imperfect information stochastic game that consists
    of a potentially unbounded number of steps. We consider the problem of deciding
    if a move is legal in a given single step of Magic. We show that the problem is
    (a) coNP-complete in general; and (b) in P if either of two small sets of cards
    are not used. Our lower bound holds even for single-player Magic games. The significant
    aspects of our results are as follows: First, in most real-life game problems,
    the task of deciding whether a given move is legal in a single step is trivial,
    and the computationally hard task is to find the best sequence of legal moves
    in the presence of multiple players. In contrast, quite uniquely our hardness
    result holds for single step and with only one-player. Second, we establish efficient
    algorithms for important special cases of Magic.'
alternative_title:
- Frontiers in Artificial Intelligence and Applications
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: 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, Ibsen-Jensen R. The complexity of deciding legality of a single
    step of magic: The gathering. In: Vol 285. IOS Press; 2016:1432-1439. doi:<a href="https://doi.org/10.3233/978-1-61499-672-9-1432">10.3233/978-1-61499-672-9-1432</a>'
  apa: 'Chatterjee, K., &#38; Ibsen-Jensen, R. (2016). The complexity of deciding
    legality of a single step of magic: The gathering (Vol. 285, pp. 1432–1439). Presented
    at the ECAI: European Conference on Artificial Intelligence, The Hague, Netherlands:
    IOS Press. <a href="https://doi.org/10.3233/978-1-61499-672-9-1432">https://doi.org/10.3233/978-1-61499-672-9-1432</a>'
  chicago: 'Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. “The Complexity of Deciding
    Legality of a Single Step of Magic: The Gathering,” 285:1432–39. IOS Press, 2016.
    <a href="https://doi.org/10.3233/978-1-61499-672-9-1432">https://doi.org/10.3233/978-1-61499-672-9-1432</a>.'
  ieee: 'K. Chatterjee and R. Ibsen-Jensen, “The complexity of deciding legality of
    a single step of magic: The gathering,” presented at the ECAI: European Conference
    on Artificial Intelligence, The Hague, Netherlands, 2016, vol. 285, pp. 1432–1439.'
  ista: 'Chatterjee K, Ibsen-Jensen R. 2016. The complexity of deciding legality of
    a single step of magic: The gathering. ECAI: European Conference on Artificial
    Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 285,
    1432–1439.'
  mla: 'Chatterjee, Krishnendu, and Rasmus Ibsen-Jensen. <i>The Complexity of Deciding
    Legality of a Single Step of Magic: The Gathering</i>. Vol. 285, IOS Press, 2016,
    pp. 1432–39, doi:<a href="https://doi.org/10.3233/978-1-61499-672-9-1432">10.3233/978-1-61499-672-9-1432</a>.'
  short: K. Chatterjee, R. Ibsen-Jensen, in:, IOS Press, 2016, pp. 1432–1439.
conference:
  end_date: 2016-09-02
  location: The Hague, Netherlands
  name: 'ECAI: European Conference on Artificial Intelligence'
  start_date: 2016-08-29
corr_author: '1'
date_created: 2018-12-11T11:46:41Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2025-09-22T14:26:27Z
day: '01'
ddc:
- '004'
department:
- _id: KrCh
doi: 10.3233/978-1-61499-672-9-1432
external_id:
  isi:
  - '000385793700166'
file:
- access_level: open_access
  checksum: 848043c812ace05e459579c923f3d3cf
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:07:59Z
  date_updated: 2020-07-14T12:46:35Z
  file_id: '4658'
  file_name: IST-2018-950-v1+1_2016_Chatterjee_The_complexity.pdf
  file_size: 2116225
  relation: main_file
file_date_updated: 2020-07-14T12:46:35Z
has_accepted_license: '1'
intvolume: '       285'
isi: 1
language:
- iso: eng
license: https://creativecommons.org/licenses/by-nc/4.0/
month: '01'
oa: 1
oa_version: Published Version
page: 1432 - 1439
publication_status: published
publisher: IOS Press
publist_id: '7342'
pubrep_id: '950'
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'The complexity of deciding legality of a single step of magic: The gathering'
tmp:
  image: /images/cc_by_nc.png
  legal_code_url: https://creativecommons.org/licenses/by-nc/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)
  short: CC BY-NC (4.0)
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 285
year: '2016'
...
---
_id: '480'
abstract:
- lang: eng
  text: Graph games provide the foundation for modeling and synthesizing reactive
    processes. In the synthesis of stochastic reactive processes, the traditional
    model is perfect-information stochastic games, where some transitions of the game
    graph are controlled by two adversarial players, and the other transitions are
    executed probabilistically. We consider such games where the objective is the
    conjunction of several quantitative objectives (specified as mean-payoff conditions),
    which we refer to as generalized mean-payoff objectives. The basic decision problem
    asks for the existence of a finite-memory strategy for a player that ensures the
    generalized mean-payoff objective be satisfied with a desired probability against
    all strategies of the opponent. A special case of the decision problem is the
    almost-sure problem where the desired probability is 1. Previous results presented
    a semi-decision procedure for -approximations of the almost-sure problem. In this
    work, we show that both the almost-sure problem as well as the general basic decision
    problem are coNP-complete, significantly improving the previous results. Moreover,
    we show that in the case of 1-player stochastic games, randomized memoryless strategies
    are sufficient and the problem can be solved in polynomial time. In contrast,
    in two-player stochastic games, we show that even with randomized strategies exponential
    memory is required in general, and present a matching exponential upper bound.
    We also study the basic decision problem with infinite-memory strategies and present
    computational complexity results for the problem. Our results are relevant in
    the synthesis of stochastic reactive systems with multiple quantitative requirements.
alternative_title:
- Proceedings Symposium on Logic in Computer Science
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: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
citation:
  ama: 'Chatterjee K, Doyen L. Perfect-information stochastic games with generalized
    mean-payoff objectives. In: Vol 05-08-July-2016. IEEE; 2016:247-256. doi:<a href="https://doi.org/10.1145/2933575.2934513">10.1145/2933575.2934513</a>'
  apa: 'Chatterjee, K., &#38; Doyen, L. (2016). Perfect-information stochastic games
    with generalized mean-payoff objectives (Vol. 05-08-July-2016, pp. 247–256). Presented
    at the LICS: Logic in Computer Science, New York, NY, USA: IEEE. <a href="https://doi.org/10.1145/2933575.2934513">https://doi.org/10.1145/2933575.2934513</a>'
  chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Perfect-Information Stochastic
    Games with Generalized Mean-Payoff Objectives,” 05-08-July-2016:247–56. IEEE,
    2016. <a href="https://doi.org/10.1145/2933575.2934513">https://doi.org/10.1145/2933575.2934513</a>.
  ieee: 'K. Chatterjee and L. Doyen, “Perfect-information stochastic games with generalized
    mean-payoff objectives,” presented at the LICS: Logic in Computer Science, New
    York, NY, USA, 2016, vol. 05-08-July-2016, pp. 247–256.'
  ista: 'Chatterjee K, Doyen L. 2016. Perfect-information stochastic games with generalized
    mean-payoff objectives. LICS: Logic in Computer Science, Proceedings Symposium
    on Logic in Computer Science, vol. 05-08-July-2016, 247–256.'
  mla: Chatterjee, Krishnendu, and Laurent Doyen. <i>Perfect-Information Stochastic
    Games with Generalized Mean-Payoff Objectives</i>. Vol. 05-08-July-2016, IEEE,
    2016, pp. 247–56, doi:<a href="https://doi.org/10.1145/2933575.2934513">10.1145/2933575.2934513</a>.
  short: K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.
conference:
  end_date: 2016-07-08
  location: New York, NY, USA
  name: 'LICS: Logic in Computer Science'
  start_date: 2016-07-05
date_created: 2018-12-11T11:46:42Z
date_published: 2016-07-05T00:00:00Z
date_updated: 2025-09-22T14:22:08Z
day: '05'
department:
- _id: KrCh
doi: 10.1145/2933575.2934513
ec_funded: 1
external_id:
  arxiv:
  - '1604.06376'
  isi:
  - '000387609200025'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1604.06376
month: '07'
oa: 1
oa_version: Preprint
page: 247 - 256
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: IEEE
publist_id: '7340'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Perfect-information stochastic games with generalized mean-payoff objectives
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 05-08-July-2016
year: '2016'
...
---
_id: '5445'
abstract:
- lang: eng
  text: 'We consider the quantitative analysis problem for interprocedural control-flow
    graphs (ICFGs). The input consists of an ICFG, a positive weight function that
    assigns every transition a positive integer-valued number, and a labelling of
    the transitions (events) as good, bad, and neutral events. The weight function
    assigns to each transition a numerical value that represents ameasure of how good
    or bad an event is. The quantitative analysis problem asks whether there is a
    run of the ICFG where the ratio of the sum of the numerical weights of good events
    versus the sum of weights of bad events in the long-run is at least a given threshold
    (or equivalently, to compute the maximal ratio among all valid paths in the ICFG).
    The quantitative analysis problem for ICFGs can be solved in polynomial time,
    and we present an efficient and practical algorithm for the problem. We show that
    several problems relevant for static program analysis, such as estimating the
    worst-case execution time of a program or the average energy consumption of a
    mobile application, can be modeled in our framework. We have implemented our algorithm
    as a tool in the Java Soot framework. We demonstrate the effectiveness of our
    approach with two case studies. First, we show that our framework provides a sound
    approach (no false positives) for the analysis of inefficiently-used containers.
    Second, we show that our approach can also be used for static profiling of programs
    which reasons about methods that are frequently invoked. Our experimental results
    show that our tool scales to relatively large benchmarks, and discovers relevant
    and useful information that can be used to optimize performance of the programs. '
alternative_title:
- IST Austria Technical Report
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Andreas
  full_name: Pavlogiannis, Andreas
  id: 49704004-F248-11E8-B48F-1D18A9856A87
  last_name: Pavlogiannis
  orcid: 0000-0002-8943-0722
- first_name: Yaron
  full_name: Velner, Yaron
  last_name: Velner
citation:
  ama: Chatterjee K, Pavlogiannis A, Velner Y. <i>Quantitative Interprocedural Analysis</i>.
    IST Austria; 2016. doi:<a href="https://doi.org/10.15479/AT:IST-2016-523-v1-1">10.15479/AT:IST-2016-523-v1-1</a>
  apa: Chatterjee, K., Pavlogiannis, A., &#38; Velner, Y. (2016). <i>Quantitative
    interprocedural analysis</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2016-523-v1-1">https://doi.org/10.15479/AT:IST-2016-523-v1-1</a>
  chicago: Chatterjee, Krishnendu, Andreas Pavlogiannis, and Yaron Velner. <i>Quantitative
    Interprocedural Analysis</i>. IST Austria, 2016. <a href="https://doi.org/10.15479/AT:IST-2016-523-v1-1">https://doi.org/10.15479/AT:IST-2016-523-v1-1</a>.
  ieee: K. Chatterjee, A. Pavlogiannis, and Y. Velner, <i>Quantitative interprocedural
    analysis</i>. IST Austria, 2016.
  ista: Chatterjee K, Pavlogiannis A, Velner Y. 2016. Quantitative interprocedural
    analysis, IST Austria, 33p.
  mla: Chatterjee, Krishnendu, et al. <i>Quantitative Interprocedural Analysis</i>.
    IST Austria, 2016, doi:<a href="https://doi.org/10.15479/AT:IST-2016-523-v1-1">10.15479/AT:IST-2016-523-v1-1</a>.
  short: K. Chatterjee, A. Pavlogiannis, Y. Velner, Quantitative Interprocedural Analysis,
    IST Austria, 2016.
date_created: 2018-12-12T11:39:22Z
date_published: 2016-03-31T00:00:00Z
date_updated: 2025-04-15T08:11:41Z
day: '31'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-523-v1-1
file:
- access_level: open_access
  checksum: cef516fa091925b5868813e355268fb4
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:52Z
  date_updated: 2020-07-14T12:46:58Z
  file_id: '5513'
  file_name: IST-2016-523-v1+1_main.pdf
  file_size: 1012204
  relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '03'
oa: 1
oa_version: Published Version
page: '33'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '523'
related_material:
  record:
  - id: '1604'
    relation: later_version
    status: public
status: public
title: Quantitative interprocedural analysis
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5449'
abstract:
- lang: eng
  text: "The fixation probability is the probability that a new mutant introduced
    in a homogeneous population eventually takes over the entire population.\r\nThe
    fixation probability is a fundamental quantity of natural selection, and known
    to depend on the population structure.\r\nAmplifiers of natural selection are
    population structures which increase the fixation probability of advantageous
    mutants, as compared to the baseline case of well-mixed populations. In this work
    we focus on symmetric population structures represented as undirected graphs.
    In the regime of undirected graphs, the strongest amplifier known has been the
    Star graph, and the existence of undirected graphs with stronger amplification
    properties has remained open for over a decade.\r\nIn this work we present the
    Comet and Comet-swarm families of undirected graphs. We show that for a range
    of fitness values of the mutants, the Comet and Comet-swarm graphs have fixation
    probability strictly larger than the fixation probability of the Star graph, for
    fixed population size and at the limit of large populations, respectively."
alternative_title:
- IST Austria Technical Report
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. <i>Amplification on Undirected
    Population Structures: Comets Beat Stars</i>. IST Austria; 2016. doi:<a href="https://doi.org/10.15479/AT:IST-2016-648-v1-1">10.15479/AT:IST-2016-648-v1-1</a>'
  apa: 'Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Amplification
    on undirected population structures: Comets beat stars</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2016-648-v1-1">https://doi.org/10.15479/AT:IST-2016-648-v1-1</a>'
  chicago: 'Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak. <i>Amplification on Undirected Population Structures: Comets Beat Stars</i>.
    IST Austria, 2016. <a href="https://doi.org/10.15479/AT:IST-2016-648-v1-1">https://doi.org/10.15479/AT:IST-2016-648-v1-1</a>.'
  ieee: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Amplification
    on undirected population structures: Comets beat stars</i>. IST Austria, 2016.'
  ista: 'Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Amplification on
    undirected population structures: Comets beat stars, IST Austria, 22p.'
  mla: 'Pavlogiannis, Andreas, et al. <i>Amplification on Undirected Population Structures:
    Comets Beat Stars</i>. IST Austria, 2016, doi:<a href="https://doi.org/10.15479/AT:IST-2016-648-v1-1">10.15479/AT:IST-2016-648-v1-1</a>.'
  short: 'A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Amplification on Undirected
    Population Structures: Comets Beat Stars, IST Austria, 2016.'
date_created: 2018-12-12T11:39:24Z
date_published: 2016-11-09T00:00:00Z
date_updated: 2025-09-18T09:50:09Z
day: '09'
ddc:
- '519'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-648-v1-1
file:
- access_level: open_access
  checksum: 8345a8c1e7d7f0cd92516d182b7fc59e
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:54:07Z
  date_updated: 2020-07-14T12:46:58Z
  file_id: '5529'
  file_name: IST-2016-648-v1+1_tr.pdf
  file_size: 1264221
  relation: main_file
file_date_updated: 2020-07-14T12:46:58Z
has_accepted_license: '1'
language:
- iso: eng
month: '11'
oa: 1
oa_version: Updated Version
page: '22'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '648'
related_material:
  record:
  - id: '512'
    relation: later_version
    status: public
status: public
title: 'Amplification on undirected population structures: Comets beat stars'
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5451'
alternative_title:
- IST Austria Technical Report
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. <i>Strong Amplifiers of Natural
    Selection</i>. IST Austria; 2016. doi:<a href="https://doi.org/10.15479/AT:IST-2016-728-v1-1">10.15479/AT:IST-2016-728-v1-1</a>
  apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Strong
    amplifiers of natural selection</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2016-728-v1-1">https://doi.org/10.15479/AT:IST-2016-728-v1-1</a>
  chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak. <i>Strong Amplifiers of Natural Selection</i>. IST Austria, 2016. <a href="https://doi.org/10.15479/AT:IST-2016-728-v1-1">https://doi.org/10.15479/AT:IST-2016-728-v1-1</a>.
  ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Strong amplifiers
    of natural selection</i>. IST Austria, 2016.
  ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Strong amplifiers
    of natural selection, IST Austria, 34p.
  mla: Pavlogiannis, Andreas, et al. <i>Strong Amplifiers of Natural Selection</i>.
    IST Austria, 2016, doi:<a href="https://doi.org/10.15479/AT:IST-2016-728-v1-1">10.15479/AT:IST-2016-728-v1-1</a>.
  short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Strong Amplifiers of
    Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:24Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2023-02-23T12:27:05Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2016-728-v1-1
file:
- access_level: open_access
  checksum: 7b8bb17c322c0556acba6ac169fa71c1
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:04Z
  date_updated: 2020-07-14T12:46:59Z
  file_id: '5465'
  file_name: IST-2016-728-v1+1_main.pdf
  file_size: 1014732
  relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '728'
status: public
title: Strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5452'
alternative_title:
- IST Austria Technical Report
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. <i>Arbitrarily Strong Amplifiers
    of Natural Selection</i>. IST Austria; 2016. doi:<a href="https://doi.org/10.15479/AT:IST-2017-728-v2-1">10.15479/AT:IST-2017-728-v2-1</a>
  apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Arbitrarily
    strong amplifiers of natural selection</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2017-728-v2-1">https://doi.org/10.15479/AT:IST-2017-728-v2-1</a>
  chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria,
    2016. <a href="https://doi.org/10.15479/AT:IST-2017-728-v2-1">https://doi.org/10.15479/AT:IST-2017-728-v2-1</a>.
  ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong
    amplifiers of natural selection</i>. IST Austria, 2016.
  ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
    amplifiers of natural selection, IST Austria, 32p.
  mla: Pavlogiannis, Andreas, et al. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>.
    IST Austria, 2016, doi:<a href="https://doi.org/10.15479/AT:IST-2017-728-v2-1">10.15479/AT:IST-2017-728-v2-1</a>.
  short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
    Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2025-04-15T07:55:39Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-728-v2-1
ec_funded: 1
file:
- access_level: open_access
  checksum: 58e895f26c82f560c0f0989bf8b08599
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:52:59Z
  date_updated: 2020-07-14T12:46:59Z
  file_id: '5460'
  file_name: IST-2017-728-v2+1_main.pdf
  file_size: 811558
  relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '32'
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '750'
related_material:
  record:
  - id: '5453'
    relation: later_version
    status: public
  - id: '5559'
    relation: popular_science
    status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '5453'
alternative_title:
- IST Austria Technical Report
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. <i>Arbitrarily Strong Amplifiers
    of Natural Selection</i>. IST Austria; 2016. doi:<a href="https://doi.org/10.15479/AT:IST-2017-749-v3-1">10.15479/AT:IST-2017-749-v3-1</a>
  apa: Pavlogiannis, A., Tkadlec, J., Chatterjee, K., &#38; Nowak, M. (2016). <i>Arbitrarily
    strong amplifiers of natural selection</i>. IST Austria. <a href="https://doi.org/10.15479/AT:IST-2017-749-v3-1">https://doi.org/10.15479/AT:IST-2017-749-v3-1</a>
  chicago: Pavlogiannis, Andreas, Josef Tkadlec, Krishnendu Chatterjee, and Martin
    Nowak. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>. IST Austria,
    2016. <a href="https://doi.org/10.15479/AT:IST-2017-749-v3-1">https://doi.org/10.15479/AT:IST-2017-749-v3-1</a>.
  ieee: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, and M. Nowak, <i>Arbitrarily strong
    amplifiers of natural selection</i>. IST Austria, 2016.
  ista: Pavlogiannis A, Tkadlec J, Chatterjee K, Nowak M. 2016. Arbitrarily strong
    amplifiers of natural selection, IST Austria, 34p.
  mla: Pavlogiannis, Andreas, et al. <i>Arbitrarily Strong Amplifiers of Natural Selection</i>.
    IST Austria, 2016, doi:<a href="https://doi.org/10.15479/AT:IST-2017-749-v3-1">10.15479/AT:IST-2017-749-v3-1</a>.
  short: A. Pavlogiannis, J. Tkadlec, K. Chatterjee, M. Nowak, Arbitrarily Strong
    Amplifiers of Natural Selection, IST Austria, 2016.
date_created: 2018-12-12T11:39:25Z
date_published: 2016-12-30T00:00:00Z
date_updated: 2025-04-15T07:55:37Z
day: '30'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.15479/AT:IST-2017-749-v3-1
file:
- access_level: open_access
  checksum: 83b0313dab3bff4bdb6ac38695026fda
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T11:53:13Z
  date_updated: 2020-07-14T12:46:59Z
  file_id: '5474'
  file_name: IST-2017-749-v3+1_main.pdf
  file_size: 1015647
  relation: main_file
file_date_updated: 2020-07-14T12:46:59Z
has_accepted_license: '1'
language:
- iso: eng
month: '12'
oa: 1
oa_version: Published Version
page: '34'
publication_identifier:
  issn:
  - 2664-1690
publication_status: published
publisher: IST Austria
pubrep_id: '755'
related_material:
  record:
  - id: '5452'
    relation: earlier_version
    status: public
status: public
title: Arbitrarily strong amplifiers of natural selection
type: technical_report
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...
---
_id: '1068'
abstract:
- lang: eng
  text: 'Games on graphs provide the appropriate framework to study several central
    problems in computer science, such as verification and synthesis of reactive systems.
    One of the most basic objectives for games on graphs is the liveness (or Büchi)
    objective that given a target set of vertices requires that some vertex in the
    target set is visited infinitely often. We study generalized Büchi objectives
    (i.e., conjunction of liveness objectives), and implications between two generalized
    Büchi objectives (known as GR(1) objectives), that arise in numerous applications
    in computer-aided verification. We present improved algorithms and conditional
    super-linear lower bounds based on widely believed assumptions about the complexity
    of (A1) combinatorial Boolean matrix multiplication and (A2) CNF-SAT. We consider
    graph games with n vertices, m edges, and generalized Büchi objectives with k
    conjunctions. First, we present an algorithm with running time O(k*n^2), improving
    the previously known O(k*n*m) and O(k^2*n^2) worst-case bounds. Our algorithm
    is optimal for dense graphs under (A1). Second, we show that the basic algorithm
    for the problem is optimal for sparse graphs when the target sets have constant
    size under (A2). Finally, we consider GR(1) objectives, with k_1 conjunctions
    in the antecedent and k_2 conjunctions in the consequent, and present an O(k_1
    k_2 n^{2.5})-time algorithm, improving the previously known O(k_1*k_2*n*m)-time
    algorithm for m &gt; n^{1.5}. '
acknowledgement: K. C., M. H., and W. D. are partially supported by the Vienna Science
  and Technology Fund (WWTF) through project ICT15-003. K. C. is partially supported
  by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and an ERC
  Start grant (279307
alternative_title:
- LIPIcs
article_number: '25'
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 M, Loitzenbauer V. Conditionally optimal
    algorithms for generalized Büchi Games. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik; 2016. doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2016.25">10.4230/LIPIcs.MFCS.2016.25</a>'
  apa: 'Chatterjee, K., Dvorák, W., Henzinger, M., &#38; Loitzenbauer, V. (2016).
    Conditionally optimal algorithms for generalized Büchi Games (Vol. 58). Presented
    at the MFCS: Mathematical Foundations of Computer Science, Krakow, Poland: Schloss
    Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2016.25">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>'
  chicago: Chatterjee, Krishnendu, Wolfgang Dvorák, Monika Henzinger, and Veronika
    Loitzenbauer. “Conditionally Optimal Algorithms for Generalized Büchi Games,”
    Vol. 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href="https://doi.org/10.4230/LIPIcs.MFCS.2016.25">https://doi.org/10.4230/LIPIcs.MFCS.2016.25</a>.
  ieee: 'K. Chatterjee, W. Dvorák, M. Henzinger, and V. Loitzenbauer, “Conditionally
    optimal algorithms for generalized Büchi Games,” presented at the MFCS: Mathematical
    Foundations of Computer Science, Krakow, Poland, 2016, vol. 58.'
  ista: 'Chatterjee K, Dvorák W, Henzinger M, Loitzenbauer V. 2016. Conditionally
    optimal algorithms for generalized Büchi Games. MFCS: Mathematical Foundations
    of Computer Science, LIPIcs, vol. 58, 25.'
  mla: Chatterjee, Krishnendu, et al. <i>Conditionally Optimal Algorithms for Generalized
    Büchi Games</i>. Vol. 58, 25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016, doi:<a href="https://doi.org/10.4230/LIPIcs.MFCS.2016.25">10.4230/LIPIcs.MFCS.2016.25</a>.
  short: K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl
    - Leibniz-Zentrum für Informatik, 2016.
conference:
  end_date: 2016-08-26
  location: Krakow, Poland
  name: 'MFCS: Mathematical Foundations of Computer Science'
  start_date: 2016-08-22
date_created: 2018-12-11T11:49:58Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-07-10T11:49:55Z
day: '01'
ddc:
- '000'
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.MFCS.2016.25
ec_funded: 1
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:02Z
  date_updated: 2018-12-12T10:16:02Z
  file_id: '5187'
  file_name: IST-2017-779-v1+1_LIPIcs-MFCS-2016-25.pdf
  file_size: 632786
  relation: main_file
file_date_updated: 2018-12-12T10:16:02Z
has_accepted_license: '1'
intvolume: '        58'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/3.0/
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 25892FC0-B435-11E9-9278-68D0E5697425
  grant_number: ICT15-003
  name: Efficient Algorithms for Computer Aided Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6317'
pubrep_id: '779'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Conditionally optimal algorithms for generalized Büchi 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: 58
year: '2016'
...
---
_id: '1069'
abstract:
- lang: eng
  text: "The Continuous Skolem Problem asks whether a real-valued function satisfying
    a linear differen-\r\ntial equation has a zero in a given interval of real numbers.
    This is a fundamental reachability\r\nproblem for continuous linear dynamical
    systems, such as linear hybrid automata and continuous-\r\ntime Markov chains.
    Decidability of the problem is currently open – indeed decidability is open\r\neven
    for the sub-problem in which a zero is sought in a bounded interval. In this paper
    we show\r\ndecidability of the bounded problem subject to Schanuel’s Conjecture,
    a unifying conjecture in\r\ntranscendental number theory. We furthermore analyse
    the unbounded problem in terms of the\r\nfrequencies of the differential equation,
    that is, the imaginary parts of the characteristic roots.\r\nWe show that the
    unbounded problem can be reduced to the bounded problem if there is at most\r\none
    rationally linearly independent frequency, or if there are two rationally linearly
    independent\r\nfrequencies and all characteristic roots are simple. We complete
    the picture by showing that de-\r\ncidability of the unbounded problem in the
    case of two (or more) rationally linearly independent\r\nfrequencies would entail
    a major new effectiveness result in Diophantine approximation, namely\r\ncomputability
    of the Diophantine-approximation types of all real algebraic numbers."
acknowledgement: 'Ventsislav Chonev is supported by Austrian Science Fund (FWF) NFN
  Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307:  Graph Games), and ERC
  Advanced Grant (267989: QUAREM).'
alternative_title:
- LIPIcs
article_number: '100'
article_processing_charge: No
author:
- first_name: Ventsislav K
  full_name: Chonev, Ventsislav K
  id: 36CBE2E6-F248-11E8-B48F-1D18A9856A87
  last_name: Chonev
- first_name: Joël
  full_name: Ouaknine, Joël
  last_name: Ouaknine
- first_name: James
  full_name: Worrell, James
  last_name: Worrell
citation:
  ama: 'Chonev VK, Ouaknine J, Worrell J. On the skolem problem for continuous linear
    dynamical systems. In: Vol 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik;
    2016. doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.100">10.4230/LIPIcs.ICALP.2016.100</a>'
  apa: 'Chonev, V. K., Ouaknine, J., &#38; Worrell, J. (2016). On the skolem problem
    for continuous linear dynamical systems (Vol. 55). Presented at the ICALP: Automata,
    Languages and Programming, Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für
    Informatik. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.100">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>'
  chicago: Chonev, Ventsislav K, Joël Ouaknine, and James Worrell. “On the Skolem
    Problem for Continuous Linear Dynamical Systems,” Vol. 55. Schloss Dagstuhl -
    Leibniz-Zentrum für Informatik, 2016. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.100">https://doi.org/10.4230/LIPIcs.ICALP.2016.100</a>.
  ieee: 'V. K. Chonev, J. Ouaknine, and J. Worrell, “On the skolem problem for continuous
    linear dynamical systems,” presented at the ICALP: Automata, Languages and Programming,
    Rome, Italy, 2016, vol. 55.'
  ista: 'Chonev VK, Ouaknine J, Worrell J. 2016. On the skolem problem for continuous
    linear dynamical systems. ICALP: Automata, Languages and Programming, LIPIcs,
    vol. 55, 100.'
  mla: Chonev, Ventsislav K., et al. <i>On the Skolem Problem for Continuous Linear
    Dynamical Systems</i>. Vol. 55, 100, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016, doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.100">10.4230/LIPIcs.ICALP.2016.100</a>.
  short: V.K. Chonev, J. Ouaknine, J. Worrell, in:, Schloss Dagstuhl - Leibniz-Zentrum
    für Informatik, 2016.
conference:
  end_date: 2016-07-15
  location: Rome, Italy
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-08-01T00:00:00Z
date_updated: 2025-06-03T11:32:08Z
day: '01'
ddc:
- '004'
- '006'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.100
ec_funded: 1
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:16:26Z
  date_updated: 2018-12-12T10:16:26Z
  file_id: '5213'
  file_name: IST-2017-778-v1+1_LIPIcs-ICALP-2016-100.pdf
  file_size: 521415
  relation: main_file
file_date_updated: 2018-12-12T10:16:26Z
has_accepted_license: '1'
intvolume: '        55'
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: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
publication_status: published
publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik
publist_id: '6314'
pubrep_id: '778'
quality_controlled: '1'
scopus_import: '1'
status: public
title: On the skolem problem for continuous linear dynamical systems
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
---
_id: '1070'
abstract:
- lang: eng
  text: 'We present a logic that extends CTL (Computation Tree Logic) with operators
    that express synchronization properties. A property is synchronized in a system
    if it holds in all paths of a certain length. The new logic is obtained by using
    the same path quantifiers and temporal operators as in CTL, but allowing a different
    order of the quantifiers. This small syntactic variation induces a logic that
    can express non-regular properties for which known extensions of MSO with equality
    of path length are undecidable. We show that our variant of CTL is decidable and
    that the model-checking problem is in Delta_3^P = P^{NP^NP}, and is DP-hard. We
    analogously consider quantifier exchange in extensions of CTL, and we present
    operators defined using basic operators of CTL* that express the occurrence of
    infinitely many synchronization points. We show that the model-checking problem
    remains in Delta_3^P. The distinguishing power of CTL and of our new logic coincide
    if the Next operator is allowed in the logics, thus the classical bisimulation
    quotient can be used for state-space reduction before model checking. '
acknowledgement: "This research was partially supported by Austrian Science Fund (FWF)
  NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), Vienna
  Science and Technology Fund (WWTF) through project ICT15-003, and European project
  Cassting (FP7-601148).\r\n\r\nWe thank Stefan Göller and anonymous reviewers for
  their insightful\r\ncomments and suggestions.\r\n"
alternative_title:
- LIPIcs
article_number: '98'
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
citation:
  ama: 'Chatterjee K, Doyen L. Computation tree logic for synchronization properties.
    In: Vol 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.98">10.4230/LIPIcs.ICALP.2016.98</a>'
  apa: 'Chatterjee, K., &#38; Doyen, L. (2016). Computation tree logic for synchronization
    properties (Vol. 55). Presented at the ICALP: Automata, Languages and Programming,
    Rome, Italy: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.98">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>'
  chicago: Chatterjee, Krishnendu, and Laurent Doyen. “Computation Tree Logic for
    Synchronization Properties,” Vol. 55. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016. <a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.98">https://doi.org/10.4230/LIPIcs.ICALP.2016.98</a>.
  ieee: 'K. Chatterjee and L. Doyen, “Computation tree logic for synchronization properties,”
    presented at the ICALP: Automata, Languages and Programming, Rome, Italy, 2016,
    vol. 55.'
  ista: 'Chatterjee K, Doyen L. 2016. Computation tree logic for synchronization properties.
    ICALP: Automata, Languages and Programming, LIPIcs, vol. 55, 98.'
  mla: Chatterjee, Krishnendu, and Laurent Doyen. <i>Computation Tree Logic for Synchronization
    Properties</i>. Vol. 55, 98, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016, doi:<a href="https://doi.org/10.4230/LIPIcs.ICALP.2016.98">10.4230/LIPIcs.ICALP.2016.98</a>.
  short: K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
    2016.
conference:
  end_date: 2016-07-15
  location: Rome, Italy
  name: 'ICALP: Automata, Languages and Programming'
  start_date: 2016-07-12
date_created: 2018-12-11T11:49:59Z
date_published: 2016-01-01T00:00:00Z
date_updated: 2025-06-03T11:18:54Z
day: '01'
ddc:
- '005'
department:
- _id: KrCh
doi: 10.4230/LIPIcs.ICALP.2016.98
ec_funded: 1
file:
- access_level: open_access
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:08:52Z
  date_updated: 2018-12-12T10:08:52Z
  file_id: '4714'
  file_name: IST-2017-812-v1+1_LIPIcs-ICALP-2016-98.pdf
  file_size: 546133
  relation: main_file
file_date_updated: 2018-12-12T10:08:52Z
has_accepted_license: '1'
intvolume: '        55'
language:
- iso: eng
month: '01'
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 für Informatik
publist_id: '6313'
pubrep_id: '812'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computation tree logic for synchronization properties
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 55
year: '2016'
...
