Resumen Técnico: iSMC – Un Verificador de Modelos Simbólico Basado en BDD con Certificación Interactiva

1. Planteamiento del Problema

La verificación de modelos es una técnica fundamental para verificar la corrección de sistemas de hardware y software. Sin embargo, garantizar la fiabilidad del propio verificador de modelos constituye un desafío crítico. Los paradigmas de certificación tradicionales se basan en protocolos no interactivos: un demostrador (el verificador de modelos) genera un certificado (por ejemplo, una asignación satisfactoria o una prueba de resolución), y un verificador lo comprueba de forma independiente.

El artículo identifica una limitación teórica fundamental en este enfoque: para muchos problemas, incluida la verificación general de modelos CTL, los certificados pueden tener una longitud exponencial en el peor de los casos en función del tamaño de la instancia. En consecuencia, el verificador requiere tiempo exponencial para comprobarlos, lo que hace que el proceso de certificación sea impráctico para sistemas grandes a menos que $NP = coNP$.

Los autores proponen la certificación interactiva, un paradigma basado en sistemas de prueba interactiva (IP), donde un demostrador y un verificador participan en un protocolo de múltiples rondas. El verificador formula preguntas de forma adaptativa, lo que le permite detectar errores con alta probabilidad en tiempo polinómico, incluso si el cálculo subyacente es complejo. Aunque las pruebas interactivas para problemas PSPACE (como la verificación de modelos CTL) están teóricamente establecidas ($IP=PSPACE$ de Shamir), hacerlas prácticas para la verificación de modelos simbólica utilizando Diagramas de Decisión Binaria (BDD) ha seguido siendo un desafío abierto.

2. Metodología

El artículo presenta iSMC, el primer verificador de modelos auto-certificable que implementa certificación interactiva para la verificación de modelos CTL con requisitos de justicia. El sistema se construye sobre tres módulos centrales:

2.1 Arquitectura

• Solver (Resolutor): Un verificador de modelos simbólico basado en BDD que calcula el conjunto de estados alcanzables que satisfacen una especificación CTL. Opera sobre modelos booleanos aplanados (formato SMV) y utiliza la biblioteca BDD clic.
• Prover (Demostrador): Se ejecuta en la misma máquina que el Solver. Ejecuta la instancia de verificación de modelos y genera un rastro de ejecución compuesto por la secuencia de llamadas a la biblioteca BDD y aserciones realizadas durante el cálculo.
• Verifier (Verificador): Un módulo ligero que puede ejecutarse en un cliente con recursos limitados. No vuelve a ejecutar el algoritmo de verificación de modelos. En su lugar, participa en un protocolo interactivo con el Prover para verificar el rastro de ejecución.

2.2 El Protocolo TraceCert

La innovación central es TraceCert, un protocolo de prueba interactiva adaptado del trabajo de certificación QBF de Couillard et al. [11].

1. Rastro a Circuito: El rastro de ejecución se transforma en un Circuito Booleano Generalizado (GBC). Cada instrucción en el rastro se convierte en una puerta, y las aserciones (por ejemplo, "el conjunto de estados $C_1$ no es equivalente a $C_0$") se convierten en afirmaciones de equivalencia.
2. Aritmetización: Las funciones booleanas se codifican como polinomios multivariados sobre un campo finito $\mathbb{F}_p$. Esto permite al verificador comprobar propiedades del cálculo evaluando polinomios en puntos aleatorios en lugar de recorrer todo el circuito.
3. Reducción de Grado: Para asegurar que los polinomios tengan un grado bajo (necesario para la verificación en tiempo polinómico), el protocolo introduce puertas de reducción de grado ($\delta_x$) que reducen los exponentes a 1 sin cambiar el valor de la función en entradas booleanas.
4. Rondas Interactivas: El protocolo avanza en rondas, recorriendo el circuito. El Prover afirma el valor de una puerta; el Verificador desafía al Prover con asignaciones aleatorias a las entradas de la puerta. El Prover debe proporcionar polinomios consistentes con la afirmación. Si el Prover miente, la probabilidad de ser descubierto está acotada por el lema de Schwartz-Zippel.

2.3 Mejoras Técnicas Clave sobre Trabajos Previos

Los autores extienden la tecnología de [11] (que se centraba en QBF) para abordar las necesidades específicas de la verificación de modelos CTL, resolviendo tres cuellos de botella principales:

