Certification Formellement Vérifiée de l'Insolvabilité des Problèmes de Planification Temporelle

Informations Fondamentales

• ID de l'article : 2510.10189
• Titre : Formally Verified Certification of Unsolvability of Temporal Planning Problems
• Auteurs : David Wang, Mohammad Abdulaziz (King's College London, Royaume-Uni)
• Classification : cs.LO (Logique en Informatique), cs.AI (Intelligence Artificielle)
• Date de publication : 11 octobre 2025 (prépublication arXiv)
• Lien de l'article : https://arxiv.org/abs/2510.10189

Résumé

Cet article propose une méthode de certification de l'insolvabilité des problèmes de planification temporelle. La méthode repose sur l'encodage des problèmes de planification en réseaux d'automates temporisés, suivi de l'utilisation d'un vérificateur de modèles efficace, puis d'un vérificateur de certificats pour certifier la sortie du vérificateur de modèles. La méthode privilégie la fiabilité de la certification : elle utilise le prouveur de théorèmes Isabelle/HOL pour vérifier formellement l'implémentation de l'encodage des automates temporisés, et utilise un vérificateur de certificats existant (également vérifié formellement dans Isabelle/HOL) pour certifier les résultats de la vérification de modèles.

Contexte de Recherche et Motivation

Problème Central

Le problème central abordé par cette recherche est la certification de l'insolvabilité des problèmes de planification temporelle. La planification temporelle est une forme riche de planification permettant aux actions d'avoir une durée et une exécution concurrente, beaucoup plus complexe que la planification classique.

Importance du Problème

1. Besoin de fiabilité : Les systèmes de planification existants sont extrêmement complexes aux niveaux algorithmique et d'implémentation, rendant crucial l'amélioration de la fiabilité de leurs résultats
2. Difficulté de certification : Contrairement aux problèmes solubles (vérifiables par exécution du plan), les affirmations d'insolvabilité ou d'optimalité sont difficiles à obtenir avec des certificats compacts
3. Complexité exponentielle : Dans le pire des cas, ces certificats peuvent croître exponentiellement par rapport à la taille de la tâche de planification

Limitations des Approches Existantes

1. Absence de garanties formelles : Les méthodes existantes de détection de l'insolvabilité en planification temporelle manquent de garanties formelles de correction
2. Complexité élevée : Les techniques algorithmiques les plus avancées en planification temporelle sont d'une grande complexité, rendant difficile la conception de schémas pratiques de certification de l'insolvabilité
3. Lacune de vérification : Comparé aux travaux de vérification formelle existants en planification classique, le domaine de la planification temporelle présente une lacune à cet égard

Motivation de la Recherche

Cet article adopte une approche de transformation par encodage : il encode les problèmes de planification temporelle en d'autres problèmes de calcul pour lesquels existent des algorithmes de certification pratiques (automates temporisés), et vérifie formellement l'ensemble du processus d'encodage et du vérificateur de certificats à l'aide d'un prouveur de théorèmes, garantissant la fiabilité de la certification.

Contributions Principales

1. Méthode d'encodage vérifiée formellement : Première vérification formelle de l'encodage de la planification temporelle en automates temporisés proposé par Heinz et al.
2. Implémentation d'ingénierie : Adaptation de l'encodage pour produire un format d'automates temporisés compatible avec le système de Wimmer et von Mutius
3. Conception de sémantique simplifiée : Conception d'une sémantique de planification temporelle plus simple que les travaux existants, facilitant le raisonnement mathématique, avec preuve d'équivalence avec la sémantique existante
4. Cadre de certification complet : Construction d'une chaîne de certification fiable complète, du problème de planification temporelle à la vérification de modèles d'automates temporisés
5. Garanties de correction théorique : Preuve de la correction de l'encodage dans Isabelle/HOL, fournissant des garanties théoriques solides

Détail de la Méthode

Définition de la Tâche

Entrée : Problème de planification temporelle P = ⟨P, A, I, G⟩

• P : ensemble de propositions
• A : ensemble d'actions de durée
• I : état initial
• G : conditions d'objectif

Sortie : Certificat formel d'insolvabilité (si le problème est effectivement insoluble)

Conditions de contrainte :

• Les actions possèdent des actions instantanées de début et de fin
• Support des conditions invariantes et des contraintes d'ordonnancement
• Satisfaction des contraintes d'exclusion mutuelle et des limites de durée

Architecture du Modèle

1. Formalisation de la Planification Temporelle

L'article définit d'abord la sémantique formelle de la planification temporelle :

Actions instantanées (Définition 1) :

h ≡ ⟨pre(h), adds(h), dels(h)⟩

Actions de durée (Définition 2) :

a ≡ ⟨a⊢, a⊣, over_all(a), L(a), U(a)⟩

où a⊢ et a⊣ sont respectivement les actions instantanées de début et de fin.

2. Encodage en Automates Temporisés

Conception des variables (Définition 24) :

• Pour chaque proposition p : variable binaire vp (encodant la valeur de vérité) et compteur de verrous lp (enregistrant le nombre d'actions actives nécessitant que p soit vrai)
• aa : nombre total d'actions actives
• ps : état de planification (0=non commencé, 1=en cours, 2=terminé)

Conception des horloges (Définition 25) :

• Deux horloges allouées à chaque action a : ca⊢ (enregistrant le temps après le début) et ca⊣ (enregistrant le temps après la fin)

Automate principal (Définition 26) : Contrôle les transitions d'état du processus de planification global, incluant l'initialisation et la vérification d'objectif.

Automates d'action (Définition 27) : Chaque action correspond à un automate, contenant les transitions clés suivantes :

• sea : application des effets du début d'action
• se'a : verrouillage des conditions invariantes
• eea : préparation avant la fin
• ee'a : application des effets de fin d'action
• iea : traitement des actions instantanées

3. Construction du Réseau

Combinaison de l'automate principal et de tous les automates d'action en un réseau d'automates temporisés (Définition 28), avec configuration initiale où tous les automates sont inactifs.

Points d'Innovation Technique

1. Support de l'exécution concurrente : Contrairement à Heinz et al. qui utilisent un verrou global, cet article utilise des contraintes d'horloge permettant l'exécution concurrente d'actions instantanées
2. Traitement des actions instantanées : Support des actions de durée zéro via l'ajout de transitions iea
3. Vérification formelle : Première preuve de correction vérifiée par machine pour ce type d'encodage
4. Simplification sémantique : Conception d'une sémantique de planification temporelle plus adaptée au raisonnement formel

Configuration Expérimentale

Environnement de Vérification Formelle

• Prouveur de théorèmes : Isabelle/HOL
• Vérificateur de certificats : Vérificateur de certificats vérifié de Wimmer et von Mutius
• Propriété cible : Vérification d'accessibilité A ⊨ EF(loc(AM) = goal)

Statistiques de Taille du Code

Comparaison avec les Travaux Connexes

Comparaison de taille avec les travaux de vérification formelle connexes :

• Planificateur basé sur SAT vérifié : ~17 500 lignes
• Vérificateur de planification classique vérifié : ~3 000 lignes
• Vérificateur de planification temporelle PDDL vérifié : ~6 500 lignes

Résultats Expérimentaux

Résultats Théoriques Principaux

Théorème 1 (Théorème de Correction Principal) : Si le plan π est valide et sans auto-chevauchement (valid(π) ∧ no_self_overlap(π)), alors l'assertion A ⊨ EF(loc(AM) = goal) est vérifiée.

Structure de la Preuve :

1. Lemme 1 : Construction d'une exécution simulant un plan parallèle induit
2. Lemme 2 : Accessibilité de la configuration encodée depuis la configuration initiale
3. Lemme 3 : Transition de l'état final à la configuration d'objectif

Résultats de Vérification Formelle

1. Preuve de complétude : Preuve réussie de la complétude de l'encodage, c'est-à-dire que chaque plan valide trouve une exécution valide dans le réseau d'automates temporisés correspondant
2. Vérification par machine : Toutes les preuves sont vérifiées par machine dans Isabelle/HOL, fournissant le plus haut niveau de garantie de fiabilité
3. Conception modulaire : Structure de preuve modulaire, facilitant la compréhension et la maintenance

Vérification de l'Implémentation d'Ingénierie

L'implémentation de l'encodage a été adaptée au format compatible avec le vérificateur de certificats vérifié existant, formant une chaîne de certification complète et exécutable.

Travaux Connexes

Certification en Planification Classique

• Eriksson et al. ont conçu des schémas compacts de certification de l'insolvabilité pour la planification classique
• Abdulaziz et Lammich ont fourni un vérificateur formel pour la planification classique

Planification Temporelle et Vérification de Modèles

• Dierks et al. ont implémenté une réduction statique d'un sous-ensemble PDDL en automates temporisés
• Heinz et al. ont défini un encodage explicite des problèmes de planification temporelle en automates temporisés
• Gigante et al. ont étudié théoriquement la complexité de la planification temporelle

Méthodes de Vérification Formelle

• Abdulaziz et Kurz ont utilisé une approche similaire pour développer un système de planification basé sur SAT certifié
• Kumar et al. et Leroy ont utilisé la vérification progressive d'encodages dans la vérification de compilateurs

Conclusion et Discussion

Conclusions Principales

1. Vérification de faisabilité : Démonstration que la certification formelle de l'insolvabilité en planification temporelle est faisable
2. Garanties théoriques : Fournit des garanties de correction solides via le prouveur de théorèmes
3. Implémentation d'ingénierie : Construction réussie d'une chaîne d'outils de certification complète

Limitations

1. Restrictions d'entrée : Accepte actuellement uniquement les problèmes de planification temporelle déjà instanciés
2. Sous-ensemble sémantique : La sémantique supportée est un sous-ensemble du vérificateur de planification vérifié existant
3. Exécutabilité : Le mécanisme de certification n'est pas encore complètement exécutable

Directions Futures

1. Preuve d'équivalence : Prévoit de prouver formellement l'équivalence entre la sémantique de cet article et celle des vérificateurs existants
2. Implémentation exécutable : Développement d'un vérificateur de certificats exécutable
3. Vérification d'instanciation : Vérification formelle des algorithmes d'instanciation, comme le solveur Datalog de Helmert
4. Relâchement de contraintes : Étude de la possibilité de relâcher la condition d'absence d'auto-chevauchement

Évaluation Approfondie

Points Forts

1. Rigueur théorique : Première preuve formelle vérifiée par machine de la certification de l'insolvabilité en planification temporelle
2. Complétude d'ingénierie : Non seulement un cadre théorique, mais aussi une intégration avec les outils existants
3. Innovation méthodologique :
   • Conception d'encodage supportant l'exécution concurrente
   • Solution élégante pour le traitement des actions instantanées
   • Conception de sémantique simplifiée mais équivalente
4. Garanties de fiabilité : Fournit le plus haut niveau de garantie de correction via le prouveur de théorèmes

Insuffisances

1. Limitations de praticité :
   • Nécessite une entrée préalablement instanciée
   • Pas encore complètement exécutable
   • Absence d'évaluation de performance
2. Couverture limitée : Supporte uniquement un sous-ensemble de la planification temporelle, ne couvre pas les caractéristiques complètes de PDDL
3. Scalabilité : L'ampleur du travail de vérification formelle (18 000 lignes de code) est relativement importante, avec des coûts de maintenance élevés

Impact

1. Contribution académique :
   • Comble le vide en vérification formelle de la planification temporelle
   • Fournit une nouvelle base théorique pour la certification de l'insolvabilité
   • Démontre la faisabilité de la vérification formelle de systèmes complexes
2. Valeur pratique :
   • Fournit une certification fiable des systèmes de planification pour les applications critiques
   • Extensible à d'autres formes de planification et problèmes de satisfaction de contraintes
   • Fournit une référence pour le développement d'outils de vérification automatisée
3. Reproductibilité : Basé sur Isabelle/HOL open-source, théoriquement complètement reproductible

Scénarios d'Application

1. Systèmes critiques : Applications de planification nécessitant des garanties de haute fiabilité (aérospatiale, dispositifs médicaux)
2. Outils de recherche : Fournit une infrastructure de vérification formelle pour la recherche en planification temporelle
3. Utilisation éducative : Cas d'étude pour l'enseignement des méthodes formelles et des algorithmes de planification
4. Développement d'outils : Fournit une base théorique pour le développement d'outils de planification fiables

Références

Les références clés incluent :

• Abdulaziz & Koller (2022) : Sémantique formelle et vérificateur pour la planification temporelle
• Heinz et al. (2019) : Encodage de la planification temporelle en automates temporisés
• Wimmer & von Mutius (2020) : Vérificateur de certificats pour automates temporisés
• Abdulaziz & Kurz (2023) : Système de planification basé sur SAT certifié

Cet article apporte une contribution importante au domaine de la vérification formelle de la planification temporelle. Bien qu'il y ait encore place à amélioration en termes de praticité, sa rigueur théorique et son innovation méthodologique jettent une base solide pour le développement futur du domaine.