Resumen Técnico: Una Guía Pragmática para la Construcción de Abstracciones Discretas Conservadoras de Sistemas Ciberfísicos

Planteamiento del Problema

Los sistemas ciberfísicos (CPS) operan en entornos críticos para la seguridad donde los fallos pueden amenazar la vida y la propiedad. Si bien la verificación de modelos simbólicos es un método eficaz para verificar propiedades complejas de lógica temporal, requiere un modelo de estados finitos. Sin embargo, los CPS del mundo real evolucionan sobre espacios de estados continuos. Para aplicar la verificación de modelos, los ingenieros deben discretizar estas dinámicas continuas en una abstracción de estados finitos.

El desafío central radica en asegurar la solidez (soundness): las garantías de verificación derivadas del modelo abstracto deben transferirse al sistema concreto. Esto requiere que la abstracción sea una sobre-aproximación conservadora del espacio de estados y los comportamientos concretos. En la práctica, los constructores de modelos encuentran frecuentemente cuatro errores que comprometen la solidez o introducen un exceso de pesimismo:

1. Sub-cobertura del espacio de estados concreto.
2. Sub-aproximación de la relación de transición (omisión de comportamientos factibles).
3. Poda no sólida (unsound pruning) de comportamientos "degenerados" (por ejemplo, eliminar bucles de auto-transición sin certificación).
4. Elevación de especificación inadecuada (improper specification lifting), fallando en preservar la implicación lógica desde la satisfacción abstracta hacia la satisfacción concreta.

Estos problemas suelen conducir a contraejemplos "espurios" donde el modelo abstracto viola una especificación que el sistema concreto sí satisface, lo que hace que la verificación sea inútil.

Metodología

El artículo propone un flujo de trabajo modular de cuatro pasos para la construcción de abstracciones discretas conservadoras. El flujo de trabajo es "conservador por construcción", lo que significa que la solidez se mantiene en cada etapa mediante garantías matemáticas específicas.

Paso 1: Abstracción del Espacio de Estados

El espacio de estados continuo $X$ se particiona en un conjunto finito de estados abstractos $\hat{X}$ utilizando una rejilla rectilínea uniforme. Una función de cuantización $\psi: X \to \hat{X}$ mapea los estados concretos a celdas abstractas. El mapeo inverso $\Psi(\hat{x})$ define la región concreta (preimagen) de cada estado abstracto. Este paso asegura que cada estado concreto y condición inicial tenga un representante en el modelo abstracto.

Paso 2: Construcción de Transiciones Conservadoras

El artículo presenta tres métodos intercambiables para computar la relación de transición $\hat{f}$ (es decir, determinar qué estados abstractos pueden seguir a otros), asegurando que cada transición concreta esté representada en el modelo abstracto:

• Caja de Delimitación Alineada con los Ejes (AABB): Computa la caja delimitadora de la imagen de una celda concreta bajo la dinámica del sistema. Cualquier celda abstracta que intersequen esta caja se añade como sucesora. Es computacionalmente eficiente pero puede ser excesivamente conservador para sistemas no lineales.
• Propagación de Polítopos: Utiliza un polítopo (envolvente convexa) para sobre-aproximar la imagen de la celda concreta. Es más ajustado que AABB para dinámicas no lineales, pero computacionalmente más costoso. Emplea el filtrado por AABB para descartar candidatos antes de realizar pruebas de intersección de polítopos más costosas.
• Muestreo con Certificados PAC: Para sistemas de "caja negra" o altamente no lineales, las transiciones se descubren mediante el muestreo del espacio de estados. En lugar de una garantía determinista, este método proporciona una garantía de Probablemente Aproximadamente Correcta (PAC). Certifica que, con alta confianza ($1-\delta$), la relación de transición construida incluye todas las transiciones "significativas" (aquellas que ocurren con probabilidad $\ge \beta$), acotando la "masa faltante" de transiciones no observadas.

Paso 3: Mitigación de Comportamientos Degenerados

Las abstracciones conservadoras a menudo introducen transiciones espurias (transiciones imposibles en el sistema concreto) y bucles de auto-transición (self-loops) (transiciones de un estado a sí mismo). Estos pueden causar falsos negativos en la verificación, particularmente para propiedades de vivacidad (liveness).

• Transiciones Espurias: Se abordan mediante Refinamiento de Abstracción Guiado por Contraejemplos (CEGAR). Si se encuentra una trayectoria de contraejemplo en el modelo abstracto, el algoritmo la valida contra la dinámica concreta. Si la trayectoria es espuria (el conjunto alcanzable se vuelve vacío), el espacio de estados se refina (se divide) para eliminar la falsa transición.
• Bucles de Auto-transición: Se abordan mediante la Eliminación Certificada de Bucles de Auto-transición. Un bucle de auto-transición se elimina solo si se puede certificar que cada trayectoria concreta que comienza en esa celda escapa dentro de un número finito de pasos ($K$). Esto se verifica ya sea mediante la iteración de la propagación del conjunto alcanzable o mediante una estrategia de muestreo con una garantía PAC.

