💻 computer science

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

Cet article présente une procédure de décision pour la logique $\mathcal{L}_{[\,]}$ , qui étend la théorie des ensembles finis avec des intervalles d'entiers finis permettant des variables non bornées, et démontre son utilité pratique grâce à l'outil $\{log\}$ dans la vérification automatique de lemmes d'invariance pour un algorithme d'ascenseur.

Auteurs originaux : Maximiliano Cristiá, Gianfranco Rossi

Publié 2026-05-05

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Maximiliano Cristiá, Gianfranco Rossi

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un organisateur expert tentant de gérer un type d'entrepôt très spécifique. Dans cet entrepôt, vous avez deux types d'objets : des boîtes (qui peuvent contenir d'autres boîtes ou des objets) et des étagères numérotées (qui contiennent une plage continue d'entiers, comme les étagères 1 à 10).

Pendant longtemps, les outils informatiques ont pu vous aider à organiser parfaitement les boîtes. Ils pouvaient vous dire si deux boîtes étaient identiques, si une boîte était contenue dans une autre, ou combien d'objets se trouvaient dans une boîte. Cependant, ces outils butaient sur un mur lorsque vous tentiez de parler des étagères numérotées. Ils ne pouvaient pas facilement raisonner sur une étagère s'étendant du « sol 3 » au « sol 10 » tout en vérifiant simultanément si une boîte spécifique d'objets était posée sur cette étagère.

Cet article présente un nouvel outil « super-organisateur » (appelé {log} ou « setlog ») capable de gérer à la fois les boîtes et les étagères numérotées en même temps. Voici comment les auteurs y sont parvenus, expliqué par le biais d'analogies simples.

1. Le Problème : Le « Vide » de l'Étagère

Auparavant, l'outil pouvait gérer :

Les boîtes : « La boîte A est-elle la même que la boîte B ? » ou « Combien de pommes y a-t-il dans la boîte C ? »
Les nombres : « Le nombre 5 est-il inférieur au nombre 10 ? »

Mais il ne pouvait pas gérer le mélange : « L'ensemble des objets sur l'étagère [3, 10] (ce qui signifie les étagères 3, 4, 5, 6, 7, 8, 9 et 10) est-il exactement le même que la boîte A ? »

Les auteurs voulaient construire un système capable de prouver automatiquement des choses comme : « Si je divise les objets de l'étagère [3, 10] en deux groupes, et que les deux groupes ont le même nombre d'objets, alors l'étagère doit avoir un nombre pair de cases. »

2. Le Tour de Magie : La « Carte d'Identité »

Pour résoudre cela, les auteurs ont découvert une « carte d'identité » mathématique astucieuse (une règle spécifique) qui agit comme un traducteur.

Considérez une étagère numérotée (un intervalle comme [3, 10]) comme une boîte très rigide, pré-emballée. Vous savez exactement ce qu'elle contient rien qu'en regardant les numéros de début et de fin.

La Règle : Si vous avez une boîte, et que vous connaissez deux choses :
1. Tout ce qui est dans la boîte tient à l'intérieur de l'étagère [3, 10].
2. La boîte contient exactement le bon nombre d'objets pour remplir cette étagère (dans ce cas, 8 objets).
- Alors : La boîte est l'étagère. Elle est identique à l'étagère [3, 10].

L'outil des auteurs utilise ce tour. Lorsqu'il voit une question complexe impliquant une étagère, il n'essaie pas de résoudre directement la partie « étagère ». Au lieu de cela, il dit : « D'accord, faisons comme si cette étagère était juste une boîte ordinaire avec un nombre spécifique d'objets. » Il traduit le problème « étagère » en un problème « boîte » que l'outil sait déjà résoudre.

3. Le Détective de la « Solution Minimale »

Une fois que l'outil a traduit l'étagère en boîte, il fait face à un nouveau défi : Comment savoir si une solution est possible sans vérifier chaque possibilité unique dans l'univers ?

