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
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).
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
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
Necesidad de Control Resiliente: Los sistemas necesitan mantener robustez ante fallos o cambios ambientales
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)
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
Marco de Comparación de Plantillas de Estrategia: Se proporciona una discusión de comparación de plantillas basada en permisividad y tamaño
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
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:
Se reduce el juego estocástico a un juego determinista (utilizando el algoritmo Reduce)
Se construye la plantilla de estrategia del juego determinista
Se transforma nuevamente a la plantilla del juego estocástico
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.
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.