Verification of Parametric Markov Automata under Time-bounded Reachability

Resumo Técnico: Verificação de Autômatos de Markov Paramétricos sob Alcance com Limite de Tempo

Definição do Problema
Autômatos de Markov (MA) são um modelo composicional para sistemas estocásticos não determinísticos e continuamente temporizados, servindo como semântica para modelos como Redes de Petri Estocásticas Generalizadas e Árvores de Falhas Dinâmicas. No entanto, os algoritmos de model checking existentes para MA exigem modelos totalmente especificados, onde todas as taxas de transição e probabilidades são conhecidas precisamente. Essa suposição é frequentemente irrealista para sistemas do mundo real, onde os parâmetros podem estar sujeitos a incerteza ambiental ou desconhecimento.

Este artigo aborda a verificação de Autômatos de Markov Paramétricos (pMA), onde as taxas de transição e as distribuições de sucessores probabilísticos são definidas por funções paramétricas em vez de constantes fixas. Os autores focam em propriedades de alcance com limite de tempo (ex: "A probabilidade de alcançar um estado de meta dentro do tempo $t$ é maior que $\theta$?"). Dois problemas específicos são abordados:

1. Verificação de Satisfação: Determinar se existe uma valoração de parâmetro dentro de uma determinada região que satisfaz ou viola uma propriedade.
2. Síntese: Particionar o espaço de parâmetros em regiões que satisfazem a propriedade e regiões que a violam.

A análise deve considerar quatro relações de satisfação distintas baseadas na interação entre o escalonador do sistema (fazendo escolhas não determinísticas) e a "natureza" (atribuindo valores aos parâmetros): Viabilidade, Auxílio Angélico, Robusta e Demoníaca.

Metodologia
A abordagem proposta resolve esses problemas através de um processo de duas etapas que transforma o modelo paramétrico contínuo em um modelo discreto passível de técnicas de síntese existentes, enquanto limita os erros introduzidos.

1. Discretização e Transformação:

   • O pMA é primeiro discretizado usando um passo $\delta$, convertendo o modelo de tempo contínuo em um Processo de Decisão de Markov Paramétrico (pMDP). Este passo generaliza resultados de discretização anteriores para MAs não paramétricos.
   • Para lidar com as transições imediatas de estados probabilísticos (que ocorrem sem passagem de tempo), os autores empregam uma técnica de eliminação de estados. Estados probabilísticos (PS) são colapsados em estados markovianos (MS), transformando o modelo em um problema padrão de alcance com limite de passos em um pMDP.
   • Como a discretização introduz termos exponenciais ($e^{-\lambda \delta}$) que são difíceis de manipular em síntese de parâmetros simbólica, os autores aproximam esses termos usando expansões de Taylor parciais. Isso resulta em um "pMA discretizado aproximado" onde as probabilidades de transição são representadas por funções racionais, limitadas por aproximações superiores e inferiores.

2. Elevação de Parâmetros (PL) e Verificação:

   • O pMDP transformado é analisado usando Elevação de Parâmetros (PL). Esta técnica abstrai dependências entre estados tratando as escolhas de parâmetros como escolhas não determinísticas feitas por um segundo jogador ("Natureza") em um jogo estocástico.
   • O método PL computa limites superiores e inferiores para a probabilidade de alcance. Esses limites são comparados contra o limiar especificado pelo usuário $\theta$.
   • A abordagem utiliza um esquema de refinamento: se os limites forem inconclusivos (ou seja, se o intervalo cruzar o limiar), a região de parâmetros é particionada e o processo é repetido.
   • O erro total é governado por três termos: o erro de discretização ($\epsilon_\delta$), o erro da aproximação de Taylor e o erro introduzido pela abstração de PL. Os autores demonstram que o erro de discretização é o fator dominante.

Principais Contribuições

• Definição de pMA: O artigo introduz formalmente os Autômatos de Markov Paramétricos, estendendo os MAs com funções de taxa e probabilidade paramétricas.
• Algoritmo para Alcance com Limite de Tempo: Os autores apresentam o primeiro algoritmo capaz de realizar verificação de satisfação e síntese de parâmetros para pMAs sob restrições de alcance com limite de tempo.
• Discretização Generalizada: Eles generalizam os resultados de discretização de Guck et al. [17] para o cenário paramétrico, provando que o pMA discretizado limita a probabilidade de alcance real do pMA.
• Discretização Aproximada: Um método é introduzido para lidar com termos exponenciais no modelo discretizado via expansão de Taylor, permitindo o uso de ferramentas de síntese baseadas em funções racionais.
• Implementação: A abordagem é implementada usando o model checker Storm (via interface Stormpy) e suporta tanto pMAs quanto CTMCs paramétricos.

Resultados Experimentais
Os autores avaliaram sua implementação em um conjunto de benchmarks do conjunto QCOMP, incluindo modelos como flexible-manufacturing, polling e kankan.

• Verificação: Para a verificação de satisfação, a ferramenta forneceu respostas conclusivas para todos os benchmarks testados, frequentemente em poucos segundos.
• Síntese: Para a síntese de parâmetros, a ferramenta conseguiu particionar espaços de parâmetros para modelos menores. No entanto, para modelos maiores ou mais complexos, o processo frequentemente atingiu o tempo limite de 15 minutos.
• Gargalos de Desempenho: A análise experimental identifica a discretização como o principal gargalo de desempenho. O custo computacional aumenta significamente conforme o passo de discretização $\delta$ diminui (para reduzir o erro) ou conforme a taxa de permanência máxima no modelo aumenta.
• Comparação: Quando comparada ao PRISM-PSY em CTMCs paramétricos (onde o PRISM-PSY não requer discretização), o método proposto foi mais lento. No entanto, o método tem sucesso onde o PRISM-PSY falha: ele pode analisar pMAs e modelos com probabilidades de transição paramétricas (não apenas taxas), como o benchmark tandem.

Significância e Alegações
O artigo afirma preencher uma lacuna na verificação formal ao permitir a análise de incerteza em Autômatos de Markov, uma classe de modelos amplamente utilizada na engenharia de confiabilidade, mas anteriormente restrita a instâncias totalmente especificadas. Os autores enfatizam que sua abordagem resolve os problemas de verificação e síntese até uma precisão arbitrária, desde que o passo de discretização seja suficientemente pequeno.

Os autores mantêm-se modestos quanto à escalabilidade, reconhecendo que a implementação atual é limitada pelo custo da discretização. Eles declaram explicitamente que os principais gargalos de desempenho originam-se da discretização do pMA. Consequentemente, sugerem que trabalhos futuros investiguem abordagens que evitem a discretização inteiramente, como analisar jogos estocásticos de tempo contínuo diretamente ou utilizar técnicas de uniformização, embora notem que essas alternativas podem introduzir seus próprios desafios computacionais. O trabalho estabelece um framework fundamental para a análise paramétrica de sistemas não determinísticos de tempo contínuo, estendendo as capacidades de ferramentas existentes como o Storm para lidar com incerteza paramétrica em uma classe mais ampla de modelos.