1. Renombrado y Equivalencia Eficientes: El protocolo original (CPCertify) manejaba las puertas de equivalencia y renombrado de manera ineficiente ($O(n^2)$ y $O(n^k)$). TraceCert optimiza estas rondas a $O(1)$ y $O(n)$ respectivamente.
2. Compatibilidad con la Recolección de Basura: Las bibliotecas BDD estándar utilizan cachés de cálculo globales y recolección de basura. El enfoque anterior requería que el Prover almacenara todos los BDD intermedios, impidiendo la recolección de basura. Los autores introducen TraceCertRev, una variante de protocolo de abajo hacia arriba que permite al Prover descartar resultados intermedios (actuando como un oráculo) sin comprometer la solidez, siempre que el Prover no conspira maliciosamente para recordar desafíos pasados.
3. Caché de Cálculo Global: La implementación anterior (blic) no podía utilizar una caché global porque manipulaba BDDs extendidos (eBDD) de una manera incompatible con la caché. Los autores introducen una representación inmutable de eBDD novedosa que utiliza campos de enlace para versionar nodos, permitiendo el uso de una tabla única global y mejorando significativamente el rendimiento.

3. Contribuciones Clave

1. Sistema iSMC: La primera implementación de un verificador de modelos auto-certificable con certificación interactiva para propiedades CTL arbitrarias con requisitos de justicia.
2. Protocolo TraceCert: Un nuevo protocolo de prueba interactiva que maneja eficientemente el renombrado de variables y las afirmaciones de equivalencia comunes en los rastros de verificación de modelos, reduciendo la complejidad de rondas de puertas específicas.
3. Implementación Optimizada de eBDD: Un nuevo algoritmo (ApplyEBDD) y estructura de datos que permiten el uso de cachés de cálculo globales y recolección de basura, superando las ineficiencias de la biblioteca blic anterior.
4. TraceCertRev: Una variante del protocolo que permite la recolección de basura durante la certificación, haciendo viable el sistema para la verificación de modelos a gran escala donde la memoria es una restricción.

4. Resultados Experimentales

Los autores evaluaron iSMC en 53 puntos de referencia de la pista de vivacidad de HWMCC'25.

• Rendimiento del Solver: En comparación con la herramienta madura NuSMV, el Solver de iSMC es en promedio 5.84 veces más lento. Los autores atribuyen esto principalmente a la falta de soporte para productos relacionales (una optimización de BDD) en el prototipo actual, ya que certificarlos interactivamente sigue siendo un problema abierto.
• Sobrecarga del Prover: El Prover se ejecuta en tiempo $O(S)$, donde $S$ es el tiempo del Solver. El factor constante es aproximadamente 2.00, lo que significa que la sobrecarga de certificación es aproximadamente el doble del tiempo de resolución.
• Eficiencia del Verificador: El Verificador es altamente eficiente. Para un tiempo de espera de 15 minutos en el Prover, el Verificador nunca tardó más de 3.6 segundos (aceleración promedio de 33.4x sobre el Prover). El tiempo de ejecución del Verificador escala linealmente con la longitud del rastro de ejecución, no con el tiempo de cálculo.
• Impacto de las Optimizaciones: Las mejoras (TraceCert, biblioteca clic, caché global) resultaron en una aceleración promedio de 2.26x en el tiempo de ejecución y una reducción de 16.12x en el uso de memoria en comparación con la implementación base que utilizaba CPCertify y blic.

5. Significado y Afirmaciones

El artículo afirma que iSMC representa un paso significativo hacia la certificación interactiva práctica para la verificación de modelos.

• Confianza en Servidores No Confiables: El sistema permite un escenario donde un cliente con recursos limitados puede delegar la verificación de modelos a un servidor potente pero no confiable. El servidor (Solver + Prover) realiza el cálculo pesado, mientras que el cliente (Verificador) certifica el resultado con alta probabilidad en tiempo polinómico.
• Verificación Polinómica: A diferencia de los métodos de certificación no interactiva que requieren tiempo exponencial para propiedades CTL generales, el Verificador de iSMC se ejecuta en tiempo polinómico en relación con el número de variables y la longitud del rastro.
• Escalabilidad: Los autores demuestran que, con sus optimizaciones, la sobrecarga de la certificación interactiva es manejable y la huella de memoria se reduce significativamente, haciendo que el enfoque sea factible para puntos de referencia no triviales.

Los autores mantienen la modestia, señalando que iSMC es un primer prototipo. Reconocen que el Solver es actualmente más lento que herramientas de última generación como NuSMV debido a la falta de optimizaciones (productos relacionales) y que la implementación actual se dirige a CTL, aunque el marco subyacente podría extenderse teóricamente al cálculo modal completo $\mu$.