Abstract model checking

So, the design undergoes a kind of translation to scaled down "abstract" version.

The set of variables are partitioned into visible and invisible depending on their change of values.

The real state space is summarized into a smaller set of the visible ones.

The real and the abstract state spaces are Galois connected.

On the other hand, if you pick an element from the real space, abstract it and concretize the abstract version, the final result will be a super set of the original.