Пространственная сложность

Amazon AWS проверяет алгоритмы DynamoDB и S3 через TLA+ model checking. SPIN верифицирует протоколы NASA. Авиационные системы сертифицируются через model checking по DO-178C. Все эти инструменты работают с PSPACE-сложностью. Пространство - другое измерение сложности, часто важнее времени для верификации.

• **AWS TLA+ для DynamoDB:** группа Лесли Лэмпорта в Amazon использует TLA+ для верификации распределённых алгоритмов. TLA+ model checker TLC проверяет свойства безопасности и живости. Доклад Newcombe et al. (2015) описывает нахождение критических багов в S3 и DynamoDB
• **SPIN и NASA:** SPIN проверяет протоколы управления космическими аппаратами. Использовался для верификации систем Mars Pathfinder. Обнаружил расовые условия в коде реального времени
• **CPAchecker (BMW, Volkswagen):** model checker для C/C++ кода встроенных систем. Автоматически верифицирует свойства безопасности ECU (electronic control unit) в автомобилях
• **Binary Decision Diagrams (BDD):** компактное представление булевых функций. Intel и AMD используют BDD-based model checking для верификации схем процессоров. Позволяет работать с пространствами состояний размером 2^100

PSPACE и его мощь

**PSPACE** - класс задач, разрешимых МТ с полиномиальным пространством (памятью). NP ⊆ PSPACE: если алгоритм работает за poly time, он использует poly space. Но PSPACE может быть больше NP: существуют задачи, решаемые за poly space, но, возможно, не за poly time. Ключевой пример: TQBF (True Quantified Boolean Formula) PSPACE-complete.

**TQBF** (True Quantified Boolean Formula): дана формула с чередующимися кванторами ∀ и ∃ над булевыми переменными, является ли она истинной? Например: ∃x₁ ∀x₂ ∃x₃ (x₁ ∨ x₂ ∨ ¬x₃). TQBF PSPACE-complete: любая PSPACE-задача poly-сводится к TQBF. Без кванторов - это SAT (NP-complete).

**Почему PSPACE важнее NP для верификации?** Model checking проверяет, выполняется ли свойство во всех возможных состояниях системы. Это PSPACE-задача: нужно исследовать экспоненциальное пространство состояний, используя poly memory через depth-first search. NP-верификация требует свидетеля - PSPACE-верификация проверяет все возможные будущие состояния.

NL и логарифмическое пространство

**L** (LOGSPACE): задачи с O(log n) рабочего пространства (не считая входа). **NL** (NLOGSPACE): аналог для недетерминированной МТ. Классический пример: **Reachability** (достижимость в графе) ∈ NL. Задача «существует ли путь от s до t в ориентированном графе?» - в NL. Важная теорема: NL = co-NL (теорема Иммермана-Шлепегрелля, 1988).

Цепочка включений: **L ⊆ NL ⊆ P ⊆ NP ⊆ PSPACE ⊆ EXPTIME**. Все включения строгие (PSPACE ⊊ EXPTIME доказано). Остальные - открытые вопросы (в том числе P vs NP). NL = co-NL - редкий случай, когда пространственный класс симметричен. Для времени: P = co-P, но NP vs co-NP открытый вопрос.

Теорема Савича: NPSPACE = PSPACE

**Теорема Савича (1970):** NSPACE(f(n)) ⊆ DSPACE(f(n)²) для f(n) ≥ log n. Следствие: NPSPACE = PSPACE. Для пространства недетерминизм даёт только квадратичное ускорение - принципиально иначе чем для времени (NP vs P - потенциально экспоненциальная разница).

Теорема Савича объясняет, почему модель PSPACE естественна: недетерминизм не помогает при полиномиальном пространстве. **PSPACE = NPSPACE** - строгий результат (не предположение, как P vs NP). Это делает PSPACE удобным классом для анализа: детерминированный и недетерминированный poly-space эквивалентны.

PSPACE в верификации: model checking

**Model checking** - автоматическая верификация систем с конечным числом состояний. Проверяется, выполняется ли темпоральное свойство (LTL, CTL) во всех достижимых состояниях. LTL model checking - PSPACE-complete. CTL model checking - P. На практике: пространство состояний может быть 2^n (symbolic model checking через BDD).

**SPIN** (Bell Labs) и **NuSMV** - промышленные model checkers. Используются для верификации протоколов связи (TCP/IP, TLS handshake), железнодорожных систем управления, авиационного ПО. Ключевая техника - **symbolic model checking** через Binary Decision Diagrams (BDD): представление множества состояний в O(poly) памяти вместо явного перечисления.

Итоги

• **Иерархия:** L ⊆ NL ⊆ P ⊆ NP ⊆ PSPACE ⊆ EXPTIME. Только P ⊊ EXPTIME строго доказано
• **Теорема Савича:** NPSPACE = PSPACE. Для пространства недетерминизм не помогает (в отличие от P vs NP). Пространство можно переиспользовать
• **NL = co-NL:** симметрия пространственных классов (теорема Иммермана, 1988). NP = co-NP - открытый вопрос
• **Model checking:** LTL PSPACE-complete, CTL в P. SPIN, NuSMV, TLC - промышленные инструменты верификации

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

Пространственная сложность дополняет временную теорию:

• P vs NP — NP ⊆ PSPACE: пространство мощнее времени. PSPACE = NPSPACE строго доказано - ориентир для P vs NP
• Контекстно-зависимые языки — КЗ-языки = NLOGSPACE(n) = языки, распознаваемые LBA - связь грамматик и пространства
• Формальная верификация — Model checking - практическое применение PSPACE-алгоритмов для верификации программ

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

• PSPACE = NPSPACE строго доказано, а P = NP неизвестно. Что делает доказательство для пространства возможным, но не для времени?
• DFS использует O(n) пространства, BFS - O(n) пространства. Есть ли алгоритм поиска пути, использующий O(log n) пространства? (Подсказка: алгоритм Рейнголда)
• LTL model checking PSPACE-complete, но SPIN решает промышленные задачи. Какие свойства реальных протоколов делают это возможным?

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

• comp-04