Формально верифицированная сертификация неразрешимости задач временного планирования

Основная информация

• ID статьи: 2510.10189
• Название: Formally Verified Certification of Unsolvability of Temporal Planning Problems
• Авторы: David Wang, Mohammad Abdulaziz (King's College London, United Kingdom)
• Классификация: cs.LO (Логика в информатике), cs.AI (Искусственный интеллект)
• Дата публикации: 11 октября 2025 г. (препринт arXiv)
• Ссылка на статью: https://arxiv.org/abs/2510.10189

Аннотация

В данной работе предложен метод сертификации неразрешимости задач временного планирования. Метод основан на кодировании задач планирования в виде сетей временных автоматов, последующем использовании эффективного проверяющего модели и применении проверяющего сертификаты для верификации выходных данных проверяющего модели. Метод приоритизирует надежность сертификации: используется формальная верификация реализации кодирования временных автоматов в доказывающей системе Isabelle/HOL, а также существующий проверяющий сертификаты (также формально верифицированный в Isabelle/HOL) для верификации результатов проверки модели.

Исследовательский контекст и мотивация

Основная проблема

Основная проблема, решаемая в данном исследовании, — сертификация неразрешимости задач временного планирования. Временное планирование — это богатая форма планирования, позволяющая действиям иметь длительность и выполняться параллельно, что значительно сложнее классического планирования.

Важность проблемы

1. Требования к надежности: Существующие системы планирования чрезвычайно сложны на алгоритмическом и реализационном уровнях, поэтому повышение надежности их выходных данных критически важно
2. Сложность сертификации: В отличие от разрешимых задач (которые можно проверить путем выполнения плана), утверждения о неразрешимости или оптимальности трудно получить в виде компактных сертификатов
3. Экспоненциальная сложность: В худшем случае такие сертификаты могут иметь экспоненциальный размер относительно размера задачи планирования

Ограничения существующих методов

1. Отсутствие формальных гарантий: Существующие методы обнаружения неразрешимости временного планирования не имеют формальных гарантий корректности
2. Высокая сложность: Современные методы временного планирования отличаются высокой технической сложностью, что затрудняет разработку практических схем сертификации неразрешимости
3. Пробел в верификации: В отличие от классического планирования, в области временного планирования существует пробел в работах по формальной верификации

Исследовательская мотивация

В работе используется подход трансформации кодирования: задачи временного планирования кодируются в другие вычислительные задачи, для которых уже существуют практические алгоритмы сертификации (временные автоматы), а весь процесс кодирования и проверяющий сертификаты верифицируются в доказывающей системе для обеспечения надежности сертификации.

Основные вклады

1. Формально верифицированный метод кодирования: Впервые проведена формальная верификация кодирования временного планирования в временные автоматы, предложенного Heinz и др.
2. Инженерная реализация: Адаптация кодирования для создания временных автоматов, совместимых с системой Wimmer и von Mutius
3. Упрощенная семантика: Разработана более простая семантика временного планирования, удобная для математических рассуждений, с доказательством эквивалентности существующей семантике
4. Полная структура сертификации: Построена полная цепь доверия от задач временного планирования к проверке модели временных автоматов
5. Теоретические гарантии корректности: Доказана корректность кодирования в Isabelle/HOL, обеспечивающая надежные теоретические гарантии

Подробное описание метода

Определение задачи

Входные данные: Задача временного планирования P = ⟨P, A, I, G⟩

• P: множество пропозиций
• A: множество действий с длительностью
• I: начальное состояние
• G: целевые условия

Выходные данные: Формальный сертификат неразрешимости (если задача действительно неразрешима)

Ограничения:

• Действия имеют начальные и конечные моментальные действия
• Поддерживаются инвариантные условия и ограничения расписания
• Соблюдаются ограничения взаимного исключения и границы длительности

Архитектура модели

1. Формализация временного планирования

Сначала определяется формальная семантика временного планирования:

Моментальные действия (Определение 1):

h ≡ ⟨pre(h), adds(h), dels(h)⟩

Действия с длительностью (Определение 2):

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

где a⊢ и a⊣ — начальное и конечное моментальные действия соответственно.

2. Кодирование временных автоматов

Проектирование переменных (Определение 24):

• Для каждой пропозиции p: двоичная переменная vp (кодирующая истинностное значение) и счетчик блокировок lp (отслеживающий активные действия, требующие p быть истинной)
• aa: количество активных действий
• ps: состояние планирования (0=не начато, 1=в процессе, 2=завершено)

Проектирование часов (Определение 25):

• Каждому действию a назначены два часа: ca⊢ (отслеживающие время после начала) и ca⊣ (отслеживающие время после завершения)

Главный автомат (Определение 26): Управляет переходами состояний всего процесса планирования, включая инициализацию и проверку целей.

Автоматы действий (Определение 27): Каждому действию соответствует автомат, содержащий следующие ключевые переходы:

• sea: применение эффектов начального действия
• se'a: блокировка инвариантных условий
• eea: подготовка перед завершением
• ee'a: применение эффектов конечного действия
• iea: обработка моментальных действий

3. Построение сети

Главный автомат и все автоматы действий объединяются в сеть временных автоматов (Определение 28), начальная конфигурация устанавливает все автоматы в неактивное состояние.

Технические инновации

1. Поддержка параллельного выполнения: В отличие от использования глобальных блокировок у Heinz и др., в работе используются ограничения на часы, позволяющие параллельное выполнение моментальных действий
2. Обработка моментальных действий: Поддержка действий нулевой длительности через добавление переходов iea
3. Формальная верификация: Впервые предоставлены проверяемые машиной доказательства корректности для такого типа кодирования
4. Упрощение семантики: Разработана семантика временного планирования, более подходящая для формальных рассуждений

Экспериментальная установка

Окружение формальной верификации

• Доказывающая система: Isabelle/HOL
• Проверяющий сертификаты: Верифицированный проверяющий сертификаты Wimmer и von Mutius
• Целевое свойство: Проверка достижимости A ⊨ EF(loc(AM) = goal)

Статистика объема кода

Сравнение с базовыми работами

Сравнение объема с соответствующими формально верифицированными работами:

• Верифицированный планировщик на основе SAT: ~17,500 строк
• Верифицированный верификатор классического планирования: ~3,000 строк
• Верифицированный верификатор временного PDDL планирования: ~6,500 строк

Результаты экспериментов

Основные теоретические результаты

Теорема 1 (основная теорема корректности): Если план π является корректным и не имеет самопересечений (valid(π) ∧ no_self_overlap(π)), то утверждение A ⊨ EF(loc(AM) = goal) справедливо.

Структура доказательства:

1. Лемма 1: Построение симуляции, индуцирующей параллельный план
2. Лемма 2: Достижимость от начальной конфигурации к закодированному состоянию
3. Лемма 3: Переход от конечного состояния к целевой конфигурации

Результаты формальной верификации

1. Доказательство полноты: Успешно доказана полнота кодирования, то есть каждый корректный план может быть найден в соответствующей сети временных автоматов
2. Проверка машиной: Все доказательства прошли проверку машиной в Isabelle/HOL, обеспечивая наивысший уровень гарантий надежности
3. Модульная конструкция: Структура доказательства модульна, что облегчает понимание и обслуживание

Верификация инженерной реализации

Реализация кодирования адаптирована к формату, совместимому с существующим верифицированным проверяющим сертификаты, формируя полную исполняемую цепь сертификации.

Связанные работы

Сертификация классического планирования

• Eriksson и др. разработали компактные схемы сертификации неразрешимости для классического планирования
• Abdulaziz и Lammich предоставили формально верифицированный верификатор классического планирования

Временное планирование и проверка моделей

• Dierks и др. реализовали статическое сокращение подмножества PDDL к временным автоматам
• Heinz и др. определили явное кодирование задач временного планирования в временные автоматы
• Gigante и др. исследовали сложность временного планирования на теоретическом уровне

Методы формальной верификации

• Abdulaziz и Kurz использовали аналогичный подход для разработки верифицированной системы планирования на основе SAT
• Kumar и др., а также Leroy использовали пошаговую верификацию кодирования в верификации компиляторов

Заключение и обсуждение

Основные выводы

1. Проверка осуществимости: Доказана осуществимость формальной сертификации неразрешимости временного планирования
2. Теоретические гарантии: Обеспечены надежные гарантии корректности через доказывающую систему
3. Инженерная реализация: Успешно построена полная цепь инструментов сертификации

Ограничения

1. Ограничения входных данных: В настоящее время принимаются только предварительно инстанцированные задачи временного планирования
2. Подмножество семантики: Поддерживаемая семантика является подмножеством верифицированного верификатора планирования
3. Исполняемость: Механизм сертификации еще не полностью исполняем

Направления будущих исследований

1. Доказательство эквивалентности: Планируется формально доказать эквивалентность семантики данной работы и существующих верификаторов
2. Исполняемая реализация: Разработка исполняемого проверяющего сертификаты
3. Верификация инстанцирования: Формальная верификация алгоритмов инстанцирования, таких как решатель Helmert Data-log
4. Ослабление ограничений: Исследование возможности ослабления условия отсутствия самопересечений

Глубокая оценка

Преимущества

1. Теоретическая строгость: Впервые предоставлены проверяемые машиной формальные доказательства для сертификации неразрешимости временного планирования
2. Инженерная полнота: Не только предоставлена теоретическая структура, но и реализована интеграция с существующими инструментами
3. Методологическая инновативность:
   • Проектирование кодирования, поддерживающее параллельное выполнение
   • Элегантное решение для обработки моментальных действий
   • Упрощенная и эквивалентная семантика
4. Гарантии надежности: Обеспечены гарантии корректности наивысшего уровня через доказывающую систему

Недостатки

1. Ограничения практичности:
   • Требуется предварительно инстанцированный ввод
   • Еще не полностью исполняемо
   • Отсутствует оценка производительности
2. Охват: Поддерживается только подмножество временного планирования, не полный PDDL
3. Масштабируемость: Объем формальной работы в 18,000 строк кода довольно значителен, что повышает затраты на обслуживание

Влияние

1. Академический вклад:
   • Заполнен пробел в формальной верификации временного планирования
   • Предоставлена новая теоретическая основа для сертификации неразрешимости
   • Продемонстрирована осуществимость формальной верификации сложных систем
2. Практическая ценность:
   • Обеспечена надежная сертификация систем планирования для критических приложений
   • Расширяемо на другие формы планирования и задачи удовлетворения ограничений
   • Предоставлена справочная информация для разработки верифицированных инструментов автоматизации
3. Воспроизводимость: На основе открытого исходного кода Isabelle/HOL, теоретически полностью воспроизводимо

Применимые сценарии

1. Критические системы: Приложения планирования, требующие высоких гарантий надежности (аэрокосмическая, медицинская техника)
2. Инструменты исследования: Предоставление инфраструктуры формальной верификации для исследований временного планирования
3. Образовательное назначение: Использование в качестве примера для преподавания формальных методов и алгоритмов планирования
4. Разработка инструментов: Предоставление теоретической основы для разработки верифицированных инструментов планирования

Библиография

Ключевые ссылки включают:

• Abdulaziz & Koller (2022): Формальная семантика и верификатор временного планирования
• Heinz et al. (2019): Кодирование временного планирования в временные автоматы
• Wimmer & von Mutius (2020): Верифицированный проверяющий сертификаты для временных автоматов
• Abdulaziz & Kurz (2023): Верифицированная система планирования на основе SAT

Данная статья вносит важный вклад в область формальной верификации временного планирования. Хотя в практическом применении еще есть место для улучшений, ее теоретическая строгость и методологическая инновативность создают прочную основу для развития этой области.