2025-11-23T10:46:16.032830

Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control

Phalakarn, Pruekprasert, Hasuo
Stochastic games are fundamental in various applications, including the control of cyber-physical systems (CPS), where both controller and environment are modeled as players. Traditional algorithms typically aim to determine a single winning strategy to develop a controller. However, in CPS control and other domains, permissive controllers are essential, as they enable the system to adapt when additional constraints arise and remain resilient to runtime changes. This work generalizes the concept of (permissive winning) strategy templates, originally introduced by Anand et al. at TACAS and CAV 2023 for deterministic games, to incorporate stochastic games. These templates capture an infinite number of winning strategies, allowing for efficient strategy adaptation to system changes. We focus on two winning criteria (almost-sure and positive winning) and five winning objectives (safety, reachability, Büchi, co-Büchi, and parity). Our contributions include algorithms for constructing templates for each winning criterion and objective and a novel approach for extracting a winning strategy from a given template. Discussions on comparisons between templates and between strategy extraction methods are provided.
academic

Plantillas de Estrategia para la Victoria Casi Segura y de Probabilidad Positiva en Juegos de Paridad Estocásticos hacia Control Permisivo y Resiliente

Información Básica

  • ID del Artículo: 2409.08607
  • Título: Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
  • Autores: Kittiphon Phalakarn, Sasinee Pruekprasert, Ichiro Hasuo
  • Clasificación: eess.SY cs.LO cs.SY
  • Fecha de Publicación: Septiembre de 2024 (arXiv v2: 16 de octubre de 2025)
  • Enlace del Artículo: https://arxiv.org/abs/2409.08607

Resumen

Los juegos estocásticos desempeñan un papel fundamental en diversas aplicaciones, particularmente en el control de sistemas ciber-físicos (CPS), donde el controlador y el entorno se modelan como participantes del juego. Los algoritmos tradicionales generalmente tienen como objetivo determinar una única estrategia ganadora para desarrollar el controlador. Sin embargo, en el control de CPS y otros campos, los controladores permisivos son cruciales porque pueden adaptarse al sistema cuando surgen restricciones adicionales y mantienen resiliencia ante cambios en tiempo de ejecución. Este trabajo generaliza el concepto de plantillas de estrategia de juegos deterministas a juegos estocásticos, permitiendo que estas plantillas capturen un número infinito de estrategias ganadoras y faciliten la adaptación eficiente de estrategias ante cambios del sistema. Nos enfocamos en dos criterios de victoria (victoria casi segura y victoria de probabilidad positiva) y cinco objetivos de victoria (seguridad, alcanzabilidad, Büchi, co-Büchi y paridad).

Antecedentes de Investigación y Motivación

Contexto del Problema

  1. Limitaciones de Métodos Tradicionales: Los algoritmos tradicionales de resolución de juegos típicamente buscan solo una única estrategia ganadora, sin considerar la permisividad (permissiveness) de la estrategia
  2. Requisitos de Aplicaciones Prácticas: En el control de sistemas ciber-físicos, se requieren controladores permisivos para adaptarse a restricciones adicionales y cambios en tiempo de ejecución
  3. Necesidad de Control Resiliente: Los sistemas necesitan mantener robustez ante fallos o cambios ambientales

Motivación de la Investigación

  • El concepto existente de plantillas de estrategia solo se aplica a juegos deterministas, careciendo de soporte para juegos estocásticos
  • Se requiere un marco que pueda capturar un número infinito de estrategias ganadoras para facilitar la adaptación rápida de estrategias
  • En aplicaciones prácticas como el control de CPS, la permisividad y la resiliencia son requisitos clave

Contribuciones Principales

  1. Algoritmo de Plantillas de Estrategia para Victoria Casi Segura: Se proponen algoritmos de construcción de plantillas de estrategia para victoria casi segura con cinco objetivos de victoria (seguridad, alcanzabilidad, Büchi, co-Büchi, paridad)
  2. Plantillas de Estrategia para Victoria de Probabilidad Positiva: Se desarrollan algoritmos de construcción y composición de plantillas de estrategia bajo el criterio de victoria de probabilidad positiva
  3. Marco de Comparación de Plantillas de Estrategia: Se proporciona una discusión de comparación de plantillas basada en permisividad y tamaño
  4. Método de Extracción de Estrategia: Se propone un nuevo método para extraer estrategias ganadoras de una plantilla dada, equilibrando el objetivo de victoria y la permisividad

