Name
Abstract | ||
|---|---|---|
Symmetry reduction is a technique to combat the state ex- plosion problem in temporal logic model checking. Its use with symbolic representation has suered from the prohibitively large BDD for the orbit relation. One suggested solution is to pre-compute a mapping from states to possibly multiple representatives of symmetry equivalence classes. In this paper, we propose a more ecien t method that determines repre- sentatives dynamically during xp oint iterations. Our scheme preserves the uniqueness of representatives. Another alternative to using the orbit relation is counter abstraction. It proved ecien t for the special case of full symmetry, provided a conducive program structure. In contrast, our solution applies also to systems with less than full symmetry, and to sys- tems where a translation into counters is not feasible. We support these claims with experimental results. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/978-3-540-31980-1_25 | Tools and Algorithms for Construction and Analysis of Systems |
Keywords | Field | DocType |
large bdd,dynamic symmetry reduction,full symmetry,conducive program structure,efficient method,symmetry reduction,symmetry equivalence class,fixpoint iteration,orbit relation,representatives dynamically,temporal logic,model checking | Kripke structure,Discrete mathematics,Uniqueness,Logic model,Model checking,Symmetry group,Computer science,Temporal logic,Equivalence class,Special case | Conference |
Volume | ISSN | ISBN |
3440 | 0302-9743 | 3-540-25333-5 |
Citations | PageRank | References |
23 | 1.08 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| e allen emerson | 1 | 7683 | 1183.13 |
| Thomas Wahl | 2 | 103 | 10.21 |