Isomorphism Checking for Symmetry Reduction

    Research output: Book/ReportReportProfessional

    14 Downloads (Pure)

    Abstract

    In this paper, we show how isomorphism checking can be used as an effective technique for symmetry reduction. Reduced state spaces are equivalent to the original ones under a strong notion of bisimilarity which preserves the multiplicity of outgoing transitions, and therefore also preserves stochastic temporal logics. We have implemented this in a setting where states are arbitrary graphs. Since no efficiently computable canonical representation is known for arbitrary graphs modulo isomorphism, we define an isomorphism-predicting hash function on the basis of an existing partition refinement algorithm. As an example, we report a factorial state space reduction on a model of an ad-hoc network connectivity protocol.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages15
    Publication statusPublished - Apr 2010

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.TR-CTIT-10-27
    ISSN (Print)1381-3625

    Keywords

    • IR-72369
    • EWI-18117
    • METIS-270902

    Cite this

    Rensink, A. (2010). Isomorphism Checking for Symmetry Reduction. (CTIT Technical Report Series; No. TR-CTIT-10-27). Enschede: Centre for Telematics and Information Technology (CTIT).
    Rensink, Arend. / Isomorphism Checking for Symmetry Reduction. Enschede : Centre for Telematics and Information Technology (CTIT), 2010. 15 p. (CTIT Technical Report Series; TR-CTIT-10-27).
    @book{63c296f2de84438585d225e73fcc004a,
    title = "Isomorphism Checking for Symmetry Reduction",
    abstract = "In this paper, we show how isomorphism checking can be used as an effective technique for symmetry reduction. Reduced state spaces are equivalent to the original ones under a strong notion of bisimilarity which preserves the multiplicity of outgoing transitions, and therefore also preserves stochastic temporal logics. We have implemented this in a setting where states are arbitrary graphs. Since no efficiently computable canonical representation is known for arbitrary graphs modulo isomorphism, we define an isomorphism-predicting hash function on the basis of an existing partition refinement algorithm. As an example, we report a factorial state space reduction on a model of an ad-hoc network connectivity protocol.",
    keywords = "IR-72369, EWI-18117, METIS-270902",
    author = "Arend Rensink",
    year = "2010",
    month = "4",
    language = "Undefined",
    series = "CTIT Technical Report Series",
    publisher = "Centre for Telematics and Information Technology (CTIT)",
    number = "TR-CTIT-10-27",
    address = "Netherlands",

    }

    Rensink, A 2010, Isomorphism Checking for Symmetry Reduction. CTIT Technical Report Series, no. TR-CTIT-10-27, Centre for Telematics and Information Technology (CTIT), Enschede.

    Isomorphism Checking for Symmetry Reduction. / Rensink, Arend.

    Enschede : Centre for Telematics and Information Technology (CTIT), 2010. 15 p. (CTIT Technical Report Series; No. TR-CTIT-10-27).

    Research output: Book/ReportReportProfessional

    TY - BOOK

    T1 - Isomorphism Checking for Symmetry Reduction

    AU - Rensink, Arend

    PY - 2010/4

    Y1 - 2010/4

    N2 - In this paper, we show how isomorphism checking can be used as an effective technique for symmetry reduction. Reduced state spaces are equivalent to the original ones under a strong notion of bisimilarity which preserves the multiplicity of outgoing transitions, and therefore also preserves stochastic temporal logics. We have implemented this in a setting where states are arbitrary graphs. Since no efficiently computable canonical representation is known for arbitrary graphs modulo isomorphism, we define an isomorphism-predicting hash function on the basis of an existing partition refinement algorithm. As an example, we report a factorial state space reduction on a model of an ad-hoc network connectivity protocol.

    AB - In this paper, we show how isomorphism checking can be used as an effective technique for symmetry reduction. Reduced state spaces are equivalent to the original ones under a strong notion of bisimilarity which preserves the multiplicity of outgoing transitions, and therefore also preserves stochastic temporal logics. We have implemented this in a setting where states are arbitrary graphs. Since no efficiently computable canonical representation is known for arbitrary graphs modulo isomorphism, we define an isomorphism-predicting hash function on the basis of an existing partition refinement algorithm. As an example, we report a factorial state space reduction on a model of an ad-hoc network connectivity protocol.

    KW - IR-72369

    KW - EWI-18117

    KW - METIS-270902

    M3 - Report

    T3 - CTIT Technical Report Series

    BT - Isomorphism Checking for Symmetry Reduction

    PB - Centre for Telematics and Information Technology (CTIT)

    CY - Enschede

    ER -

    Rensink A. Isomorphism Checking for Symmetry Reduction. Enschede: Centre for Telematics and Information Technology (CTIT), 2010. 15 p. (CTIT Technical Report Series; TR-CTIT-10-27).