Detecting and Exploiting Data Type Symmetries of Algebraic System Nets during Reachability Analysis

Reference:

Tommi Junttila. Detecting and exploiting data type symmetries of algebraic system nets during reachability analysis. Research Report A57, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science, Espoo, Finland, December 1999.

Abstract:

The symmetry reduction method is a technique designed to alleviate the combinatorial state space explosion problem by exploiting the symmetries of state spaces. This work describes a way how state space symmetries of a high-level Petri net formalism, algebraic system nets, can be detected and exploited during the reachability analysis. The main idea is that permuting the domains of data types used in nets produces corresponding permutations to the state space level.

As the main result a sufficient condition is defined for data type domain permutations ensuring that the produced state space permutations are actually automorphisms i.e. symmetries. Since verification of the condition is shown to be a co-NP-complete problem, an approximation rule for the condition is also given. Use of the developed theory is illustrated by defining the class of extended well-formed nets and by examining data type symmetries of such nets. It is shown that checking the symmetricity of two markings of a net in this class is equivalent to checking whether two graphs are isomorphic.

Keywords:

Symmetry, reachability analysis, Petri nets, algebraic system nets

Suggested BibTeX entry:

@techreport{HUT-TCS-A57,
    address = {Espoo, Finland},
    author = {Junttila, Tommi},
    institution = {Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science},
    month = {December},
    number = {A57},
    pages = {67},
    title = {Detecting and Exploiting Data Type Symmetries of Algebraic System Nets during Reachability Analysis},
    type = {Research Report},
    year = {1999},
}