In model checking a symmetry reduction is a technique where rather than exploring every state, we explore one representative of each equivalence class of states. This is generally done by reducing every state we explore to the representative of their equivalence class and then continuing the search from there.

To make this specific, the most commonly used equivalence class is the node / participant ordering. Suppose we have a set of participants, labelled by an integer $1,\dots ,𝑁$. If our invariant only is on a per participant basis, then we can take every state, and generate the full equivalence class by working through every permutation of participant labels. The normal thing to do is to sort the equivalence class somehow (in the limit just the in-memory representation) and use the lowest element as the representative.

Diving into the theory a bit, a symmetry reduction $𝑔$ is only safe if:

• It preserves the initial state: $𝑠\in 𝐼\iff 𝑔\left(𝑠\right)\in 𝐼$
• It preserves transitions: $𝑠\to 𝑡\iff 𝑔\left(𝑠\right)\to 𝑔\left(𝑡\right)$
• It preserves labels (invariants): $𝐿\left(𝑠\right)=𝐿\left(𝑔\left(𝑠\right)\right)$