@inproceedings{10884,
  abstract     = {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.
We 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.},
  author       = {Aminof, Benjamin and Jacobs, Swen and Khalimov, Ayrat and Rubin, Sasha},
  booktitle    = {Verification, Model Checking, and Abstract Interpretation},
  isbn         = {9783642540127},
  issn         = {1611-3349},
  location     = {San Diego, CA, United States},
  pages        = {262--281},
  publisher    = {Springer Nature},
  title        = {{Parameterized model checking of token-passing systems}},
  doi          = {10.1007/978-3-642-54013-4_15},
  volume       = {8318},
  year         = {2014},
}

@inproceedings{10885,
  abstract     = {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.
In 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.
We present algorithms and complexity results for deciding the existence of doomsday equilibria for various classes of ω-regular objectives, both for imperfect-information games, and for perfect-information games.We provide optimal complexity bounds for imperfect-information games, and in most cases for perfect-information games.},
  author       = {Chatterjee, Krishnendu and Doyen, Laurent and Filiot, Emmanuel and Raskin, Jean-François},
  booktitle    = {VMCAI 2014: Verification, Model Checking, and Abstract Interpretation},
  isbn         = {9783642540127},
  issn         = {1611-3349},
  location     = {San Diego, CA, United States},
  pages        = {78--97},
  publisher    = {Springer Nature},
  title        = {{Doomsday equilibria for omega-regular games}},
  doi          = {10.1007/978-3-642-54013-4_5},
  volume       = {8318},
  year         = {2014},
}