Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Parameterized Model Checking of Token-Passing Systems
verfasst von : Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, Sasha Rubin
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.