Using canonical forms for isomorphism reduction in graph-based model checking

Graph isomorphism checking can be used in graph-based model checking to achieve symmetry reduction. Instead of one-to-one comparing the graph representations of states, canonical forms of state graphs can be computed. These canonical forms can be used to store and compare states. However, computing a canonical form for a graph is computationally expensive. Whether computing a ca-nonical representation for states and reducing the state space is more efficient than using canonical hashcodes for states and comparing states one-to-one is not a pri-ori clear. In this paper these approaches to isomorphism reduction are described and a preliminary comparison is presented for checking isomorphism of pairs of graphs. An existing algorithm that does not compute a canonica