Effective Stochastic Automata Model Checking by Interval Abstraction (extended version)

Declaración del Problema
Los Autómatas Estocásticos (SA, por sus siglas en inglés) son un formalismo para modelar sistemas dependientes y de alto rendimiento donde las fallas de los componentes, el mantenimiento y los tiempos de servicio siguen distribuciones de probabilidad continua general (por ejemplo, Weibull, uniforme) en lugar de las distribuciones exponenciales requeridas por las Cadenas de Markov de Tiempo Continuo (CTMC) o las Redes de Petri Estocásticas Generalizadas (GSPN). Aunque los SA ofrecen una representación más realista de los sistemas no markovianos, su análisis es un desafío debido a la combinación de tiempo continuo, distribuciones generales y elecciones no deterministas.

Los enfoques de análisis existentes enfrentan limitaciones significativas:

• Verificación de Modelos Estadística (SMC): Herramientas como Fig emplean simulación de Monte Carlo, pero están restringidas a SA (débilmente) deterministas, donde las probabilidades de alcanzabilidad mínima y máxima coinciden. No pueden manejar SA no deterministas generales.
• Métodos Analíticos: Los algoritmos previos para SA generales (por ejemplo, de Bryans et al.) dependen de "árboles de regiones" que requieren integrales anidadas que se vuelven inviables a medida que aumenta la profundidad del modelo, o utilizan discretización que carece de soporte para herramientas. Otros formalismos como los Autómatas Híbridos Estocásticos (SHA) o los Autómatas Temporizados Estocásticos (STA) existen, pero su verificación de modelos suele sufrir problemas de escalabilidad debido a la complejidad del alcance híbrido o la rigidez de la semántica de reloj digital (pasos de tiempo fijos).

Metodología
El artículo propone el primer enfoque de verificación de modelos dedicado, general y efectivo para SA basado en la abstracción por intervalos. La metodología central consiste en transformar un SA de estado infinito en un Proceso de Decisión de Markov (MDP) finito que sobreaproxima la semántica original.

1. Abstracción por Intervalos: En lugar de discretizar el resultado del muestreo de una distribución de probabilidad continua (CPD), el método particiona el soporte de cada distribución en un conjunto finito de intervalos.

   • El muestreo de un valor de una CPD se reemplaza por un proceso de dos pasos: (1) una elección probabilística discreta de un intervalo (basada en la masa de probabilidad de ese intervalo), seguido de (2) una elección no determinista continua de un valor específico dentro de ese intervalo.
   • Esto transforma el SA en un MDP donde los estados rastrean la ubicación actual y los intervalos que contienen los valores posibles de los temporizadores activos.

2. Semántica de Grandes Pasos de Tiempo: El enfoque utiliza la semántica de "grandes pasos de tiempo" de los SA. Las transiciones ocurren solo cuando un temporizador expira o se satisface un conjunto de guardas, en lugar de en cada paso de tiempo infinitesimal. Esto evita la complejidad del "tiempo denso" encontrada en otras semánticas.

   • La abstracción propaga los intervalos simbólicamente. Cuando un temporizador expira, el sistema transiciona a un nuevo estado donde el intervalo del temporizador se actualiza o se reinicia.
   • El MDP resultante es finito porque el número de ubicaciones es finito y el número de combinaciones de intervalos está fijado por la partición definida por el usuario.

3. Sobreaproximación y Límites:

   • La estrategia del MDP puede elegir el valor preciso dentro de un intervalo, mientras que la semántica original de los SA implica una elección aleatoria. Esto introduce no determinismo que sobreaproxima el sistema original.
   • En consecuencia, calcular la probabilidad máxima de alcanzabilidad en el MDP produce un límite superior para el SA, y la probabilidad mínima de alcanzabilidad produce un límite inferior.
   • El artículo demuestra que a medida que los intervalos se vuelven más pequeños, se espera que el error de aproximación disminuya, aunque la monotonicidad no está garantizada con todas las estrategias de partición.

