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

Enunciado do Problema
Autômatos Estocásticos (SA) são um formalismo para modelar sistemas dependentes e de alto desempenho onde falhas de componentes, manutenção e tempos de serviço seguem distribuições de probabilidade contínua geral (ex: Weibull, uniforme) em vez das distribuições exponenciais exigidas por Cadeias de Markov de Tempo Contínuo (CTMCs) ou Redes de Petri Estocásticas Generalizadas (GSPNs). Embora os SA ofereçam uma representação mais realista de sistemas não-markovianos, sua análise é desafiadora devido à combinação de tempo contínuo, distribuições gerais e escolhas não-determinísticas.

As abordagens de análise existentes enfrentam limitações significativas:

• Verificação de Modelo Estatística (SMC): Ferramentas como o Fig empregam simulação de Monte Carlo, mas são restritas a SA (fracamente) determinísticos, onde as probabilidades de alcançabilidade mínima e máxima coincidem. Elas não conseguem lidar com SA não-determinísticos gerais.
• Métodos Analíticos: Algoritmos anteriores para SA geral (ex: por Bryans et al.) dependem de "árvores de regiões" que exigem integrais aninhadas que se tornam inviáveis conforme a profundidade do modelo aumenta, ou utilizam discretização que carece de suporte de ferramentas. Outros formalismos como Autômatos Híbridos Estocásticos (SHA) ou Autômatos Temporais Estocásticos (STA) existem, mas sua verificação de modelo sofre com problemas de escalabilidade devido à complexidade da alcançabilidade híbrida ou à rigidez da semântica de relógio digital (passos de tempo fixos).

Metodologia
O artigo propõe a primeira abordagem de verificação de modelo dedicada, geral e eficaz para SA baseada em abstração de intervalo. A metodologia central envolve a transformação de um SA de estado infinito em um Processo de Decisão de Markov (MDP) finito que sobre-aproxima a semântica original.

1. Abstração de Intervalo: Em vez de discretizar o resultado da amostragem de uma Distribuição de Probabilidade Contínua (CPD), o método particiona o suporte de cada distribuição em um conjunto finito de intervalos.

   • A amostragem de um valor de uma CPD é substituída por um processo de duas etapas: (1) uma escolha probabilística discreta de um intervalo (baseada na massa de probabilidade desse intervalo), seguida por (2) uma escolha não-determinística contínua de um valor específico dentro desse intervalo.
   • Isso transforma o SA em um MDP onde os estados rastreiam a localização atual e os intervalos contendo os valores possíveis dos temporizadores ativos.

2. Semântica de Grandes Passos de Tempo (Big Time Steps): A abordagem utiliza a semântica de "grandes passos de tempo" dos SA. As transições ocorrem apenas quando um temporizador expira ou um conjunto de guarda é satisfeito, em vez de ocorrer em cada passo de tempo infinitesimal. Isso evita a complexidade de "tempo denso" encontrada em outras semânticas.

   • A abstração propaga intervalos simbolicamente. Quando um temporizador expira, o sistema transiciona para um novo estado onde o intervalo do temporizador é atualizado ou reiniciado.
   • O MDP resultante é finito porque o número de localizações é finito e o número de combinações de intervalos é fixado pela partição definida pelo usuário.

3. Sobre-aproximação e Limites (Bounds):

   • A estratégia do MDP pode escolher o valor preciso dentro de um intervalo, enquanto a semântica original do SA envolve uma escolha aleatória. Isso introduz não-determinismo que sobre-aproxima o sistema original.
   • Consequentemente, computar a probabilidade máxima de alcançabilidade no MDP fornece um limite superior para o SA, e a probabilidade mínima de alcançabilidade fornece um limite inferior.
   • O artigo prova que, à medida que os intervalos se tornam menores, espera-se que o erro de aproximação diminua, embora a monotonicidade não seja garantida com todas as estratégias de particionamento.

