Модальная логика

1977: Амир Пнюэли публикует работу о темпоральной логике. Вопрос: как доказать, что программа НИКОГДА не зайдёт в дедлок? Классическая логика не справляется - в ней нет понятия "всегда" и "когда-нибудь". Классическая логика видит снимок: истинно или ложно сейчас. Темпоральная логика видит фильм: что происходит на каждом шаге бесконечного выполнения. За это Пнюэли получит премию Тьюринга в 1996 году.

• **Верификация протоколов:** NASA использует model checking (SPIN, LTL) для верификации бортового ПО - ошибки в протоколах связи стоят миссий, а не просто времени разработчика.
• **Аппаратная верификация:** После ошибки FDIV в Pentium (1994, $475 млн убытков) Intel перешёл на формальную верификацию процессорных блоков с помощью CTL model checking.
• **Эпистемическая логика в криптографии:** Протоколы безопасности (TLS, Kerberos) формально верифицируются через логику знания - что знает атакующий, что знает сервер, какие миры доступны каждому агенту.

Предварительные знания

• Пропозициональная логика - операторы AND, OR, NOT, импликация
• Предикатная логика - кванторы, формулы, интерпретации
• Теория моделей - понятие структуры, истинность формулы в модели (ml-11)

• Теория моделей: структуры, истинность, теорема полноты Гёделя

Оператор необходимости []

Классическая логика описывает, что **есть** - истинно или ложно. Модальная логика описывает, что **должно быть** или **могло бы быть**. Оператор **необходимости** [] (читается "box" или "квадрат"): []phi означает "phi истинно во всех возможных мирах, доступных из текущего". Если phi - закон природы, то []phi; если phi - случайный факт, то phi может быть истинно, но []phi - нет.

**Аксиома K** (минимальная система): [](p -> q) -> ([]p -> []q). Необходимость дистрибутивна по импликации: если необходимо, что p влечёт q, и необходимо p, то необходимо q. Все расширения модальной логики содержат K как базу.

В системе **S5** необходимость совпадает с истинностью во всех мирах без ограничений: []p <-> p истинно во всех мирах. Математические теоремы - необходимо истинны в S5: в любом возможном мире 2+2=4. Случайный факт "Наполеон проиграл при Ватерлоо" - истинен в нашем мире, но не в каждом возможном.

**История:** Модальная логика восходит к Аристотелю. C.I. Льюис ввёл первую современную систему строгой импликации в "A Survey of Symbolic Logic" (1918), а семейство S1-S5 формализовал вместе с Лангфордом в "Symbolic Logic" (1932). Современная семантика возможных миров дана Солом Крипке в 1959-1963 годах - см. следующий концепт.

Оператор возможности <> и двойственность

Оператор **возможности** <> (читается "diamond" или "ромб"): <>phi означает "phi истинно хотя бы в одном возможном мире, доступном из текущего". Формально: <>phi = -[]-phi. Возможность - это двойник необходимости, как существование - двойник всеобщности в логике предикатов.

**Двойственность Box и Diamond:** - []phi <-> -<>-phi (необходимость = невозможность отрицания) - <>phi <-> -[]-phi (возможность = не-необходимость отрицания) Аналогия: (для всех x) <-> (не существует x, что не), то есть всеобщность и существование - двойники.

**Эпистемическая логика** (Jaakko Hintikka, "Knowledge and Belief", 1962) - первое систематическое применение семантики возможных миров к знанию. []_i phi читается "агент i знает phi". Аксиома знания: []_i phi -> phi (нельзя знать ложь). Эта система оказалась фундаментом для теории игр, криптографии и верификации протоколов.

**Деонтическая логика** (логика обязательства): []phi = "phi обязательно", <>phi = "phi разрешено". Применяется в юридических системах и этике. Парадокс Росса (Ross 1941): из "отправь письмо" выводится "отправь письмо или сожги его" - проблема для стандартной деонтической логики, предмет активных исследований.

Семантика Крипке и возможные миры

В 1959 году 18-летний Саул Крипке опубликовал статью с полной семантикой для модальной логики. **Крипке-структура** (или Крипке-фрейм) - это тройка (W, R, V), где W - непустое множество возможных миров, R ⊆ W x W - отношение доступности ("из мира w доступен мир v"), V: Prop x W -> {true, false} - функция оценки атомарных формул.