4. Herramientas y Formalismos:

   • Los autores extendieron el lenguaje de modelado Modest y el formato de intercambio Jani para soportar SA, incluyendo declaraciones de temporizadores y conjuntos de guardas.
   • Una herramienta prototipo implementada en Rust realiza la abstracción por intervalos, construye el MDP y calcula los límites utilizando Iteración de Valor (VI).

Contribuciones Clave

• Primer Verificador de Modelos Dedicado para SA: El artículo presenta la primera herramienta para la verificación de modelos de SA generales que no está limitada a subclases deterministas.
• Abstracción por Intervalos para SA: Adapta la abstracción por intervalos (utilizada previamente para SHA) específicamente para SA, reemplazando las elecciones probabilísticas continuas por elecciones probabilísticas discretas seguidas de elecciones no deterministas continuas, lo que resulta en un MDP finito.
• Corrección Formal: Los autores proporcionan una prueba formal (Teorema 1) que establece que las probabilidades de alcanzabilidad del MDP acotan las probabilidades reales del SA ($p_{min}^{MDP} \le p_{min}^{SA} \le p_{max}^{SA} \le p_{max}^{MDP}$).
• Extensiones de Lenguaje: La extensión de Modest y Jani para soportar SA proporciona una interfaz de modelado de alto nivel amigable para el usuario y un estándar para el intercambio de modelos.
• Implementación de Prototipo: Un prototipo basado en Rust demuestra la viabilidad del enfoque.

Resultados Experimentales
Los autores evaluaron el prototipo en tres conjuntos de ejemplos:

1. Modelos SA Pequeños: Incluyendo el ejemplo de ejecución y modelos de la literatura que distinguen clases de estrategia. La herramienta calculó con éxito los límites que aproximan estrechamente las probabilidades reales (por ejemplo, aproximando 0.25 y 0.75 con límites de [0.245, 0.755] usando 0.0125 de probabilidad por intervalo).
2. Modelos de Colas: Colas M/M/1 y Weibull/E6/1 no markovianas con límites de búfer. A pesar de generar MDPs con millones de estados (por ejemplo, ~3.3 millones de estados), la herramienta completó el análisis en menos de 3 minutos en una computadora portátil estándar.
3. Modelo de Servidor de Archivos: Una comparación con la herramienta mcsta (que utiliza relojes digitales para STA).
   • Para distribuciones uniformes, el enfoque de SA logró una mayor precisión en menos del 30% del tiempo de ejecución de mcsta, debido principalmente a que la semántica de "grandes pasos de tiempo" resultó en MDPs significativamente más pequeños que el enfoque de reloj digital (que fuerza pasos de tiempo de duración 1).
   • Para distribuciones exponenciales, los intervalos de ancho fijo de mcsta funcionaron mejor que los intervalos de probabilidad igual utilizados en el prototipo, resaltando que las estrategias de generación de intervalos impactan el rendimiento. Los autores señalan que el refinamiento de intervalos por temporizador es posible en su enfoque, a diferencia de la restricción de ancho fijo de los relojes digitales.

Significancia y Reivindicaciones
El artículo afirma introducir un enfoque de verificación de modelos general y efectivo para SA que impone pocas restricciones a los modelos de entrada.

• Escalabilidad: Los resultados experimentales sugieren que el enfoque escala bien para ejemplos no triviales, manejando modelos con cientos de miles a millones de estados de MDP, algo que las técnicas analíticas previas no podían gestionar.
• Practicidad: A pesar de ser un prototipo, la herramienta funciona bien para SA de tamaño razonable y proporciona límites útiles para el análisis de seguridad y rendimiento.
• Flexibilidad: El enfoque soporta varias distribuciones continuas (Uniforme, Exponencial, Erlang, Weibull) y características complejas como carreras de temporizadores (timer races) y elecciones no deterministas.

Los autores mantienen la modestia respecto al proceso de refinamiento, señalando que, si bien intervalos más pequeños generalmente mejoran la precisión, la relación no es estrictamente monotónica con su estrategia de partición actual, y una prueba de convergencia formal sigue siendo un desafío abierto. Posicionan este trabajo como una base para futuras herramientas optimizadas para el rendimiento y extensiones a árboles de fallas dinámicos y propiedades de tiempo limitado.