Explicación Detallada de Métodos

Definición de Tareas

Definición de Juego Estocástico: G = (V, E, (V□, V○, V△)), donde:

  • V es el conjunto de vértices, E es el conjunto de aristas
  • V□, V○, V△ representan respectivamente los vértices del jugador Par, jugador Impar y jugador Aleatorio
  • Se denomina juego de "2.5" jugadores, que contiene dos jugadores principales y un jugador aleatorio

Definición de Plantilla de Estrategia: T = (P, L, C), donde:

  • P ⊆ E□ es el conjunto de aristas deshabilitadas
  • L ⊆ 2^E□ es el conjunto de grupos activos
  • C ⊆ E□ es el conjunto de aristas coactivas

Arquitectura del Modelo

1. Construcción de Plantillas de Estrategia para Victoria Casi Segura

Objetivo de Seguridad (G X):

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

Objetivo de Alcanzabilidad (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)

Objetivo Büchi (GF X): Se construyen grupos activos mediante la función LiveGroups, asegurando que los caminos visiten el conjunto objetivo infinitas veces.

Objetivo de Paridad:

  1. Se reduce el juego estocástico a un juego determinista (utilizando el algoritmo Reduce)
  2. Se construye la plantilla de estrategia del juego determinista
  3. Se transforma nuevamente a la plantilla del juego estocástico

2. Construcción de Plantillas de Estrategia para Victoria de Probabilidad Positiva

PositiveTemplate(G, φ):
1. Calcular W□, W○ y plantilla de victoria casi segura 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))

