Isomorphism Checking for Symmetry Reduction

Research output: Book/ReportReportProfessional

13 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).