線性時態邏輯問題

Question

我知道CTL是可能的。但有沒有可能說

「有可能從某個點開始p總是成立」。

使用LTL。

Answer 1

FGp意味着至少有一個狀態（在此之後），其完整的後繼是p。所以這個過程中有一點是p從來沒有過的。

其中Fp表示P將最終保持（在隨後的路徑上的某處）。 Gp表示p將出現在當前節點的所有後繼中。