Временная логика линейного времени (LTL) в Spin

Формулы темпоральной или временной логики линейного времени (Linear Temporal Logic) используются в качестве спецификаций (ограничений, требований) модели на языке Promela.

Каждая такая формула может состоять из имен глобальных (и даже локальных — специальный синтаксис <имя-процесса>[<номер-процесса>]:<имя-переменной>) переменных, соединенных логическими связками логики нулевого порядка и операторами LTL.

Темпоральные операторы LTL в Spin

Формулы LTL строятся с использованием темпоральных операторов, которые описывают поведение переменных во времени — то, как значения должны изменяться или оставаться неизменными на разных шагах симуляции.

В таблице ниже приведены основные операторы LTL, поддерживаемые инструментом Spin.

Графические обозначения (используются в литературе по LTL) Короткие обозначения операторов в Spin Альтернативные обозначения операторов в Spin Описания операторов

Графические обозначения (используются в литературе по LTL)	Короткие обозначения операторов в Spin	Альтернативные обозначения операторов в Spin	Описания операторов
□ или G	`[]`	`always`	Формула `□φ` читается, как «всегда истинна формула φ» или «формула φ истинна глобально». Это означает, что `φ` обязана быть истинной на каждом шаге симуляции модели: начальном, текущем и всех будущих.
◊ или F	`<>`	`eventually`	Формула `◊φ` читается, как «формула φ когда-нибудь станет истинной». Это означает, что `φ` обязана оказаться истинной хотя бы один раз — либо на текущем шаге, либо когда-нибудь в будущем.
∪ или U	`U`	`until` или `stronguntil`	Формула `φ U ψ` читается, как «формула φ истинна до тех пор, пока однажды формула ψ не станет истинной». Это значит, что `ψ` должна стать истинной либо на текущем шаге, либо в будущем; до этого `φ` обязана быть истинной.
W	`W`	`weakuntil`	Формула `φ W ψ` читается, как «формула φ обязана оставаться истинной до тех пор, пока формула ψ ложна». Это то же, что и `φ U ψ`, но `ψ` не обязана становиться истинной (тогда `φ` должно выполняться всегда): `φ W ψ = (φ U ψ) ∨ □φ`.
R	`V`	`release`	Формула `φ V ψ` читается, как «формула φ освобождает формулу ψ». Формула `V` двойственна формуле until (`U`): `¬(φ U ψ) = ¬φ V ¬ψ`. Смысл `φ V ψ`: `ψ` должна оставаться истинной либо всегда, либо до момента (включая его), когда `φ` станет истинной.
◯	`X`	`next`	Формула `◯φ` читается, как «на следующем шаге формула φ станет истинной».

□ или G

[]

always

Формула □φ читается, как «всегда истинна формула φ» или «формула φ истинна глобально». Это означает, что φ обязана быть истинной на каждом шаге симуляции модели: начальном, текущем и всех будущих.

◊ или F

<>

eventually

Формула ◊φ читается, как «формула φ когда-нибудь станет истинной». Это означает, что φ обязана оказаться истинной хотя бы один раз — либо на текущем шаге, либо когда-нибудь в будущем.

∪ или U

U

until или stronguntil

Формула φ U ψ читается, как «формула φ истинна до тех пор, пока однажды формула ψ не станет истинной». Это значит, что ψ должна стать истинной либо на текущем шаге, либо в будущем; до этого φ обязана быть истинной.

W

weakuntil

Формула φ W ψ читается, как «формула φ обязана оставаться истинной до тех пор, пока формула ψ ложна». Это то же, что и φ U ψ, но ψ не обязана становиться истинной (тогда φ должно выполняться всегда): φ W ψ = (φ U ψ) ∨ □φ.

V

release

Формула φ V ψ читается, как «формула φ освобождает формулу ψ». Формула V двойственна формуле until (U): ¬(φ U ψ) = ¬φ V ¬ψ. Смысл φ V ψ: ψ должна оставаться истинной либо всегда, либо до момента (включая его), когда φ станет истинной.

◯

X

next

Формула ◯φ читается, как «на следующем шаге формула φ станет истинной».

Обозначения логических связок, допустимых в LTL Spin

Помимо темпоральных операторов, в формулах LTL используются обычные логические связки — отрицание, конъюнкция, дизъюнкция и другие.

В таблице ниже приведены их обозначения в Spin и в литературе по LTL.

Графическое обозначение (в литературе) Короткое обозначение в Spin Альтернативное обозначение в Spin Описание

Графическое обозначение (в литературе)	Короткое обозначение в Spin	Альтернативное обозначение в Spin	Описание
¬	`!`		Отрицание.
∧	`&&`	`/\`	Конъюнкция (логическое «И»).
∨	`\|\|`	`\/`	Дизъюнкция (логическое «ИЛИ»).
⨁	`^`		Исключающее «ИЛИ» (XOR).
⟹	`→`	`implies`	Импликация («если …, то …»).
⟺	`<→`	`equivalent`	Эквивалентность («тогда и только тогда»). Формула `φ ⟺ ψ` эквивалентна `(φ ⟹ ψ) ∧ (ψ ⟹ φ)`.

!

Отрицание.

∧

&&

/\

Конъюнкция (логическое «И»).

∨

||

\/

Дизъюнкция (логическое «ИЛИ»).

⨁

^

Исключающее «ИЛИ» (XOR).

⟹

→

implies

Импликация («если …, то …»).

⟺

<→

equivalent

Эквивалентность («тогда и только тогда»). Формула φ ⟺ ψ эквивалентна (φ ⟹ ψ) ∧ (ψ ⟹ φ).

Временная логика линейного времени (LTL) в Spin

Темпоральные операторы LTL в Spin

Обозначения логических связок, допустимых в LTL Spin

Полезные ссылки