A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

1. Planteamiento del Problema

El artículo aborda el desafío de comparar cuantitativamente los comportamientos de procesos no deterministas.

• Contexto: El álgebra de procesos tradicional y la teoría de autómatas se basan en nociones booleanas de equivalencia (por ejemplo, bisimilitud, equivalencia de lenguajes). Aunque útiles, estas suelen ser demasiado rígidas para sistemas modernos que involucran aspectos probabilísticos o cuantitativos, donde es necesario medir qué tan separados están dos comportamientos en lugar de simplemente si son idénticos.
• Brecha Específica: Si bien las distancias de comportamiento han sido estudiadas para sistemas probabilísticos y autómatas deterministas (DFA), existe una falta de un marco axiomático sólido y completo para procesos no deterministas (específicamente los diagramas de Milner).
• Desafío: El no determinismo desplaza el foco semántico de la equivalencia de lenguajes a la bisimilitud. Las sintaxis algebraicas existentes (como expresiones regulares con ligadores) luchan por capturar estos comportamientos de manera composicional sin mecanismos de sustitución complejos. Además, extender el razonamiento cuantitativo a sistemas no deterministas requiere manejar el "levantamiento de Hausdorff" de métricas, lo cual es técnicamente difícil de axiomatizar.

2. Metodología

Los autores adoptan un enfoque diagramático utilizando diagramas de cuerda (el lenguaje gráfico de las categorías monoidales simétricas) para representar y razonar sobre los comportamientos de los procesos.

• Modelo Semántico (Diagramas): El artículo se centra en los diagramas de Milner, que generalizan los autómatas no deterministas de estado finito (NFA) reemplazando los estados de aceptación con salidas variables. La semántica se define sobre una categoría de comportamientos regulares ($\Omega$), equipada con una estructura de pseudométrica.
• Definición de Métrica: La distancia de comportamiento se define mediante un marco coalgebraico. Utiliza:
  1. Levantamiento de Transiciones: Elevar una métrica sobre estados a una métrica sobre transiciones (bordes etiquetados y salidas variables).
  2. Levantamiento de Hausdorff: Elevar la métrica a conjuntos de transiciones (para manejar el no determinismo).
  3. Caracterización de Punto Fijo: La distancia es el menor punto fijo de un operador monótono en el retículo de pseudométricas. Se caracteriza concretamente por la estratificación de la bisimilitud (lógica de Hennessy-Milner), donde la distancia es $2^{-n}$ si dos procesos son bisimilares hasta la profundidad $n$ pero no $n+1$.
• Sintaxis (Diagramas de Cuerda): Los autores utilizan diagramas de cuerda como sintaxis. Esta elección ofrece:
  • Representación sin variables: La recursión se maneja mediante bucles de retroalimentación (trazas) en lugar de ligadores explícitos y sustitución.
  • Semántica Composicional: Los diagramas se mapean naturalmente a la estructura categórica de los comportamientos regulares.
  • Construcción Int: Para manejar el flujo de datos bidireccional (entradas/salidas) y bucles de retroalimentación, los autores utilizan la construcción Int para transformar la categoría monoidal trazada de comportamientos en una categoría compactamente cerrada, permitiendo el doblado local de cables.

3. Contribuciones Clave

A. Un Sistema de Inferencia Cuantitativo

El artículo propone un conjunto de reglas ecuacionales cuantitativas (sistema de inferencia) para derivar cotas sobre las distancias de comportamiento ($s \equiv_\epsilon t$).

