【发布时间】：2013-01-23 01:57:05
【问题描述】：
什么是用于检查 Kripke 结构的不变量的（伪代码）算法，以便在违反不变量的情况下，该算法返回的反例具有最小长度？
【问题讨论】：
-
你的 kripke 结构是如何表示的？它是一个明确的图表吗？一个BDD？一组CNF公式？每一个都会有不同的答案。
-
我对 Kripke 结构很熟悉，但是虽然结构被抽象为图 - 但在实践中很少以这种方式实现。它通常被实现为 BDD，甚至更常见的是一组 CNF 公式。
-
你知道如何确定 DSP 在 Kripke 结构上的时间复杂度，以检测是否违反了时间属性 f：/ 就大小 M（状态空间中的状态数）和f(公式中使用的原子命题数)
标签： algorithm logic automata temporal model-checking