Semi-Competitive Differential Game Logic

Resumo Técnico: Lógica de Jogo Diferencial Semi-Competitiva (dGLsc)

Definição do Problema
A verificação de segurança de Sistemas Ciber-Físicos (CPS), particularmente aqueles que envolvem interações entre múltiplos agentes (ex: veículos autônomos, aeronaves), apresenta desafios significativos. Abordagens tradicionais frequentemente modelam essas interações usando a Lógica de Jogo Diferencial (dGL), que assume uma relação de soma zero e adversária, onde o ganho de um jogador é a perda do outro. Embora isso resulte em resultados seguros, é frequentemente excessivamente conservador. Em muitos cenários do mundo real, como a prevenção de colisões, os agentes compartilham objetivos de segurança (ex: nenhum deles quer bater) enquanto buscam objetivos individuais distintos (ex: alcançar destinos diferentes). Uma suposição de soma zero falha em capturar o potencial de cooperação nesses jogos "não de soma zero", levando à falha de verificação de sistemas que são, na verdade, seguros. Além disso, as lógicas de não-soma zero existentes muitas vezes têm dificuldade com dinâmicas contínuas ou exigem árvores de jogo complexas que são intratáveis para sistemas híbridos de profundidade ilimitada.

Metodologia
O artigo introduz a Lógica de Jogo Diferencial Semi-Competitiva (dGLsc), uma lógica formal projetada para verificar jogos híbridos onde dois jogadores (Anjo e Demônio) possuem objetivos individuais, potencialmente sobrepostos. A metodologia central baseia-se no conceito de semi-competitividade:

1. Modelo Comportamental: Os jogadores cooperam quando é benéfico para ambos alcançarem seus respectivos objetivos, mas competem quando necessário. Especificamente, um jogador nunca perderá de propósito. Se múltiplas opções de vitória existirem, o jogador escolhe uma que também ajude o oponente a vencer. Se nenhuma opção levar à vitória para o jogador, ele não ajudará altruisticamente o oponente.
2. Sintaxe: A dGLsc estende a sintaxe da dGL modificando as modalidades. Em vez de $\langle \alpha \rangle P$ (Anjo vence $\alpha$ para alcançar $P$) e $[\alpha] Q$ (Demônio vence $\alpha$ para alcançar $Q$), a dGLsc usa $\langle \alpha \rangle (P, Q)$ e $[\alpha] (P, Q)$. Estas modalidades codificam explicitamente os objetivos de ambos os jogadores dentro da fórmula, permitindo que a lógica raciocine sobre a interação de objetivos individuais.
3. Semântica: A semântica define regiões de vitória $\varsigma_\alpha(X, Y)$ para o Anjo e $\delta_\alpha(X, Y)$ para o Demônio, onde $X$ e $Y$ são os conjuntos de objetivos. Ao contrário da dGL, estas regiões não são complementares. A semântica considera a cooperação ao incluir estados onde ambos os jogadores podem vencer simultaneamente. Por exemplo, em um jogo contínuo, a região de vitória do Demônio inclui estados onde o Anjo (que controla a evolução) interrompe o sistema em um ponto onde ambos os objetivos são atendidos. As semáticas para jogos de repetição ($\alpha^*$) são definidas via pontos fixos que distinguem entre cenários competitivos e cooperativos, utilizando o ponto fixo inferior para o Anjo e o ponto fixo superior para o Demônio para garantir unicidade e monotonicidade.
4. Cálculo de Prova: É apresentado um cálculo de prova são e relativamente completo. Ele inclui axiomas para cada operador de jogo híbrido (atribuição, evolução contínua, teste, escolha, sequência, dual, repetição) adaptados à estrutura de dois objetivos. Crucialmente, o cálculo inclui uma Regra de Ponto Fixo (FP) que caracteriza jogos de repetição como a união de dois pontos fixos inferiores (um para competição, um para cooperação). O sistema também inclui regras de monotonicidade e um axioma de determinância para casos onde os objetivos são complementares.

Principais Contribuições

• Lógica Formal dGLsc: A introdução de uma lógica especificamente para jogos híbridos de não-soma zero com dinâmicas contínuas, permitindo a verificação de sistemas críticos de segurança onde os agentes possuem objetivos sobrepostos, mas distintos.
• Semântica Semi-Competitiva: Um novo framework semântico onde os jogadores agem cooperativamente se isso auxiliar seu próprio sucesso, resolvendo a tensão entre otimização individual e segurança mútua sem exigir protocolos de negociação explícitos.
• Propriedades Teóricas:
  • Monotonicidade: Provado que aumentar o conjunto de objetivos de um jogador expande sua região de vitória.
  • Equivalência à dGL: Demonstrado que quando os objetivos são complementares (opostos), a dGLsc reduz-se à dGL padrão de soma zero.
  • Equivalência Geral: Mostrou que qualquer região de vitória dGLsc pode ser expressa como uma disjunção de regiões de vitória em um jogo dGL transformado (removendo operadores duais) e um jogo dGL padrão, provando a expressividade da lógica.
• Cálculo de Prova: Um cálculo são e relativamente completo que evita a necessidade de codificação manual de conceitos de não-soma zero (o que seria necessário se utilizasse a dGL padrão) e suporta o raciocínio modular.

Resultados
O artigo estabelece a correção do cálculo de prova, garantindo que todas as fórmulas provadas são válidas. Ele demonstra ainda a completude relativa, mostrando que qualquer fórmula válida em dGLsc pode ser provada se a lógica de primeira ordem subjacente for diferencialmente expressiva. O artigo ilustra a utilidade da dGLsc através de um exemplo canônico de dois aviões trocando estoques de combustível. Neste cenário, a dGL padrão falharia em verificar a segurança porque os agentes não conseguem controlar as variáveis críticas para o objetivo do outro. No entanto, a dGLsc verifica com sucesso a segurança da interação porque a semântica semi-competitiva permite que os agentes cooperem (ex: o Anjo abastecendo o tanque do Demônio) para garantir que ambos alcancem seus respectivos alvos.

Significância
O artigo afirma que a dGLsc fornece uma maneira natural e intuitiva de expressar e raciocinar sobre jogos híbridos de não-soma zero, que são prevalentes em CPS multi-agente, mas difíceis de verificar sob suposições conservadoras de soma zero. Ao formalizar o comportamento semi-competitivo, a lógica permite provas de segurança para situações que seriam inseguras sob suposições de soma zero, mas que são seguras na realidade devido ao potencial de cooperação. O trabalho preenche a lacuna entre os conceitos de equilíbrio de não-soma zero da teoria dos jogos e a verificação formal de sistemas híbridos com dinâmicas contínuas, oferecendo uma ferramenta que é mais precisa que modelos adversariais, mantendo-se computacionalmente tratável em comparação com abordagens gerais de teoria dos jogos.