Optimized canonical labeling algorithm for graph rewriting systems

Kazuhiro Miyahara, Kazunori Ueda

    Research output: Contribution to journalArticle

    Abstract

    In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representa- tion to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we re- formulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.

    Original languageEnglish
    Pages (from-to)126-149
    Number of pages24
    JournalComputer Software
    Volume33
    Issue number1
    Publication statusPublished - 2016 Feb 1

    Fingerprint

    Labeling
    Model checking

    ASJC Scopus subject areas

    • Software

    Cite this

    Optimized canonical labeling algorithm for graph rewriting systems. / Miyahara, Kazuhiro; Ueda, Kazunori.

    In: Computer Software, Vol. 33, No. 1, 01.02.2016, p. 126-149.

    Research output: Contribution to journalArticle

    @article{197feea6a0f84c229139f00b62b4b5f4,
    title = "Optimized canonical labeling algorithm for graph rewriting systems",
    abstract = "In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representa- tion to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we re- formulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.",
    author = "Kazuhiro Miyahara and Kazunori Ueda",
    year = "2016",
    month = "2",
    day = "1",
    language = "English",
    volume = "33",
    pages = "126--149",
    journal = "Computer Software",
    issn = "0289-6540",
    publisher = "Japan Society for Software Science and Technology",
    number = "1",

    }

    TY - JOUR

    T1 - Optimized canonical labeling algorithm for graph rewriting systems

    AU - Miyahara, Kazuhiro

    AU - Ueda, Kazunori

    PY - 2016/2/1

    Y1 - 2016/2/1

    N2 - In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representa- tion to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we re- formulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.

    AB - In graph-based model checking, systems are modeled with graph structures which are highly expressive and feature a symmetry reduction mechanism. However, it involves frequent isomorphism checking of graphs generated in the course of model checking. Canonical labeling of graphs, which gives a unique representa- tion to isomorphic graphs, is expected to be an effective method to check isomorphism among many graphs efficiently. It is therefore important to efficiently compute canonical forms of graphs in graph rewriting systems. For this purpose, we propose an optimization technique for McKay's canonical labeling algorithm that reuses information of graph structures that does not change by rewriting. To enable reuse, we re- formulated McKay's algorithm to clarify what substructures of graphs are utilized in its execution, and designed an algorithm for successive graph canonicalization that organizes graph information in such a way that recomputation may be minimized. We evaluated the performance of the proposed algorithm, and found that it achieved sublinear time complexity with respect to the number of vertices for many cases of re-canonicalization.

    UR - http://www.scopus.com/inward/record.url?scp=84957711423&partnerID=8YFLogxK

    UR - http://www.scopus.com/inward/citedby.url?scp=84957711423&partnerID=8YFLogxK

    M3 - Article

    AN - SCOPUS:84957711423

    VL - 33

    SP - 126

    EP - 149

    JO - Computer Software

    JF - Computer Software

    SN - 0289-6540

    IS - 1

    ER -