Imaginez que vous essayez de trouver le plus petit groupe possible de personnes qui satisfait une règle.

L'outil trouve d'abord le plus petit groupe possible (la « solution minimale ») qui respecte les règles.
La Logique : Si le plus petit groupe échoue à satisfaire la règle, alors n'importe quel groupe plus grand échouera aussi. C'est comme essayer de faire entrer un éléphant géant dans une petite voiture ; si la voiture est trop petite pour l'éléphant, ajouter plus d'éléphants n'aidera pas.
À l'inverse, si le plus petit groupe fonctionne, alors la règle est satisfaite.

En ne vérifiant que ces scénarios « minimaux », l'outil évite de rester coincé dans une boucle infinie de vérification de chaque combinaison possible. Il prouve que si le cas le plus simple fonctionne (ou échoue), tout le problème est résolu.

4. Le Test de l'Ascenseur (Étude de Cas)

Pour prouver que leur nouvel outil fonctionne dans le monde réel, les auteurs l'ont testé sur un problème classique : l'Algorithme de l'Ascenseur.

Imaginez un ascenseur se déplaçant entre les étages. Il a des demandes (des personnes voulant monter ou descendre). L'outil devait prouver que la logique de l'ascenseur était sûre et correcte.

Le Défi : L'ascenseur doit savoir des choses comme : « Si je suis à l'étage 3 en montant, et qu'il y a des demandes aux étages 5 et 8, à quel étage vais-je ensuite ? » Cela implique de raisonner sur une plage d'étages (intervalles) et sur l'ensemble des demandes (boîtes).
Le Résultat : L'outil a vérifié automatiquement toutes les règles (invariants) du système d'ascenseur. Il a prouvé que l'ascenseur ne resterait jamais coincé, qu'il se déplacerait toujours dans la bonne direction et qu'il gérerait correctement les demandes. Il a fait cela sans qu'un humain ait à vérifier manuellement chaque étape, prouvant ainsi que le système était logiquement solide.

5. Pourquoi Cela Compte

Avant cet article, si vous vouliez vérifier un logiciel traitant à la fois des ensembles de données et des plages de nombres (comme les tableaux dans les programmes informatiques ou les intervalles de temps), vous deviez souvent le faire à la main ou utiliser des outils incapables de gérer cette complexité.

Cet article fournit une procédure de décision. En français courant, cela signifie que l'outil est une machine « oui/non » capable de répondre définitivement : « Cette affirmation concernant les ensembles et les plages de nombres est-elle vraie ou fausse ? » Il garantit une réponse en un temps fini.

Résumé

Les auteurs ont construit un pont entre deux mondes : les Ensembles (groupes de choses) et les Intervalles (plages de nombres). Ils ont fait cela en :

Créant une règle qui transforme une « plage de nombres » en un « groupe d'objets » si la taille correspond.
Utilisant une stratégie de « cas le plus petit » pour éviter de se perdre dans des possibilités infinies.
Prouvant que cela fonctionne en automatisant avec succès les vérifications de sécurité pour un système d'ascenseur.

Le résultat est un outil capable de vérifier automatiquement des règles logiques complexes impliquant à la fois des collections d'objets et des plages de nombres continues, quelque chose qui était auparavant très difficile à faire automatiquement.

Résumé technique : Une procédure de décision pour une théorie des ensembles finis avec des intervalles entiers finis

Énoncé du problème

