Delayed Constraints in Narrowing for the Logic-Based Analyses of Real-Time Systems

Resumo Técnico: Restrições Adiadas em Narrowing para Análises Baseadas em Lógica de Sistemas de Tempo Real

Declaração do Problema
A análise formal de sistemas de tempo real enfrenta dois desafios primordiais em relação ao infinito: o potencial para um número ilimitado de agentes e mensagens, e um espaço de estados que é infinito devido ao tempo denso. Os métodos de verificação tradicionais em Lógica de Reescrita (RL), particularmente aqueles implementados no motor de reescrita Maude, têm sido historicamente limitados. Embora o Maude suporte a verificação de invariantes para sistemas com componentes totalmente especificados (termos fundamentais) e restrições SMT, ele apresenta dificuldades com sistemas contendo um número desconhecido de agentes ou parâmetros arbitrários. Além disso, técnicas simbólicas anteriores frequentemente dependiam de amostragem de tempo, o que carece de correção (soundness) e completude em configurações de tempo denso. Abordagens existentes utilizando variáveis lógicas para agentes ilimitados resultam frequentemente em procedimentos de semidecisão com espaços de busca infinitos, carecendo de mecanismos para garantir a terminação.

Metodologia
Os autores propõem um novo framework de verificação que integra três técnicas principais para abordar essas limitações:

1. Reescrita Modulo SMT: Utilização de teorias SMT para a representação simbólica de restrições de tempo.
2. Narrowing com Variáveis Lógicas: Emprego de variáveis lógicas para raciocinar sobre sistemas com um número desconhecido ou arbitrário de agentes.
3. Restrições Adiadas e Folding: Introdução de um armazenamento de restrições (constraint store) sobre termos parcialmente instanciados, inspirado em Programação de Lógica com Restrições (CLP).

A inovação central é o Delayed Folding Narrowing. Diferente do narrowing padrão, este método permite que expressões SMT em condições de regras contenham partes "adiadas" — subexpressões que não podem ser avaliadas até que os termos sejam mais aprofundamente instanciados. Isso é alcançado através de uma Extensão SMT onde expressões SMT não válidas (por exemplo, mte(t, T') representando um tempo máximo decorrido) são abstraídas em variáveis novas. Essas restrições são acumuladas e apenas resolvidas ou propagadas uma vez que os termos estejam suficientemente instanciados.

O framework define Teorias de Reescrita de Tempo Real Lógicas, que estendem teorias de reescrita de tempo real padrão para permitir:

• Condições em regras de reescrita incluírem expressões SMT com partes adiadas.
• Lados direitos (RHS) incluírem variáveis não presentes no lado esquerdo (LHS).
• Consultas (queries) conterem variáveis compartilhadas nos estados iniciais e alvos.

Para garantir a terminação, o método emprega um mecanismo de folding. Um grafo de estados é construído onde um estado simbólico $v'$ é removido se for uma instância de um estado previamente explorado modulo a teoria equacional. Os autores provam que, sob condições específicas (especificamente, uma hierarquia de tipos/sorts cuidadosamente desenhada), esta preordenação de folding garante um espaço de busca finito, transformando o procedimento de semidecisão em um procedimento de decisão para verificação de invariantes.

Principais Contribuições

1. Delayed Folding Narrowing: A definição e implementação de uma relação de narrowing que lida com expressões SMT estendidas com restrições adiadas. Isso permite a verificação de sistemas com arbitrárias variáveis lógicas e SMT tanto na configuração inicial quanto no invariante.
2. Verificação do Protocolo de Fischer Temporizado: O artigo apresenta a primeira verificação automática da correção do protocolo de exclusão mútua de Fischer temporizado em seu cenário mais geral. Isso inclui um número arbitrário de processos e parâmetros temporais arbitrários ($\gamma$ e $\delta$). Isso foi alcançado através do design de uma hierarquia de tipos específica para garantir a terminação do procedimento de folding e utilizando variáveis lógicas para representar o número não especificado de processos.
3. Síntese de Controlador para o Problema dos Filósofos Comilões: O framework é aplicado a um problema de filósofos comilões temporizado para sintetizar um controlador (o "lackey"). Ao deixar as transições do controlador não especificadas (representadas por variáveis lógicas), o procedimento de narrowing sintetiza as transições ausentes necessárias para satisfazer uma propriedade de alcançabilidade (por exemplo, filósofos específicos entrando na sala de jantar antes de um prazo).

Resultos
O método foi implementado como uma extensão do motor de reescrita Maude usando recursos de meta-nível.

• Protocolo de Fischer: Os autores verificaram com sucesso a exclusão mútua para um número arbitrário de processos. Quando o estado inicial foi restringido de modo que $\gamma > \delta$, o espaço de busca foi finito (contendo apenas 3 estados devido ao folding), e a ferramenta confirmou que nenhum estado alcançável violava o invariante. Inversamente, quando $\delta \ge \gamma$, um contraexemplo foi encontrado.
• Filósofos Comilões: O sistema sintetizou com sucesso um autômato "lackey" que permitiu que filósofos específicos entrassem na sala de jantar. A saída forneceu um conjunto concreto de transições e localizações para o controlador, demonstrando a capacidade do framework para tarefas de síntese.
• Eficiência: O mecanismo de folding reduziu significamente o espaço de busca, permitindo a análise de sistemas que seriam de outra forma intratáveis devido a espaços de estados infinitos.

Significância e Alegações
O artigo alega fornecer uma base sonora e expressiva para a verificação simbólica de teorias de reescrita de tempo real. Sua significância reside em preencher a lacuna entre a expressividade da programação lógica (lidando com agentes ilimitados via variáveis lógicas) e a precisão da análise de tempo real (lidando com tempo denso via SMT e restrições adiadas).

Os autores enfatizam que sua abordagem vai além do "padrão" Maude e das ferramentas existentes para Autômatos Temporizados Paramétricos (PTA), que tipicamente exigem números fixos de processos ou limites de tempo fixos. Ao suportar agentes arbitrários e um número ilimitado de agentes dentro de um único framework, o método oferece uma abordagem uniforme para analisar modelos de tempo real complexos, incluindo a síntese de componentes ausentes do sistema. O trabalho sugere que restrições adiadas são um mecanismo crucial para alcançar a terminação em análises simbólicas de sistemas de tempo real de estado infinito.