Symmetry and Reduced Symmetry in Model-Checking

In the last few years there has been much interest in symmetry based methods for state space reductions in model-checking of concurrent systems. Many techniques have been developed using this approach [9,2,3,4,7,11]. All these methods are based on determining permutations on the process indices or on variables that induce an auto-morphism on the global state graph. In this paper, we generalize the symmetry based approach so that arbitrary auto-morphisms are considered and so that some systems with little or no symmetry can also be handled. We present new symmetry based methods, that employ formula decomposition and sub-formula tracking for efficient model-checking of CTL formulas.