Semi-Competitive Differential Game Logic

Résumé Technique : Logique de Jeu Différentiel Semi-Compétitive (dGLsc)

Énoncé du Problème
La vérification de la sûreté des Systèmes Cyber-Physiques (CPS), particulièrement ceux impliquant des interactions entre plusieurs agents (par exemple, des véhicules autonomes, des avions), présente des défis importants. Les approches traditionnelles modélisent souvent ces interactions à l'aide d'une logique de jeu différentiel (dGL), qui suppose une relation de somme nulle et antagoniste où le gain d'un joueur est la perte de l'autre. Bien que cela produise des résultats sûrs, c'est souvent excessivement conservateur. Dans de nombreux scénarios réels, tels que l'évitement de collisions, les agents partagent des objectifs de sûreté (par exemple, aucun ne veut s'écraser) tout en poursuivant des buts individuels distincts (par exemple, atteindre des destinations différentes). Une hypothèse de somme nulle ne parvient pas à capturer le potentiel de coopération dans ces jeux « à somme non nulle », menant à des échecs de vérification pour des systèmes qui sont pourtant sûrs. De plus, les logiques existantes à somme non nulle peinent souvent avec les dynamiques continues ou nécessitent des arbres de jeu complexes, ce qui est impraticable pour les systèmes hybrides à profondeur non bornée.

Méthodologie
L'article introduit la Logique de Jeu Différentiel Semi-Compétitive (dGLsc), une logique formelle conçue pour vérifier des jeux hybrides où deux joueurs (l'Ange et le Démon) possèdent des objectifs individuels, potentiellement chevauchants. La méthodologie centrale repose sur le concept de semi-compétitivité :

1. Modèle de Comportement : Les joueurs coopèrent lorsqu'il est utile aux deux d'atteindre leurs objectifs respectifs, mais entrent en compétition lorsque cela est nécessaire. Plus précisément, un joueur ne perdra jamais exprès. Si plusieurs options de victoire existent, un joueur en choisit une qui aide également l'adversaire à gagner. Si aucune option ne mène à une victoire pour le joueur, celui-ci n'aide pas altruistiquement l'adversaire.
2. Syntaxe : La dGLsc étend la syntaxe de la dGL en modifiant les modalités. Au lieu de $\langle \alpha \rangle P$ (l'Ange gagne $\alpha$ pour atteindre $P$) et $[\alpha] Q$ (le Démon gagne $\alpha$ pour atteindre $Q$), la dGLsc utilise $\langle \alpha \rangle (P, Q)$ et $[\alpha] (P, Q)$. Ces modalités encodent explicitement les objectifs des deux joueurs au sein de la formule, permettant à la logique de raisonner sur l'interaction des objectifs individuels.
3. Sémantique : La sémantique définit les régions de victoire $\varsigma_\alpha(X, Y)$ pour l'Ange et $\delta_\alpha(X, Y)$ pour le Démon, où $X$ et $Y$ sont les ensembles d'objectifs. Contrairement à la dGL, ces régions ne sont pas complémentaires. La sémantique tient compte de la coopération en incluant des états où les deux joueurs peuvent gagner simultanément. Par exemple, dans un jeu continu, la région de victoire du Démon inclut des états où l'Ange (qui contrôle l'évolution) arrête le système à un point où les deux objectifs sont atteints. La sémantique pour les jeux de répétition ($\alpha^*$) est définie via des points fixes qui distinguent les scénarios compétitifs et coopératifs, utilisant le plus petit point fixe pour l'Ange et le plus grand point fixe pour le Démon afin de garantir l'unicité et la monotonie.
4. Calcul de Preuve : Un calcul de preuve sain et relativement complet est présenté. Il comprend des axiomes pour chaque opérateur de jeu hybride (affectation, évolution continue, test, choix, séquence, duel, répétition) adaptés à la structure à deux objectifs. Crucialement, le calcul inclut une Règle de Point Fixe (FP) qui caractérise les jeux de répétition comme l'union de deux plus petits points fixes (un pour la compétition, un pour la coopération). Le système comprend également des règles de monotonie et un axiome de déterminisme pour les cas où les objectifs sont complémentaires.

Contributions Clés

• Logique Formelle dGLsc : L'introduction d'une logique spécifiquement conçue pour les jeux hybrides à somme non nulle avec des dynamiques continues, permettant la vérification de systèmes critiques de sûreté où les agents ont des objectifs chevauchants mais distincts.
• Sémantique Semi-Compétitive : Un cadre sémantique novateur où les joueurs agissent de manière coopérative si cela favorise leur propre succès, résolvant la tension entre l'optimisation individuelle et la sûreté mutuelle sans nécessiter de protocoles de négociation explicites.
• Propriétés Théoriques :
  • Monotonie : Il est prouvé qu'augmenter l'ensemble des objectifs d'un joueur étend sa région de victoire.
  • Équivalence à la dGL : Il est démontré que lorsque les objectifs sont complémentaires (opposés), la dGLsc se réduit à la dGL standard à somme nulle.
  • Équivalence Générale : Montre que toute région de victoire dGLsc peut être exprimée comme une disjonction de régions de victoire dans un jeu dGL transformé (supprimant les opérateurs duaux) et un jeu dGL standard, prouvant ainsi l'expressivité de la logique.
• Calcul de Preuve : Un calcul sain et relativement complet qui évite le besoin de codage manuel des concepts à somme non nulle (ce qui serait requis si l'on utilisait la dGL standard) et supporte le raisonnement modulaire.

Résultats
L'article établit la correction du calcul de preuve, garantissant que toutes les formules prouvables sont valides. Il prouve en outre la complétude relative, montrant que toute formule valide dans la dGLsc peut être prouvée si la logique du premier ordre est différentiellement expressive. L'article illustre l'utilité de la dGLsc à travers un exemple canonique de deux avions échangeant des stocks de carburant. Dans ce scénario, la dGL standard échouerait à vérifier la sûreté car les agents ne contrôlent pas les variables critiques pour l'objectif de l'autre. Cependant, la dGLsc vérifie avec succès la sûreté de l'interaction car la sémantique semi-compétitive permet aux agents de coopérer (par exemple, l'Ange remplissant le réservoir du Démon) pour garantir que tous deux atteignent leurs cibles respectives.

Signification
L'article affirme que la dGLsc offre une manière naturelle et intuitive d'exprimer et de raisonner sur les jeux hybrides à somme non nulle, qui sont prévalents dans les CPS multi-agents mais difficiles à vérifier sous des hypothèses conservatrices de somme nulle. En formalisant le comportement semi-compétitif, la logique permet des preuves de sûreté pour des situations qui sont jugées dangereuses sous l'hypothèse de somme nulle, mais qui sont sûres en réalité grâce au potentiel de coopération. Ce travail comble le fossé entre les concepts de jeu de théorie des jeux de l'équilibre à somme non nulle et la vérification formelle des systèmes hybrides avec des dynamiques continues, offrant un outil plus précis que les modèles adverses tout en restant plus traitable par le calcul que les approches générales de la théorie des jeux.