Dans le contexte de la vérification formelle et de l'analyse, les outils de raisonnement automatisé sont essentiels pour éliminer les conditions de vérification. Bien que les outils existants basés sur la théorie des ensembles (par exemple, B, ProB) soient efficaces, ils manquent souvent de procédures de décision pour des fragments spécifiques de la théorie des ensembles qui combinent des ensembles finis avec des intervalles entiers. Plus précisément, l'algèbre booléenne des ensembles finis étendue avec des contraintes de cardinalité (notée $L|\cdot|$ ) est décidable, mais elle ne peut pas exprimer ou raisonner nativement sur des intervalles entiers finis (plages) où les limites peuvent être des variables non bornées. Cette limitation entrave la vérification automatique de propriétés impliquant des opérations sur les ensembles, telles que la recherche du minimum ou du maximum d'un ensemble, la partition d'ensembles basée sur des seuils entiers, ou le raisonnement sur des domaines de tableaux définis par des intervalles. Le problème central abordé est la décidabilité d'une théorie qui intègre des ensembles finis, des contraintes de cardinalité et des intervalles entiers finis (notés $L[\ ]$ ) au sein d'une logique sans quantificateurs.

Méthodologie

Les auteurs proposent une procédure de décision, SAT $[\ ]$ , qui étend le solveur existant SAT $|\cdot|$ (pour $L|\cdot|$ ) afin de gérer les intervalles entiers. La méthodologie repose sur une théorie de base des ensembles héréditairement finis implémentée dans le langage de Programmation Logique sous Contraintes (CLP) CLP($SET$) et l'outil {log}.

Composants techniques clés :

Extension du langage ( $L[\ ]$ ) :
- Le langage est étendu pour inclure des termes d'ensemble de la forme $[k, m]$ , représentant l'ensemble $\{p \in \mathbb{Z} \mid k \le p \le m\}$ .
- Les limites d'intervalle ( $k, m$ ) peuvent être des termes linéaires entiers, y compris des variables.
- La logique reste sans quantificateurs, utilisant des conjonctions et des disjonctions de contraintes impliquant l'appartenance à un ensemble, l'union, la disjonction, la cardinalité et l'appartenance à un intervalle.
Identité centrale et stratégie de réduction :
- L'insight théorique central est l'identité : $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$ .
- Cette identité permet à la procédure de transformer les contraintes impliquant une égalité avec un intervalle en contraintes impliquant des relations de sous-ensemble et de cardinalité.
- Le solveur réécrit les formules en une conjonction d'une formule standard $L|\cdot|$ ( $\Phi_{|\cdot|}$ ) et d'un ensemble de contraintes de sous-ensemble impliquant des intervalles ( $\Phi_{\subseteq[\ ]}$ ), typiquement de la forme $X \subseteq [p, q]$ où $X$ est une variable.
L'algorithme SAT $[\ ]$ :
- Règles de réécriture : Le solveur utilise un ensemble de règles de réécriture (STEPS $[\ ]$ ) qui réduisent la complexité syntaxique. Ces règles gèrent l'égalité, l'appartenance, l'union, la disjonction et les contraintes de cardinalité impliquant des intervalles.
- Réduction vers l'arithmétique entière : De nombreuses règles réécrivent les contraintes d'ensemble impliquant des intervalles directement en contraintes d'arithmétique linéaire entière (LIA).
- Vérification de la solution minimale : Lorsque des contraintes irréductibles de la forme $X \subseteq [p, q]$ $X \subseteq [p, q]$ subsistent, la procédure ne se contente pas d'échouer. Au lieu de cela, elle exploite la propriété selon laquelle, si une formule est satisfaisable, elle doit avoir une « solution minimale » (une solution où les ensembles ont la cardinalité minimale possible).
  - Le solveur calcule la solution minimale pour la partie $L|\cdot|$ ( $\Phi_{|\cdot|}$ ).
  - Il vérifie ensuite si cette solution minimale satisfait les contraintes d'intervalle ( $\Phi_{\subseteq[\ ]}$ ).
  - Les auteurs prouvent que si aucune solution minimale ne satisfait la formule complète, alors aucune solution plus grande ne le fera non plus, rendant la formule insatisfaisable.
