Шаблоны стратегий для почти достоверного и положительного выигрыша в стохастических играх четности в направлении разрешающего и устойчивого управления

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

• ID статьи: 2409.08607
• Название: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
• Авторы: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
• Классификация: eess.SY cs.LO cs.SY
• Дата публикации: сентябрь 2024 г. (arXiv v2: 16 октября 2025 г.)
• Ссылка на статью: https://arxiv.org/abs/2409.08607

Аннотация

Стохастические игры играют фундаментальную роль в различных приложениях, особенно в управлении киберфизическими системами (КФС), где контроллер и окружение моделируются как участники игры. Традиционные алгоритмы обычно направлены на определение единственной выигрышной стратегии для разработки контроллера. Однако в управлении КФС и других областях разрешающие контроллеры имеют критическое значение, поскольку они способны адаптироваться к системе при возникновении дополнительных ограничений и сохранять устойчивость к изменениям во время выполнения. В данной работе концепция шаблонов стратегий обобщается с детерминированных игр на стохастические игры, причем эти шаблоны способны захватывать бесконечное количество выигрышных стратегий, позволяя эффективно адаптировать стратегии к изменениям системы. Мы сосредоточиваемся на двух критериях выигрыша (почти достоверный выигрыш и положительный выигрыш) и пяти целях выигрыша (безопасность, достижимость, Бюхи, ко-Бюхи и четность).

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

Проблемный контекст

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

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

• Существующая концепция шаблонов стратегий применима только к детерминированным играм, отсутствует поддержка стохастических игр
• Необходима структура, способная захватывать бесконечное количество выигрышных стратегий для поддержки быстрой адаптации стратегий
• В практических приложениях, таких как управление КФС, разрешающий характер и устойчивость являются ключевыми требованиями

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

1. Алгоритм шаблонов стратегий почти достоверного выигрыша: Предложены алгоритмы построения шаблонов стратегий почти достоверного выигрыша для пяти целей выигрыша (безопасность, достижимость, Бюхи, ко-Бюхи, четность)
2. Шаблоны стратегий положительного выигрыша: Разработаны алгоритмы построения и композиции шаблонов стратегий при критерии положительного выигрыша
3. Структура сравнения шаблонов стратегий: Предоставлено обсуждение сравнения шаблонов на основе разрешающего характера и размера
4. Методы извлечения стратегий: Предложены новые методы извлечения выигрышных стратегий из заданного шаблона, балансирующие цель выигрыша и разрешающий характер

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

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

Определение стохастической игры: G = (V, E, (V□, V○, V△)), где:

• V — множество вершин, E — множество ребер
• V□, V○, V△ обозначают вершины игроков Even, Odd и Random соответственно
• Называется игрой "2.5" игроков, содержащей двух основных игроков и одного случайного игрока

Определение шаблона стратегии: T = (P, L, C), где:

• P ⊆ E□ — множество запрещенных ребер
• L ⊆ 2^E□ — множество активных групп
• C ⊆ E□ — множество совместно активных ребер

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

1. Построение шаблонов стратегий почти достоверного выигрыша

Цель безопасности (G X):

SafetyTemplate(G, X):
1. W□ ← νY.(X ∩ (Pre□(Y) ∪ Pre(Y)))
2. P ← Edges□(W□, V \ W□)
3. return (P, ∅, ∅)

Цель достижимости (F X):

ReachabilityTemplate(G, X):
1. A ← Attr'(X)
2. W□ ← Attr'□(A)
3. P ← Edges□(W□, V \ W□)
4. C ← Edges□(W□ \ A, W□ \ A)
5. return (P, ∅, C)

Цель Бюхи (GF X): Построение активных групп через функцию LiveGroups, обеспечивающее бесконечное посещение целевого множества на пути.

Цель четности:

1. Сведение стохастической игры к детерминированной игре (с использованием алгоритма Reduce)
2. Построение шаблона стратегии детерминированной игры
3. Преобразование обратно в шаблон стохастической игры

2. Построение шаблонов стратегий положительного выигрыша

