Partial order reduction and symmetry with multiple representatives

D. Bosnacki, M. Scheffer

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)

Abstract

Symmetry reduction is one of the most successful techniques to cope with the state explosion problem in model-checking. One of the central issues in symmetry reduction is the problem of finding unique (canonical) representatives of equivalence classes of symmetric states. This problem is equivalent to the graph isomorphism problem, for which no polynomial algorithm is known. On the other hand finding multiple (non-canonical) representatives is much easier because it usually boils down to sorting algorithms. As a consequence, with multiple representatives one can significantly improve the verification times. In this paper we show that symmetry reduction with multiple representatives can be combined with partial order reduction, another efficient state space reduction technique. To this end we introduce a new weaker notion of independence which requires confluence only up to bisimulation.
Original languageEnglish
Title of host publicationNASA Formal Methods Symposium
Subtitle of host publication7th International Symposium, NFM'15, Pasadena CA, USA, April 27-29, 2015. Proceedings
EditorsK. Havelund, G. Holzmann, R. Joshi
PublisherSpringer
Pages97-111
ISBN (Print)978-3-319-17523-2
DOIs
Publication statusPublished - 8 Apr 2015
Event7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA - Pasadena, CA, United States
Duration: 27 Apr 201529 Apr 2015

Publication series

NameLecture Notes in Computer Science
Volume9058
ISSN (Print)0302-9743

Conference

Conference7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Abbreviated titleNFM 2015
Country/TerritoryUnited States
CityPasadena, CA
Period27/04/1529/04/15

Fingerprint

Dive into the research topics of 'Partial order reduction and symmetry with multiple representatives'. Together they form a unique fingerprint.

Cite this