algorithm - 克里普克结构

Question

什么是用于检查 Kripke 结构上的不变量的（伪代码）算法，以便在违反不变量的情况下，算法返回的反例具有最小长度？

Answer 1

您没有在问题中提供足够的详细信息，但如果我不得不猜测，我会说您正在寻找广度优先搜索。