Résumé Technique : Surveillance des diamètres de graphes de communication causale avec la logique spatio-temporelle

1. Énoncé du problème

La vérification des systèmes multi-agents (SMA) opérant dans un espace et un temps continus fait face à des défis importants en raison de la nature dynamique de leurs topologies de communication. Dans des systèmes tels que les flottes de véhicules autonomes ou les essaims de drones, les liens de communication ne sont pas statiques ; ils évoluent à mesure que les agents se déplacent, créant des chaînes de communication causales où le flux d'informations est intrinsèquement dirigé et dépendant du temps.

Les méthodes de vérification formelle existantes peinent souvent à gérer ces dynamiques. Bien que la µ-TGL (Logique de Graphe Temporelle avec point fixe) offre un cadre pour exprimer des propriétés spatio-temporelles entrelacées via des opérateurs de point fixe, elle possède une limitation critique : elle manque d'expressivité pour analyser la accessibilité au sein de bornes de distance spécifiques ou pour suivre la longueur et le coût des chaînes de communication. Plus précisément, la µ-TGL classique ne peut pas contraindre la propagation spatiale de l'information (par exemple, limiter une chaîne à un nombre spécifique de sauts ou à un coût spatial maximal). Cette capacité est fondamentale pour la surveillance décentralisée et l'analyse des protocoles distribués (tels que le consensus ou l'allocation de tâches), où la complexité algorithmique et la consommation de ressources (énergie, cycles de communication) sont directement liées au diamètre du graphe de communication.

2. Méthodologie

Les auteurs proposent une extension de la µ-TGL ainsi qu'un algorithme de surveillance hors ligne correspondant pour répondre à ces limitations.

2.1 Extension de la logique : L'horizon spatial

La contribution centrale est l'introduction d'un nouvel opérateur, l'horizon spatial ($\bullet_s \phi$), qui reflète l'horizon temporel ($H_h \phi$) existant dans la µ-TGL.

• Syntaxe : La grammaire est étendue pour inclure $\bullet_s \phi$, où $s$ est un nombre réel non négatif représentant un budget spatial (ex: distance ou coût de communication).
• Sémantique : La sémantique est étendue d'une fonction de type $\mathbb{R}_{\ge 0} \times \mathbb{R} \times A \to \mathbb{3}$ (temps, budget temporel, agent) à $\mathbb{R}_{\ge 0} \times \mathbb{R} \times \mathbb{R} \times A \to \mathbb{3}$, ajoutant un paramètre d'horizon spatial.
  • La sémantique suit explicitement les budgets de temps et d'espace.
  • La modalité spatiale ($\Diamond_D$) est redéfinie pour respecter le budget d'espace : un lien entre agents n'est valide que si son poids tombe dans l'intervalle cible $D$ et ne dépasse pas le budget d'espace restant.
  • L'opérateur d'horizon spatial $\bullet_s$ agit comme une contrainte : il évalue la formule interne avec un budget d'espace $s$. Si la formule nécessite plus d'espace que $s$ pour être déterminée, le résultat peut être indéterminé ($\top\bot$) ou faux, selon le contexte.
