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
StatePublished - 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

Fingerprint

Isomorphism
State space
Arbitrary
Graph in graph theory
Canonical representation
Symmetry reduction
Network connectivity
Hash function
Factorial
Temporal logic
Ad hoc networks
Modulo
Multiplicity
Refinement
Partition
Model

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; No. TR-CTIT-10-27).

Research output: ProfessionalReport

@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",
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: ProfessionalReport

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)

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