Name
Abstract | ||
|---|---|---|
Symmetry reduction holds great promise to counter the state explosion problem. However, currently it is "conducting a life on the fringe", and is not widely applied, mainly due to the restricted applicability of many of the techniques. In this paper we propose a symmetry reduction technique applied to high-level formal specification languages (B and Z). Not only does symmetry arise naturally in most models, it can also be exploited without restriction by our method. This method translates states of a formal model into directed graphs, and then uses graph canonicalisation to detect symmetries. We use the tool NAUTY to efficiently perform graph canonicalisation, which we have interfaced with the model checker PRO_B. In this paper we present the general technique, show how states can be translated first into vertex-coloured graphs suitable for NAUTY. We present empirical results, showing the effectiveness of our method as well as analysing the cost of graph canonicalisation. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1109/TASE.2008.33 | Nanjing |
Keywords | Field | DocType |
z models,graph canonicalisation,tool nauty,symmetry reduction.1,symmetry reduction technique,formal model,general technique,high-level formal specification language,model checker pro_b,b-method,model checking,method translates state,effective symmetry reduction,symmetry reduction,tool support,vertex-coloured graph,animation,formal specification,software engineering,formal verification,directed graphs,b method,set theory,formal specifications,logic,debugging | Graph automorphism,Set theory,Model checking,Computer science,Directed graph,Theoretical computer science,Formal specification,B-Method,Homogeneous space,Formal verification | Conference |
ISBN | Citations | PageRank |
978-0-7695-3249-3 | 13 | 0.60 |
References | Authors | |
10 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Corinna Spermann | 1 | 46 | 2.31 |
| Michael Leuschel | 2 | 2156 | 135.89 |