问线性时态逻辑问题(2)

EN

首先是一些术语：

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

格式良好的公式(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的(这看起来很接近，但并不相同，因为整个路径都是p的)。

困惑了吗？我是。

我认为

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

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

FGp应该意味着在随后的路径上有一个位置，从那时起，p总是站在那里。

我不确定，但可以证明GFGp和FGp是一样的

与GFp相同的FGFp。

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

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

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

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

现在<>[]<>p意味着最终p将无限频繁出现，这与p无限频繁出现完全相同，也就是<.[]<>p=[]<>p。

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