Partial order reduction and symmetry with multiple representatives

D. Bosnacki, M. Scheffer

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

2 Citaten (Scopus)

Samenvatting

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.
Originele taal-2Engels
TitelNASA Formal Methods Symposium
Subtitel7th International Symposium, NFM'15, Pasadena CA, USA, April 27-29, 2015. Proceedings
RedacteurenK. Havelund, G. Holzmann, R. Joshi
UitgeverijSpringer
Pagina's97-111
ISBN van geprinte versie978-3-319-17523-2
DOI's
StatusGepubliceerd - 8 apr. 2015
Evenement7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA - Pasadena, CA, Verenigde Staten van Amerika
Duur: 27 apr. 201529 apr. 2015

Publicatie series

NaamLecture Notes in Computer Science
Volume9058
ISSN van geprinte versie0302-9743

Congres

Congres7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Verkorte titelNFM 2015
Land/RegioVerenigde Staten van Amerika
StadPasadena, CA
Periode27/04/1529/04/15
Ander7th International Symposium on Formal Methods

Vingerafdruk

Duik in de onderzoeksthema's van 'Partial order reduction and symmetry with multiple representatives'. Samen vormen ze een unieke vingerafdruk.

Citeer dit