Темпоральная логика

Программа работает сейчас. Но будет ли она работать через час? Через год? Не зависнет ли? Классическая логика описывает статичные факты. Но программы - динамические системы. Темпоральная логика позволяет доказывать: «это свойство будет выполняться всегда».

• **Верификация протоколов**: доказательство отсутствия deadlock в распределённых системах (Amazon, NASA)
• **Смарт-контракты**: формальная проверка, что контракт никогда не заблокирует средства
• **Медицинские устройства**: доказательство, что кардиостимулятор всегда отреагирует на аритмию

Темпоральная логика

**Темпоральная логика** - раздел модальной логики, формализующий рассуждения о **времени**. Вместо «необходимо» и «возможно» здесь операторы «всегда», «когда-нибудь», «до тех пор пока».

Темпоральная логика - основа **верификации программ**. Model checking (Нобелевская премия Тьюринга 2007) использует её для доказательства корректности систем.

Зачем нужна логика времени? Многие свойства систем невозможно выразить без неё:

Существуют два основных вида темпоральной логики: **LTL** (Linear Temporal Logic) - время как линейная последовательность, и **CTL** (Computation Tree Logic) - время как дерево возможностей.

Оператор [] (Always / Globally)

Оператор **□φ** (читается «box φ» или «globally φ», в LTL обозначается **G**) означает: φ **истинно сейчас и во все будущие моменты времени**.

**Safety properties** (свойства безопасности) выражаются через □: «плохое никогда не произойдёт». Пример: □¬crash - «система никогда не упадёт».

Связь с модальной логикой: □ в темпоральной логике похож на □ (необходимость), но интерпретируется как «во всех будущих состояниях», а не «во всех возможных мирах».

Оператор <> (Eventually / Finally)

Оператор **◇φ** (читается «diamond φ» или «eventually φ», в LTL обозначается **F**) означает: φ **станет истинным когда-нибудь в будущем** (включая настоящий момент).

Связь между □ и ◇ - двойственность, как у ∀ и ∃:

**Liveness properties** (свойства живости) выражаются через ◇: «хорошее когда-нибудь произойдёт». Пример: ◇terminated - «программа когда-нибудь завершится».

Оператор U (Until)

Оператор **φ U ψ** («φ until ψ») означает: φ **остаётся истинным до тех пор, пока не станет истинным ψ**, и ψ обязательно станет истинным.

Важно: в **strong until** (φ U ψ) ψ обязательно должен наступить. Есть также **weak until** (φ W ψ), где ψ может не наступить - тогда φ остаётся истинным навсегда.

U - самый мощный оператор LTL. Он позволяет выразить **последовательность событий**: «сначала A, потом B». Без него можно говорить только «когда-нибудь», но не «в правильном порядке».

Полная система операторов

LTL включает операторы для **прошлого** и **будущего**, а также **next** (X) - «в следующий момент». CTL добавляет кванторы по путям.

CTL (Computation Tree Logic) добавляет кванторы по путям:

**Model checking**: алгоритмы автоматически проверяют, удовлетворяет ли система (конечный автомат) темпоральной формуле. NuSMV, SPIN, UPPAAL - инструменты верификации.

Применения: верификация протоколов, контроллеров, смарт-контрактов, медицинских устройств - везде, где ошибка критична.

Ключевые идеи

• **□φ (Always)** — φ истинно сейчас и во всех будущих состояниях. Выражает safety properties
• **◇φ (Eventually)** — φ станет истинным когда-нибудь. Выражает liveness properties
• **φ U ψ (Until)** — φ держится до ψ, и ψ обязательно наступит. Базовый оператор LTL
• **LTL vs CTL**: линейное время (один путь) vs ветвящееся время (дерево путей с кванторами A/E)

Связанные темы

Темпоральная логика - часть семейства модальных логик:

• Модальная логика — Темпоральные операторы - интерпретация модальных в терминах времени
• Деонтическая логика — Комбинация: «обязательство выполнить когда-нибудь» - ◇Oφ

Вопросы для размышления

• Можно ли выразить «бесконечно часто» через □ и ◇? (Подсказка: □◇φ)
• В чём практическая разница между «φ U ψ» и «φ W ψ»? Когда важно, чтобы ψ обязательно наступил?
• Почему модельная проверка (model checking) возможна для конечных автоматов, но затруднена для бесконечных систем?

Связанные уроки

• fl-05-regex