automata-theory - 线性时间逻辑问题(2)

Question

如果您不熟悉 LTL(线性时序逻辑)，请跳过此问题!是的，LTL 对编程非常重要，因为它是我们用来验证程序的模型检查系统的核心。

鉴于这些命题符号及其含义...
Gp - 总是 P
Fp - 有时 P

下面的语句是什么意思？

GFGp = ?  
FGFp = ?

我很难理解 LTL 的逻辑，无法理解上述陈述，感谢您的帮助!

Answer 1

首先是一些术语:

合式公式是逻辑上满足所有组合规则的句子。通常对此有一个归纳定义，大意是原子命题是格式正确的公式，以下也是:

良构公式 (WFF) 与(替换通常的逻辑符号...)&&、||、! 和 => 的组合也是良构公式。这都是标准的 FOL。 (Linear) Temporal Logic 添加了更多的组合可能性，因此 F(WFF)、G(WFF) 和 X(WFF) 本身就是合式公式。

由于 F(WFF) 本身可以是合式公式，我们可以将 F(F(WFF) 作为合式公式，G(F(F(WFF) 和许多其他奇异的公式也可以看起来聚集。但它们是什么意思？

就我个人而言，对于复杂的公式，我觉得用命题集来思考是很有用的，其中G指的是一组命题，F指的是一个命题。正如您提到的，给定某个当前节点，Fp 意味着 p 将出现在该节点的至少一个后继者中，而 Gp 意味着 p 将出现在当前节点的所有后继者中。

那么，GFp 表示每个状态(在这个状态之后)至少有一个后继状态，其中 p 出现。因此，p 保证在每次操作后发生(在将来的某个时间)。

FGp 表示至少有一个状态(在这个状态之后)其完整的后继集合是p。所以在这个过程中有一个点是 p 之后。

进一步FGFp 说在某个点之后GFp 成立。同样，GFp 要求每个操作都遵循(至少一次)p，所以整个事情大致意味着将来某个时候我们会得到 p 来自所有的东西(当然，这可能意味着它是从那一点开始的所有 p 或者 p 只是最后一个状态)。

GFGp 表示每个状态的后继都是FGp。我想这意味着路径中的每个点都有一些后继状态，其后代都是 p 的(这看起来很接近，但并不相同，因为整个路径是 p)。

还在迷茫吗？我是。