[] = всегдаLinear Temporal Logic (LTL) вопросы
O = следующая
! = Отрицание
<> = в конце концов
Удивление это [] <> является то, что эквивалентно просто []?
Также трудно понять, как распределить временную логику.
[] [] (а ИЛИ! Б)
! <>
[] ([] A ==> <> б)
Я буду использовать следующие обозначения (а и б!):
F = в конце концов, не
G = всегда
X = следующая
U = до
В моей модели проверки, конечно, мы определили Лт следующим образом:
LTL: р | φ ∩ ψ | ¬φ | Xφ | φ U ф
С F будучи синтаксически:
F (будущего)
F^= True U Ф
и G:
G (глобальный)
Gφ = ¬F¬φ
При том, что ваш вопрос:
Верно ли, что: Сф?= GFφ
GFφ < => G (Правда U φ)
Зная, что:
P ⊧ ф U ф < => существует я> = 0: P _ (> = я) ⊧ ψ И FORALL 0 < = J < я: Р- (< = J) ⊧ ф
того, мы можем ясно видеть, что GFφ указывает на то, что она всегда должна быть Tru e, что φ будет всегда проверяться через некоторое время i, а до этого (j перед i) True должно быть проверено (тривиально).
Но Gφ указывает, что φ всегда должно быть истинным, «отныне навсегда», а не «от i до бесконечности».
Gр показывает, что во все времена р держит. GFp указывает, что в любое время, в конечном итоге p будет храниться. Таким образом, в то время как бесконечный след pppppp ... удовлетворяет обе спецификации, бесконечный след формы р (! Р) (! Р!) Р (! Р) р ... удовлетворяет только GFp, но не Gp.
Чтобы быть ясным, оба этих примера трасс должны содержать бесконечно много мест, где находится p. Но в случае GFp, и только в этом случае допустимо, что между ними находятся места, где p не поддерживается.
Таким образом, короткий ответ на вышеуказанный вопрос по контрпримеру: нет, эти две спецификации не совпадают.