Paso 4: Elevación Sólida de Especificaciones LTL

Para verificar el modelo abstracto, la especificación LTL $\phi$ definida en el espacio concreto debe elevarse a una especificación abstracta $\hat{\phi}$. El artículo emplea semántica de "puede" y "debe" (may-must semantics):

• Predicados "debe" (must): Una proposición atómica se cumple en un estado abstracto solo si se cumple para todos los estados concretos en esa celda.
• Predicados "puede" (may): Una proposición atómica se cumple si se cumple para al menos un estado concreto.
  El operador de elevación $\rho$ transforma $\phi$ en $\hat{\phi}$ fortaleciendo las proposiciones atómicas a "debe" (para seguridad) o debilitándolas a "puede" (según sea apropiado para la estructura de la lógica), asegurando que $\hat{s} \models \hat{\phi} \implies s \models \phi$.

Contribuciones Clave

1. Un Flujo de Trabajo Pragmático: Un flujo de trabajo unificado de cuatro pasos que integra la partición de estados, la construcción de transiciones, la mitigación de comportamientos degenerados y la elevación de especificaciones en un único marco sólido.
2. Subrutinas Intercambiables: La metodología soporta múltiples enfoques para la construcción de transiciones (AABB, Polítopo, Muestreo) y la eliminación de comportamientos degenerados (CEGAR, Eliminación Certificada), permitiendo a los usuarios equilibrar el costo computacional con la precisión de la abstracción.
3. Garantías PAC para el Muestreo: Introduce un enfoque basado en datos para la construcción de transiciones que proporciona certificados de cobertura probabilística rigurosos (mediante el estimador de Good-Turing y los límites de McAllester-Schapire) para sistemas donde la sobre-aproximación analítica es intratable.
4. Manejo Sistemático de la Degeneración: Aborda explícitamente la eliminación de bucles de auto-transición y transiciones espurias mediante la eliminación certificada y CEGAR, evitando el pesimismo que suele afectar a las abstracciones conservadoras.

Resultados Experimentales

Los autores evaluaron el flujo de trabajo en tres casos de estudio: un sistema lineal sintético, el benchmark Mountain Car (no lineal, política aprendida) y un Uniciclo Autónomo (modelo de Dubins).

• Construcción de Transiciones: Los métodos basados en muestreo generalmente produjeron relaciones de transición más dispersas con menos bucles de auto-transición y menor variabilidad en el número de sucesores en comparación con los métodos AABB y de Polítopos, particularmente para sistemas no lineales. Esto condujo a tasas de verdaderos positivos (TPR) más altas en la verificación.
• Eliminación de Bucles de Auto-transición: La eliminación de los bucles de auto-transición mejoró significativamente los resultados de la verificación. Para el caso del Uniciclo, la TPR aumentó de ~0.19 a ~0.63 tras la eliminación. En el caso de Mountain Car, la TPR mejoró de ~0.83 a ~0.93.
• CEGAR: Aunque el CEGAR aumentó sustancialmente el tamaño del modelo y el tiempo de construcción, redujo consistentemente la proporción de bucles de auto-transición (SLP). Produjo mejoras notables en la TPR para el sistema Mountain Car, pero tuvo un impacto mínimo en el Uniciclo, donde una alta SLP se atribuyó a contraejemplos triviales difíciles de eliminar sin una eliminación dirigida.
• Granularidad: Las granularidades de espacio de estados más finas produjeron consistentemente TPR más altas, confirmando la compensación entre el tamaño del modelo y la precisión de la verificación.

Significado

El artículo reclama su importancia como una guía pragmática para ingenieros e investigadores que construyen abstracciones para CPS. Aborda la brecha entre las técnicas de abstracción teóricas y la implementación práctica al:

• Proporcionar un flujo de trabajo sólido por construcción que evita errores comunes que conducen a una verificación no sólida.
• Ofrecer herramientas modulares que permiten a los profesionales elegir entre métodos deterministas (AABB/Polítopo) y probabilísticos (Muestreo) basados en la complejidad del sistema y los recursos computacionales disponibles.
• Demostrar que mitigar los comportamientos degenerados (transiciones espurias y bucles de auto-transición) no es meramente una optimización, sino un paso crítico para lograr resultados de verificación significativos, particularmente para propiedades de vivacidad.

Los autores concluyen que, si bien la verificación de modelos simbólicos es poderosa, su utilidad para los CPS depende enteramente de la calidad de la abstracción. Este flujo de trabajo proporciona un marco riguroso y adaptable para lograr esa calidad, equilibrando el pesimismo con la tractabilidad.