Résumé Technique : Certificats de Barrière Co-Büchi pour les Systèmes Dynamiques à Temps Discret

Définition du Problème

L'article traite du défi de la vérification des systèmes dynamiques à temps discret par rapport aux propriétés $\omega$-régulières, spécifiquement celles qui exigent la preuve qu'un ensemble spécifique d'états (ou une région) n'est visité que fini de fois. La vérification de sûreté traditionnelle garantit qu'un système n'entre jamais dans un ensemble non sûr. Cependant, de nombreuses propriétés de logique temporelle (par exemple, celles spécifiées par des automates universels de Co-Büchi ou le complément d'automates de Büchi) nécessitent de démontrer qu'un système ne visite pas un état acceptant une infinité de fois.

Les approches existantes font face à des limitations significatives :

1. Approche par Triplets d'États : Les méthodes précédentes (par exemple, Wongpiromsarn et al.) utilisent des certificats de barrière pour « couper » les chemins dans un automate en brisant les triplets d'états. Bien qu'efficace pour les automates de mots finis ou les langages co-sûrs, cette approche est conservatrice et échoue souvent pour les automates de mots infinis généraux. Elle ne peut pas vérifier des systèmes dont les traces atteignent un état acceptant plus de deux fois, même si le nombre total de visites est fini.
2. Limitations de la Synthèse Bornée : Bien que la synthèse bornée convertisse les spécifications LTL en problèmes de sûreté en bornant les visites d'états, les techniques standards nécessitent souvent le déploiement de l'automate ou traitent des constructions de produits complexes qui manquent de garanties incrémentales.
3. Complexité : Le model checking traditionnel sur des espaces continus souffre de la malédiction de la dimensionnalité, tandis que les méthodes de certificats de barrière existantes pour la logique temporelle reposent souvent sur des modèles spécifiques ou manquent de garanties de nécessité.

Le problème central est de développer une surapproximation fonctionnelle (un certificat) qui prouve que les traces d'un système visitent une région spécifique un nombre limité de fois, sans construire explicitement le produit complet du système ou déployer l'automate indéfiniment.

Méthodologie

Les auteurs proposent des Certificats de Barrière Co-Büchi (CBBC), une généralisation des classiques certificats de barrière. La méthodologie repose sur les étapes conceptuelles et computationnelles suivantes :

1. Cadre Conceptuel : La Visitation Bornée comme Sûreté

L'idée centrale est que, bien que « visiter une région un nombre fini de fois » ne soit pas une propriété de sûreté directe, cela peut être transformé en une telle en augmentant le système avec un compteur.

• Système Étendu : Le système original $S$ est conceptuellement étendu à $S'$ en ajoutant un compteur $\ell$ qui s'incrémente chaque fois que le système entre dans la région cible $X_{VF}$.
• Réduction à la Sûreté : Prouver que $X_{VF}$ est visitée un nombre fini de fois est équivalent à prouver que le système étendu $S'$ n'atteint jamais un état où le compteur dépasse une borne fixe $k$. Cela transforme le problème en un problème standard de vérification de sûreté sur l'espace d'états étendu.

2. Définition des CBBC

Un Certificat de Barrière Co-Büchi est une fonction $B: X \times [0..k] \to \mathbb{R}$ qui satisfait des conditions spécifiques garantissant que le compteur ne dépasse jamais $k$ :

• Condition Initiale : $B(x, 0) \le 0$ pour tous les états initiaux.
• Condition d'Insécurité : $B(x, k) > 0$ pour tous les états dans la région cible $X_{VF}$ (indiquant que l'atteinte de la région avec un compteur de $k$ est « non sûre »).
• Étape Inductive :
  • Si le système n'est pas dans $X_{VF}$, la valeur de $B$ doit être non croissante (le compteur reste identique).
  • Si le système est dans $X_{VF}$, la valeur de $B$ à l'étape suivante (avec le compteur incrémenté) doit être non croissante par rapport à l'étape actuelle.

L'article prouve que l'existence d'une telle fonction est à la fois suffisante et nécessaire (sous hypothèses d'oracle) pour que le système visite la région au plus $k$ fois.

3. Vérification par Théorie des Automates

Pour vérifier des propriétés spécifiées par un Automate Universel de Co-Büchi (UCA) $A_{c,k}$ :

• Le système $S$ est synchronisé avec l'automate pour former un système produit.
• La région « non sûre » pour le CBBC est définie comme l'ensemble des états du produit où l'automate est dans un état acceptant.
• L'algorithme de vérification recherche un CBBC avec une borne $k$. Si trouvé, le système satisfait la propriété. Sinon, $k$ est incrémenté et la recherche se répète. Cela fournit une approche de vérification incrémentale.

4. Approches Computationnelles

