Resumen Técnico: Un Procedimiento de Decisión para una Teoría de Conjuntos Finitos con Intervalos Enteros Finitos

Enunciado del Problema

En el contexto de la verificación formal y el análisis, las herramientas de razonamiento automatizado son esenciales para descargar condiciones de verificación. Aunque las herramientas existentes basadas en la teoría de conjuntos (por ejemplo, B, ProB) son efectivas, a menudo carecen de procedimientos de decisión para fragmentos específicos de la teoría de conjuntos que combinan conjuntos finitos con intervalos enteros. Específicamente, el álgebra booleana de conjuntos finitos extendida con restricciones de cardinalidad (denotada como $L|\cdot|$) es decidible, pero no puede expresar ni razonar de forma nativa sobre intervalos enteros finitos (rangos) donde los límites pueden ser variables no acotadas. Esta limitación obstaculiza la verificación automática de propiedades que involucran operaciones de conjuntos, como encontrar el mínimo o el máximo de un conjunto, particionar conjuntos basándose en umbrales enteros o razonar sobre dominios de arrays definidos por intervalos. El problema central abordado es la decidibilidad de una teoría que integra conjuntos finitos, restricciones de cardinalidad e intervalos enteros finitos (denotada como $L[\ ]$) dentro de una lógica libre de cuantificadores.

Metodología

Los autores proponen un procedimiento de decisión, SAT $[\ ]$, que extiende el solucionador existente SAT $|\cdot|$ (para $L|\cdot|$) para manejar intervalos enteros. La metodología se basa en una teoría base de conjuntos finitamente heredados implementada dentro del lenguaje de Programación Lógica con Restricciones (CLP) CLP($SET$) y la herramienta {log}.

Componentes Técnicos Clave:

1. Extensión del Lenguaje ($L[\ ]$):

   • El lenguaje se extiende para incluir términos de conjunto de la forma $[k, m]$, que representan el conjunto $\{p \in \mathbb{Z} \mid k \le p \le m\}$.
   • Los límites del intervalo ($k, m$) pueden ser términos lineales enteros, incluidas variables.
   • La lógica permanece libre de cuantificadores, utilizando conjunciones y disyunciones de restricciones que involucran pertenencia a conjuntos, unión, disyunción, cardinalidad y pertenencia a intervalos.

2. Identidad Central y Estrategia de Reducción:

   • La idea teórica central es la identidad: $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$.
   • Esta identidad permite que el procedimiento transforme restricciones que involucran igualdad con un intervalo en restricciones que involucran relaciones de subconjunto y cardinalidad.
   • El solucionador reescribe las fórmulas en una conjunción de una fórmula estándar $L|\cdot|$ ($\Phi_{|\cdot|}$) y un conjunto de restricciones de subconjunto que involucran intervalos ($\Phi_{\subseteq[\ ]}$), típicamente de la forma $X \subseteq [p, q]$ donde $X$ es una variable.

3. El Algoritmo SAT $[\ ]$:

   • Reglas de Reescritura: El solucionador emplea un conjunto de reglas de reescritura (STEPS$[\ ]$) que reducen la complejidad sintáctica. Estas reglas manejan restricciones de igualdad, pertenencia, unión, disyunción y cardinalidad que involucran intervalos.
   • Reducción a Aritmética Entera: Muchas reglas reescriben las restricciones de conjuntos que involucran intervalos directamente en restricciones de aritmética lineal entera (LIA).
   • Verificación de la Solución Mínima: Cuando quedan restricciones irreducibles de la forma $X \subseteq [p, q]$, el procedimiento no falla simplemente. En su lugar, aprovecha la propiedad de que si una fórmula es satisfacible, debe tener una "solución mínima" (una solución donde los conjuntos tienen la cardinalidad posible mínima).
     • El solucionador calcula la solución mínima para la parte $L|\cdot|$ ($\Phi_{|\cdot|}$).
     • Luego verifica si esta solución mínima satisface las restricciones de intervalo ($\Phi_{\subseteq[\ ]}$).
     • Los autores demuestran que si ninguna solución mínima satisface la fórmula completa, entonces ninguna solución más grande lo hará tampoco, haciendo que la fórmula sea insatisfacible.