Implémentation dans {log} :
- La procédure est implémentée dans {log} (setlog), un outil basé sur Prolog.
- L'implémentation inclut un schéma de mémorisation pour suivre les substitutions de variables pour les intervalles, évitant ainsi les réécritures redondantes et améliorant l'efficacité.
- Les contraintes dérivées (par exemple, intersection, différence) sont définies en termes de contraintes primitives pour maintenir la cohérence.

Contributions clés

Preuve de décidabilité : L'article fournit la première preuve que l'algèbre booléenne des ensembles finis étendue avec des contraintes de cardinalité et des intervalles entiers finis ( $L[\ ]$ ) est décidable.
Procédure de décision (SAT $[\ ]$ ) : Un algorithme complet est présenté qui décide de la satisfaisabilité des formules $L[\ ]$ . La procédure est prouvée être correcte, complète et terminante.
Intégration des intervalles et des ensembles : Contrairement aux approches qui traitent les intervalles comme un domaine séparé ou qui nécessitent des limites constantes, ce travail intègre de manière transparente des intervalles entiers à limites variables dans la théorie des ensembles, permettant l'expression d'opérateurs non triviaux (par exemple, le $i$ -ème plus petit élément, la partition par un seuil) dans une logique sans quantificateurs.
Implémentation et outils : La procédure de décision est implémentée comme une extension de l'outil {log}, offrant une double capacité en tant que langage de programmation logique sous contraintes et en tant que solveur de satisfaisabilité.

Résultats et évaluation

L'article présente des preuves empiriques et une étude de cas pour démontrer l'utilité pratique de l'approche :

Évaluation sur des benchmarks : Un ensemble de 60 formules $L[\ ]$ , représentant des propriétés d'opérateurs définis dans l'article (par exemple, minimum, maximum, $i$ -ème élément), a été résolu. {log} a résolu tous les problèmes en moyenne en 0,51 seconde par problème, un seul ayant pris plus de 5 secondes.
Étude de cas (Algorithme d'ascenseur) : Les auteurs ont modélisé un système de contrôle d'ascenseur où l'ascenseur doit servir les demandes dans une direction spécifique. Le modèle a utilisé des intervalles entiers pour définir les étages et les demandes.
- Le système comprenait 7 opérations (par exemple, ajouter des demandes, servir la demande suivante).
- {log} a été utilisé pour éliminer automatiquement 49 lemmes d'invariance (prouvant que les opérations d'état préservent 7 invariants d'état) et 7 vérifications d'état initial.
- Toutes les preuves ont été complétées en environ 0,5 seconde sur un ordinateur portable standard.
- L'outil a généré avec succès des contre-exemples lorsque les invariants ont été intentionnellement affaiblis, démontrant ses capacités de débogage.

Importance et affirmations

Les auteurs affirment que ce travail représente une avancée significative dans le raisonnement automatisé pour la vérification formelle. En étendant le fragment décidable de la théorie des ensembles pour inclure des intervalles entiers finis avec des limites variables, l'approche permet la vérification automatique de propriétés qui étaient précédemment difficiles ou impossibles à exprimer sans quantificateurs.

L'article souligne que l'approche est ancrée dans la théorie des ensembles, la distinguant d'autres outils de raisonnement sur les intervalles (comme ceux basés sur l'algèbre des intervalles d'Allen ou les treillis d'analyse statique) qui manquent souvent de la capacité de combiner les intervalles avec des opérations d'ensemble générales. L'intégration du raisonnement sur les intervalles dans le cadre {log} permet aux utilisateurs d'écrire des programmes et de prouver leurs propriétés en utilisant le même code et le même outil, exploitant la dualité entre formule et programme. Les auteurs notent modestement que, bien que l'approche soit générale et cohérente, elle peut entraîner des coûts d'efficacité par rapport à des solveurs spécialisés pour des problèmes spécifiques uniquement aux intervalles, mais que le compromis est la capacité de raisonner sur des structures hybrides complexes d'ensembles-intervalles.