Semi-Competitive Differential Game Logic

Resumen Técnico: Lógica de Juego Diferencial Semi-Competitiva (dGLsc)

Planteamiento del Problema
La verificación de seguridad de los Sistemas Ciber-Físicos (CPS), particularmente aquellos que involucran interacciones entre múltiples agentes (por ejemplo, vehículos autónomos, aeronaves), presenta desafíos significativos. Los enfoques tradicionales suelen modelar estas interacciones utilizando la Lógica de Juego Diferencial (dGL), la cual asume una relación de suma cero y adversarial, donde la ganancia de un jugador es la pérdida del otro. Si bien esto produce resultados seguros, suele ser excesivamente conservador. En muchos escenarios del mundo real, como la evitación de colisiones, los agentes comparten objetivos de seguridad (por ejemplo, ninguno quiere chocar) mientras persiguen metas individuales distintas (por ejemplo, llegar a diferentes destinos). Una suposición de suma cero no logra capturar el potencial de cooperación en estos juegos de "suma no nula", lo que conduce a fallos de verificación en sistemas que son en realidad seguros. Además, las lógicas de suma no nula existentes suelen tener dificultades con la dinámica continua o requieren árboles de juego complejos que son intratables para sistemas híbridos de profundidad ilimitada.

Metodología
El artículo introduce la Lógica de Juego Diferencial Semi-Competitiva (dGLsc), una lógica formal diseñada para verificar juegos híbridos donde dos jugadores (Ángel y Demonio) poseen metas individuales, potencialmente superpuestas. La metodología central se basa en el concepto de semi-competitividad:

1. Modelo de Comportamiento: Los jugadores cooperan cuando es beneficioso para ambos alcanzar sus respectivos objetivos, pero compiten cuando es necesario. Específicamente, un jugador nunca perderá a propósito. Si existen múltiples opciones de victoria, un jugador elige una que también ayude al oponente a ganar. Si ninguna opción conduce a una victoria para el jugador, este no ayudará altruistamente al oponente.
2. Sintaxis: dGLsc extiende la sintaxis de dGL modificando las modalidades. En lugar de $\langle \alpha \rangle P$ (Ángel gana $\alpha$ para alcanzar $P$) y $[\alpha] Q$ (Demonio gana $\alpha$ para alcanzar $Q$), dGLsc utiliza $\langle \alpha \rangle (P, Q)$ y $[\alpha] (P, Q)$. Estas modalidades codifican explícitamente los objetivos de ambos jugadores dentro de la fórmula, permitiendo que la lógica razone sobre la interacción de los objetivos individuales.
3. Semántica: La semántica define regiones de victoria $\varsigma_\alpha(X, Y)$ para el Ángel y $\delta_\alpha(X, Y)$ para el Demonio, donde $X$ e $Y$ son los conjuntos de metas. A diferencia de dGL, estas regiones no son complementarias. La semántica tiene en cuenta la cooperación al incluir estados donde ambos jugadores pueden ganar simultáneamente. Por ejemplo, en un juego continuo, la región de victoria del Demonio incluye estados donde el Ángel (quien controla la evolución) detiene el sistema en un punto donde ambos objetivos se cumplen. Las semánticas para juegos de repetición ($\alpha^*$) se definen mediante puntos fijos que distinguen entre escenarios competitivos y cooperativos, utilizando el punto fijo menor para el Ángel y el punto fijo mayor para el Demonio para asegurar la unicidad y la monotonicidad.
4. Cálculo de Prueba: Se presenta un cálculo de prueba sano y relativamente completo. Incluye axiomas para cada operador de juego híbrido (asignación, evolución continua, prueba, elección, secuencia, dual, repetición) adaptados a la estructura de dos metas. Crucialmente, el cálculo incluye una Regla de Punto Fijo (FP) que caracteriza los juegos de repetición como la unión de dos puntos fijos menores (uno para la competición y otro para la cooperación). El sistema también incluye reglas de monotonicidad y un axioma de determinismo para casos donde las metas son complementarias.

Contribuciones Clave

• Lógica Formal dGLsc: La introducción de una lógica diseñada específicamente para juegos híbridos de suma no nula con dinámica continua, permitiendo la verificación de sistemas críticos de seguridad donde los agentes tienen objetivos superpuestos pero distintos.
• Semántica Semi-Competitiva: Un marco semántico novedoso donde los jugadores actúan de forma cooperativa si esto favorece su propio éxito, resolviendo la tensión entre la optimización individual y la seguridad mutua sin requerir protocolos de negociación explícitos.
• Propiedades Teóricas:
  • Monotonicidad: Se demuestra que aumentar el conjunto de metas de un jugador expande su región de victoria.
  • Equivalencia con dGL: Se demuestra que cuando las metas son complementarias (opuestas), dGLsc se reduce a la dGL estándar de suma cero.
  • Equivalencia General: Se muestra que cualquier región de victoria de dGLsc puede expresarse como una disyunción de regiones de victoria en un juego dGL transformado (eliminando operadores duales) y un juego dGL estándar, demostiendo la expresividad de la lógica.
• Cálculo de Prueba: Un cálculo sano y relativamente completo que evita la necesidad de codificación manual de conceptos de suma no nula (lo cual sería requerido si se utilizara la dGL estándar) y soporta el razonamiento modular.

Resultados
El artículo establece la corrección (soundness) del cálculo de prueba, asegurando que todas las fórmulas demostrables son válidas. Además, demuestra su completitud relativa, mostrando que cualquier fórmula válida en dGLsc puede ser probada si la lógica de primer orden subyacente es diferencialmente expresiva. El artículo ilustra la utilidad de dGLsc a través de un ejemplo canónico de dos aviones intercambiando reservas de combustible. En este escenario, la dGL estándar fallaría al verificar la seguridad porque los agentes no pueden controlar las variables críticas para el objetivo del otro. Sin embargo, dGLsc verifica con éxito la seguridad de la interacción porque la semántica semi-competitiva permite que los agentes cooperen (por ejemplo, que el Ángel llene el tanque del Demonio) para asegurar que ambos alcancen sus respectivos objetivos.

Significancia
El artículo sostiene que dGLsc proporciona una forma natural e intuitiva de expresar y razonar sobre juegos híbridos de suma no nula, los cuales son prevalentes en los CPS multi-agente pero difíciles de verificar bajo supuestos conservadores de suma cero. Al formalizar el comportamiento semi-competitivo, la lógica permite pruebas de seguridad para situaciones que serían inseguras bajo supuestos de suma cero, pero que son seguras en la realidad debido al potencial de cooperación. Este trabajo cierra la brecha entre los conceptos de equilibrio de suma no nula de la teoría de juegos y la verificación formal de sistemas híbridos con dinámica continua, ofreciendo una herramienta que es más precisa que los modelos adversariales y, al mismo tiempo, más tratable computacionalmente que los enfoques generales de la teoría de juegos.