4. Implementación en {log}:

   • El procedimiento se implementa en {log} (setlog), una herramienta basada en Prolog.
   • La implementación incluye un esquema de memorización para rastrear las sustituciones de variables para intervalos, evitando reescrituras redundantes y mejorando la eficiencia.
   • Las restricciones derivadas (por ejemplo, intersección, diferencia) se definen en términos de restricciones primitivas para mantener la consistencia.

Contribuciones Clave

1. Prueba de Decidibilidad: El artículo proporciona la primera prueba de que el álgebra booleana de conjuntos finitos extendida con restricciones de cardinalidad e intervalos enteros finitos ($L[\ ]$) es decidible.
2. Procedimiento de Decisión (SAT $[\ ]$): Se presenta un algoritmo completo que decide la satisfacibilidad de las fórmulas $L[\ ]$. Se demuestra que el procedimiento es correcto, completo y terminante.
3. Integración de Intervalos y Conjuntos: A diferencia de enfoques que tratan los intervalos como un dominio separado o requieren límites constantes, este trabajo integra sin fisuras intervalos enteros acotados por variables en la teoría de conjuntos, permitiendo la expresión de operadores no triviales (por ejemplo, el $i$-ésimo elemento más pequeño, partición por un umbral) en una lógica libre de cuantificadores.
4. Implementación y Herramientas: El procedimiento de decisión se implementa como una extensión de la herramienta {log}, proporcionando una capacidad dual como lenguaje de programación lógica con restricciones y como solucionador de satisfacibilidad.

Resultados y Evaluación

El artículo presenta evidencia empírica y un estudio de caso para demostrar la utilidad práctica del enfoque:

• Evaluación de Referencias: Se resolvió un conjunto de 60 fórmulas $L[\ ]$, que representan propiedades de operadores definidos en el artículo (por ejemplo, mínimo, máximo, $i$-ésimo elemento). {log} resolvió todos los problemas en un promedio de 0.51 segundos por problema, con solo uno que tardó más de 5 segundos.
• Estudio de Caso (Algoritmo de Ascensor): Los autores modelaron un sistema de control de ascensores donde el ascensor debe atender solicitudes en una dirección específica. El modelo utilizó intervalos enteros para definir pisos y solicitudes.
  • El sistema incluía 7 operaciones (por ejemplo, agregar solicitudes, atender la siguiente solicitud).
  • {log} se utilizó para descargar automáticamente 49 lemas de invarianza (demostrando que las operaciones de estado preservan 7 invariantes de estado) y 7 comprobaciones de estado inicial.
  • Todas las pruebas se completaron en aproximadamente 0.5 segundos en una computadora portátil estándar.
  • La herramienta generó exitosamente contraejemplos cuando los invariantes se debilitaron intencionalmente, demostrando sus capacidades de depuración.

Significado y Afirmaciones

Los autores afirman que este trabajo representa un paso significativo hacia adelante en el razonamiento automatizado para la verificación formal. Al extender el fragmento decidible de la teoría de conjuntos para incluir intervalos enteros finitos con límites variables, el enfoque permite la verificación automática de propiedades que anteriormente eran difíciles o imposibles de expresar sin cuantificadores.

El artículo enfatiza que el enfoque está arraigado en la teoría de conjuntos, distinguiéndolo de otras herramientas de razonamiento de intervalos (como las basadas en el álgebra de intervalos de Allen o retículos de análisis estático) que a menudo carecen de la capacidad de combinar intervalos con operaciones de conjuntos generales. La integración del razonamiento de intervalos en el marco {log} permite a los usuarios escribir programas y demostrar sus propiedades utilizando el mismo código y herramienta, aprovechando la dualidad de fórmula y programa. Los autores notan modestamente que, aunque el enfoque es general y coherente, puede incurrir en costos de eficiencia en comparación con solucionadores especializados para problemas específicos de solo intervalos, pero la compensación es la capacidad de razonar sobre estructuras híbridas complejas de conjuntos e intervalos.