Вопросы линейной временной логики (LTL)

Я буду использовать следующие обозначения:

F = когда-нибудь
G = всегда
X = следующий
U = пока

В моем курсе по проверке моделей мы определили LTL следующим образом:

ЛТЛ: п | φ ∩ ψ | ¬φ | Хф | φ U ψ

Где F является синтаксическим сахаром для:

F (будущее)
Fφ = True U φ

и Г:

G (глобальный)
Gφ = ¬F¬φ

При этом ваш вопрос:

Верно ли, что : Gφ ?= GFφ

GFφ ‹=› G (Истинно U φ)

Знаю это :

P ⊧ φ U ψ ‹=› существует i ›= 0: P_(›= i) ⊧ ψ И для всех 0 ‹= j ‹ i : P_(‹= j) ⊧ φ

Из этого мы можем ясно видеть, что GFφ указывает, что всегда должно быть истинным, что φ всегда будет проверено через некоторое время i, а до этого (j до i) True должно быть проверено (тривиально).
Но Gφ указывает, что φ всегда должно быть истинным, отныне и навсегда, а не от i до вечности.

G p указывает, что всегда выполняется p. GF p указывает, что всегда, в конце концов, p будет сохраняться. Таким образом, хотя бесконечная трассировка pppppp... удовлетворяет обеим спецификациям, бесконечная трассировка вида p(!p)(!p!)p(!p)p... удовлетворяет только GF p, но не G p.

Чтобы было ясно, обе эти примерные трассировки должны содержать бесконечно много местоположений, где выполняется p. Но в случае GF p и только в этом случае допустимо наличие промежуточных положений, где p не выполняется. .

Итак, краткий ответ на поставленный выше вопрос с помощью контрпримера: нет, эти две спецификации не совпадают.