PositiveTemplate(G, φ):
1. Вычисление W□, W○ и шаблона почти достоверного выигрыша T^(a)
2. W? ← V \ (W□ ∪ W○)
3. P^(p) ← P^(a) ∪ Edges□(W?, W○)
4. C^(p) ← C^(a) ∪ Edges□(W?, W?)
5. return T^(p) = (P^(p), L^(p), C^(p))

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

1. Расширение операций над множествами: Введены новые операторы над множествами, учитывающие игрока Random, такие как Pre△(X', X) и Attr'□(X)
2. Алгоритм композиции шаблонов: Предложен механизм обнаружения конфликтов с пересчетом при возникновении конфликта шаблонов
3. Параметризованное извлечение стратегий: Использование параметров α и β для балансирования разрешающего характера и скорости достижения цели
4. Расширение на положительный выигрыш: Первое расширение шаблонов стратегий на критерий положительного выигрыша

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

Теоретическая верификация

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

• Теоремы корректности для каждого алгоритма построения шаблонов
• Теоремы разрешающего характера для методов извлечения стратегий
• Доказательства корректности алгоритмов композиции шаблонов

Анализ сложности

• Наихудшее время выполнения алгоритмов построения стратегий соответствует стандартным алгоритмам
• Композиция шаблонов и извлечение стратегий могут выполняться эффективно во время выполнения

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

Теоретические результаты

Теоремы 10-14: Доказана корректность алгоритмов построения шаблонов стратегий для каждой цели выигрыша

• Шаблон, построенный SafetyTemplate, почти достоверно выигрывает для G X
• Шаблон, построенный ReachabilityTemplate, почти достоверно выигрывает для F X
• Аналогично применяется к другим целям

Теорема 18: Шаблон, построенный PositiveTemplate, является как почти достоверно выигрывающим, так и положительно выигрывающим

Теорема 27: Параметризованный метод извлечения более разрешающий, чем исходный метод Extract

Анализ разрешающего характера

Предложение 22: Если P ⊇ P', L ⊇ L', C ⊇ C', то T не более разрешающий, чем T'

Предложение 23: Если T не более разрешающий, чем T' и T' выигрывающий, то T также выигрывающий

Потенциал практического применения

Статья указывает, что на основе результатов для детерминированных игр шаблоны стратегий могут достичь ускорения как минимум в 2 раза при инкрементальном синтезе и эффективно снизить пересчеты при отказоустойчивом управлении даже при запрещении 30% выборов.

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

Классическая теория разрешающего характера

• Ramadge и Wonham (1987) формально ввели концепцию разрешающего характера в контексте надзорного управления
• Bernet и др. доказали существование максимально разрешающих стратегий в играх четности

Развитие шаблонов стратегий

• Anand и др. ввели шаблоны стратегий для детерминированных игр в TACAS и CAV 2023
• Данная работа является первым исследованием расширения шаблонов стратегий на стохастические игры

Решение стохастических игр

• Метод сведения стохастических игр четности Chatterjee и др.
• Операторы над множествами для стохастических игр Banerjee и др.

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

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

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

Ограничения

1. Стратегии положительного выигрыша не гарантируют оптимальную вероятность
2. Реализация алгоритмов и экспериментальная верификация требуют завершения
3. Рассмотрены только конечные игры

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

1. Построение шаблонов с сохранением того же разрешающего характера, но меньшего размера
2. Расширение на формулы метрической временной логики (MTL)
3. Применение к системам реального времени

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

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

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

Недостатки

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

Влияние

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

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

1. Робастное управление киберфизическими системами
2. Автоматизированные системы, требующие адаптивности
3. Проектирование систем управления с многоцелевой оптимизацией
4. Отказоустойчивые системы управления

Список литературы

Статья цитирует 35 связанных источников, охватывающих в основном:

• Фундаментальную литературу по теории игр
• Теорию надзорного управления
• Работы, связанные с шаблонами стратегий
• Алгоритмы решения стохастических игр
• Линейную временную логику и проверку моделей

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