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?

Was it helpful?

Solution

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.

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top