线性时间逻辑“X”连接的自我引用状态的有效性

Question

让我们说我们有类似于上面的模型或者节点引用的类似型号。

现在让我们说如果我想知道公式的有效性：

$ m，s_2 \ models xr $

这将是有效的。在我的教科书中，它说：

$ \ pi \ models x \ phi $ iff $ \ pi ^ 2 \ models \ phi $

如果我们从状态2开始，那么我们的路径将是 $ s_2 - > s_2 - > ... $

所以，我不确定，因为州2实际上没有转换到像状态0或1.这样的另一个状态，否则将在路径中转换到path $ \ pi $中的相同状态足以满足“x”连接。

Answer 1

您的教科书正确地说明了

$ \ pi \ models x \ phi $ iff $ \ pi ^ 2 \ models \ phi $

在假设 $ \ pi $ 是转换系统的单词/轨迹，并且单词的字符以1开始编号。

所以你应该问的问题是如何从州 $ s_2 $ 的无限痕迹看起来像，然后评估该跟踪上的公式。 LTL仅在无限迹线上定义，因此这些是您应该看的。

请注意，检查是否

$ m，s_2 \ models xr $

保留没有意义（一般），因为LTL在迹线上定义，但从标记的转换系统中的状态，可以有多个迹线。因此，不清楚 $ m，s_2 \ models xr $ 应该意味着它意味着它意味着它在任何跟踪或每个痕迹？此语法似乎来自计算树逻辑（CTL）。