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

Question

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

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

以下陈述是什么意思？

GFGp = ?  
FGFp = ?

我很难理解围绕 LTL 的逻辑，并且无法理解上述陈述，感谢您的帮助！

Answer 1

首先是一些术语：

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

格式正确的公式 (WFF) 与（替换通常的逻辑符号...）&&、||、! 和 => 的组合也是格式正确的公式。这都是标准的 FOL。（线性）时序逻辑增加了更多的组合可能性，因此 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's （这似乎接近，但不一样，因为整个路径都是p's）。

迷茫了吗？我是。

Answer 2

我觉得

Fp 意味着 P 将最终保持（在后续路径上的某处）。

因此，GFp 应该意味着 p 将保持在后续路径上的某个位置，无论您在路径中的哪个位置“站立”。或者，换句话说，p 将保持在路径的无限后续位置。

FGp 应该意味着在随后的路径上有一个地方 p 从那时起总是站立。

我不确定，但可以证明 GFGp 与 FGp 相同

FGFp 与 GFp 相同。

Answer 3

为了使事情更容易理解，我将使用另一种表示法：

G = globally = [] = always
F = finally = <> = eventually

所以 []<>p 意味着 p 无限频繁地出现，即它永远不会停止出现。例如**p ******* p*****p***p***...

公式 <>[]p 表示序列中有某个位置，之后只有 p 不间断地出现。例如 ***pppp...

现在<>[]<>p 表示最终p 将无限频繁出现，这与p 无限频繁出现完全相同，即<.[]<>p=[]<>p。

类似地，[]<>[]p 意味着从任何时间点开始，最终总是 p。但这正是说最终是 p，所以 []<>[]p=<>[]p。

Answer 4

GFGp = FGp 例子：所有的狗最终都会去天堂，总有一天会永远呆在那里

FGFp = GFp ：迟早所有的狗都会去天堂（如果它们在地球上下降/重生等，它们将再次去避风港）。