Using Canonical Forms for Isomorphism Reduction in Graph-based Model Checking

Gijs Kant

    Research output: Book/ReportReportProfessional

    261 Downloads (Pure)


    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 canonical 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 priori 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 canonical form performs better that tools that do for graphs that are used in graph-based model checking. Computing canonical forms seems to scale better for larger graphs.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages34
    Publication statusPublished - Jul 2010

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1381-3625


    • Graph Isomorphism
    • IR-72368
    • EWI-18116
    • Graph-based Model Checking
    • METIS-276046
    • Canonical Form

    Cite this