Count before tuning

For n jobs and four possible phases, the phase function alone has 4^n possible values. Two arbitrary subsets add 2^n choices each, so the crude Cartesian upper bound is 16^n. Guards make many combinations unreachable, but the arithmetic explains why one extra identity can cost far more than one extra state.

Record generated states, distinct states, graph depth, runtime, and peak memory for each deliberate model change. A faster run without a before/after claim is not evidence that the reduction was sound.

Four levers, four obligations

1. Abstraction maps several concrete values to one abstract value. Show that merged states admit matching relevant observations and steps.
2. Symmetry identifies states that differ only by a permutation of truly interchangeable atoms. Show that the initial predicate, actions, and property are invariant under that renaming.
3. Constraints declare some states outside the model. Justify them as an environmental assumption, never as mere acceleration.
4. Derived values remove redundant coordinates. Show that the removed value is a total function of retained state and is not independently changed.

Partial-order and refinement techniques can go further, but the governing question remains the same: which observations survive the transformation?

Under the hood: quotient, simulation, refusal

A symmetry reduction explores equivalence classes of states rather than every renaming. An abstraction usually needs a mapping from concrete to abstract states and a simulation argument: every relevant concrete step is represented by an admitted abstract step with the same observation. Neither argument is created by a smaller state count.

When that obligation is too expensive, keep the larger model or narrow the claim explicitly. “We checked a constrained model in which cancellation never occurs” is honest and weak. Calling the same run cancellation-safe is not.

Lessons

• Product structure explains exponential growth before any tool-specific tuning.
• A reduction is sound only relative to a named observation and property.
• Symmetry requires true interchangeability under behavior and the claim.
• Constraints are assumptions that narrow the model.
• Measurements report cost; simulation or equivalence arguments report meaning.

Practice

1. Retrieval. Name the four reduction levers and one obligation for each.
2. Discrimination. Can two jobs be symmetric if one alone has administrator authority used by the property?
3. Transfer. Simplify a replicated configuration model while preserving the observation “all replicas eventually agree on the chosen version.”

References

1. Leslie Lamport. Specifying Systems, Chapters 14–15. — TLC constraints, symmetry, and model-checking practice
2. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. — abstraction and state-space reduction