For model checking we have a model and we prove invariants about that model by generating every state and explicitly checking the invariant on that state.
From a theory perspective model checking is a constructive proof that an invariant holds on all states. Ie we have a model which goes through a series of steps, and if we have a proof that is something like βfor state A the invariant holds, as well as state B, and C andβ¦, and there are no other statesβ then that candidate invariant is true of the entire system.
We can reduce this work by using a symmetry reduction.
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 . 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:
So we only have to check one representative from each equivalence class.
We can also reduce that work by instead finding an inductive invariant and checking that.
Suppose that we have an infinite model. In that case exploration is not feasible. Instead we can find an inductive invariant, prove that it is inductive, then prove that it proves our invariants.
For example suppose we want to prove Inv. Then we discover some other invariant SysInv and show:
SysInv holds for all InitSysInv holds for all NextSysInv proves InvMy claim is that finding an inductive invariant is simply reducing the system to a single equivalence class that we then check. The obvious issue being that the inductive invariant for things like Raft is not concrete, and often relies on ghost variables for commit evidence etc.
This leads to the following points.
| Reduction | Cost | |
|---|---|---|
| No reduction | None | Free |
| Id permutations | Slight | Cheap |
| Finitisation | Substantial | Expensive |
| β¦ | β¦ | β¦ |
| Inductive Invariant | Complete | Uncomputable |
The question then is: What is the minimum number of states necessary to check to satisfy the inductive invariant? Or: Can we constructively go from a spec and the invariants, directly to the best possible computable symmetry reduction?