Hassen Saïdi
Discovering Symmetries
In SRI Technical Notes. 2005.
Abstract
When model checking concurrent software applications, symmetry reduction techniques narrow dramatically the size of the state space search by identifying computations that, because of symmetries in the system, are redundant. While state-exploration algorithms exploiting symmetry reduction are well developed, little has been done in {\em discovering} the nature of the symmetries of a system. What is even less researched is discovering symmetries that are particular to a temporal property. This paper proposes a general framework for discovering symmetries in systems that exhibit {\em absolute} or {\em relative} symmetries depending on the property of interest. Our work extends previous symmetry reduction techniques by making advances in automating generalized model automorphism discovery.