Semi-Competitive Differential Game Logic

Sintesi Tecnica: Logica di Gioco Differenziale Semi-Competitiva (dGLsc)

Definizione del Problema
La verifica della sicurezza dei Sistemi Cyber-Fisici (CPS), in particolare quelli che coinvolgono l'interazione tra più agenti (ad esempio, veicoli autonomi, aeroplani), presenta sfide significative. Gli approcci tradizionali spesso modellano queste interazioni utilizzando la Logica di Gioco Differenziale (dGL), che assume una relazione zero-somma e avversaria in cui il guadagno di un giocatore è la perdita dell'altro. Sebbene ciò fornisca risultati sicuri, è spesso eccessivamente conservativo. In molti scenari del mondo reale, come l'evitamento delle collisioni, gli agenti condividono obiettivi di sicurezza (ad esempio, nessuno dei due vuole schiantarsi) pur perseguendo obiettivi individuali distinti (ad esempio, raggiungere destinazioni diverse). Un'assunzione zero-somma non riesce a catturare il potenziale di cooperazione in questi giochi "non a somma zero", portando al fallimento della verifica di sistemi che sono in realtà sicuri. Inoltre, le logiche non a somma zero esistenti spesso faticano con la dinamica continua o richiedono alberi di gioco complessi che sono intrattabili per sistemi ibridi con profondità illimitata.

Metodologia
Il documento introduce la Logica di Gioco Differenziale Semi-Competitiva (dGLsc), una logica formale progettata per verificare giochi ibridi in cui due giocatori (Angelo e Demone) possiedono obiettivi individuali, potenzialmente sovrapponibili. La metodologia centrale si basa sul concetto di semi-competitività:

1. Modello Comportamentale: I giocatori cooperano quando è utile per entrambi raggiungere i rispettivi obiettivi, ma competono quando necessario. Specificamente, un giocatore non perderà mai intenzionalmente. Se esistono molteplici opzioni di vittoria, un giocatore ne sceglie una che aiuti anche l'avversario a vincere. Se nessuna opzione porta alla vittoria per il giocatore, questi non aiuterà altruisticamente l'avversario.
2. Sintassi: La dGLsc estende la sintassi della dGL modificando le modalità. Invece di $\langle \alpha \rangle P$ (l'Angelo vince $\alpha$ per raggiungere $P$) e $[\alpha] Q$ (il Demone vince $\alpha$ per raggiungere $Q$), la dGLsc utilizza $\langle \alpha \rangle (P, Q)$ e $[\alpha] (P, Q)$. Queste modalità codificano esplicitamente entrambi gli obiettivi dei giocatori all'interno della formula, permettendo alla logica di ragionare sull'interazione di obiettivi individuali.
3. Semantica: La semantica definisce le regioni di vittoria $\varsigma_\alpha(X, Y)$ per l'Angelo e $\delta_\alpha(X, Y)$ per il Demone, dove $X$ e $Y$ sono gli insiemi degli obiettivi. A differenza della dGL, queste regioni non sono complementari. La semantica tiene conto della cooperazione includendo stati in cui entrambi i giocatori possono vincere simultaneamente. Ad esempio, in un gioco continuo, la regione di vittoria del Demone include stati in cui l'Angelo (che controlla l'evoluzione) ferma il sistema in un punto in cui entrambi gli obiettivi sono soddisfatti. La semantica per i giochi di ripetizione ($\alpha^*$) è definita tramite punti fissi che distinguono tra scenari competitivi e cooperativi, utilizzando il punto fisso inferiore per l'Angelo e il punto fisso superiore per il Demone per garantire unicità e monotonicità.
4. Calcolo delle Prove: Viene presentato un calcolo delle prove sano e relativamente completo. Include assiomi per ogni operatore di gioco ibrido (assegnazione, evoluzione continua, test, scelta, sequenza, duale, ripetizione) adattati alla struttura a due obiettivi. Fondamentalmente, il calcolo include una Regola di Punto Fisso (FP) che caratterizza i giochi di ripetizione come l'unione di due punti fissi inferiori (uno per la competizione, uno per la cooperazione). Il sistema include anche regole di monotonicità e un assioma di determinazione per i casi in cui gli obiettivi sono complementari.

Contributi Chiave

• Logica Formale dGLsc: L'introduzione di una logica specificamente progettata per giochi ibridi non a somma zero con dinamiche continue, consentendo la verifica di sistemi critici per la sicurezza in cui gli agenti hanno obiettivi sovrapponibili ma distinti.
• Semantica Semi-Competitiva: Un nuovo framework semantico in cui i giocatori agiscono cooperativamente se ciò favorisce il proprio successo, risolvendo la tensione tra ottimizzazione individuale e sicurezza mutua senza richiedere protocolli di negoziazione espliciti.
• Proprietà Teoriche:
  • Monotonicità: È stato dimostrato che l'aumento dell'insieme degli obiettivi di un giocatore espande la sua regione di vittoria.
  • Equivalenza a dGL: È stato dimostrato che quando gli obiettivi sono complementari (opposti), la dGLsc si riduce alla dGL standard a somma zero.
  • Equivalenza Generale: È stato mostrato che qualsiasi regione di vittoria dGLsc può essere espressa come una disgiunzione di regioni di vittoria in un gioco dGL trasformato (rimuovendo gli operatori duali) e in un gioco dGL standard, dimostrando l'espressività della logica.
• Calcolo delle Prove: Un calcolo sano e relativamente completo che evita la necessità di codifica manuale di concetti non a somma zero (che sarebbe necessaria se si utilizzasse la dGL standard) e supporta il ragionamento modulare.

Risultati
Il documento stabilisce la correttezza del calcolo delle prove, garantendo che tutte le formule dimostrate siano valide. Dimostra inoltre la completezza relativa, mostrando che qualsiasi formula valida in dGLsc può essere dimostrata se la logica del primo ordine sottostante è differenzialmente espressiva. Il documento illustra l'utilità della dGLsc attraverso un esempio canonico di due aerei che scambiano scorte di carburante. In questo scenario, la dGL standard fallirebbe la verifica della sicurezza perché gli agenti non possono controllare le variabili critiche per l'obiettivo dell'altro. Tuttavia, la dGLsc verifica con successo la sicurezza dell'interazione perché la semantica semi-competitiva permette agli agenti di cooperare (ad esempio, l'Angelo riempie il serbatoio del Demone) per garantire che entrambi raggiungano i rispettivi obiettivi.

Significato
L'articolo sostiene che la dGLsc fornisce un modo naturale e intuitivo per esprimere e ragionare su giochi ibridi non a somma zero, che sono prevalenti nei CPS multi-agente ma difficili da verificare sotto assunzioni zero-somma conservative. Formalizzando il comportamento semi-competitivo, la logica consente prove di sicurezza per situazioni che sarebbero insicure sotto assunzioni zero-somma, ma sicure nella realtà grazie al potenziale di cooperazione. Il lavoro colma il divario tra i concetti di teoria del gioco degli equilibri non a somma zero e la verifica formale di sistemi ibridi con dinamiche continue, offrendo uno strumento che è più preciso dei modelli avversari pur rimanendo computazionalmente trattabile rispetto agli approcci generali della teoria dei giochi.