4. Ferramental e Formalismos:

   • Os autores estenderam a linguagem de modelagem Modest e o formato de intercâmbio Jani para suportar SA, incluindo declarações de temporizadores e conjuntos de guarda.
   • Um protótipo implementado em Rust realiza a abstração de intervalo, constrói o MDP e calcula os limites usando Iteração de Valor (VI).

Principais Contribuições

• Primeiro Verificador de Modelo Dedicado para SA: O artigo apresenta a primeira abordagem baseada em ferramenta para verificação de modelo de SA geral que não é limitada a subclasses determinísticas.
• Abstração de Intervalo para SA: Adapta a abstração de intervalo (previamente usada para SHA) especificamente para SA, substituindo escolhas probabilísticas contínuas por escolhas probabilísticas discretas seguidas de escolhas não-determinísticas contínuas, resultando em um MDP finito.
• Corretude Formal: Os autores fornecem uma prova formal (Teorema 1) estabelecendo que as probabilidades de alcançabilidade do MDP limitam as probabilidades reais do SA ($p_{min}^{MDP} \le p_{min}^{SA} \le p_{max}^{SA} \le p_{max}^{MDP}$).
• Extensões de Linguagem: A extensão do Modest e do Jani para suportar SA fornece uma interface de modelagem de alto nível amigável ao usuário e um padrão para intercâmbio de modelos.
• Implementação de Protótipo: Um protótipo em Rust demonstra a viabilidade da abordagem.

Resultados Experimentais
Os autores avaliaram o protótipo em três conjuntos de exemplos:

1. Modelos SA Pequenos: Incluindo o exemplo de execução e modelos da literatura que distinguem classes de estratégia. A ferramenta computou com sucesso os limites que aproximam de perto as probabilidades reais (ex: aproximando 0,25 e 0,75 com limites de [0,245, 0,755] usando 0,0125 de probabilidade por intervalo).
2. Modelos de Filas: Filas M/M/1 e Weibull/E6/1 não-markovianas com limites de buffer. Apesar de gerar MDPs com milhões de estados (ex: ~3,3 milhões de estados), a ferramenta completou a análise em menos de 3 minutos em um laptop padrão.
3. Modelo de Servidor de Arquivos: Uma comparação com a ferramenta mcsta (que usa relógios digitais para STA).
   • Para distribuições uniformes, a abordagem de SA alcançou maior precisão em menos de 30% do tempo de execução em comparação com o mcsta, principalmente porque a semântica de "grandes passos de tempo" resultou em MDPs significativamente menores do que a abordagem de relógio digital (que força passos de tempo de duração 1).
   • Para distribuições exponenciais, os intervalos de largura fixa do mcsta tiveram melhor desempenho do que os intervalos de igual probabilidade do protótipo, destacando como as estratégias de geração de intervalos impactam o desempenho. Os autores observam que o refinamento de intervalos por temporizador é possível em sua abordagem, ao contrário da restrição de largura fixa dos relógios digitais.

Significância e Alegações
O artigo afirma introduzir uma abordagem de verificação de modelo geral e eficaz para SA que impõe poucas restrições aos modelos de entrada.

• Escalabilidade: Os resultados experimentais sugerem que a abordagem escala bem para exemplos não triviais, lidando com modelos de centenas de milhares a milhões de estados de MDP, algo que técnicas analíticas anteriores não conseguiam gerenciar.
• Praticidade: Apesar de ser um protótipo, a ferramenta funciona bem para SA de tamanho razoável e fornece limites úteis para análise de segurança e desempenho.
• Flexibilidade: A abordagem suporta várias distribuições contínuas (Uniforme, Exponencial, Erlang, Weibull) e recursos complexos como corridas de temporizadores (timer races) e escolhas não-determinísticas.

Os autores permanecem modestos quanto ao processo de refinamento, observando que, embora intervalos menores geralmente melhorem a precisão, a relação não é estritamente monotônica com sua estratégia de particionamento atual, e uma prova de convergência formal permanece como um desafio em aberto. Eles posicionam este trabalho como uma fundação para futuras ferramentas otimizadas de desempenho e extensões para árvores de falhas dinâmicas e propriedades de tempo limitado.