---
_id: '10884'
abstract:
- lang: eng
  text: "We revisit the parameterized model checking problem for token-passing systems
    and specifications in indexed CTL  ∗ \\X. Emerson and Namjoshi (1995, 2003) have
    shown that parameterized model checking of indexed CTL  ∗ \\X in uni-directional
    token rings can be reduced to checking rings up to some cutoff size. Clarke et
    al. (2004) have shown a similar result for general topologies and indexed LTL
    \\X, provided processes cannot choose the directions for sending or receiving
    the token.\r\nWe unify and substantially extend these results by systematically
    exploring fragments of indexed CTL  ∗ \\X with respect to general topologies.
    For each fragment we establish whether a cutoff exists, and for some concrete
    topologies, such as rings, cliques and stars, we infer small cutoffs. Finally,
    we show that the problem becomes undecidable, and thus no cutoffs exist, if processes
    are allowed to choose the directions in which they send or from which they receive
    the token."
acknowledgement: "This work was supported by the Austrian Science Fund through grant
  P23499-N23\r\nand through the RiSE network (S11403, S11405, S11406, S11407-N23);
  ERC Starting Grant (279307: Graph Games); Vienna Science and Technology Fund (WWTF)\r\ngrants
  PROSEED, ICT12-059, and VRG11-005."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Benjamin
  full_name: Aminof, Benjamin
  id: 4A55BD00-F248-11E8-B48F-1D18A9856A87
  last_name: Aminof
- first_name: Swen
  full_name: Jacobs, Swen
  last_name: Jacobs
- first_name: Ayrat
  full_name: Khalimov, Ayrat
  last_name: Khalimov
- first_name: Sasha
  full_name: Rubin, Sasha
  id: 2EC51194-F248-11E8-B48F-1D18A9856A87
  last_name: Rubin
citation:
  ama: 'Aminof B, Jacobs S, Khalimov A, Rubin S. Parameterized model checking of token-passing
    systems. In: <i>Verification, Model Checking, and Abstract Interpretation</i>.
    Vol 8318. Springer Nature; 2014:262-281. doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_15">10.1007/978-3-642-54013-4_15</a>'
  apa: 'Aminof, B., Jacobs, S., Khalimov, A., &#38; Rubin, S. (2014). Parameterized
    model checking of token-passing systems. In <i>Verification, Model Checking, and
    Abstract Interpretation</i> (Vol. 8318, pp. 262–281). San Diego, CA, United States:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-642-54013-4_15">https://doi.org/10.1007/978-3-642-54013-4_15</a>'
  chicago: Aminof, Benjamin, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. “Parameterized
    Model Checking of Token-Passing Systems.” In <i>Verification, Model Checking,
    and Abstract Interpretation</i>, 8318:262–81. Springer Nature, 2014. <a href="https://doi.org/10.1007/978-3-642-54013-4_15">https://doi.org/10.1007/978-3-642-54013-4_15</a>.
  ieee: B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin, “Parameterized model checking
    of token-passing systems,” in <i>Verification, Model Checking, and Abstract Interpretation</i>,
    San Diego, CA, United States, 2014, vol. 8318, pp. 262–281.
  ista: 'Aminof B, Jacobs S, Khalimov A, Rubin S. 2014. Parameterized model checking
    of token-passing systems. Verification, Model Checking, and Abstract Interpretation.
    VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318,
    262–281.'
  mla: Aminof, Benjamin, et al. “Parameterized Model Checking of Token-Passing Systems.”
    <i>Verification, Model Checking, and Abstract Interpretation</i>, vol. 8318, Springer
    Nature, 2014, pp. 262–81, doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_15">10.1007/978-3-642-54013-4_15</a>.
  short: B. Aminof, S. Jacobs, A. Khalimov, S. Rubin, in:, Verification, Model Checking,
    and Abstract Interpretation, Springer Nature, 2014, pp. 262–281.
conference:
  end_date: 2014-01-21
  location: San Diego, CA, United States
  name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
  start_date: 2014-01-19
date_created: 2022-03-18T13:01:22Z
date_published: 2014-01-30T00:00:00Z
date_updated: 2022-05-17T08:36:01Z
day: '30'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54013-4_15
ec_funded: 1
external_id:
  arxiv:
  - '1311.4425'
intvolume: '      8318'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: ' https://doi.org/10.48550/arXiv.1311.4425'
month: '01'
oa: 1
oa_version: Preprint
page: 262-281
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
publication: Verification, Model Checking, and Abstract Interpretation
publication_identifier:
  eisbn:
  - '9783642540134'
  eissn:
  - 1611-3349
  isbn:
  - '9783642540127'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parameterized model checking of token-passing systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...
