Resumo Técnico: Extensão do QuAK com Autômatos Quantitativos Aninhados

Declaração do Problema

Autômatos quantitativos (AQs) estendem autômatos $\omega$ de estados finitos com transições ponderadas para especificar propriedades quantitativas de sistemas, como carga de trabalho média ou uso máximo de memória. No entanto, os AQs padrão são limitados por conjuntos de pesos finitos, o que impede a expressão de propriedades que requerem valores ilimitados, como tempo médio de resposta. Em tais cenários, o atraso entre uma solicitação e uma concessão pode ser arbitrariamente grande, uma restrição que pesos de transição finitos não conseguem capturar.

Embora os Autômatos Quantitativos Aninhados (AQAs) tenham sido introduzidos teoricamente para resolver isso, permitindo que um autômato pai gere autômatos filhos que computam valores ilimitados sobre infixos finitos, os AQAs historicamente careciam de suporte prático de ferramentas. Os procedimentos de decisão existentes para AQAs permaneceram teóricos, deixando uma lacuna entre os resultados de decidibilidade e a verificação automatizada.

Metodologia

Os autores abordam essa lacuna estendendo o QuAK (Quantitative Automata Kit), uma ferramenta de software para análise de AQs, para suportar AQAs. A metodologia central baseia-se em procedimentos de achatamento que reduzem instâncias de AQAs a instâncias padrão de AQs. Essa redução preserva as respostas aos problemas de decisão de limiar (vazio e universalidade) sem necessariamente preservar a equivalência semântica entre o AQA de entrada e o AQ de saída.

O pipeline de achatamento, implementado em C++, lida com as seguintes estratégias algorítmicas com base na combinação de agregadores pais ($f$) e agregadores filhos ($g$):

1. Filhos Regulares ($g \in \{Min, Max, SumB\}$): Como o conjunto de valores de retorno possíveis é finito, a ferramenta adivinha o valor de retorno do filho e o verifica usando uma abordagem baseada em obrigações. Isso envolve rastrear configurações de filhos possíveis em paralelo e podar aquelas que não podem atingir um estado final com o valor adivinhado.
2. Limitação Baseada em Limiar ($f \in \{Sup, LimSup, Inf, LimInf\}, g \in \{Sum+, Sum-\}$): Para esses casos, os valores de retorno do filho que excedem um limiar específico $\lambda$ são truncados. Isso reduz o problema ao caso limitado $SumB$, permitindo a construção de filhos regulares.
3. Pais Extremais com Filhos Monotônicos: Para verificação de vazio com pais extremais ($Sup, LimSup, Inf, LimInf$) e filhos monotônicos, a ferramenta evita calcular valores de retorno exatos. Em vez disso, reduz cada invocação de filho a um resultado binário de limiar (o filho pode retornar um valor $\ge \lambda$?). Isso permite procedimentos especializados de "adivinhar-e-verificar" que rastreiam apenas o status de limiar necessário, reduzindo significativamente o espaço de estados em comparação com reduções gerais.
4. Média-Limite com Filhos Ilimitados:
   • Para $(LimSupAvg, Sum+)$, a ferramenta primeiro verifica se os valores de retorno do filho podem crescer ilimitadamente. Se sim, a vazio vale trivialmente; caso contrário, reduz-se ao caso limitado $SumB$.
   • Para $(LimInfAvg, Sum-)$e$(LimSupAvg, Sum-)$, a ferramenta emprega uma construção de sincronização onde todos os filhos ativos avançam simultaneamente, rastreando um multiconjunto limitado de estados de filhos ativos.
5. Eliminação de Pesos Silenciosos: O processo de achatamento gera AQs com pesos silenciosos (transições que não invocam nenhum filho). Estes são eliminados substituindo-os por pesos neutros (por exemplo, $-\infty$ para $Sup$) ou por construções de compressão de caminho para objetivos de média-limite.
6. Universalidade Baseada em Anticadeias: Para decidir a universalidade, a ferramenta realiza uma busca sob demanda por palavras contraexemplo, usando anticadeias para podar o espaço de exploração. Contextos são enriquecidos com resumos de valores para lidar com limites quantitativos juntamente com alcançabilidade.

Contribuições Principais

1. Implementação de Ferramenta: A primeira implementação prática de algoritmos de análise de AQAs, estendendo o framework QuAK.
2. Suíte Abrangente de Achatamento: Implementação de procedimentos de achatamento para todas as combinações de agregadores pais e filhos onde vazio e universalidade são conhecidos por serem decidíveis. Isso cobre funções pais $\{Sup, Inf, LimSup, LimInf, LimSupAvg, LimInfAvg\}$ e funções filhos $\{Min, Max, SumB, Sum+, Sum-\}$.
3. Arquitetura Modular: Um pipeline que traduz AQAs em AQs com pesos silenciosos, que são então processados pelos procedimentos de decisão existentes do QuAK para vazio, inclusão e análise de segurança-vitalidade.
4. Avaliação Experimental: A ferramenta foi avaliada em duas famílias de benchmarks:
   • Tempo de Resposta: AQAs paramétricos ($A_{n,k}$) modelando protocolos de solicitação-concessão com solicitações pendentes limitadas ($n$) e tempos de resposta ($k$).
   • Consumo de Recursos: AQAs paramétricos ($B_{n,k}$) modelando sistemas com processos iniciados/terminados dinamicamente e padrões de acesso a recursos.

Resultados

A avaliação experimental demonstra a eficácia e escalabilidade do QuAK em diferentes tipos de AQAs:

• Benchmarks de Tempo de Resposta:
  • Para vazio $(Sup, Sum+)$, a ferramenta escala bem, com tempo de execução mostrando uma dependência quase quadrática no limite de tempo de resposta $k$ e dependência suave no número de solicitações pendentes $n$.
  • Para vazio $(LimSupAvg, Sum+)$ e universalidade $(Sup, SumB)$, o tempo de execução cresce mais rapidamente com ambos os parâmetros. A universalidade é consistentemente mais cara devido à necessidade de procedimentos PSpace para lidar com não determinismo no autômato achatado.
• Benchmarks de Consumo de Recursos:
  • A verificação de vazio $(Sup, Max)$ exibe rápida explosão em ambos os parâmetros ($n$ e $k$) devido à explosão combinatória de subconjuntos de recursos rastreados por filhos ativos.
  • O caso $(LimSupAvg, Max)$ é substancialmente mais difícil, pois requer preservar valores de retorno exatos para todos os filhos ativos, levando ao esgotamento de memória em valores de parâmetro menores em comparação com o caso supremo.

Os resultados confirmam que, embora o achatamento explícito possa incorrer em grandes espaços de estados — particularmente quando muitas instâncias de filhos estão ativas simultaneamente ou as configurações de filhos são densas — a ferramenta lida com sucesso com instâncias decidíveis de propriedades quantitativas complexas.

Significado

O artigo afirma preencher a lacuna entre a decidibilidade teórica de AQAs e a verificação prática. Ao estender o QuAK, os autores habilitam a verificação automatizada de propriedades quantitativas, como tempo médio de resposta, que são expressíveis em AQAs, mas não em AQs padrão. O trabalho estabelece uma fundação para analisar sistemas com tarefas geradas dinamicamente e custos ilimitados, fornecendo um framework prático para análise de latência de protocolo, monitoramento de tempo de resposta ao nível de serviço e análise de consumo de recursos. Os autores observam que, embora a implementação atual dependa de construção explícita de estados, trabalhos futuros podem explorar representações simbólicas para mitigar a explosão de espaço de estados.