Abstract: We present algorithms that perform on-the-fly symbolic model checking for temporal safety properties, using symmetry reduction. We further extend these algorithm for checking liveness properties as well.

Our methods are fully automatic. The user should supply some basic information about the symmetry in the verified system. However, the methods are robust and work correctly even if the information supplied by the user is incorrect. Moreover, the methods return correct results even in case the computation of the symmetry reduction has not been completed due to memory or time explosion.

We implemented our methods within IBM's model checker RuleBase, and compared the performance of our methods with that of RuleBase. In most cases, our algorithms outperformed RuleBase with respect to both time and space.