2013/11/18 by Benjamin Aminof, Aminof, Benjamin, Swen Jacobs +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1311.4425
openalex publication_date 2013/11/18 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We revisit the parameterized model checking problem for token-passing systems and specifications in indexed \textsfCTL^∗ \backslash \textsfX. Emerson and Namjoshi (1995, 2003) have shown that parameterized model checking of indexed \textsfCTL^∗ \backslash \textsfX 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 \textsfLTL \backslash \textsfX, 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 \textsfCTL^∗ \backslash \textsfX 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.