Kripke structure

Question

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?

Answer 1

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.