L'article présente deux méthodes pour calculer les CBBC :

1. Approche Somme de Carrés (SOS) : Suppose que la dynamique du système et les ensembles d'états sont semi-algébriques (définis par des inégalités polynomiales). La recherche du certificat de barrière est formulée comme un problème de programmation semi-définie (SDP). La complexité est polynomiale par rapport à la dimension de l'espace d'états (en supposant un modèle de degré polynomial fixe) et linéaire par rapport à la borne $k$.
2. Approche Basée sur SMT (CEGIS) : Utilise la Synthèse Inductive Guidée par Contre-exemple. Elle échantillonne des points de l'espace d'états, encode les contraintes du CBBC sous forme de requêtes de Satisfiabilité Modulo Theories (SMT) sur l'arithmétique réelle linéaire, et affine itérativement le certificat candidat à l'aide de contre-exemples jusqu'à ce qu'une fonction valide soit trouvée ou qu'un délai d'attente (timeout) survienne.

Principales Contributions

1. Nouvelle Définition de Certificat : L'introduction des Certificats de Barrière Co-Büchi (CBBC), qui généralisent les classiques certificats de barrière pour gérer les propriétés de « visitation finie » en incorporant une variable de compteur directement dans la fonction de certificat.
2. Garanties Théoriques : L'article établit que les CBBC sont non seulement des conditions suffisantes mais aussi nécessaires pour vérifier les propriétés de visitation bornée, une affirmation plus forte que de nombreuses méthodes de vérification temporelle existantes.
3. Généralisation de l'Approche par Triplets d'États : Les auteurs démontrent que l'approche par CBBC englobe l'approche par « triplet d'états ». Ils fournissent une preuve constructive montrant que si un système peut être vérifié via la méthode du triplet d'états, il peut aussi être vérifié via les CBBC, mais la réciproque n'est pas vraie (les CBBC peuvent vérifier des systèmes que la méthode du triplet ne peut pas).
4. Stratégie de Vérification Incrémentale : La méthodologie proposée permet une recherche incrémentale de la borne $k$. L'algorithme commence avec $k=0$ et augmente la borne uniquement lorsqu'un certificat ne peut être trouvé, offrant un compromis pratique entre coût computationnel et puissance de vérification.
5. Cadres Computationnels : La fourniture d'algorithmes tant basés sur SOS (pour les systèmes polynomiaux) que sur SMT (pour les systèmes généraux) pour synthétiser ces certificats.

Résultats et Études de Cas

L'article valide l'approche à travers trois études de cas :

1. Modèle de Température d'une Pièce (Échec du Triplet d'États) : Un système où l'approche par triplet d'états échoue en raison de labels chevauchants sur les arêtes de l'automate (spécifiquement, l'incapacité de couper les chemins avec des labels répétés). L'approche CBBC a réussi à trouver un certificat avec $k=4$, prouvant que la propriété est respectée là où la méthode précédente était non concluante.
2. Oscillateur de Van der Pol 2D : Un système non linéaire vérifié contre un UCA. En utilisant l'approche SOS, un CBBC de degré 6 a été trouvé avec $k=3$ en environ 5 minutes, prouvant que les états acceptants sont visités au plus 3 fois.
3. Oscillateur de Kuramoto 3D : Un système de dimension supérieure avec une dynamique trigonométrique (approximée par un développement de Taylor). Un CBBC de degré 4 a été trouvé avec $k=2$ en environ 20 minutes, vérifiant la visitation finie d'une région spécifique.

Signification et Revendications

L'article affirme que les CBBC fournissent un cadre robuste et sans abstraction pour la vérification des propriétés $\omega$-régulières sur les systèmes dynamiques à temps discret. Sa signification réside dans :

• Surmonter le Conservatisme : Il répond aux limitations de l'approche par triplet d'états, qui est souvent trop conservatrice pour les automates de mots infinis généraux.
• Scalabilité : En évitant la construction explicite de produits d'automates complexes avec de grands espaces d'états et en s'appuyant sur des surapproximations fonctionnelles, la méthode passe à l'échelle de manière polynomiale avec la dimension de l'état (pour des modèles fixes), atténuant la malédiction de la dimensionnalité.
• Nécessité : Contraৰ aux approches heuristiques, l'article soutient la nécessité de ces certificats, suggérant que si un système satisfait la propriété, un CBBC existe théoriquement.

Les auteurs notent que bien que les CBBC soient efficaces pour la vérification, leur application à la synthèse (conception de contrôleur) reste complexe en raison des difficultés liées au non-déterminisme et au besoin d'automates déterministes pour les problèmes de réalisabilité. Ils identifient cela comme une direction pour des travaux futurs, parallèlement à l'extension de l'approche aux automates pondérés, stochastiques et temporellement étendus.