The Complexity of Second-order HyperLTL

1. Problématique et Contexte

Contexte :
Les propriétés hyper-temporelles (hyperproperties) relient plusieurs exécutions d'un système et sont essentielles pour la vérification de propriétés de sécurité et d'information (ex: non-interférence, confidentialité). Le HyperLTL a été introduit pour spécifier ces propriétés en ajoutant une quantification du premier ordre sur les traces. Bien que le modèle-checking du HyperLTL soit décidable (complet pour la classe Tower), sa satisfiabilité est $\Sigma^1_1$-complète (très indécidable).

Cependant, le HyperLTL ne peut pas exprimer certaines propriétés cruciales comme la connaissance commune dans les systèmes multi-agents ou les propriétés hyper-temporelles asynchrones. Pour pallier cela, Beutner et al. ont introduit le Hyper2LTL, qui étend le HyperLTL par une quantification du second ordre sur les ensembles de traces.

Problème :
La complexité exacte de la vérification du Hyper2LTL (satisfiabilité, satisfiabilité sur les systèmes finis, et modèle-checking) était inconnue. Bien que le modèle-checking ait été montré comme étant $\Sigma^1_1$-difficile, aucune borne supérieure n'était établie. De plus, il était unclear si les fragments restreints (quantification sur les ensembles minimaux/maximaux ou points fixes) réduisaient significativement cette complexité.

2. Méthodologie

Les auteurs adoptent une approche basée sur la théorie des modèles et la hiérarchie arithmétique/analytique pour classifier la complexité des problèmes indécidables.

Outils clés :

• Hiérarchie Arithmétique et Analytique : Utilisation des classes de complexité basées sur la vérité dans l'arithmétique d'ordre $k$ (ici, ordre 2 et ordre 3).
  • $\Sigma^1_1$ : Vérité dans l'arithmétique du second ordre.
  • $\Sigma^2_1$ : Vérité dans l'arithmétique du troisième ordre.
• Encodage des ensembles : Construction de formules qui forcent les modèles à contenir des ensembles de traces de cardinalité spécifique (dénombrable ou non-dénombrable).
  • Le HyperLTL ne possède que des modèles dénombrables.
  • Le Hyper2LTL permet d'encoder des ensembles de nombres naturels (traces) et des ensembles d'ensembles de nombres naturels (ensembles de traces), simulant ainsi des objets de type 2.
• Arbres de témoins (Witness Trees) : Pour les fragments à point fixe, les auteurs utilisent des arbres finis étiquetés par des traces pour caractériser l'appartenance à un point fixe, évitant ainsi une quantification explicite sur des ensembles infinis dans la réduction.
• Sémantique "Closed-World" : Introduction d'une sémantique où les quantificateurs du second ordre ne parcourent que les sous-ensembles du modèle (par opposition à l'ensemble de toutes les traces possibles), afin d'analyser l'impact de cette restriction.

3. Contributions Clés et Résultats

Les auteurs déterminent la complexité exacte pour le Hyper2LTL complet et deux de ses fragments principaux, sous deux sémantiques (standard et "closed-world").

A. Hyper2LTL Complet

Pour le langage complet avec quantification du second ordre arbitraire :

• Satisfiabilité, Satisfiabilité sur systèmes finis, et Modèle-checking sont tous équivalents à la vérité dans l'arithmétique du troisième ordre (niveau $\Sigma^2_1$ de la hiérarchie analytique).
• Résultat surprenant : La satisfiabilité sur les systèmes finis est aussi difficile que la satisfiabilité générale. Contrairement au HyperLTL où la satisfiabilité sur systèmes finis est $\Sigma^0_1$-complète (récursivement énumérable), ici, la quantification sur les ensembles de traces permet de simuler l'arithmétique du troisième ordre même avec un système de transition fini (car l'ensemble des traces d'un système fini peut être infini/non-dénombrable).

B. Fragment Hyper2LTL$_{mm}$ (Minimaux/Maximaux)

Ce fragment restreint la quantification du second ordre aux ensembles minimaux ou maximaux satisfaisant une garde.

• Résultat : La complexité reste inchangée. Les trois problèmes sont toujours équivalents à la vérité dans l'arithmétique du troisième ordre.
• Implication : Restreindre la quantification aux ensembles extremaux ne suffit pas à réduire la complexité.

