Please use this identifier to cite or link to this item:
|Title:||A complete method for symmetry reduction in safety verification|
|Citation:||Chu, D.-H.,Jaffar, J. (2012). A complete method for symmetry reduction in safety verification. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 7358 LNCS : 616-633. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-31424-7_43|
|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 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 SMTand 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. © 2012 Springer-Verlag.|
|Source Title:||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Appears in Collections:||Staff Publications|
Show full item record
Files in This Item:
There are no files associated with this item.
checked on Dec 10, 2018
checked on Nov 24, 2018
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.