logic - 线性时序逻辑 (LTL) 问题

Question

[] = 总是

O = 下一个

！= 否定

<> = 最终

---

想知道 []<> 是否等同于 []？

---

也很难理解如何分配时间逻辑。

1. [][] (a OR !b)

2. !<>(!a AND b)

3. []([] a ==> <> b)

Answer 1

我将使用以下符号：

F = 最终
G = 总是
X = 下一个
U = 直到

在我的模型检查课程中，我们通过以下方式定义 LTL：

零担：p | φ ∩ ψ | ¬φ | Xφ | φ U ψ

F 是 的语法糖：

F（未来）
Fφ = 真 U φ

和 G：

G（全局）
Gφ = ¬F¬φ

有了这个，你的问题是：

是不是真的：Gφ ?= GFφ

GFφ <=> G（真 U φ）

知道 ：

P ⊧ φ U ψ <=> 存在 i >= 0: P_(>= i) ⊧ ψ AND forall 0 <= j < i : P_(<= j) ⊧ φ

从中我们可以清楚地看到，GFφ 表示在某个时间 i 之后始终验证 φ 必须始终为真，而在此之前（j before i）必须验证真（平凡）。
但 Gφ 表明 φ 必须始终为真，“从现在到永远”而不是“从 i 到永远”。

Answer 2

G p表明 p 在任何时候都成立。GF p表明在任何时候，p最终都会成立。因此，虽然无限迹线 pppppp ... 满足这两个规范，但形式为p(!p)(!p!)p(!p)p ... 的无限迹线仅满足GF p但不满足G p。

需要明确的是，这两个示例轨迹都需要包含无限多个位置，其中p成立。但是在GF p的情况下，并且仅在这种情况下，可以接受介于两者之间的位置，其中p不成立。

因此，通过反例对上述问题的简短回答是：不，这两个规范不一样。