What is a (pseudocode) algorithm for checking invariant over Kripke structures, such that in case the invariant is violated, the counterexample returned by the algorithm is of minimal length?
You did not provide sufficient detail in the question, but if I had to guess, I would say you are looking for breadth-first search.