A Complete Method for Symmetry Reduction in Safety Verification

Duc-Hiep Chu and Joxan Jaffar

Abstract

Symmetry reduction is a well-investigated technique to counter the state space explosion problem for reasoning about a concurrent system of similar processes. Here we present a general method for its application, restricted to verification of safety properties, but \emph{without} any prior knowledge about global symmetry. We start by using a notion of \emph{weak symmetry} which allows for more reduction than in previous notions of symmetry. This notion is relative to the target safety property. % which is used to enhance the occurrence of symmetry. The key idea is to perform symmetric transformations on \emph{state interpolation}, a concept which has been used widely for pruning in SMT and CEGAR. Our method naturally favors ``quite symmetric'' systems: more similarity among the processes leads to greater pruning of the tree. The main result is that the method is \emph{complete} wrt. weak symmetry: it only considers states which are not symmetric to an already encountered state