Definability of Functional Properties in the Basic Modal-Temporal Language over Ordered Frames

Resumen Técnico: Definibilidad de Propiedades Funcionales en el Lenguaje Modal-Temporal Básico sobre Marcos Ordenados

Planteamiento del Problema
Este artículo investiga el poder expresivo del lenguaje modal-temporal básico $LT \times W$, formado al añadir los operadores temporales de Prior $G$ (siempre en el futuro) y $H$ (siempre en el pasado) al lenguaje modal básico con $\Box$ (en todas las imágenes funcionales). El estudio se centra en la definibilidad de nueve propiedades funcionales específicas —totalidad, no totalidad, inyectividad, suryectividad, monotonicidad, monotonicidad estricta, antitonicidad, antitonicidad estricta y constancia— a través de cinco tipos de orden distintos: preórdenes (PRE), preórdenes estrictos (sPRE), órdenes parciales (PO), órdenes lineales (LO) y órdenes lineales estrictos (sLO).

Un desafío central abordado es el entorno de "multiflow" (multiflujo), donde coexisten múltiples funciones de accesibilidad y los operadores modales cuantifican indiscriminadamente sobre sus imágenes combinadas. Trabajos previos (p. ej., [1, 3]) habían restringido el análisis a órdenes lineales estrictos y propiedades de Dominio Uniforme (U-Dom). Este artículo tiene como objetivo determinar si estas propiedades son definibles de forma aislada y cómo su definibilidad varía a través de un espectro más amplio de estructuras de orden, examinando específicamente el impacto de dos lecturas semánticas: la interpretación estándar (que incluye el instante actual) y la interpretación estricta (que excluye el instante actual).

Metodología
Los autores emplean un enfoque analítico de dos etapas para mapear los límites expresivos de $LT \times W$:

1. Entorno de Multiflujo Ordenado Arbitrario: El estudio establece primero los límites de definibilidad en el entorno general donde los marcos consisten en familias arbitrarias de funciones. Aquí, los operadores modales actúan como cuantificadores de segundo orden sobre la unión de todas las imágenes funcionales. Los autores utilizan p-morfismos suryectivos (que inducen bisimulaciones funcionales) para probar la no definibilidad. Si un p-morfismo mapea un marco que satisface una propiedad hacia uno que no la satisface, la propiedad es indefinible.
2. Refinamiento Estructural (Marcos Mínimos): Para aislar la fuente de las limitaciones de expresividad, los autores introducen "marcos funcionales mínimos" (la familia $O_2$), restringiendo los marcos a como máximo dos flujos y una única función de accesibilidad. Esta reducción colapsa la complejidad de segundo orden del entorno de multiflujo en una lectura relacional de primer orden.
3. Análisis Comparativo: El estudio compara los resultados de los marcos mínimos contra otros dos marcos:
   • Lenguajes Indexados: Donde los operadores están explícitamente etiquetados para distinguir funciones específicas.
   • Marcos de Dominio Uniforme (U-Dom): Donde todas las funciones en un marco comparten un dominio común.
4. Variaciones Semánticas: El análisis se lleva a cabo bajo tanto la interpretación estándar ($G, H$) como la estricta ($G^*, H^*$) para determinar si excluir el instante actual altera el panorama de la definibilidad.

Contribuciones Clave y Resultados

• Límites Expresivos en el Entorno de Multiflujo:
  En el entorno general de multiflujo, el lenguaje es significativamente débil. El estudio demuestra que solo la totalidad y la suryectividad son definibles, y solo dentro de órdenes lineales (LO y sLO). Todas las demás propiedades (inyectividad, monotonicidad, constancia, etc.) son indefinibles en cualquier tipo de orden, incluyendo los lineales. Esto se atribuye a la "cuantificación indiscriminada" sobre múltiples funciones, lo que oscurece los comportamientos funcionales individuales.

• El Impacto de los Marcos Mínimos:
  Al restringir la semántica a marcos mínimos (función única), el panorama de la definibilidad se expande drásticamente:

  • Monotonicidad y Antitonicidad: Estas se vuelven definibles en todos los tipos de orden (PRE, sPRE, PO, LO, sLO).
  • Inyectividad: Se vuelve definible en órdenes lineales estrictos (sLO) bajo la interpretación estándar.
  • Monotonicidad/Antitonicidad Estricta: Se vuelven definibles en preórdenes estrictos y órdenes lineales estrictos.
  • Constancia: Permanece indefinible en órdenes no lineales (PRE, sPRE, PO) incluso en marcos mínimos, requiriendo un argumento de equivalencia semántica distinto (ya que es preservada por p-morfismos).

• El Rol de la Interpretación Estricta:
  En el entorno general de multiflujo, la elección entre interpretaciones estándar y estricta produce resultados idénticos. Sin embargo, en marcos mínimos, la interpretación estricta ($G^*, H^*$) proporciona ganancias cruciales:

  • Permite la definición de inyectividad en órdenes lineales (LO) donde la interpretación estándar falla.
  • Permite la definición de monotonicidad estricta y antitonicidad estricta en todos los tipos de orden, incluyendo los no estrictos (PRE, PO, LO), al tratarlos efectivamente como sus contrapartes estrictas.

• Equivalencia de Marcos:
  El artículo demuestra que los patrones de definibilidad obtenidos en marcos mínimos son idénticos a los de los lenguajes indexados (don donde las funciones se distinguen sintácticamente) y los marcos de Dominio Uniforme (U-Dom). Esto indica que las limitaciones de expresividad del marco original provienen no de la debilidad de los operadores en sí, sino de la multiplicidad incontrolada de funciones con dominios divergentes. Una vez que la multiplicidad funcional se controla (vía simplificación estructural, uniformidad de dominio o indexación sintáctica), los operadores básicos recuperan su plena capacidad.

• Obstáculos Fundamentales:
  Incluso tras controlar la multiplicidad funcional, un "núcleo duro" de propiedades —totalidad, no totalidad, inyectividad, suryectividad y constancia— permanece indefinible en todos los órdenes no lineales (PRE, sPRE, PO). Los autores concluyen que la falta de conectividad (incomparabilidad de puntos) es un obstáculo fundamental que las modalidades temporales no pueden superar, independientemente de la interpretación o el refinamiento estructural.

Significancia
El artículo proporciona una clasificación sistemática de los límites expresivos del lenguaje modal-temporal básico sobre marcos ordenados. Su principal significancia radica en identificar que la incapacidad de definir propiedades funcionales fundamentales en el entorno original de multiflujo es un artefacto estructural de la multiplicidad funcional incontrolada, no un fallo inherente de los operadores temporales.

Al mostrar que los marcos mínimos, los lenguajes indexados y los marcos U-Dom producen patrones de definibilidad idénticos, el trabajo clarifica las condiciones precisas bajo las cuales las propiedades funcionales se vuelven definibles. Establece que, si bien la simplificación estructural puede recuperar la definibilidad de la monotonicidad y la antitonicidad en todos los órdenes, la falta de conectividad lineal sigue siendo una barrera persistente para las propiedades que requieren comparaciones globales de dominio (como la totalidad y la inyectividad) en estructuras no lineales. El estudio también destaca el estatus especial de la constancia, la cual resiste las pruebas estándar de no definibilidad mediante p-morfismos en marcos mínimos, requiriendo un argumento de equivalencia semántica único.