C. Fragment lfp-Hyper2LTL$_{mm}$ (Points Fixes)

Ce fragment restreint davantage la quantification aux points fixes minimaux de fonctions définies par le HyperLTL.

• Sous sémantique standard :
  • Satisfiabilité : $\Sigma^2_1$-complète.
  • Satisfiabilité sur systèmes finis et Modèle-checking : Équivalents à la vérité dans l'arithmétique du second ordre ($\Sigma^1_1$).
• Sous sémantique "Closed-World" (C-W) :
  • Satisfiabilité : $\Sigma^1_1$-complète (équivalente au HyperLTL).
  • Satisfiabilité sur systèmes finis et Modèle-checking : $\Sigma^1_1$-complète.
• Analyse : La restriction aux points fixes combinée à la sémantique "closed-world" (où l'on ne quantifie que sur les sous-ensembles du modèle) force l'existence de modèles dénombrables, ramenant la complexité de la satisfiabilité au niveau du HyperLTL.

D. Sémantique Closed-World

L'article introduit et analyse cette sémantique où les quantificateurs du second ordre ne parcourent que les sous-ensembles du modèle donné.

• Pour la plupart des cas, la complexité est identique à la sémantique standard.
• L'exception majeure est la satisfiabilité du fragment lfp sous sémantique C-W, qui devient significativement plus simple ($\Sigma^1_1$).

4. Tableau Récapitulatif des Complexités

Logique	Satisfiabilité	Satisfiabilité (Syst. Finis)	Modèle-Checking
HyperLTL	$\Sigma^1_1$-complet	$\Sigma^0_1$-complet	Tower-complet
Hyper2LTL (Standard)	$\Sigma^2_1$-complet (T3A)	$\Sigma^2_1$-complet (T3A)	$\Sigma^2_1$-complet (T3A)
Hyper2LTL$_{mm}$	$\Sigma^2_1$-complet (T3A)	$\Sigma^2_1$-complet (T3A)	$\Sigma^2_1$-complet (T3A)
lfp-Hyper2LTL$_{mm}$ (Std)	$\Sigma^2_1$-complet	$\Sigma^1_1$-complet (T2A)	$\Sigma^1_1$-complet (T2A)
lfp-Hyper2LTL$_{mm}$ (C-W)	$\Sigma^1_1$-complet	$\Sigma^1_1$-complet	$\Sigma^1_1$-complet

(T3A = Arithmétique du 3ème ordre, T2A = Arithmétique du 2ème ordre)

5. Signification et Impact

1. Coût de l'expressivité : L'article démontre que l'ajout de la quantification du second ordre sur les ensembles de traces augmente drastiquement la complexité de la vérification, la faisant passer d'une classe indécidable mais "accessible" ($\Sigma^1_1$) à une classe beaucoup plus haute ($\Sigma^2_1$), rendant la vérification complète théoriquement impossible pour les cas généraux.
2. Limites des fragments : La restriction aux ensembles minimaux/maximaux (Hyper2LTL$_{mm}$) ne réduit pas la complexité. Seule la restriction aux points fixes (lfp) apporte une réduction, mais celle-ci dépend fortement de la sémantique utilisée.
3. Importance de la sémantique : La distinction entre sémantique standard (quantification sur tous les ensembles de traces possibles) et "closed-world" (quantification sur les sous-ensembles du modèle) est cruciale pour la satisfiabilité du fragment lfp. Cela suggère que pour les applications pratiques où l'on s'intéresse à un système donné, l'approche "closed-world" pourrait offrir des perspectives de vérification plus réalistes.
4. Fondements théoriques : Ce travail établit une base solide pour comprendre les limites de la vérification des hyperpropriétés avancées et guide les chercheurs vers l'utilisation de fragments plus restreints (comme lfp sous sémantique C-W) pour des applications pratiques, tout en avertissant de l'indécidabilité inhérente des versions complètes.

En conclusion, ce papier résout des problèmes ouverts majeurs en théorie de la vérification, montrant que la généralisation du HyperLTL vers le second ordre rend la vérification extrêmement difficile, mais identifie des sous-ensembles (points fixes, sémantique fermée) qui, bien que toujours indécidables, sont plus gérables théoriquement.