**Соответствие аксиом и свойств отношения R:** - Аксиома T: []p -> p <-> R рефлексивно (каждый мир доступен из себя) - Аксиома 4: []p -> [][]p <-> R транзитивно - Аксиома B: p -> []<>p <-> R симметрично - Аксиома 5: <>p -> []<>p <-> R евклидово (из wRv и wRu следует vRu) S5 = K + T + 4 + 5 <-> R является отношением эквивалентности (рефл. + симм. + транз.)

Это соответствие - главный результат Крипке: **теорема о полноте** для каждой стандартной системы. Например, формула phi общезначима в S4 (истинна в любом рефлексивном и транзитивном фрейме) тогда и только тогда, когда phi выводима в аксиоматике S4. Это связывает синтаксис (вывод) и семантику (истинность в структурах).

**Применения семантики Крипке:** логика доказуемости GL (Лёб, 1955; Крипке-семантика через конечные частичные порядки), интуиционистская логика (фреймы - частичные порядки, монотонная оценка), логики знания в многоагентных системах (каждый агент имеет своё отношение доступности R_i).

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

В 1977 году Амир Пнюэли предложил **линейную темпоральную логику (LTL)** для рассуждений о поведении реактивных систем во времени. LTL расширяет пропозициональную логику четырьмя операторами: **X** (next - на следующем шаге), **F** (finally/eventually - когда-нибудь), **G** (globally/always - всегда), **U** (until - до тех пор пока).

**CTL (Computation Tree Logic)** предложена Кларком и Эмерсоном в 1981 году. В отличие от LTL (линейное время - фиксированный путь), CTL работает с **деревом вычислений** - все возможные пути из текущего состояния. CTL добавляет кванторы по путям: **A** (all paths) и **E** (exists a path). Операторы пишутся парами: AG, AF, EG, EF, AX, EX, AU, EU.

**Премия Тьюринга 2007:** Эдмунд Кларк, Аллен Эмерсон и Жозеф Сифакис получили её за создание **model checking** - автоматической верификации конечных систем. Инструменты: SPIN (LTL, Bell Labs), NuSMV (CTL+LTL), PRISM (вероятностный MC). Intel использует model checking для верификации аппаратных протоколов с 1990-х - после ошибки в Pentium FDIV (1994), стоившей компании 475 млн долларов.

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

• **Модальные операторы:** [] (необходимо - во всех доступных мирах) и <> (возможно - хотя бы в одном). Они двойственны: <>phi = -[]-phi. Разные аксиомы (K, T, 4, B, 5) дают системы K, T, S4, S5 с разными свойствами отношения доступности.
• **Семантика Крипке (1963):** Фрейм (W, R, V) - множество миров, отношение доступности, оценка атомов. Аксиомы соответствуют свойствам R: T <-> рефлексивность, 4 <-> транзитивность, S5 <-> R является отношением эквивалентности.
• **LTL vs CTL:** LTL рассуждает о поведении на линейных путях (G, F, X, U), CTL квантифицирует по путям в дереве вычислений (AG, EF, ...). Они несравнимы по выразительности. Model checking - автоматическая верификация: CTL за O(|S|*|phi|), LTL - PSPACE.

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

Модальная логика пронизывает и математику, и computer science:

• Теория моделей и теорема полноты — Семантика Крипке - частный случай общей теории моделей; теорема полноты Крипке аналогична теореме Гёделя
• Алгоритмы и верификация — Model checking - алгоритмическая задача на графах: обход дерева состояний, проверка LTL/CTL свойств

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

• Если свобода воли принимается за истину, какая модальная система лучше её описывает - S4 (вложенная необходимость) или S5 (все миры равнодоступны)? Почему детерминизм соответствовал бы системе с пустым отношением доступности?
• Аксиома знания: []_i phi -> phi (нельзя знать ложь). Что случится с логикой, если заменить знание на веру (belief)? Какую аксиому придётся убрать, и как это меняет структуру фреймов?
• Свойство liveness в LTL: AF phi (рано или поздно phi). Почему его сложнее проверить, чем safety (AG -bad)? Как связана эта сложность с понятием справедливости (fairness) в планировании процессов?

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

• fl-01-intro