Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
A Complete Method for Symmetry Reduction in Safety Verification
verfasst von : Duc-Hiep Chu, Joxan Jaffar
Erschienen in: Computer Aided Verification
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
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
without
any prior knowledge about global symmetry. We start by using a notion of
weak symmetry
which allows for more reduction than in previous notions of symmetry. This notion is relative to the target safety property. The key idea is to perform symmetric transformations on
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
complete
wrt. weak symmetry: it only considers states which are not weakly symmetric to an already encountered state.