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

Question

[] = всегда

O = следующий

! = отрицание

<> = в конце концов

---

Интересно, это []<> это эквивалентно просто []?

---

Также трудно понять, как распределить временную логику.

1. [] [] (ИЛИ! b)

2. !<> (! а и б)

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

Answer 1

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

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

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

LTL: p | φ ∩ ψ | ¬φ | Xφ | φ U ψ

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

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

и G:

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

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

Правда ли, что: Gφ? = GFφ

GFφ <=> G (True U φ)

Знаю это:

P ⊧ φ U = <=> существует i >= 0: P_(>= i) ψ ψ И, наконец, 0 <= j

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

Answer 2

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

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

Таким образом, короткий ответ на контрпример: "Нет, эти две спецификации не совпадают.