Resumen Técnico: TREBL – Lógica Temporal de Event-B Relativamente Completa

1. Planteamiento del Problema

La verificación de condiciones de vivacidad (liveness) es un aspecto crítico en los métodos formales basados en estados, como Event-B. Sin embargo, existen desafíos fundamentales en la integración de la lógica temporal con estos métodos:

• Limitación de Expresividad vs. Completitud: Las lógicas temporales clásicas (LTL, CTL) son completas pero proposicionales, lo que limita su capacidad para expresar propiedades de sistemas complejos definidos mediante lógica de primer orden. Por otro lado, las extensiones temporales de la lógica de primer orden son más expresivas pero inherentemente incompletas.
• Interpretación sobre Trazas vs. Estados: En los métodos basados en estados (como Event-B), un estado determina todas las trazas que comienzan en él. Las lógicas temporales tradicionales interpretan fórmulas sobre trazas arbitrarias, lo que rompe la conexión directa con la especificación del estado y dificulta la completitud de las reglas de derivación.
• Falta de Completitud Relativa: Trabajos anteriores (como los de Hoang y Abrial, y Ferrarotti et al.) lograron definir reglas de derivación sonoras para fragmentos de LTL(EB), pero la completitud relativa (la capacidad de derivar cualquier fórmula válida) estaba restringida a máquinas "tail-homogéneas" (donde la no-determinidad intrínseca está restringida) y requería que las fórmulas se interpretaran sobre trazas, no sobre estados.

El objetivo es desarrollar una lógica temporal para Event-B que sea expresiva (capaz de manejar condiciones de vivacidad complejas), sonora y relativamente completa, interpretando las fórmulas sobre estados en lugar de trazas.

2. Metodología

Los autores proponen TREBL (Temporal Event-B Logic), un fragmento de una lógica extendida llamada $L_{ext}$. La metodología se basa en los siguientes pilares:

A. Extensión de la Lógica de Event-B ($L_{ext}$)

En lugar de tratar las trazas como objetos de primer orden, los autores extienden la lógica de Event-B para capturar explícitamente los efectos de las transiciones:

• Conjuntos de Actualización (Update Sets): Se introducen fórmulas para describir el conjunto de cambios que un evento provoca en un estado.
• Operadores Modales de Actualización: Se define el operador $[X]\phi$, que significa "si se aplica el conjunto de actualización $X$, entonces $\phi$ se cumple en el estado resultante".
• Composición de Pasos: Se definen fórmulas recursivas $USet^*(k, X)$ para representar conjuntos de actualización compuestos por $k$ pasos, permitiendo razonar sobre secuencias de estados sin salir del marco de la lógica de primer orden.

B. Definición de Operadores Temporales como Atajos

Los operadores temporales estándar ($\square$ - siempre, $\diamond$ - eventualmente, $U$ - hasta) y sus variantes para trazas individuales ($\square_1, \diamond_1$) o subconjuntos definibles de trazas, se definen como atajos sintácticos de fórmulas complejas en $L_{ext}$.

• Ventaja clave: Aunque expresan propiedades de trazas, todas las fórmulas de TREBL se interpretan sobre estados iniciales. Esto alinea la lógica con la naturaleza de Event-B, donde un estado determina el futuro.

C. Sistema de Derivación y Variantes

Para lograr la completitud relativa, se introduce un sistema de reglas de derivación que depende de la existencia de términos de variante (variant terms):

• Se definen varios tipos de variantes (c-variantes para convergencia, d-variantes para divergencia, e-variantes para alcanzabilidad, y variantes condicionales/simultáneas para progresos complejos).
• Estas variantes toman valores en conjuntos bien fundados (como los números naturales) y garantizan que las condiciones de vivacidad se cumplan al disminuir o mantenerse en el tiempo.

D. Refinamiento Conservador

