Identification and Counter Abstraction for Full Virtual Symmetry
Abstract
Symmetry reduction is an effective approach for dealing with the state
explosion problem: when applicable, it enables
exponential statespace reduction. Thus, it is appealing to
extend the power of symmetry reduction to systems which are ``not
quite symmetric''. Emerson et al. identified a class of these,
called virtually symmetric.
In this
paper, we study symmetry from the point of view of abstraction, which
allows us to present an efficient procedure for
identifying full virtual symmetry. We also explore techniques for combining
virtual symmetry with symbolic model-checking and
report on experiments that illustrate the feasibility of
our approach.