2

基本上，模型检查处理模型“m”（系统的行为描述）和系统应满足的属性“p”。对于这两个工件，模型检查器确定模型是否满足属性。

我的问题是是否可以将模型“m”指定为 LTL 公式并检查模型作为 LTL“m”是否满足属性“p”。

从理论上讲，我相信这种方法应该有效，因为我们可以生成两个 Büchi 自动机，一个用于 LTL 公式“p”，另一个用于描述模型“m”的 LTL 属性。如果两个非确定性自动机的交集为空，则作为 LTL 的模型“m”满足该性质。

有人可以给我一个提示吗？可能吗？

4

1 回答 1

1

有趣的问题：简短的回答可能是否定的。

https://en.wikipedia.org/wiki/Linear_temporal_logic_to_B%C3%BCchi_automaton

通常在模型检查期间，执行 LTL 到 Buchi Automata 的转换。这是可能的，因为 LTL 的表现力远不如 Buchi Automata。但是，如果您有一些预先存在的设计，则不太可能能够在 LTL 中捕获它。例如，当设计有很多很多状态时，LTL 可能会出现问题。

于 2015-02-05T00:09:12.690 回答