Resumen Técnico: Lógica de Procesos Etiquetada

1. Planteamiento del Problema

La Lógica de Procesos (PL) extiende la Lógica Dinámica (DL) al desplazar el enfoque del razonamiento sobre estados finales de programas hacia el razonamiento sobre trazas de ejecución completas. Aunque la teoría proposicional de la Lógica de Procesos (PPL) es bien conocida en cuanto a su decidibilidad y completitud, la extensión de primer orden (FOPL) presenta desafíos significativos.

La dificultad central radica en el razonamiento composicional requerido para la lógica de procesos de primer orden sobre programas regulares. En la Lógica Dinámica estándar, una fórmula $[\alpha]\phi$ afirma que toda ejecución terminante de $\alpha$ finaliza en un estado que satisface $\phi$. En la Lógica de Procesos, $[\alpha]\pi$ afirma que cada traza de ejecución de $\alpha$ satisface una propiedad temporal $\pi$ (expresada mediante operadores de Lógica Temporal Lineal como siguiente, siempre, eventualmente y hasta).

Los sistemas de cálculo composicional existentes para fragmentos de esta lógica (por ejemplo, el cálculo de secuentes de Beckert para programas while deterministas, o extensiones como DLT y DTL) no logran proporcionar un tratamiento completo para la lógica de procesos de primer orden completa sobre programas regulares (potencialmente no deterministas). Específicamente:

• Las reglas composicionales para programas secuenciales (dividir una propiedad de traza $\pi$ a través de $\alpha; \beta$) a menudo dependen fuertemente de la forma específica de la fórmula temporal (por ejemplo, reglas específicas para "siempre" frente a "eventualmente").
• Algunas reglas propuestas son insuficientes para programas regulares generales porque las pruebas (tests) en composiciones secuenciales pueden bloquear trazas, invalidando divisiones composicionales simples.
• Ningún sistema existente ofrece un marco uniforme donde las propiedades basadas en trazas y los cálculos de primer orden se manejen dentro de la misma estructura de prueba.

2. Metodología: Sistemas de Prueba Cíclicos Etiquetados

El artículo propone un novedoso marco de prueba teórica que enriquece las fórmulas de la lógica de procesos con etiquetas para registrar explícitamente la información de ejecución durante las derivaciones, en lugar de depender de reglas composicionales cada vez más complejas.

2.1 Fórmulas Etiquetadas

Los autores introducen fórmulas etiquetadas de la forma $\sigma : \phi$, donde:

• $\phi$ es una fórmula de lógica de procesos.
• $\sigma$ es una etiqueta que representa la traza de ejecución o la configuración del programa acumulada hasta el momento.
  • En la Lógica de Procesos Proposicional (PPL), las etiquetas son trazas de mundos ($\sigma \in L$), construidas a partir de variables de mundo, variables de traza y concatenación.
  • En la Lógica de Procesos de Primer Orden (FOPL), las etiquetas se enriquecen con actualizaciones de programa ($U$) para registrar el efecto acumulativo de las asignaciones (por ejemplo, $\{u := e\}$) sobre una estructura aritmética.

Este enfoque pone la información de ejecución intermedia a disposición del sistema de prueba. En consecuencia, el sistema de prueba ya no necesita dividir trazas secuenciales utilizando reglas temporales de propósito específico en el punto de la secuencia; en su lugar, despliega la estructura del programa mientras acumula la información en la etiqueta.

2.2 Estructura de Prueba Cíclica

Dado que los programas regulares incluyen iteración ($\alpha^*$), la búsqueda de pruebas puede generar derivaciones infinitas. Para manejar esto, los autores adoptan la teoría de pruebas cíclicas.

• Prepruebas: Árboles finitos donde los nodos hoja (brotes) pueden "re-enlazar" a nodos ancestros con formas sintácticas idénticas (modulo el renombramiento de variables).
• Condición Cíclica: Para asegurar la corrección, no todas las ciclos son válidos. El artículo define una traza de derivación progresiva. Una derivación es una prueba cíclica válida si cada camino infinito contiene un "paso progresivo" (por ejemplo, aplicar una regla que reduce la complejidad de la traza o de la fórmula).
• Mecanismo de Corrección: Los autores demuestran la corrección mostrando que cualquier derivación infinta que satisfaga la condición cíclica induce un descenso infinito en un orden de multiconjunto bien fundado de "trazas de contraejemplo mínimas". Esta contradicción asegura que ninguna fórmula inválida pueda ser probada.

2.3 Los Sistemas de Prueba

Se definen dos sistemas específicos:

1. G3PPL: Un sistema de prueba etiquetado cíclico para la Lógica de Procesos Proposicional. Extiende las técnicas de secuentes etiquetados para lógicas modales, adaptándolas a la semántica de trazas.
2. G3FOPL: Un sistema de prueba etiquetado cíclico para la Lógica de Procesos de Primer Orden. Extiende G3PPL reemplazando las reglas de programas atómicos por reglas para asignaciones (actualizando la etiqueta) y añadiendo reglas estándar de cuantificadores de primer orden.

3. Contribuciones Clave

El artículo realiza las siguientes contribuciones específicas:

• Fórmulas Etiquetadas: La introducción de etiquetas de traza para PPL y etiquetas basadas en actualizaciones para FOPL, permitiendo el seguimiento explícito del historial de ejecución dentro de la estructura de la prueba.
• Sistemas Etiquetados Cíclicos: La definición de G3PPL y G3FOPL, que comparten un marco etiquetado común pero utilizan reglas específicas para la lógica de procesos proposicional y de primer orden, respectivamente.
• Pruebas de Corrección: Una prueba de corrección para ambos sistemas. El argumento se basa en reducir cada camino de derivación infinita progresiva a un descenso infinito en un orden de multiconjunto bien fundado de trazas de contraejemplo mínimas.
• Pruebas de Completitud:
  • Para G3PPL, la completitud se establece demostrando que el sistema etiquetado puede derivar cada axioma y regla del sistema de prueba de estilo Hilbert establecido para PPL.
  • Para G3FOPL, la completitud se establece adaptando el argumento clásico de completitud para la Lógica Dinámica de Primer Orden (FODL) al entorno basado en trazas, utilizando codificaciones aritméticas.

4. Resultados

• Marco Uniforme: El artículo construye con éxito un marco uniforme donde las propiedades de programas basadas en trazas y los cálculos de primer orden se manejan dentro de la misma estructura de prueba.
• Completitud para Programas Regulares: Los sistemas proporcionan el primer marco lógico completo para la lógica de procesos de primer orden completa sobre programas regulares (incluyendo la elección no determinista y la iteración).
• Corrección y Completitud: Tanto G3PPL como G3FOPL son probados como correctos y completos con respecto a sus respectivas semánticas.

5. Significado

El artículo afirma que este trabajo aborda un vacío persistente en la literatura. Los sistemas previos:

• Estaban limitados a programas deterministas (por ejemplo, DLT, DTL).
• Carecían de completitud para programas regulares generales.
• No podían manejar uniformemente todos los operadores LTL (por ejemplo, hasta) en presencia de no determinismo.

Al utilizar etiquetas para externalizar la información de ejecución y pruebas cíclicas para manejar la iteración, los autores proporcionan un mecanismo principiado y uniforme para razonar sobre propiedades de traza. Esto permite la verificación de especificaciones donde el comportamiento intermedio es esencial, sin requerir reglas composicionales ad-hoc para cada operador temporal. El marco unifica el tratamiento de los niveles proposicional y de primer orden, ofreciendo una base robusta para la verificación de programas que involucran propiedades temporales complejas.