TY - CONF AB - 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. AU - Aminof, Benjamin AU - Jacobs, Swen AU - Khalimov, Ayrat AU - Rubin, Sasha ID - 10884 SN - 0302-9743 T2 - Verification, Model Checking, and Abstract Interpretation TI - Parameterized model checking of token-passing systems VL - 8318 ER - TY - CONF AB - A standard technique for solving the parameterized model checking problem is to reduce it to the classic model checking problem of finitely many finite-state systems. This work considers some of the theoretical power and limitations of this technique. We focus on concurrent systems in which processes communicate via pairwise rendezvous, as well as the special cases of disjunctive guards and token passing; specifications are expressed in indexed temporal logic without the next operator; and the underlying network topologies are generated by suitable Monadic Second Order Logic formulas and graph operations. First, we settle the exact computational complexity of the parameterized model checking problem for some of our concurrent systems, and establish new decidability results for others. Second, we consider the cases that model checking the parameterized system can be reduced to model checking some fixed number of processes, the number is known as a cutoff. We provide many cases for when such cutoffs can be computed, establish lower bounds on the size of such cutoffs, and identify cases where no cutoff exists. Third, we consider cases for which the parameterized system is equivalent to a single finite-state system (more precisely a Büchi word automaton), and establish tight bounds on the sizes of such automata. AU - Aminof, Benjamin AU - Kotek, Tomer AU - Rubin, Sacha AU - Spegni, Francesco AU - Veith, Helmut ED - Baldan, Paolo ED - Gorla, Daniele ID - 2052 T2 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) TI - Parameterized model checking of rendezvous systems VL - 8704 ER - TY - CONF AB - First cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are traditionally of interest because of their connection with infinite-duration games such as parity and mean-payoff games. We study the memory requirements for winning strategies of FCGs and certain associated infinite duration games. We exhibit a simple FCG that is not memoryless determined (this corrects a mistake in Memoryless determinacy of parity and mean payoff games: a simple proof by Bj⋯orklund, Sandberg, Vorobyov (2004) that claims that FCGs for which Y is closed under cyclic permutations are memoryless determined). We show that θ (n)! memory (where n is the number of nodes in the graph), which is always sufficient, may be necessary to win some FCGs. On the other hand, we identify easy to check conditions on Y (i.e., Y is closed under cyclic permutations, and both Y and its complement are closed under concatenation) that are sufficient to ensure that the corresponding FCGs and their associated infinite duration games are memoryless determined. We demonstrate that many games considered in the literature, such as mean-payoff, parity, energy, etc., satisfy these conditions. On the complexity side, we show (for efficiently computable Y) that while solving FCGs is in PSPACE, solving some families of FCGs is PSPACE-hard. AU - Aminof, Benjamin AU - Rubin, Sasha ID - 475 T2 - Electronic Proceedings in Theoretical Computer Science, EPTCS TI - First cycle games VL - 146 ER -