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.