Symmetry reduction with inter-component references

Symmetry reduction was proposed in the early 1990s as a method for ameliorating the state-space explosion problem in model checking. The technique exploits replication in the structure of a concurrent system: structure-preserving permutations of process identifiers induce symmetries of the state-space associated with a system model. Symmetry partitions the state-space into orbits, and to verify a large class of temporal properties it is sufficient to check just a single representative state from each orbit.

Over the last 16 years, a wealth of techniques have been developed for efficiently computing orbit representatives. A common approach is to represent an orbit by the smallest state in the orbit (under a suitable total ordering). Under a simple model of computation where processes do not hold references to one another, the problem of computing the minimum representative of an orbit with respect to an arbitrary symmetry group is known as the Constructive Orbit Problem (COP), and is known to be NP-hard. However, for the special case of full symmetry the COP can be solved in polynomial time by sorting.

Practical models of software systems and protocols involve inter-component references. For example, in a leader election protocol based on construction of a spanning tree, each process holds “parent” and “child” references to other processes. This leads to the Constructive Orbit Problem with References (COPR), a natural generalisation of the COP to a model of computation with inter-component references. For symmetry reduction to be a useful technique in software model checking, efficient solutions to the COPR are required.

I will discuss the relationship between the COP and COPR, showing that the problems are polynomial time equivalent, but that the approach to solving the COP efficiently under full symmetry, by sorting, does not generalise to the COPR. I will then describe practical techniques for symmetry reduction in the presence of references developed during my PhD studies at the University of Glasgow, in conjunction with Alice Miller. Recently I have been thinking about the COPR, for the special case of full symmetry, from a new angle: I will discuss my preliminary findings.

I will conclude with a brief discussion of the problems associated with handling references when exploiting symmetry using generic representatives, a radically different method proposed for combining symmetry reduction with symbolic model checking.