Un componente crucial de la metodología es la demostración de que, para cualquier máquina Event-B que satisfaga una propiedad de vivacidad, siempre existe un refinamiento conservador en el que los términos de variante necesarios pueden definirse explícitamente. Esto elimina la necesidad de asumir restricciones artificiales como la "homogeneidad de cola" (tail-homogeneity).

3. Contribuciones Clave

1. Definición de TREBL: Se define formalmente el fragmento de lógica temporal que cubre invariantes, existencia, progreso, persistencia y alcanzabilidad, tanto para todas las trazas como para trazas individuales o subconjuntos definibles.
2. Interpretación sobre Estados: Se logra que las fórmulas temporales se interpreten sobre estados, simplificando la semántica y permitiendo la integración con las herramientas de prueba existentes de Event-B (como RODIN).
3. Completitud Relativa sin Restricciones: Se demuestra que el sistema de reglas de derivación es relativamente completo para máquinas suficientemente refinadas. A diferencia de trabajos previos, esto se logra sin la restricción de que las máquinas deban ser tail-homogéneas.
4. Nuevas Reglas de Derivación: Se presentan reglas sonoras para:
   • Invarianza (para todas las trazas y trazas individuales).
   • Existencia y Persistencia (usando variantes c, d, lc, ld, pld, pd).
   • Progreso (usando variantes simultáneas y condicionales).
   • Alcanzabilidad.
5. Aplicación a Seguridad: Se demuestra la utilidad de TREBL en problemas de seguridad complejos, como la no interferencia (non-interference) y la deducibilidad acotada (bounded deducibility), mostrando que condiciones que en LTL son difíciles de expresar se vuelven invariantes simples en TREBL.

4. Resultados Principales

• Teorema de Sonido: El sistema de reglas de derivación $R$ es sonoro; si una fórmula $\phi$ es derivable ($M \vdash_R \phi$), entonces es válida en la máquina ($M \models \phi$).
• Teorema de Completitud Relativa: Si una máquina $M$ satisface las "suposiciones de relatividad" (es consistente, incluye todas las invariantes necesarias y está suficientemente refinada para definir las variantes), y una fórmula $\phi \in TREBL$ es válida ($M \models \phi$), entonces existe una derivación formal ($M \vdash_R \phi$).
• Existencia de Refinamientos: Se prueba constructivamente que siempre es posible refinar una máquina Event-B para incluir los términos de variante necesarios, garantizando así que la completitud relativa es alcanzable en la práctica.
• Eliminación de Restricciones: Se elimina la restricción de "tail-homogeneidad" requerida en trabajos anteriores, permitiendo el razonamiento sobre máquinas con no-determinismo intrínseco más general.

5. Significado e Impacto

El trabajo representa un avance significativo en la verificación formal de sistemas críticos:

• Puente entre Lógica Temporal y Métodos Formales: Resuelve la dicotomía entre la expresividad de la lógica temporal y la completitud de los métodos basados en estados. Al interpretar las fórmulas sobre estados, TREBL permite utilizar la potencia de la lógica de primer orden de Event-B para probar propiedades de trazas.
• Viabilidad de la Verificación Automática: Al demostrar que las variantes necesarias siempre pueden definirse mediante refinamiento, se establece que la verificación de condiciones de vivacidad complejas es mecánicamente posible, no solo teóricamente.
• Aplicabilidad en Seguridad: La capacidad de expresar propiedades de seguridad (como la no interferencia) como invariantes simples en lugar de propiedades temporales complejas facilita enormemente su verificación en herramientas como RODIN.
• Generalidad: Aunque se centra en Event-B, la metodología es aplicable a otros métodos basados en estados rigurosos (como ASM, B, TLA+), siempre que permitan definir conjuntos de actualización y lógica de estados.

En conclusión, TREBL proporciona un marco teórico robusto y completo para la verificación de propiedades de vivacidad en sistemas Event-B, superando las limitaciones de expresividad y completitud de las aproximaciones anteriores y allanando el camino para una implementación práctica en herramientas de verificación asistida por computadora (mencionado que se abordará en la Parte II del trabajo).