Reducing Arbitrary Metric Temporal Formulas into Logic Programs under Answer Set Semantics

Problema
La Lógica de Equilibrio Temporal Métrico (MEL) extiende la Lógica de Equilibrio Temporal (TEL) incorporando restricciones temporales cuantitativas, lo que permite la especificación de plazos y duraciones en sistemas dinámicos como los sistemas embebidos y ciberfísicos. Aunque MEL permite expresiones precisas como "un evento debe ocurrir en un plazo de 5 milisegundos", las implementaciones existentes enfrentan desafíos. Reducciones previas de MEL a la Programación de Conjuntos de Respuestas (ASP) proposicional (por ejemplo, por Becker et al.) a menudo resultan en programas lógicos que contienen átomos de futuro puro en las cabezas de las reglas, creando dependencias de futuro. Estas dependencias obstaculizan la eficiencia de los resolvedores incrementales y de múltiples disparos (multi-shot), los cuales funcionan mejor cuando las derivaciones del estado actual dependen únicamente de la información de estados computados previamente en lugar de estados futuros no computados. Además, las traducciones existentes no manejan completamente los operadores temporales métricos binarios, tales como el hasta métrico o la liberación métrica.

Metodología
Los autores proponen una traducción de tipo Tseitin que mapea fórmulas temporales métricas arbitrarias en un fragmento específico de programas de lógica temporal métrica. La metodología central involucra:

1. Restricción a Trazas Estrictas: El enfoque asume trazas estrictas donde los puntos temporales aumentan estrictamente ($\tau(i) < \tau(i+1)$). Esto permite que los operadores métricos binarios con intervalos $[0..n]$ se desplieguen recursivamente mediante equivalencias que colapsan los operadores en sus argumentos de la derecha o constantes de verdad cuando el intervalo es $[0..0]$.
2. Definición de Clausura: Inspirados en la clausura de Fisher-Ladner en lógicas dinámicas, los autores definen un conjunto de clausura $cl(\phi)$ para una fórmula $\phi$. Este conjunto incluye no solo subfórmulas, sino también las expansiones recursivas de los operadores métricos binarios (por ejemplo, $\phi U_{\le n} \psi$ genera $\bigcirc^i(\phi U_{\le n-i} \psi)$).
3. Semántica de Tres Valores: Para probar la corrección de la traducción, el artículo utiliza una caracterización de tres valores de la lógica de Métrica Aquí-y-Allá (MHT). Esta semántica, equivalente a MHT, simplifica la verificación de las equivalencias lógicas requeridas para la reducción.
4. Reglas de Traducción: La traducción introduce átomos auxiliares (etiquetas) para cada fórmula en la clausura. Genera reglas donde los operadores de futuro afectan únicamente a las implicaciones, mientras que los cuerpos y las cabezas de estas implicaciones contienen solo referencias al pasado y al presente. La traducción distingue entre reglas dinámicas (que involucran operadores de siguiente/anterior) y reglas iniciales/finales.
5. Orden Bien Fundado: Para manejar la naturaleza no estructural de la clausura (donde las fórmulas desplegadas no son subfórmulas propiamente dichas), los autores definen una medida de complejidad $u(\phi)$ basada en el despliegue de los operadores, estableciendo un orden parcial estricto bien fundado para apoyar las pruebas inductivas.

Contribuciones Clave

• Reducción tipo Tseitin: Una reducción formal de fórmulas temporales métricas arbitrarias a programas de lógica temporal métrica restringidos a operadores de pasado en los cuerpos de las reglas.
• Manejo de Operadores Binarios: La traducción maneja explícitamente los operadores métricos binarios ($U_{\le n}, R_{\le n}, S_{\le n}, T_{\le n}$) con intervalos de la forma $[0..n]$, una limitación en las codificaciones previas de ASP proposicional.
• Eliminación de Dependencias de Futuro: Al asegurar que los cuerpos de las reglas dependan solo de información pasada y presente, los programas lógicos resultantes son compatibles con técnicas de resolución incremental utilizadas en resolvedores como telingo.
• Corrección Formal: El artículo demuestra que la traducción preserva el conjunto de Modelos de Equilibrio Métrico (equivalencia fuerte módulo átomos auxiliares) y establece un límite polinomial sobre el tamaño del programa generado en relación con el tamaño de la fórmula de entrada y el valor del intervalo máximo $n$.

Resultos
El artículo demuestra que para cualquier fórmula temporal métrica $\phi$, existe un programa de lógica temporal métrica $\Gamma$ tal que los modelos de equilibrio métrico de $\phi$ corresponden exactamente a la proyección de los modelos de equilibrio métrico de $\Gamma$ sobre el alfabeto original. El tamaño del programa generado está acotado por una función polinomial de la función del tamaño de la fórmula y el valor máximo del intervalo $n$. Se muestra que la traducción es correcta bajo el supuesto de trazas estrictas e intervalos de la forma $[0..n]$.

Significancia
El artículo afirma proporcionar una "forma normal" para interpretar teorías temporales métricas bajo la semántica de conjuntos de respuestas. Al vincular las fórmulas temporales métricas con programas lógicos restringidos a operadores de pasado, el trabajo permite aprovechar los resolvedores de ASP existentes y eficientes (específicamente aquellos que soportan resolución de múltiples disparos e incremental) para el razonamiento sobre restricciones temporales métricas. Esto facilita la implementación práctica de MEL en dominios que requieren una precisión temporal, como el software de tiempo real y los sistemas embebidos, sin las ineficiencias asociadas con las dependencias de futuro. Los autores señalan que, si bien el trabajo actual se limita a intervalos $[0..n]$, sienta las bases para extender estas reducciones a intervalos arbitrarios e integrarlas en el resolvedor telingo.