Résumé Technique : Vérification de Modèles Symbolique utilisant des Intervalles de Vecteurs

1. Énoncé du Problème

La vérification de modèles est une technique de vérification formelle robuste pour garantir que les systèmes logiciels et matériels respectent des spécifications. Cependant, elle est sévèrement entravée par le problème d'explosion de l'espace d'états, où le nombre d'états et de transitions possibles croît exponentiellement avec la taille du système. Ce défi est particulièrement aigu dans la vérification de modèles globale, où l'objectif est d'identifier tous les états satisfaisant une formule de logique d'arbre de calcul (CTL), plutôt que de vérifier une seule configuration.

Les techniques existantes, telles que les diagrammes de décision (DD), les abstractions et la réduction d'ordre partiel, atténuent ce problème mais font face à des limites à mesure que les modèles deviennent plus sophistiqués. Spécifiquement, les approches classiques basées sur les intervalles (par exemple, les diagrammes de décision d'intervalles) encodent des ensembles de vecteurs sous forme de vecteurs d'intervalles. Cet article soutient qu'une approche plus efficace pour les réseaux de Petri consiste à encoder les ensembles de marquages en utilisant des intervalles généralisés de vecteurs (intervalles de vecteurs), plutôt que des vecteurs d'intervalles. Cette distinction est cruciale car les espaces vectoriels impliquent souvent des ordres partiels non totaux, rendant les définitions d'intervalles simples insuffisantes.

2. Méthodologie

Les auteurs proposent une nouvelle structure symbolique appelée Ensembles de Vecteurs Symboliques (SVS - Symbolic Vector Sets) pour encoder les ensembles de marquages de réseaux de Petri. La méthodologie repose sur trois piliers fondamentaux :

2.1. Vecteurs et Ensembles Symboliques

Un Vecteur Symbolique est défini comme une paire $(a, b)$, où $a$ et $b$ sont des ensembles de vecteurs (marquages).

• Inclusion ($a$) : Un marquage $q$ appartient au vecteur symbolique s'il inclut tous les vecteurs de $a$ (sous un ordre partiel non strict $\subseteq_f$).
• Exclusion ($b$) : Un marquage $q$ appartient au vecteur symbolique s'il n'inclut aucun vecteur de $b$.
• Généralisation : Cela généralise l'intervalle de nombres naturels $[a, b]$ (où $a \le x \le b$) aux vecteurs. Puisque les vecteurs ne sont pas toujours comparables, la structure nécessite un ensemble de bornes inférieures ($a$) et un ensemble de bornes supérieures ($b$) plutôt qu'une seule borne.

Un Ensemble de Vecteurs Symboliques est une collection de ces vecteurs symboliques, représentant l'union de leurs ensembles de marquages sous-jacents.

2.2. Forme Canonique et Opérations

Pour assurer l'efficacité et éviter la redondance, les auteurs définissent une forme canonique pour les vecteurs et ensembles symboliques. Les propriétés clés incluent :

• Unicité : Chaque ensemble de marquages possède exactement une représentation canonique.
• Opérations Homomorphes : Le papier définit des opérations homomorphes (union, intersection, différence, négation) qui opèrent directement sur les structures symboliques sans les décoder en marquages individuels.
• Fusionnabilité et Partageabilité : Pour maintenir la canonicité, les auteurs introduisent des relations pour déterminer quand deux vecteurs symboliques peuvent être fusionnés ou lorsqu'un composant « partageable » existe entre eux. Cela implique un ordre total lexicographique pour résoudre les ambiguïtés dans les ordres partiels non totaux, assurant un traitement déterministe des contraintes chevauchantes.

2.3. Vérification de Modèles CTL sur les Réseaux de Petri

Le cadre applique ces structures aux réseaux de Petri à capacités finies.

• Opération Pre : Le cœur de la vérification de modèles globale est l'opération pre, qui calcule les marquages prédécesseurs. Les auteurs définissent une opération pre symbolique qui travaille sur les ensembles de vecteurs symboliques, gérant la réversibilité des transitions et les contraintes de capacité.
• Évaluation de Point Fixe : Les formules CTL (par exemple, $EF$, $EG$, $EU$) sont évaluées via des calculs de points fixes (points fixes inférieurs et supérieurs) sur les ensembles de vecteurs symboliques. La satisfaction d'une formule est déterminée en vérifiant si un marquage appartient à l'ensemble de vecteurs symboliques résultant.

2.4. Optimisations

