Technical Report No. 184 - Abstract

Alberto Lluch Lafuente
First Attempts to Combine Symmetry Reduction and Heuristic Search for Error Detection

The state explosion problem is the main limitation of model checking. Symmetries in the system being verified can be exploited in order to avoid this problem. A symmetry relation on the system is defined, which induces a semantically equivalent quotient system of smaller size. On the other hand, heuristic search algorithms can be applied to improve error detection. Such algorithms use heuristic functions to guide the exploration. Best-first is used for accelerating the search, while A* guarantees optimal error trails if combined with admissible estimates. We analyze some aspects of combining both approaches, presenting an admissible estimate that allows A* to provide optimal counterexamples when combined with symmetry reduction. Experimental results are also included.