• Expressivité : Cette extension permet de coder des propriétés globales comme Reach (connectivité dans une borne de coût) et Escape (propagation au-delà d'une borne de coût) de manière causale et temporelle, ce qui n'était possible auparavant que dans des logiques non temporelisées comme STREL.

2.2 Algorithme de surveillance

Le document présente un algorithme de surveillance centralisé hors ligne capable d'évaluer ces spécifications étendues.

• Structure de données : L'algorithme opère sur des "signaux discrets", représentant le graphe temporel comme une séquence d'échantillons où le graphe est constant par morceaux entre les étapes de temps. La sortie est une structure de signal imbriquée représentant les valeurs de vérité sur le temps, l'horizon temporel et l'horizon spatial.
• Terminaison et bornage : Un défi technique majeur est d'assurer la terminaison des calculs de point fixe en présence d'exigences d'information non bornées.
  • Les auteurs prouvent que pour un horizon temporel $T$ borné et un horizon spatial $s$ borné, le calcul ne nécessite qu'une quantité finie d'informations.
  • Ils construisent des ensembles finis de points temporels, de budgets temporels et de budgets spatiaux dérivés de la structure de la formule et du signal d'entrée.
  • En restreignant le calcul à ces ensembles finis, ils prouvent que les itérations de point fixe se terminent en un nombre fini d'étapes.
• Sémantique à trois valeurs : L'algorithme utilise une logique à trois valeurs ($\top, \bot, \top\bot$) pour gérer les situations où les observations sont insuffisantes pour déterminer la satisfaction ou la violation, une nécessité pour les scénarios de surveillance en ligne.

3. Contributions clés

1. Extension syntaxique et sémantique : L'introduction de l'opérateur d'horizon spatial ($\bullet_s$) à la µ-TGL, permettant la spécification de chaînes de communication causales spatialement bornées.
2. Preuve d'expressivité : Démonstration que la logique étendue peut encoder des modalités telles que Reach et Escape dans un contexte causal et temporel, augmentant strictement l'expressivité par rapport à la µ-TGL classique.
3. Garantie de terminaison : Une preuve formelle que l'algorithme de surveillance se termine pour des horizons de temps et d'espace bornés, malgré la présence d'opérateurs de point fixe et la nécessité de suivre les budgets spatiaux.
4. Implémentation et étude de cas : Implémentation de l'algorithme en OCaml et son application aux algorithmes de regroupement basés sur le consensus (CBBA), un protocole distribué pour l'allocation de tâches.

4. Résultats

Les auteurs ont évalué leur approche à l'aide de simulations de 10 agents effectuant une allocation de tâches dans une zone 2D.

• Surveillance du diamètre : L'algorithme a surveillé avec succès le diamètre du graphe de communication causale au fil du temps. Il a identifié des intervalles temporels spécifiques où le graphe était entièrement connecté (diamètre $\le 6$) et des intervalles où la connectivité était clairsemée (le diamètre n'atteignant jamais 1, soit pas un clique).
• Analyse de la longueur de chaîne : Le système a surveillé la longueur maximale des chaînes de communication nécessaires pour que les agents atteignent une cible spécifique, fournissant des informations sur l'efficacité du protocole distribué.
• Scalabilité :
  • Pour 10 agents, la surveillance a pris en moyenne 267 secondes pour une trace d'environ 12 000 étapes temporelles (environ 0,022s par étape de temps).
  • Les tests de scalabilité faisant varier le nombre d'agents ($n \in [3, 50]$) ont montré que la surveillance d'une spécification bornée par $n/2$ passe bien jusqu'à 30 agents (moyenne de 17ms par étape de temps).
  • Pour 50 agents, le temps est passé à 142ms par étape de temps. Les auteurs notent que bien que cela soit acceptable pour des systèmes physiques à faible vélocité, la surveillance du diamètre global (nécessitant des vérifications pour tous les agents) serait trop coûteuse en termes de calcul pour des systèmes de plus grande envergure.

5. Signification et affirmations

Le papier affirme que ce travail comble une lacune fondamentale dans la vérification formelle des systèmes multi-agents mobiles et distribués. En permettant la spécification et la surveillance de diamètres de communication causale bornés, la logique fournit un outil pour vérifier des métriques de performance critiques (comme le nombre de cycles de protocole et la consommation d'énergie) qui dépendent de la topologie du graphe.

Les auteurs soulignent que, bien que l'implémentation actuelle soit un algorithme hors ligne, la conception soignée de la sémantique (notamment la gestion des valeurs indéterminées et des horizons) pose les bases d'une surveillance en ligne. Ils positionnent cela comme une étape vers l'intégration de cette logique dans les boucles de contrôle en tant que "bouclier de sécurité" ou pour le filtrage en temps réel des décisions dans les systèmes décentralisés. Le travail ne prétend pas résoudre les problèmes de scalabilité de la surveillance entièrement centralisée pour les systèmes à grande échelle, mais démontre la faisabilité pour des systèmes de taille modérée et met en évidence la voie vers une surveillance décentralisée où chaque agent surveille ses propres contraintes de connectivité locale.