• Saturation : Pour traiter l'« effet de pic » où les solutions intermédiaires dans les calculs de points fixes croissent inutilement, les auteurs implémentent une stratégie de saturation. Cela implique d'itérer sur les bornes de capacité et de tirer parti des résultats précédents pour calculer les étapes suivantes, réduisant ainsi considérablement le nombre de vecteurs symboliques intermédiaires.
• Clustering : Le papier mentionne le clustering comme une optimisation potentielle pour la réachabilité, où de plus petits vecteurs sont combinés, bien que cela soit noté comme un concept pour une description formelle future.

3. Contributions Clés

1. Encodage Novateur : Introduction des Ensembles de Vecteurs Symboliques, une structure qui généralise les intervalles aux vecteurs, spécifiquement conçue pour gérer l'ordre partiel non total des marquages de réseaux de Petri.
2. Canonicalisation Formelle : Une définition rigoureuse d'une forme canonique pour les vecteurs et ensembles symboliques, incluant des preuves d'unicité et le développement d'opérations homomorphes (union, intersection, différence, négation) qui préservent cette canonicité.
3. Cadre de Vérification de Modèles Globale : Un formalisme complet pour évaluer les formules CTL sur les réseaux de Petri utilisant ces structures symboliques, incluant la définition de l'opération pre symbolique.
4. Algorithme de Saturation : Une adaptation des principes de saturation (dérivés d'autres techniques symboliques) au contexte des ensembles de vecteurs symboliques pour atténuer les pics de calcul lors des itérations de points fixes.
5. Implémentation (SVSKit) : Une bibliothèque Swift implémentant la théorie, testée contre des benchmarks du Model Checking Contest (MCC) 2022.

4. Résultats

Les auteurs ont évalué leur approche à l'aide de l'outil SVSKit sur des exemples du MCC 2022, spécifiquement le modèle Circadian Clock.

• Scalabilité avec la Saturation : Les expériences sur le modèle Circadian Clock (14 places, 16 transitions) ont démontré que la saturation est critique. Sans saturation, le temps de calcul augmentait exponentiellement avec la capacité des places (dépassant 5 heures pour une capacité de 6). Avec la saturation, le temps est resté constant (environ 3,2s) pour des capacités de 2 et plus, et le nombre de vecteurs symboliques est resté stable.
• Gestion de Grands Espaces d'États : L'outil a géré avec succès des capacités allant jusqu'à $N=100\,000$, encodant environ $10^{84}$ marquages avec un ensemble final de seulement 26 vecteurs symboliques.
• Performance de Benchmark : Dans la catégorie de fireabilité CTL de MCC 2022, les outils existants (GreatSPN, ITS-Tools, Tapaal) n'ont pas pu répondre à toutes les 16 requêtes dans la limite de 60 minutes (Tapaal a répondu à 9/16). L'approche SVSKit a résolu les 16 requêtes en environ 30 minutes.
• Limitations : Les auteurs reconnaissent que l'implémentation actuelle fait face à des défis de scalabilité dus à la complexité dans le pire des cas des opérations canoniques ($O(n!)$). L'efficacité repose lourdement sur l'implémentation de ces opérations, et l'outil a été restreint à des réseaux de Petri relativement petits dans les benchmarks en raison de ces contraintes.

5. Signification et Revendications

Le papier affirme offrir une alternative prometteuse aux techniques existantes de vérification de modèles symboliques en passant de « vecteurs d'intervalles » à des « intervalles de vecteurs ».

• Contribution Théorique : Il fournit un cadre algébrique formel pour manipuler des ensembles de vecteurs sous des ordres partiels, comblant un vide dans la littérature où ces structures étaient auparavant stagnantes (référence aux « structures de prédicats » originales d'il y a 30 ans).
• Viabilité Pratique : Les résultats suggèrent que cette approche peut gérer des espaces d'états infinis ou très grands plus efficacement que l'énumération explicite et peut potentiellement surpasser les outils actuels sur des tâches spécifiques de vérification de modèles globale, particulièrement celles impliquant de grandes capacités.
• Directions Futures : Les auteurs suggèrent modestement que l'implémentation actuelle nécessite un raffinement, notamment pour optimiser les opérations canoniques. Ils proposent des travaux futurs sur la vérification de modèles locale, étendant l'approche à des modèles au-delà des réseaux de Petri, et l'intégration de cette méthode avec les diagrammes de décision, postulant que les deux approches sont orthogonales et pourraient bénéficier d'une hybridation.

Le papier conclut que, bien que l'implémentation actuelle présente des limitations, le fondement théorique et les résultats expérimentaux initiaux valident le potentiel des ensembles de vecteurs symboliques pour la vérification de modèles globale.