Name
Abstract | ||
|---|---|---|
Two well-accepted techniques to tackle combinatorial explosion in model-checking are exploitation of symmetries and the use of reduced decision diagrams. Some work showed that these two techniques can be stacked in specific cases. This paper presents a novel and more general approach to combine these two techniques. Expected benefits of this combination are:· in symmetry-based reduction, the main source of complexity resides in the canonization computation that must be performed for each new encountered state, the use of shared decision diagrams allows one to canonize sets of states at once.· in decision diagram based techniques, dependencies between variables induce explosion in representation size, the manipulation of canonical states allows to partly overcome this limitation. We show that this combination is experimentally effective in many typical cases. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/ACSD.2012.28 | ACSD |
Keywords | Field | DocType |
decision diagrams,canonization computation,reduced decision diagram,canonical state,state space analysis,combinatorial explosion,general approach,main source,complexity resides,decision diagram,shared decision diagram,expected benefit,boolean functions,model checking,formal verification,symmetries,data structures,tin | Boolean function,Data structure,Computer science,Theoretical computer science,Influence diagram,Combinatorial explosion,State space,Homogeneous space,Computation,Formal verification | Conference |
Citations | PageRank | References |
3 | 0.42 | 9 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Maximilien Colange | 1 | 42 | 5.94 |
| Fabrice Kordon | 2 | 603 | 61.72 |
| Yann Thierry-Mieg | 3 | 225 | 18.17 |
| Souheib Baarir | 4 | 35 | 10.01 |