Computing Distinguishing Formulae for Threshold-Based Behavioural Distances

1. Problema y Contexto

En sistemas que manejan información cuantitativa (probabilística, ponderada, difusa, etc.), las equivalencias comportamentales de dos valores (verdadero/falso) a menudo son demasiado rígidas para capturar matices en el comportamiento. Las distancias comportamentales ofrecen una medida más fina y estable para comparar procesos.

El problema central abordado en este trabajo es la caracterización lógica y el cálculo eficiente de estas distancias. Específicamente:

• ¿Cómo se pueden caracterizar las distancias comportamentales basadas en umbrales (donde se permite una desviación $\varepsilon$) mediante lógica modal?
• ¿Es posible extraer fórmulas distinguitorias (fórmulas que demuestran que dos estados tienen una distancia mayor a un $\varepsilon$ dado) de manera eficiente (tiempo polinómico)?
• Existe una brecha en la literatura: aunque se conocen resultados para distancias específicas (como la distancia de Lévy-Prokhorov en cadenas de Markov), faltan marcos unificados y algoritmos generales para la extracción de fórmulas con garantías de complejidad polinómica en diversos tipos de sistemas.

2. Metodología y Marco Teórico

Los autores desarrollan un marco unificado basado en la teoría de coalgebras (universal coalgebra).

A. Fundamentos Coalgebraicos

• Los sistemas se modelan como coalgebras $(X, \xi)$ para un funtor $F$.
• Se introducen levantamientos de predicados (predicate liftings) de tipo 2 a V (donde $V = [0, 1]$ es el intervalo unitario). Estos transforman predicados binarios ($2^X$) en predicados cuantitativos ($V^{FX}$). Un ejemplo clásico es el operador de probabilidad que mapea un conjunto a su probabilidad.
• Se definen $\varepsilon$-simulaciones y $\varepsilon$-bisimulaciones: relaciones donde las probabilidades (o valores) de los estados sucesores pueden desviarse en un máximo de $\varepsilon$. La distancia comportamental $d_\Lambda(x, y)$ se define como el ínfimo de todos los $\varepsilon$ para los cuales $x$ y $y$ son $\varepsilon$-similares.

B. Juegos de Codensidad (Codensity Games)

Para abordar el problema algorítmico, los autores definen un juego Spoiler-Duplicador (codensity game) hasta un umbral $\varepsilon$:

• Spoiler (S) intenta demostrar que dos estados no son $\varepsilon$-similares eligiendo predicados que violan la condición de similitud.
• Duplicador (D) intenta mantener la similitud eligiendo pares de estados relacionados.
• Se demuestra que Duplicador gana la posición $(x, y)$ si y solo si $d_\Lambda(x, y) \leq \varepsilon$.
• La región ganadora de Spoiler se calcula como un punto fijo mínimo mediante iteración de Kleene, lo que permite la extracción de estrategias ganadoras en tiempo polinómico bajo ciertas condiciones de solvencia de los levantamientos de predicados.

C. Lógicas Modal

Se desarrollan dos lógicas para caracterizar la distancia:

1. Lógica Binaria (Two-Valued) con satisfacción hasta $\varepsilon$:
   • Utiliza los levantamientos originales 2 a V.
   • Introduce una noción de satisfacción relajada ($x \models_\varepsilon \phi$), donde los umbrales de los operadores modales se reducen en $\varepsilon$.
   • Caracteriza la distancia comportamental en sistemas de ramificación finita.
2. Lógica Cuantitativa (Sugeno):
   • Construye levantamientos de predicados V a V a partir de los levantamientos 2 a V originales mediante integración de Sugeno.
   • Estos nuevos operadores se denominan modalidades Sugeno.
   • La lógica resultante es no expansiva (non-expansive) y caracteriza la misma distancia comportamental, donde la distancia lógica coincide con la distancia comportamental.

3. Contribuciones Clave

