# Isomorph-free Model Enumeration

**Authors:**Daniel Jackson, Somesh Jha, and Craig A. Damon
Submitted for publication.

Download the PostScript.

## Abstract

Software specifications often involve data structures with huge numbers of
values, and consequently cannot be checked using standard state exploration
or model checking techniques. Data structures can be expressed with binary
relations, and operations over such structures can be expressed as formulae
involving relational variables. Checking properties such as preservation of
an invariant thus reduces to determining the validity of a formula, or,
equivalently, finding a model (of the formula's negation).
A new method for finding relational models is presented. It exploits the
permutation invariance of models-if two interpretations are isomorphic,
then neither is a model or both are-by partitioning the space into
equivalence classes of symmetrical interpretations. Representatives of
these classes are constructed incrementally by using the symmetry of the
partial interpretation to limit the enumeration of new relation values. The
notion of symmetry depends on the type structure of the formula; by picking
the weakest typing, larger equivalence classes (and thus fewer
representatives) are obtained. A more refined notion of symmetry that
exploits the meaning of the relational operators is also described.
The method typically leads to exponential reductions, often of 6 orders of
magnitude, making the automatic analysis of relational specifications
possible for the first time.

### Keywords:

model checking, symmetry, relational calculus, formal specification, Z.

Back to Nitpick Home Page