• Reglas Métricas Estándar: Reflexividad, Simetría, Desigualdad Triangular y una regla de "Continuidad" (si $s \equiv_{\epsilon'} t$ para todo $\epsilon' > \epsilon$, entonces $s \equiv_\epsilon t$).
• Reglas Composicionales: Reglas para la composición secuencial y la composición paralela (tensor) que preservan la no expansión.
• Reglas Específicas del Dominio:
  • (Pref): El prefijado con una acción $a$ reduce la distancia a la mitad ($d(a.s, a.t) = \frac{1}{2}d(s, t)$). Esto captura la intuición de que distinguir dos procesos requiere un paso más.
  • (Codel): Un diagrama sin estado inicial (bloqueo) está a distancia 0 del diagrama vacío.
  • Axiomas Ecuacionales: Un conjunto de axiomas (A1-B11) que capturan la bisimilitud fuerte (distancia 0), incluyendo leyes para la elección no determinista, la fusión de variables y la recursión (axiomas de la teoría de Conway).

B. Solidez y Completitud

El logro técnico central es la prueba de que el sistema de inferencia es tanto sólido como completo.

• Solidez (Teorema 16): Cada ecuación cuantitativa derivable $f \equiv_\epsilon g$ es válida (es decir, la distancia de comportamiento real $d(\llbracket f \rrbracket, \llbracket g \rrbracket) \leq \epsilon$).
• Completitud (Teorema 31): Si la distancia de comportamiento entre dos diagramas es $\leq \epsilon$, entonces la ecuación $f \equiv_\epsilon g$ es derivable utilizando las reglas propuestas.
  • Estrategia de Prueba: La prueba de completitud implica transformar diagramas arbitrarios en una forma normal (que representa un pre-diagrama finito). Luego simula el cálculo del levantamiento de Hausdorff y la iteración de punto fijo (teorema de Kleene) sintácticamente utilizando las reglas de inferencia. La regla de Continuidad (Cont) es crucial para cerrar la brecha entre la aproximación sintáctica y el límite exacto.

C. Estructura Categórica

El artículo establece que la categoría de comportamientos regulares ($\text{RegBeh}$) es una Teoría de Conway (un tipo específico de categoría monoidal trazada) y que la estructura de pseudométrica la convierte en una categoría enriquecida sobre la categoría de espacios de pseudométricas ($\text{PMet}$). Esto asegura que todas las operaciones categóricas (composición, tensor, traza/daga) sean no expansivas.

4. Resultados

• Caracterización Formal: El artículo proporciona la primera axiomatización completa de la distancia de comportamiento para los diagramas de Milner (procesos no deterministas con salidas).
• Simulación Sintáctica de Métricas: Los autores demuestran que cálculos métricos complejos, como la distancia de Hausdorff entre conjuntos de transiciones, pueden simularse puramente mediante la manipulación sintáctica de diagramas de cuerda.
• Ejemplo de Aplicación: El artículo incluye una derivación detallada que muestra cómo probar que dos diagramas específicos (uno con un bloqueo después de dos 'a's, y el otro con infinitos 'a's) están a una distancia exactamente de $1/4$. Esto se logra desenrollando la recursión y aplicando la regla (Pref) dos veces.

5. Significado

• Puente entre Teoría y Práctica: Al pasar de la equivalencia booleana a la distancia cuantitativa, el trabajo permite un análisis más matizado de sistemas donde "casi equivalente" es un concepto significativo (por ejemplo, en la verificación de sistemas aproximados o sistemas probabilísticos).
• Marco Diagramático Unificado: El uso de diagramas de cuerda evita la complejidad del ligamiento de variables y la sustitución encontrada en las álgebras de procesos tradicionales. Esto sugiere un camino hacia un marco unificado para axiomatizar equivalencias y distancias en diversos modelos computacionales (deterministas, no deterministas, probabilistas, ponderados).
• Fundamento para Trabajo Futuro: El artículo sienta las bases para extender estos resultados a sistemas de transición ponderados y autómatas probabilistas, donde las distancias de comportamiento son aún más críticas. También sugiere aplicaciones potenciales en el razonamiento sobre algoritmos de descompilación y el Álgebra de Kleene Guardada con Pruebas (GKAT).
• Avance Teórico: Conecta las métricas de comportamiento coalgebraicas, la lógica ecuacional cuantitativa y el álgebra diagramática, mostrando cómo estos campos pueden integrarse para resolver problemas de larga data en la teoría de procesos.

En resumen, este artículo traduce con éxito la definición abstracta y coalgebraica de la distancia de comportamiento para procesos no deterministas en un cálculo concreto, diagramático y completamente axiomatizado, demostrando que el razonamiento cuantitativo sobre el comportamiento de los procesos puede realizarse enteramente mediante la manipulación sintáctica de diagramas de cuerda.