Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-31424-7_43
Title: A complete method for symmetry reduction in safety verification
Authors: Chu, D.-H.
Jaffar, J. 
Issue Date: 2012
Source: 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)
URI: http://scholarbank.nus.edu.sg/handle/10635/40008
ISBN: 9783642314230
ISSN: 03029743
DOI: 10.1007/978-3-642-31424-7_43
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

6
checked on Dec 5, 2017

Page view(s)

51
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.