Extending Symmetry Reduction Techniques to a Realistic Model of Computation

Abstract : Much of the literature on symmetry reductions for model checking assumes a simple model of computation where the local state of each component in a concurrent system can be represented by an integer, and where components do not hold references to one another. Symmetry reduction techniques for model checking usually require a solution to the NP-hard Constructive Orbit Problem (COP)--computing the minimum element in the equivalence class of a given state under a symmetry group. Polynomial time strategies to solve instances of the COP under the simple model of computation are known for a large class of symmetry groups. We show that these strategies are not directly applicable when the model of computation is extended to allow components to hold references to one another, and present an approach to their extension, resulting in tractable, memory optimal symmetry reduction techniques for a realistic model of computation. Experimental results using the TopSPIN symmetry reduction package for the SPIN model checker illustrate the effectiveness of our techniques.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.63-76, 2006
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089491
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:13:53
Dernière modification le : vendredi 18 août 2006 - 19:57:43
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:37:59

Identifiants

  • HAL Id : inria-00089491, version 1

Collections

Citation

Alastair Donaldson, Alice Miller. Extending Symmetry Reduction Techniques to a Realistic Model of Computation. Stephan Merz and Tobias Nipkow. Automatic Verification of Critical Systems, Sep 2006, Nancy/France, pp.63-76, 2006. 〈inria-00089491〉

Partager

Métriques

Consultations de la notice

54

Téléchargements de fichiers

66