Certificación Formalmente Verificada de la Insolubilidad de Problemas de Planificación Temporal

Información Básica

• ID del Artículo: 2510.10189
• Título: Formally Verified Certification of Unsolvability of Temporal Planning Problems
• Autores: David Wang, Mohammad Abdulaziz (King's College London, Reino Unido)
• Clasificación: cs.LO (Lógica en Informática), cs.AI (Inteligencia Artificial)
• Fecha de Publicación: 11 de octubre de 2025 (preimpresión en arXiv)
• Enlace del Artículo: https://arxiv.org/abs/2510.10189

Resumen

Este artículo propone un método para la certificación de insolubilidad de problemas de planificación temporal. El método se basa en codificar problemas de planificación como redes de autómatas temporales, aplicar verificadores de modelos eficientes en la red y, posteriormente, utilizar verificadores de certificados para autenticar la salida del verificador de modelos. El método prioriza la confiabilidad de la certificación: utiliza el demostrador de teoremas Isabelle/HOL para verificar formalmente la implementación de la codificación de autómatas temporales, y emplea un verificador de certificados existente (también verificado formalmente en Isabelle/HOL) para autenticar los resultados de la verificación de modelos.

Contexto de Investigación y Motivación

Problema Central

El problema central que aborda esta investigación es la certificación de insolubilidad de problemas de planificación temporal. La planificación temporal es una forma de planificación más rica que permite que las acciones tengan duración y se ejecuten de manera concurrente, siendo considerablemente más compleja que la planificación clásica.

Importancia del Problema

1. Requisitos de Confiabilidad: Los sistemas de planificación existentes son extremadamente complejos tanto a nivel algorítmico como de implementación, por lo que es crucial mejorar la confiabilidad de sus resultados
2. Dificultad de Certificación: A diferencia de los problemas solubles (que pueden verificarse ejecutando un plan), las afirmaciones de insolubilidad u optimalidad son difíciles de certificar de manera compacta
3. Complejidad Exponencial: En el peor caso, tales certificados pueden crecer exponencialmente con respecto al tamaño de la tarea de planificación

Limitaciones de Métodos Existentes

1. Falta de Garantías Formales: Los métodos existentes para detectar insolubilidad en planificación temporal carecen de garantías formales de corrección
2. Alta Complejidad: Las técnicas algorítmicas más avanzadas en planificación temporal tienen una complejidad muy alta, lo que dificulta el diseño de esquemas prácticos de certificación de insolubilidad
3. Vacío en Verificación: En comparación con el trabajo de verificación formal existente en planificación clásica, existe un vacío en este aspecto para planificación temporal

Motivación de la Investigación

Este artículo adopta un enfoque de transformación de codificación: codifica problemas de planificación temporal en otros problemas computacionales para los cuales existen algoritmos de certificación prácticos (autómatas temporales), y verifica formalmente todo el proceso de codificación y el verificador de certificados mediante un demostrador de teoremas, asegurando la confiabilidad de la certificación.

Contribuciones Principales

1. Método de Codificación Verificado Formalmente: Primera verificación formal de la codificación de planificación temporal a autómatas temporales de Heinz et al.
2. Implementación de Ingeniería: Adaptación de la codificación para producir formatos de autómatas temporales compatibles con el sistema de Wimmer y von Mutius
3. Diseño de Semántica Simplificada: Diseño de una semántica de planificación temporal más simple que trabajos previos, facilitando el razonamiento matemático, con prueba de equivalencia con semánticas existentes
4. Marco de Certificación Completo: Construcción de una cadena de certificación confiable completa desde problemas de planificación temporal hasta verificación de modelos de autómatas temporales
5. Garantías de Corrección Teórica: Prueba de corrección de la codificación en Isabelle/HOL, proporcionando garantías teóricas sólidas

Explicación Detallada del Método

Definición de la Tarea

Entrada: Problema de planificación temporal P = ⟨P, A, I, G⟩

• P: conjunto de proposiciones
• A: conjunto de acciones de duración
• I: estado inicial
• G: condiciones de objetivo

Salida: Certificado formal de insolubilidad (si el problema es efectivamente insoluble)

Restricciones:

• Las acciones poseen acciones de captura de inicio y fin
• Soporte para condiciones invariantes y restricciones de programación
• Satisfacción de restricciones de exclusión mutua y límites de duración

Arquitectura del Modelo

1. Formalización de Planificación Temporal

El artículo define primero la semántica formal de la planificación temporal:

Acciones de Captura (Definición 1):

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

Acciones de Duración (Definición 2):

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

donde a⊢ y a⊣ son las acciones de captura de inicio y fin respectivamente.

2. Codificación de Autómatas Temporales

Diseño de Variables (Definición 24):

• Para cada proposición p: variable binaria vp (codificando valor de verdad) y contador de bloqueo lp (registrando acciones activas que requieren que p sea verdadero)
• aa: número total de acciones activas
• ps: estado de planificación (0=no iniciado, 1=en planificación, 2=completado)

Diseño de Relojes (Definición 25):

• Dos relojes asignados a cada acción a: ca⊢ (registrando tiempo después del inicio) y ca⊣ (registrando tiempo después del fin)

Autómata Principal (Definición 26): Controla las transiciones de estado de todo el proceso de planificación, incluyendo inicialización y verificación de objetivo.

Autómatas de Acción (Definición 27): Cada acción corresponde a un autómata, conteniendo las siguientes transiciones clave:

• sea: aplicación de efectos de inicio de acción
• se'a: bloqueo de condiciones invariantes
• eea: preparación antes del fin
• ee'a: aplicación de efectos de fin de acción
• iea: manejo de acciones instantáneas

3. Construcción de Red

Combinación del autómata principal y todos los autómatas de acción en una red de autómatas temporales (Definición 28), con configuración inicial estableciendo todos los autómatas en estado inactivo.

Puntos de Innovación Técnica

1. Soporte para Ejecución Concurrente: A diferencia de Heinz et al. que utilizan bloqueos globales, este trabajo utiliza restricciones de reloj permitiendo ejecución concurrente de acciones de captura
2. Manejo de Acciones Instantáneas: Soporte para acciones de duración cero mediante la adición de transiciones iea
3. Verificación Formal: Primera provisión de pruebas de corrección verificadas por máquina para tales codificaciones
4. Simplificación de Semántica: Diseño de semántica de planificación temporal más adecuada para razonamiento formal

Configuración Experimental

Entorno de Verificación Formal

• Demostrador de Teoremas: Isabelle/HOL
• Verificador de Certificados: Verificador de certificados verificado de Wimmer y von Mutius
• Propiedad Objetivo: Verificación de alcanzabilidad A ⊨ EF(loc(AM) = goal)

Estadísticas de Código

Comparación con Trabajos Relacionados

Comparación de escala con trabajos de verificación formal relacionados:

• Planificador basado en SAT verificado: ~17,500 líneas
• Verificador de planificación clásica verificado: ~3,000 líneas
• Verificador de planificación temporal PDDL verificado: ~6,500 líneas

Resultados Experimentales

Resultados Teóricos Principales

Teorema 1 (Teorema de Corrección Principal): Si el plan π es válido y sin auto-solapamiento (valid(π) ∧ no_self_overlap(π)), entonces se cumple la afirmación A ⊨ EF(loc(AM) = goal).

Estructura de Prueba:

1. Lema 1: Construcción de simulación induciendo ejecución de plan paralelo
2. Lema 2: Alcanzabilidad desde configuración inicial a estado codificado
3. Lema 3: Transición desde estado final a configuración de objetivo

Logros de Verificación Formal

1. Prueba de Completitud: Prueba exitosa de completitud de la codificación, es decir, cada plan válido puede encontrar una ejecución válida en la red de autómatas temporales correspondiente
2. Verificación por Máquina: Todas las pruebas han sido verificadas por máquina mediante Isabelle/HOL, proporcionando el más alto nivel de garantía de confiabilidad
3. Diseño Modular: Estructura de prueba modular, facilitando comprensión y mantenimiento

Verificación de Implementación de Ingeniería

La implementación de codificación ha sido adaptada al formato compatible con verificadores de certificados verificados existentes, formando una cadena de certificación completamente ejecutable.

Trabajo Relacionado

Certificación en Planificación Clásica

• Eriksson et al. diseñaron esquemas compactos de certificación de insolubilidad para planificación clásica
• Abdulaziz y Lammich proporcionaron verificadores formales para planificación clásica

Planificación Temporal y Verificación de Modelos

• Dierks et al. implementaron reducción estática de subconjunto PDDL a autómatas temporales
• Heinz et al. definieron codificación explícita de problemas de planificación temporal a autómatas temporales
• Gigante et al. estudiaron complejidad de planificación temporal a nivel teórico

Métodos de Verificación Formal

• Abdulaziz y Kurz utilizaron método similar para desarrollar sistema de planificación basado en SAT certificado
• Kumar et al. y Leroy utilizaron método de verificación gradual de codificación en verificación de compiladores

Conclusiones y Discusión

Conclusiones Principales

1. Verificación de Viabilidad: Demuestra que la certificación formal de insolubilidad en planificación temporal es viable
2. Garantías Teóricas: Proporciona garantías sólidas de corrección mediante demostrador de teoremas
3. Implementación de Ingeniería: Construcción exitosa de cadena de herramientas de certificación completa

Limitaciones

1. Restricciones de Entrada: Actualmente solo acepta problemas de planificación temporal ya instanciados como entrada
2. Subconjunto de Semántica: La semántica soportada es un subconjunto del verificador de planificación verificado existente
3. Ejecutabilidad: El mecanismo de certificación aún no es completamente ejecutable

Direcciones Futuras

1. Prueba de Equivalencia: Planificación para prueba formal de equivalencia entre semántica de este trabajo y semántica de verificadores existentes
2. Implementación Ejecutable: Desarrollo de verificador de certificados ejecutable
3. Verificación de Instanciación: Verificación formal de algoritmos de instanciación, como el solucionador de registro de datos de Helmert
4. Relajación de Restricciones: Investigación de posibilidades de relajar la condición de no auto-solapamiento

Evaluación Profunda

Fortalezas

1. Rigor Teórico: Primera provisión de prueba formal verificada por máquina para certificación de insolubilidad en planificación temporal
2. Completitud de Ingeniería: No solo proporciona marco teórico, sino también implementa integración con herramientas existentes
3. Innovación Metodológica:
   • Diseño de codificación que soporta ejecución concurrente
   • Solución elegante para manejo de acciones instantáneas
   • Diseño de semántica simplificada pero equivalente
4. Garantía de Confiabilidad: Proporciona el más alto nivel de garantía de corrección mediante demostrador de teoremas

Deficiencias

1. Limitaciones de Practicidad:
   • Requiere entrada pre-instanciada
   • Aún no completamente ejecutable
   • Carece de evaluación de rendimiento
2. Rango de Cobertura: Solo soporta subconjunto de planificación temporal, no características PDDL completas
3. Escalabilidad: Escala de trabajo formal de 18,000 líneas de código es relativamente grande, con alto costo de mantenimiento

Impacto

1. Contribución Académica:
   • Llena vacío en verificación formal de planificación temporal
   • Proporciona nueva base teórica para certificación de insolubilidad
   • Demuestra viabilidad de verificación formal de sistemas complejos
2. Valor Práctico:
   • Proporciona certificación confiable de sistemas de planificación para aplicaciones críticas
   • Extensible a otras formas de planificación y problemas de satisfacción de restricciones
   • Proporciona referencia para desarrollo de herramientas de verificación automatizada
3. Reproducibilidad: Basado en Isabelle/HOL de código abierto, teóricamente completamente reproducible

Escenarios de Aplicación

1. Sistemas Críticos: Aplicaciones de planificación que requieren garantías de alta confiabilidad (como aeroespacial, dispositivos médicos)
2. Herramientas de Investigación: Proporciona infraestructura de verificación formal para investigación en planificación temporal
3. Propósitos Educativos: Sirve como caso de estudio para enseñanza de métodos formales y algoritmos de planificación
4. Desarrollo de Herramientas: Proporciona base teórica para desarrollo de herramientas de planificación confiables

Referencias Bibliográficas

Las referencias clave incluyen:

• Abdulaziz & Koller (2022): Semántica formal y verificador para planificación temporal
• Heinz et al. (2019): Codificación de planificación temporal a autómatas temporales
• Wimmer & von Mutius (2020): Verificador de certificados verificado para autómatas temporales
• Abdulaziz & Kurz (2023): Sistema de planificación basado en SAT verificado

Este artículo realiza contribuciones importantes en el campo de la verificación formal de planificación temporal. Aunque aún hay espacio para mejora en aspectos de practicidad, su rigor teórico e innovación metodológica sientan una base sólida para el desarrollo futuro de este campo.