Puntos de Innovación Técnica

  1. Extensión de Operaciones de Conjuntos: Se introducen nuevos operadores de conjuntos que consideran al jugador Aleatorio, como Pre△(X', X) y Attr'□(X)
  2. Algoritmo de Composición de Plantillas: Se propone un mecanismo de detección de conflictos que recalcula cuando las plantillas entran en conflicto
  3. Extracción de Estrategia Parametrizada: Se utilizan parámetros α y β para equilibrar la permisividad y la velocidad de logro del objetivo
  4. Extensión a Victoria de Probabilidad Positiva: Primera extensión de plantillas de estrategia al criterio de victoria de probabilidad positiva

Configuración Experimental

Verificación Teórica

El artículo verifica principalmente la corrección de los algoritmos mediante pruebas teóricas, incluyendo:

  • Teoremas de corrección para cada algoritmo de construcción de plantillas
  • Teoremas de permisividad para el método de extracción de estrategia
  • Pruebas de corrección para el algoritmo de composición de plantillas

Análisis de Complejidad

  • El tiempo de ejecución en el peor caso de los algoritmos de construcción de estrategia coincide con los algoritmos estándar
  • La composición de plantillas y la extracción de estrategia pueden ejecutarse eficientemente en tiempo de ejecución

Resultados Experimentales

Resultados Teóricos

Teoremas 10-14: Se prueba la corrección de los algoritmos de construcción de plantillas de estrategia para cada objetivo de victoria

  • SafetyTemplate construye plantillas que son casi seguramente ganadoras para G X
  • ReachabilityTemplate construye plantillas que son casi seguramente ganadoras para F X
  • Se aplica de manera similar a otros objetivos

Teorema 18: La plantilla construida por PositiveTemplate es tanto casi seguramente ganadora como ganadora de probabilidad positiva

Teorema 27: El método de extracción parametrizado es más permisivo que el método Extract original

Análisis de Permisividad

Proposición 22: Si P ⊇ P', L ⊇ L', C ⊇ C', entonces T no es más permisivo que T'

Proposición 23: Si T no es más permisivo que T' y T' es ganadora, entonces T también es ganadora

Potencial de Aplicación Práctica

El artículo señala que, basándose en resultados experimentales de juegos deterministas, las plantillas de estrategia pueden lograr al menos una aceleración de 2 veces en síntesis incremental y reducir efectivamente el recálculo incluso cuando el 30% de las opciones se deshabilitan en control tolerante a fallos.

Trabajo Relacionado

Teoría Clásica de Permisividad

  • Ramadge y Wonham (1987) introdujeron formalmente el concepto de permisividad en control supervisado
  • Bernet et al. probaron la existencia de estrategias máximamente permisivas en juegos de paridad

Desarrollo de Plantillas de Estrategia

  • Anand et al. introdujeron plantillas de estrategia para juegos deterministas en TACAS y CAV 2023
  • Este trabajo es la primera investigación que extiende plantillas de estrategia a juegos estocásticos

Resolución de Juegos Estocásticos

  • Método de reducción de juegos de paridad estocásticos de Chatterjee et al.
  • Operadores de conjuntos para juegos estocásticos de Banerjee et al.

Conclusiones y Discusión

Conclusiones Principales

  1. Se extiende exitosamente el concepto de plantillas de estrategia de juegos deterministas a juegos estocásticos
  2. Se proporciona un marco algorítmico completo que cubre dos criterios de victoria y cinco objetivos de victoria
  3. El nuevo método de extracción de estrategia mejora la permisividad mientras garantiza la corrección

Limitaciones

  1. Las estrategias de victoria de probabilidad positiva no garantizan probabilidad óptima
  2. La implementación de algoritmos y verificación experimental están pendientes
  3. Solo se consideran juegos de estado finito

Direcciones Futuras

  1. Construir plantillas que mantengan la misma permisividad pero sean más pequeñas
  2. Extender a objetivos definidos por fórmulas de lógica temporal métrica (MTL)
  3. Aplicar a sistemas en tiempo real

Evaluación Profunda

Ventajas

  1. Contribución Teórica Significativa: Primera extensión de plantillas de estrategia a juegos estocásticos con marco teórico completo
  2. Diseño de Algoritmo Razonable: Utiliza ingeniosamente operaciones de conjuntos existentes y técnicas de reducción
  3. Perspectivas de Aplicación Amplias: Tiene importancia práctica significativa para el control de sistemas ciber-físicos
  4. Rigor Matemático: Proporciona pruebas de corrección completas

Insuficiencias

  1. Falta de Verificación Experimental: Principalmente trabajo teórico, carece de implementación práctica y evaluación de rendimiento
  2. Problema de Optimalidad: Las estrategias de victoria de probabilidad positiva no garantizan optimalidad
  3. Análisis de Complejidad Insuficiente: El análisis de complejidad computacional real es relativamente superficial

Impacto

  1. Valor Académico: Proporciona nuevas herramientas y métodos para la teoría de juegos estocásticos
  2. Valor Práctico: Proporciona base teórica para el diseño de controladores permisivos
  3. Extensibilidad: Proporciona un buen marco base para investigaciones posteriores

Escenarios Aplicables

  1. Control robusto de sistemas ciber-físicos
  2. Sistemas de automatización que requieren adaptabilidad
  3. Diseño de sistemas de control de optimización multiobjetivo
  4. Sistemas de control tolerante a fallos

Referencias

El artículo cita 35 referencias relacionadas, que cubren principalmente:

  • Literatura fundamental de teoría de juegos
  • Teoría de control supervisado
  • Trabajos relacionados con plantillas de estrategia
  • Algoritmos de resolución de juegos estocásticos
  • Lógica temporal lineal y verificación de modelos

Evaluación General: Este es un artículo de investigación teórica de alta calidad que extiende exitosamente el concepto de plantillas de estrategia de juegos deterministas a juegos estocásticos, proporcionando una base teórica importante para control permisivo y resiliente. Aunque carece de verificación experimental, la contribución teórica es significativa y tiene un impacto importante en impulsar campos relacionados.