---
_id: '10885'
abstract:
- lang: eng
  text: "Two-player games on graphs provide the theoretical framework for many important
    problems such as reactive synthesis. While the traditional study of two-player
    zero-sum games has been extended to multi-player games with several notions of
    equilibria, they are decidable only for perfect-information games, whereas several
    applications require imperfect-information games.\r\nIn this paper we propose
    a new notion of equilibria, called doomsday equilibria, which is a strategy profile
    such that all players satisfy their own objective, and if any coalition of players
    deviates and violates even one of the players objective, then the objective of
    every player is violated.\r\nWe present algorithms and complexity results for
    deciding the existence of doomsday equilibria for various classes of ω-regular
    objectives, both for imperfect-information games, and for perfect-information
    games.We provide optimal complexity bounds for imperfect-information games, and
    in most cases for perfect-information games."
acknowledgement: " Supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF
  NFN Grant No\r\nS11407-N23 (RiSE), ERC Start grant (279307: Graph Games), and Microsoft
  faculty fellows award."
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Emmanuel
  full_name: Filiot, Emmanuel
  last_name: Filiot
- first_name: Jean-François
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: 'Chatterjee K, Doyen L, Filiot E, Raskin J-F. Doomsday equilibria for omega-regular
    games. In: <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>.
    Vol 8318. Springer Nature; 2014:78-97. doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_5">10.1007/978-3-642-54013-4_5</a>'
  apa: 'Chatterjee, K., Doyen, L., Filiot, E., &#38; Raskin, J.-F. (2014). Doomsday
    equilibria for omega-regular games. In <i>VMCAI 2014: Verification, Model Checking,
    and Abstract Interpretation</i> (Vol. 8318, pp. 78–97). San Diego, CA, United
    States: Springer Nature. <a href="https://doi.org/10.1007/978-3-642-54013-4_5">https://doi.org/10.1007/978-3-642-54013-4_5</a>'
  chicago: 'Chatterjee, Krishnendu, Laurent Doyen, Emmanuel Filiot, and Jean-François
    Raskin. “Doomsday Equilibria for Omega-Regular Games.” In <i>VMCAI 2014: Verification,
    Model Checking, and Abstract Interpretation</i>, 8318:78–97. Springer Nature,
    2014. <a href="https://doi.org/10.1007/978-3-642-54013-4_5">https://doi.org/10.1007/978-3-642-54013-4_5</a>.'
  ieee: 'K. Chatterjee, L. Doyen, E. Filiot, and J.-F. Raskin, “Doomsday equilibria
    for omega-regular games,” in <i>VMCAI 2014: Verification, Model Checking, and
    Abstract Interpretation</i>, San Diego, CA, United States, 2014, vol. 8318, pp.
    78–97.'
  ista: 'Chatterjee K, Doyen L, Filiot E, Raskin J-F. 2014. Doomsday equilibria for
    omega-regular games. VMCAI 2014: Verification, Model Checking, and Abstract Interpretation.
    VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 8318,
    78–97.'
  mla: 'Chatterjee, Krishnendu, et al. “Doomsday Equilibria for Omega-Regular Games.”
    <i>VMCAI 2014: Verification, Model Checking, and Abstract Interpretation</i>,
    vol. 8318, Springer Nature, 2014, pp. 78–97, doi:<a href="https://doi.org/10.1007/978-3-642-54013-4_5">10.1007/978-3-642-54013-4_5</a>.'
  short: 'K. Chatterjee, L. Doyen, E. Filiot, J.-F. Raskin, in:, VMCAI 2014: Verification,
    Model Checking, and Abstract Interpretation, Springer Nature, 2014, pp. 78–97.'
conference:
  end_date: 2014-01-21
  location: San Diego, CA, United States
  name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
  start_date: 2014-01-19
date_created: 2022-03-18T13:03:15Z
date_published: 2014-01-30T00:00:00Z
date_updated: 2023-02-23T12:52:24Z
day: '30'
department:
- _id: KrCh
doi: 10.1007/978-3-642-54013-4_5
ec_funded: 1
external_id:
  arxiv:
  - '1311.3238'
intvolume: '      8318'
language:
- iso: eng
month: '01'
oa_version: Preprint
page: 78-97
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: 'VMCAI 2014: Verification, Model Checking, and Abstract Interpretation'
publication_identifier:
  eisbn:
  - '9783642540134'
  eissn:
  - 1611-3349
  isbn:
  - '9783642540127'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '681'
    relation: later_version
    status: public
scopus_import: '1'
status: public
title: Doomsday equilibria for omega-regular games
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8318
year: '2014'
...