1. Unificación de Distancias Basadas en Umbrales:

   • Se demuestra que la distancia comportamental inducida por $\varepsilon$-simulaciones coincide con la inducida por una extensión laxa cuantitativa específica (Lax extension) derivada de las modalidades dadas.
   • Esto generaliza resultados conocidos, como la caracterización de la distancia $\varepsilon$ en cadenas de Markov como la distancia comportamental inducida por la métrica de Lévy-Prokhorov.

2. Construcción de Modalidades Sugeno:

   • Se introduce una técnica para convertir levantamientos 2 a V en levantamientos V a V usando integración de Sugeno.
   • Se prueba que la extensión laxa inducida por estas modalidades Sugeno coincide con la extensión basada en umbrales original.
   • Esto conecta la distancia de Lévy-Prokhorov con la modalidad "generally" (generalmente) utilizada en representación de conocimiento probabilístico.

3. Algoritmos de Extracción de Fórmulas Distinguitorias:

   • Se presentan algoritmos (basados en estrategias de Spoiler en el juego de codensidad) para extraer fórmulas distinguitorias tanto para la lógica binaria como para la cuantitativa.
   • Resultado de Complejidad: Bajo suposiciones de solvencia polinómica de los levantamientos de predicados, las fórmulas distinguitorias se pueden calcular en tiempo polinómico.
   • Las fórmulas tienen un tamaño de DAG (grafo acíclico dirigido) polinómico (específicamente cuártico), evitando la explosión exponencial típica del tamaño de árbol en lógicas modales estándar.

4. Resultados Principales

• Teorema de Correspondencia (Lógica vs. Comportamiento): Para sistemas de ramificación finita, la distancia comportamental basada en umbrales coincide exactamente con la distancia lógica inducida tanto por la lógica binaria (con satisfacción hasta $\varepsilon$) como por la lógica cuantitativa Sugeno.
• Caracterización de Lévy-Prokhorov: Se confirma que la distancia $\varepsilon$ en cadenas de Markov es inducida por la métrica de Lévy-Prokhorov y puede ser caracterizada por la modalidad "generally".
• Nuevos Resultados Específicos:
  • Se obtienen por primera vez resultados de extracción polinómica de fórmulas distinguitorias para:
    • Distancia de Lévy-Prokhorov en cadenas de Markov (tanto lógica binaria como cuantitativa).
    • Sistemas de transición probabilísticos generativos.
    • Sistemas de transición difusos (fuzzy).
    • Sistemas de transición métricos.
• Solvabilidad Polinómica: Se demuestra que para los casos mencionados (Markov, difusos, métricos), la verificación de si dos estados tienen distancia $\leq \varepsilon$ y la extracción de la fórmula distinguitoria son problemas resolubles en tiempo polinómico.

5. Significado e Impacto

• Avance Teórico: El trabajo proporciona un marco general que unifica diversas nociones de distancia comportamental bajo la teoría de coalgebras, mostrando que muchas distancias "ad hoc" son instancias de un mismo principio basado en umbrales y levantamientos de predicados.
• Avance Algorítmico: La capacidad de calcular fórmulas distinguitorias en tiempo polinómico es crucial para la verificación formal y el diagnóstico de sistemas. Permite no solo decir "estos sistemas son diferentes", sino explicar por qué (mediante la fórmula) de manera eficiente.
• Aplicabilidad: Los resultados tienen implicaciones directas en áreas donde la robustez estadística y la privacidad son importantes, como en el aprendizaje automático (conformal prediction), seguridad móvil y privacidad diferencial, donde la distancia de Lévy-Prokhorov es fundamental.
• Novedad: Mientras que resultados anteriores (como los de Desharnais et al.) establecían la existencia de lógicas características, este trabajo aporta la eficiencia computacional (tamaño de fórmula y tiempo de cálculo) que antes no estaba garantizada o era desconocida para la mayoría de los casos.

En resumen, el artículo establece un puente sólido entre la teoría de coalgebras, la lógica modal cuantitativa y la complejidad computacional, ofreciendo herramientas prácticas para analizar y comparar sistemas cuantitativos complejos con garantías de eficiencia.