Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

Resumen Técnico: Restricciones Diferidas en el Estrechamiento para los Análisis Basados en Lógica de Sistemas en Tiempo Real

Planteamiento del Problema
El análisis formal de sistemas en tiempo real enfrenta dos desafíos primarios respecto al infinito: la posibilidad de un número ilimitado de agentes y mensajes, y un espacio de estados que es infinito debido al tiempo denso. Los métodos de verificación tradicionales en Lógica de Reescritura (RL), particularmente aquellos implementados en el motor de reescritura Maude, han sido históricamente limitados. Si bien Maude soporta la verificación de invariantes para sistemas con componentes totalmente especificados (términos de base) y restricciones SMT, tiene dificultades con sistemas que contienen un número desconocido de agentes o parámetros arbitrarios. Además, las técnicas simbólicas previas a menudo dependían del muestreo de tiempo, lo cual carece de solidez y completitud en entornos de tiempo denso. Los enfoques existentes que utilizan variables lógicas para agentes ilimitados suelen resultar en procedimientos de semi-decisión con espacios de búsqueda infinitos, careciendo de mecanismos para garantizar la terminación.

Metodología
Los autores proponen un novedoso marco de verificación que integra tres técnicas principales para abordar estas limitaciones:

1. Reescritura Modulo SMT: Utilización de teorías SMT para la representación simbólica de las restricciones de tiempo.
2. Estrechamiento con Variables Lógicas: Empleo de variables lógicas para razonar sobre sistemas con un número desconocido o arbitrario de agentes.
3. Restricciones Diferidas y Plegado (Folding): Introducción de un almacén de restricciones sobre términos parcialmente instanciados, inspirado en la Programación Lógica con Restricciones (CLP).

La innovación central es el Estrechamiento de Plegado Diferido (Delayed Folding Narrowing). A diferencia del estrechamiento estándar, este método permite que las expresiones SMT en las condiciones de las reglas contengan partes "diferidas": subexpresiones que no pueden evaluarse hasta que los términos estén más instanciados. Esto se logra mediante una Extensión SMT donde las expresiones SMT no válidas (por ejemplo, mte(t, T') que representa un tiempo máximo transcurrido) se abstraen en variables frescas. Estas restricciones se acumulan y solo se resuelven o propagan una vez que los términos están suficientemente instanciados.

El marco define Teorías de Reescritura en Tiempo Real Lógicas, que extienden las teorías de reescritura en tiempo real estándar para permitir:

• Que las condiciones en las reglas de reescritura incluyan expresiones SMT con partes diferidas.
• Que los lados derechos (RHS) incluyan variables no presentes en el lado izquierdo (LHS).
• Que las consultas contengan variables compartidas en los estados inicial y objetivo.

Para asegurar la terminación, el método emplea un mecanismo de plegado. Se construye un grafo de estados donde un estado simbólico $v'$ es eliminado si es una instancia de un estado previamente explorado modulo la teoría ecuacional. Los autores demuestran que bajo condiciones específicas (específicamente, una jerarquía de tipos/sorts cuidadosamente diseñada), este preorden de plegado asegura un espacio de búsqueda finito, transformando el procedimiento de semi-decisión en un procedimiento de decisión para la verificación de invariantes.

Contribuciones Clave

1. Estrechamiento de Plegado Diferido: La definición e implementación de una relación de estrechamiento que maneja expresiones SMT extendidas con restricciones diferidas. Esto permite la verificación de sistemas con arbitrarias variables lógicas y SMT tanto en la configuración inicial como en el invariante.
2. Verificación del Protocolo de Fischer con Tiempo: El artículo presenta la primera verificación automática de la corrección del protocolo de exclusión mutua de Fischer con tiempo en su configuración más general. Esto incluye un número arbitrario de procesos y parámetros temporales arbitrarios ($\gamma$ y $\delta$). Esto se logró diseñando una jerarquía de tipos específica para garantizar la terminación del procedimiento de plegado y utilizando variables lógicas para representar el número no especificado de procesos.
3. Síntesis de Controlador para los Filósofos Comensales: El marco se aplica a un problema de filósofos comensales con tiempo para sintetizar un controlador (el "lackey" o ayudante). Al dejar las transiciones del controlador no especificadas (representadas por variables lógicas), el procedimiento de estrechamiento sintetiza las transiciones faltantes requeridas para satisfacer una propiedad de alcanzabilidad (por ejemplo, que filósofos específicos entren a la sala antes de un plazo determinado).

Resultos
El método ha sido implementado como una extensión del motor de reescritura Maude utilizando características de meta-nivel.

• Protocolo de Fischer: Los autores verificaron con éxito la exclusión mutua para un número arbitrario de procesos. Cuando el estado inicial fue restringido de tal manera que $\gamma > \delta$, el espacio de búsqueda fue finito (conteniendo solo 3 estados debido al plegado), y la herramienta confirmó que ningún estado alcanzable violaba el invariante. Por el contrario, cuando $\delta \ge \gamma$, se encontró un contraejemplo.
• Filósofos Comensales: El sistema sintetizó con éxito un autómata "lackey" que permitía que filósofos específicos entraran a la sala. La salida proporcionó un conjunto concreto de transiciones y ubicaciones para el controlador, demostrando la capacidad del marco para manejar tareas de síntesis.
• Eficiencia: El mecanismo de plegado redujo significamente el espacio de búsqueda, permitiendo el análisis de sistemas que de otro modo serían intratables debido a espacios de estados infinitos.

Significancia y Reivindicaciones
El artículo afirma proporcionar una base sólida y expresiva para la verificación simbólica de teorías de reescritura en tiempo real. Su significancia radica en cerrar la brecha entre la expresividad de la programación lógica (manejo de agentes ilimitados vía variables lógicas) y la precisión del análisis en tiempo real (manejo de tiempo denso vía SMT y restricciones diferidas).

Los autores enfatizan que su enfoque va más allá de Maude "estándar" y de las herramientas existentes de Autómatas Temporizados Paramétricos (PTA), que típicamente requieren un número fijo de procesos o límites de tiempo fijos. Al soportar un número arbitrario de parámetros y un número ilimitado de agentes dentro de un mismo marco, el método ofrece un enfoque uniforme para analizar modelos complejos en tiempo real, incluyendo la síntesis de componentes faltantes del sistema. El trabajo sugiere que las restricciones diferidas son un mecanismo crucial para lograr la terminación en análisis simbólicos de sistemas de estado infinito.