В рамках курса по валидации систем критической безопасности (AA228V) в Стэнфорде прошла лекция, посвященная методам дискретной достижимости (Reachability). После разбора нелинейных систем на предыдущих занятиях профессора перешли к одной из самых надежных стратегий анализа безопасности — преобразованию непрерывных динамических систем в дискретные графы. В ходе лекции были представлены методы борьбы с эффектом «раздувания» множеств и способы получения вероятностных гарантий безопасности даже в условиях неопределенности.
🛠 От интервалов к Тейлоровским моделям 0:05
Лекция началась с ретроспективы проблем, возникших при анализе нелинейных систем, таких как перевернутый маятник. Основная сложность заключалась в том, что использование интервальной арифметики и естественных функций включения приводило к слишком грубой переаппроксимации (over-approximation) . Множество достижимости «раздувалось» настолько быстро, что сделать вывод о безопасности системы становилось невозможно. Даже функции включения на основе теоремы о среднем значении лишь ненадолго откладывали этот процесс .
Ключевым решением стали модели Тейлора (Taylor models). В отличие от стандартных функций включения, которые всегда выдают на выходе гиперпрямоугольники, модели Тейлора позволяют работать с гораздо более выразительными формами .
Особенности моделей Тейлора:
- Состав: Полином Тейлора степени $n-1$ плюс интервальный остаток ($\alpha$) .
- Смысл: Полином аппроксимирует функцию, а интервал $\alpha$ (остаток Лагранжа) ограничивает ошибку этой аппроксимации .
- Гибкость: При использовании моделей второго порядка мы получаем политопы, а третьего — невыпуклые гладкие формы .
Однако лектор подчеркнула, что работа с невыпуклыми множествами третьего и выше порядков крайне затруднительна — операции пересечения таких множеств с «опасными зонами» (avoid sets) вычислительно сложны .
📉 Консервативная линеаризация 11:57
Частным случаем моделей Тейлора второго порядка является консервативная линеаризация . Этот метод позволяет свести сложную нелинейную задачу к линейной достижимости, с которой инженеры уже умеют работать.
Процесс выглядит следующим образом:
- Функция линеаризуется в центре текущего множества с использованием Якобиана ($J$) .
- К линейному преобразованию добавляется интервальный остаток, учитывающий ошибку линеаризации.
- Для вычислений используются суммы Минковского и матричное умножение .
На примере маятника было показано, что консервативная линеаризация дает гораздо более плотные границы множеств, чем простые интервалы, хотя в долгосрочной перспективе даже она может привести к расхождению границ .
🧬 Символьная vs Конкретная достижимость 18:13
Собеседники обсудили два концептуальных подхода к вычислению множеств во времени:
- Символьная достижимость: Рассматривает функцию «развертки» (roll-out) на несколько шагов вперед как единый объект. Она не страдает от «эффекта обертывания», но вычислительно дорога из-за накопления нелинейностей .
- Конкретная достижимость (Concretization): Аппроксимирует и фиксирует (конкретизирует) множество на каждом временном шаге .
Главный риск конкретной достижимости — эффект обертывания (wrapping effect). Это накопление ошибки из-за того, что на каждом шаге мы вынуждены описывать реальное множество сложной формы более простой фигурой (например, прямоугольником), включая в расчет лишние, недостижимые состояния .
Тем не менее, комбинация конкретизации и консервативной линеаризации позволила успешно верифицировать безопасность маятника на 14 шагов вперед, что ранее было недоступно .
📊 Дискретная абстракция и графы 34:00
Центральной темой второй половины лекции стал переход к дискретной достижимости. Любую систему с дискретными состояниями можно представить в виде направленного графа, где узлы — это состояния, а ребра — переходы с определенными весами (вероятностями) .
Алгоритмы на графах позволяют выполнять:
- Прямую достижимость (Forward reachability): Поиск всех состояний, достижимых из начального с помощью поиска в ширину (BFS) .
- Обратную достижимость (Backward reachability): Определение состояний, из которых можно попасть в «плохую» зону .
- Поиск инвариантных множеств: Легко проверяется через подмножества узлов графа .
По мнению лектора, даже если система непрерывна, ее выгодно «дискретизировать» через разбиение (partitioning) пространства состояний на ячейки. Каждая ячейка становится узлом графа. Чтобы сохранить гарантии безопасности, ребра в таком графе должны строиться из условия перекрытия: если из ячейки А можно попасть в область, задевающую ячейку Б, в графе рисуется ребро А $\rightarrow$ Б . Чем мельче разбиение, тем точнее аппроксимация .
🎲 Вероятностная достижимость 47:27
В отличие от детерминированного подхода («достижимо или нет»), вероятностная достижимость отвечает на вопрос: «С какой вероятностью мы окажемся в опасности?» .
Для объяснения лектор привела личный пример спора с мужем: что произойдет быстрее — она отобьет битой мяч на скорости 90 миль в час или он выполнит «тройной прыжок» через скакалку? . Обычный анализ достижимости скажет, что оба события возможны. Вероятностный же анализ покажет, что шанс случайно отбить мяч значительно выше .
В лекции были выведены две ключевые метрики:
- Probability of Occupancy: Вероятность нахождения в конкретном состоянии $s$ в момент времени $t$ .
- Probability of Reachability: Общая вероятность того, что система попадет в целевое множество за отведенный горизонт времени .
В финале лекции эксперты сошлись во мнении, что методы достижимости находят реальное применение в навигации роботов и, что особенно актуально, в анализе выходных множеств нейронных сетей умеренного размера .
